与功能扩展性作斗争

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 }.

现在，我想证明将多个rets 链接到一个程序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

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

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.  

阅读材料：

• A Gentle Introduction to Type Classes and Relations in Coq Pierre Castéran 和 Matthieu Sozeau

• A New Look at Generalized Rewriting in Type Theory by Matthieu Sozeau

Answer 2

我将概括一下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 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.