Annotating Coq proofs

user_521179 0
Viewed 103

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?

coq
2 Answers

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.

user_23054580

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.

user_153746210
Related