functional-programming - Coq: "lens is closed under composition"的证明

Question

我是一名对 Coq 完全陌生的函数式程序员。事实上，我刚刚完成 Mike Naha's tutorial .特别是，我对这种语言感兴趣，可以将一些与光学相关的法律形式化。例如，我想知道如何对 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.

话虽如此:

• 我写这个证明的路径正确吗？有没有其他方法可以更好地处理它？<​​/li>
• 我在哪里可以找到用作指导示例的类似示例？
• 根据我的 FP 背景，继续学习 Coq 的更好 Material 是什么？ (我正在考虑 Benjamin C. Pierce 的 Software Foundations。)

谢谢!

Answer 1

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

首先，您不妨删除两个“存在”量词(将它们更改为简单含义)。

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