coq - 注释 Coq 证明

Question

我是 Coq 的初学者。

虽然计算机为我验证了证明令人满意，但众所周知，满足 Coq 的证明对人类来说难以阅读。这是一个简单的例子，假设您没有看到任何评论:

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.

老实说，如果没有评论，我无法阅读证明，如果我想向不了解 Coq 的观众展示它，则更是如此。

手动编写这些注释很乏味，但 Coq 还是会生成它们。我想知道 Coq 是否可以简单地自动注释我的证明以使其更具可读性？

Answer 1

这不是您真正要求的，因为它不会向 .v 文件本身添加文本 (afaik)，而是 Alectryon允许您在将鼠标悬停在战术上时目标状态出现的位置生成文档。参见 here举几个例子。