CODEWITHSUNDEEP
coq
Andrew Au
Andrew Au

Reputation: 832

Annotating Coq proofs

I am a beginner Coq user.

While it is satisfying that the computer verified the proof for me, proofs that satisfy Coq are notoriously difficult to read for humans. Here is a simple example, imagine you don't see any of the comments:

Theorem add_comm : forall n m : nat,
  n + m = m + n.
Proof.
  intros n m.
  induction m as [|m Hm].
  -                        (*     n + 0 = 0 + n       *)
    simpl.                 (*     n + 0 = n           *)
    apply add_0_r.         (*                         *)
  -                        (*   n + S m = S m + n     *)
    simpl.                 (*   n + S m = S (m + n)   *)
    rewrite <- Hm.         (*   n + S m = S (n + m)   *)
    rewrite <- plus_n_Sm.  (* S (n + m) = S (n + m)   *)
    reflexivity.           (*                         *)
  Qed.

I honestly cannot read the proof without the comments, even less so if I want to show it to audiences who don't know about Coq.

Writing these comments manually is tedious, and Coq generates them anyway. I wonder if Coq can simply automatically annotate my proof so to make it more readable?

Upvotes: 3

Views: 219

Answers (2)

Meven Lennon-Bertrand
Meven Lennon-Bertrand

Reputation: 1296

An alternative solution to annotating the proof is to replay it, by opening the file and stepping through it to see the intermediate goals. I think even experts often do this to understand a proof, and many Coq demos also resort to this to go over proofs. Depending on your setting and goals, this might be simpler than setting Alectryon up.

Upvotes: 1

Ana Borges
Ana Borges

Reputation: 1376

It's not literally what you asked for, as it doesn't add text to the .v file itself (afaik), but Alectryon allows you to generate documentation where the goal state appears when you hover the mouse on top of a tactic. See here for several examples.

Upvotes: 3

Related Questions