与功能扩展性作斗争

Question

我已经使用 Coq 编程几个月了。特别是，我对函数无处不在的函数式编程证明很感兴趣（optics、state monad 等）。从这个意义上说，处理 功能扩展性 已经变得必不可少，尽管非常烦人。为了说明这种情况，让我们假设 Monad 的简化（仅定义了一个定律）：

Class Monad (m : Type -> Type) :=
{ ret : forall {X}, X -> m X
; bind : forall {A B}, m A -> (A -> m B) -> m B
}.
Notation "ma >>= f" := (bind ma f) (at level 50, left associativity).

Class MonadLaws m `{Monad m} :=
{ right_id : forall X (p : m X), p >>= ret = p }.

现在，我想证明将几个 ret 链接到一个程序 p 应该等同于同一个程序：

Example ugly_proof :
  forall m `{MonadLaws m} A (p : m A), 
    p >>= (fun a1 => ret a1 >>= (fun a2 => ret a2 >>= ret)) = p.
Proof.
  intros.
  destruct H0 as [r_id].

  assert (J : (fun a2 : A => ret a2 >>= ret) =
              (fun a2 : A => ret a2)).
  { auto using functional_extensionality. }
  rewrite J.

  assert (K : (fun a1 : A => ret a1 >>= (fun a2 : A => ret a2)) =
              (fun a1 : A => ret a1)).
  { auto using functional_extensionality. }
  rewrite K.

  now rewrite r_id.
Qed.

证明是正确的，但是迭代的assert模式让它变得非常麻烦。事实上，当事情变得更复杂时，它变得不切实际，正如您在 this proof 中所见（这证明仿射遍历在组合下是封闭的）。

话虽如此，实现上述证明的最佳方式是什么？有没有关于功能外延性的项目或文章（比this one更平易近人）可以参考？

Answer 1

我要概括一下right_id定律：

Require Import Coq.Logic.FunctionalExtensionality.
Generalizable Variables m A.

Lemma right_id_gen `{ml : MonadLaws m} `{p : m A} r :
  r = ret -> p >>= r = p.
Proof. intros ->; apply ml. Qed.

现在我们可以使用反向推理了：

Example not_so_ugly_proof `{ml : MonadLaws m} `{p : m A} :
  p >>= (fun a1 => ret a1 >>= (fun a2 => ret a2 >>= ret)) = p.
Proof.
  apply right_id_gen, functional_extensionality; intros.
  apply right_id_gen, functional_extensionality; intros.
  now apply right_id_gen.
Qed.

Answer 2

有一种使用 setoid_rewrite 策略的方法（我试图在中演示它）：

Require Import Coq.Logic.FunctionalExtensionality.
Require Import Coq.Setoids.Setoid.
Require Import Coq.Classes.Morphisms.

Generalizable All Variables.

Instance pointwise_eq_ext {A B : Type} `(sb : subrelation B RB eq)
  : subrelation (pointwise_relation A RB) eq.
Proof. intros f g Hfg. apply functional_extensionality. intro x; apply sb, (Hfg x). Qed.

Example easy_proof `{ml : MonadLaws m} `{p : m A} :
  p >>= (fun a1 => ret a1 >>= (fun a2 => ret a2 >>= ret)) = p.
Proof. now repeat setoid_rewrite right_id. Qed.

阅读material：

A Gentle Introduction to Type Classes and Relations in Coq 作者：皮埃尔·卡斯特运行和马修·索佐
A New Look at Generalized Rewriting in Type Theory 马蒂厄·索索

Answer 3

您可以将 RHS 重写为 p >>= ret 并使用 f_equal 向后推理，将目标更改为 (fun _ => ...) = ret 其中 functional_extensionality 适用。

Class MonadLaws m `{Monad m} :=
  { right_id : forall X (p : m X), p >>= ret = p }.
Example ugly_proof :
  forall m `{MonadLaws m} A (p : m A), 
    p >>= (fun a1 => ret a1 >>= (fun a2 => ret a2 >>= ret)) = p.
Proof.
  intros.
  transitivity (p >>= ret).
  rewrite <- (right_id _ p) at 2.
  f_equal.
  apply functional_extensionality.
  intro x.
  rewrite <- (right_id _ (ret x)) at 2.
  f_equal.
  apply functional_extensionality.
  intro x0.
  rewrite <- (right_id _ (ret x0)) at 2.
  auto.
Qed.

与功能扩展性作斗争

Struggling with functional extensionality

function

proof

coq