为何Coq中两个命题逻辑定理可使用相同证明序列？

为什么相同的left; right; left能搞定两个定理？ #

Coq的left和right是纯语法导向的命令：它们只看当前目标析取式的结构层次，不关心分支里的命题是什么。

拆解两个定理的目标结构：

• or_lots2的目标是(Q ∨ P ∨ P) ∨ Q，语法树层级是：最外层为A ∨ Q（A是Q ∨ P ∨ P），A本身是Q ∨ B（B是P ∨ P），B是P ∨ P。left选最外层的A，right选A里的B，left选B里的第一个P——正好匹配假设的P。
• or_lots3的目标是(P ∨ P ∨ Q) ∨ Q，语法树层级是：最外层为C ∨ Q（C是P ∨ P ∨ Q），C本身是P ∨ D（D是P ∨ Q），D是P ∨ Q。left选最外层的C，right选C里的D，left选D里的第一个P——也正好匹配假设的P。

本质是两个定理的语法树里，都存在一条左→右→左的路径指向P，所以相同的命令序列能凑效，这是语法结构的巧合，和命题逻辑的语义证明规则无关。

能区分两个定理的替代证明 #

如果要让证明过程不一样，可以刻意选择不同的语法路径，或者用更明确的构造器调用：

仅适用于or_lots2的证明 #

Theorem or_lots2 : P -> (Q ∨ P ∨ P) ∨ Q.
Proof.
  intros S.
  left; right; right. (* 选最外层左分支 → 右分支 → 右分支的P *)
  assumption.
Qed.

仅适用于or_lots3的证明 #

Theorem or_lots3 : P -> (P ∨ P ∨ Q) ∨ Q.
Proof.
  intros S.
  left; left. (* 选最外层左分支 → 左分支的P *)
  assumption.
Qed.

或者直接用析取构造器or_introl/or_intror（对应left/right的底层逻辑），更直观：

• or_lots2的证明可以写成：intros S; apply or_introl; apply or_intror; apply or_intror; assumption.
• or_lots3的证明可以写成：intros S; apply or_introl; apply or_introl; assumption.

这样两个证明序列完全不同，对应了各自目标中不同的P分支位置。

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