Coq："lens is closed under composition" 的证明

Question

我是一个完全不熟悉 Coq 的函数式程序员。事实上，我刚刚完成 Mike Naha's tutorial. Particularly, I'm interested in this language to formalize some laws related to optics. For example, I'd like to know how to encode that lens is closed under composition.

我开始处理GetPut。上述教程不包括记录，但我认为它们是我编码镜头所需要的。据我所知，组合方法应该实现为Definition。最后，我假设我的定理需要接收合成镜头的 GetPut 的证据，以通过等式证明相同的定律适用于生成的镜头。不是很有帮助，但这是我的（不完整且错误的）证明框架：

Record lens (S : Type) (A : Type) := mkLens {
  get : S -> A;
  put : S -> A -> S }.

Definition compose_ln (S A B : Type) (ln1: lens S A) (ln2 : lens A B) : lens S B :=
  {| get := fun (s : S) => get ln1 s;
     put := fun (s : S) (a : A) => put ln1 s (put ln2 (get ln1 s) a) |}.

Theorem closed_GetPut :
    (forall S A B : Type,
    (forall (s : S),
    (forall (ln1 : lens S A) (ln2 : lens A B),
    (exists GetPut_proof : ln1 (* ln1 holds GetPut? *)),
    (exists GetPut_proof : ln2 (* ln2 holds GetPut? *)),
    (put (compose_ln ln1 ln2) s (get (compose_ln ln1 ln2) s) = s)))).
Proof.
  (* ... *)
Qed.

话虽如此：

我写这个证明的路径正确吗？还有其他更好的方法吗？
在哪里可以找到用作指导示例的类似示例？
根据我的 FP 背景，material 继续学习 Coq 哪个更好？（我正在考虑 Benjamin C. Pierce 的 Software Foundations。）

谢谢！

Answer 1

这看起来大致合理，但需要一些整理。

首先，您不妨删除两个 "exists" 量词（将它们更改为简单含义）。

其次，最后两个假设的类型不应该只是"ln1"和"ln2"，而是"very_well_behaved ln1"和"very_well_behaved ln2"。（然后最终结果的类型可以是"very_well_behaved (compose ln2 ln2)".

Answer 2

阅读 Logical Foundations 的第一章后（如果您的背景是 功能性 ，我绝对推荐您阅读）我能够实现镜头关闭的证明Coq 中的成分。首先，我们需要定义 lens 和 compose:

Record lens (S A : Type) := {
  get : S -> A;
  put : S -> A -> S }.

Definition compose {S A B : Type} (ln1 : lens S A) (ln2 : lens A B) : lens S B :=
  {| get := fun (s : S) => ln2.(get A B) (ln1.(get S A) s);
     put := fun (s : S) (b : B) => ln1.(put S A) s (ln2.(put A B) (ln1.(get S A) s) b) |}.

(*) 注意访问记录字段的固定语法。

然后，我们需要声明涉及的属性，最终达到very_well_behaved（由@Benjamin Pierce 在接受的答案中建议）：

Definition get_put {S A : Type} (ln : lens S A) : Prop :=
  forall (s : S), ln.(put S A) s (ln.(get S A) s) = s.

Definition put_get {S A : Type} (ln : lens S A) : Prop :=
  forall (s : S) (a : A), ln.(get S A) (ln.(put S A) s a) = a.

Definition put_put {S A : Type} (ln : lens S A) : Prop :=
  forall (s : S) (a1 : A) (a2 : A), 
    ln.(put S A) (ln.(put S A) s a1) a2 = ln.(put S A) s a2.

Definition very_well_behaved {S A : Type} (ln : lens S A) : Prop :=
  get_put ln /\ put_get ln /\ put_put ln.

定义属性后，下一个（也是最大的）挑战在于证明非常良好的镜头在合成下是封闭的。为此，我们可以使用以下定理框架：

Theorem compose_is_closed : forall (S A B : Type) (ln1 : lens S A) (ln2 : lens A B),
    very_well_behaved ln1 -> very_well_behaved ln2 -> very_well_behaved (compose ln1 ln2).
Proof.
  (* tactics here *)
Qed.

目前，我对 Coq 的了解非常有限，这就是为什么我没有在这里包含这些策略的原因，因为我觉得我目前的实现仍然很幼稚。无论如何，如果你对此感到好奇，你可以找到完整的证明in this gist。

Coq："lens is closed under composition" 的证明

Coq: proof of "lens is closed under composition"

functional-programming

coq

proof

lenses