Coq是否支持自动为证明添加注释以提升人工可读性？

Coq 原生没有内置自动为证明步骤插入目标状态注释的功能，但社区有成熟的工具链可以完全覆盖这个需求，无需手动编写注释：

• 要直接把注释写入.v源码文件
  可以用社区开源的coq-annotate脚本，或是Emacs平台Proof General插件自带的proof-general-insert-all-goal-comments命令。工具会自动遍历你证明的每一步执行状态，将当前步骤对应的目标内容按照你示例里的格式作为注释插入到对应证明行的尾部，还支持自定义缩进、是否显示上下文等配置项。
• 要给非Coq受众做展示
  更推荐使用Alectryon工具，它可以直接把Coq证明文件渲染成交互式文档，每一步证明对应的目标、上下文都会实时展示在侧边栏，不需要把注释硬编码到源码里，可读性更高，也不用额外调整格式适配阅读需求。

如果只是你自己写证明时需要查看每一步的状态，所有主流Coq编辑器（VSCoq、CoqIDE、Proof General）都会在侧边栏实时显示当前目标和上下文，不需要额外生成注释。

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