Coq入门FP开发者求助：透镜复合封闭性证明及学习资源咨询

First: Fixing Your Lens Composition & GetPut Definition #

First, let's address a couple of critical issues in your code. Your compose_ln function has an error in the get component—since ln1 maps S to A and ln2 maps A to B, the composed get should first retrieve the A value from S via ln1, then extract the B value from that A via ln2. Additionally, we should define a clear predicate for the GetPut law instead of trying to quantify over proofs directly:

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

(* Correct composition: get uses both lenses, put updates through the inner lens first *)
Definition compose_ln (S A B : Type) (ln1 : lens S A) (ln2 : lens A B) : lens S B :=
  {| get := fun s => get ln2 (get ln1 s);
     put := fun s b => put ln1 s (put ln2 (get ln1 s) b) |}.

(* Define the GetPut law as a reusable predicate on lenses *)
Definition GetPut (S A : Type) (ln : lens S A) :=
  forall s : S, put ln s (get ln s) = s.

Is Your Proof Path Correct? (And How to Fix It) #

Your initial theorem statement overcomplicated things with existential quantifiers for proofs. The standard Coq approach here is to use implications: if ln1 satisfies GetPut and ln2 satisfies GetPut, then their composition does too. Here's the corrected theorem:

Theorem closed_GetPut : forall (S A B : Type) (ln1 : lens S A) (ln2 : lens A B),
  GetPut S A ln1 -> GetPut A B ln2 -> GetPut S B (compose_ln ln1 ln2).

Proof Outline #

This proof becomes straightforward once you unfold definitions and apply your hypotheses:

Proof.
  intros S A B ln1 ln2 H1 H2. (* Introduce variables and hypotheses: H1 = ln1's GetPut, H2 = ln2's GetPut *)
  unfold GetPut. (* Unfold the predicate to show we need to prove for all s, put (compose ...) s (get ... s) = s *)
  intros s. (* Take an arbitrary state s *)
  unfold compose_ln. (* Unfold the composition definition to expose the underlying get/put calls *)
  rewrite H2. (* Apply ln2's GetPut law: put ln2 (get ln1 s) (get ln2 (get ln1 s)) = get ln1 s *)
  rewrite H1. (* Apply ln1's GetPut law: put ln1 s (get ln1 s) = s *)
  reflexivity. (* The remaining goal is s = s, which is trivially true *)
Qed.

This path is correct once you fix the theorem structure and compose function. The key insight was separating the lens structure from its compliance with laws (via a predicate) and using implications to link the premises (individual lenses satisfy GetPut) to the conclusion (their composition does too).

Better Approaches to Consider #

• Typeclasses: Once you’re comfortable with basic proofs, you can use typeclasses to mark lenses that satisfy specific laws. For example:

  Class GetPutLens (S A : Type) := {
    lens_obj : lens S A;
    get_put : GetPut S A lens_obj
  }.
  

  This lets you write theorems that apply to any lens in the GetPutLens class, but it’s a bit more advanced.
• Dependent Types: Some formalizations encode laws directly into the lens record (using dependent types to ensure only valid lenses can be constructed). This guarantees correctness by construction but is probably overkill while you’re learning.

Where to Find Similar Examples #

• Search for "Coq lens formalization" to find examples in GitHub repositories, academic papers, and blog posts—many cover composition and lens laws.
• The Coq Standard Library has examples of composing algebraic structures (like monoids or functors) and proving closure properties, which follow similar patterns.
• Software Foundations (Volume 2, "Functional Verification") includes sections on proving properties of record types and composed functions, which align perfectly with your work.

Recommended Learning Resources for Your FP Background #

• Software Foundations: This is an ideal starting point. Volume 1 ("Logical Foundations") begins with functional programming in Coq (familiar territory for you) and gradually introduces proofs. Volume 2 ("Functional Verification") dives into proving properties of functions and record structures—exactly what you need for lens laws.
• Coq in a Hurry: A concise reference for quickly looking up syntax and proof tactics when you’re stuck on a step.
• Certified Programming with Dependent Types (CPDT): Once you master the basics, this book covers advanced topics like dependent types and modular proofs. It’s written for an FP audience and includes examples of formalizing abstract structures like lenses.

内容的提问来源于stack exchange，提问作者neutropolis