注释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。

Answer 2

注释证明的另一种解决方案是重放它，方法是打开文件并逐步通过它来查看中间目标。我认为，即使是专家也经常这样做，以了解证据，许多Coq演示也利用这一点来检查证据。根据您的设置和目标，这可能比设置Alectryon更简单。