Coq能否记忆已证元素属性？如何自动化简单证明？

针对你遇到的重复证明同一归纳属性的问题，这里有几个简单实用的方案，适合Coq初学者快速上手：

1. 用内置策略一键完成简单证明 #

你的例子里的证明逻辑非常规律：反复拆解列表（apply g'），然后匹配对应的good/goodL构造子。Coq的repeat配合auto就能自动完成整个过程：

Example ex0: goodL [P ; (L P P); C [P ; L P P]].
Proof. repeat apply g'; auto. Qed.

• repeat apply g'会不断对goodL目标应用g'构造子，直到列表被拆解到空（nil）。
• auto会自动匹配所有无需额外前提的构造子（比如gP、gL、g0），以及递归解决good (C ff)需要的goodL ff目标。

2. 明确记忆已证事实 #

如果某些元素的good属性会重复出现数十次，你可以提前证明并保存这些事实，避免重复构造证明：

方法一：临时保存局部引理 #

在证明过程中用assert提前证出重复用到的命题，之后让auto优先使用这些引理：

Example ex0: goodL [P ; (L P P); C [P ; L P P]].
Proof.
  (* 提前证明并保存两个重复用到的事实 *)
  assert (H_P : good P) by apply gP.
  assert (H_LPP : good (L P P)) by apply gL.
  (* 用auto using指定可用的局部引理 *)
  repeat apply g'; auto using H_P, H_LPP.
Qed.

方法二：全局添加提示 #

如果这些属性在多个证明中都要用到，可以全局添加提示，让auto默认识别这些构造子：

(* 将常用构造子加入auto的默认提示库 *)
Hint Resolve gP gL g0 : core.

Example ex0: goodL [P ; (L P P); C [P ; L P P]].
Proof. repeat apply g'; auto. Qed.

这样所有后续的auto调用都会自动使用gP、gL、g0，无需重复指定。

3. 自定义策略应对复杂场景 #

如果你的good规则有更固定的模式，可以用Ltac写一个自定义策略，针对性处理所有情况：

Ltac solve_good :=
  repeat match goal with
         | [ |- goodL _ ] => apply g'
         | [ |- good P ] => apply gP
         | [ |- good (L P P) ] => apply gL
         | [ |- good (C _) ] => apply gC; solve_good
         | [ |- goodL nil ] => apply g0
         end.

Example ex0: goodL [P ; (L P P); C [P ; L P P]].
Proof. solve_good. Qed.

这个策略会递归遍历所有目标，自动应用对应的构造子，完全不需要手动输入步骤。

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