Coq分情况证明中apply QthenR报错‘未找到环境引用’问题

你的证明出错的核心是变量作用域的问题，具体是destruct H的位置错误：

1. 执行intros H [h' |h'']时，Coq已将证明拆分为两个独立分支：
   • 第一个分支：持有假设H : (P->R)/\(Q->R)和h' : P
   • 第二个分支：持有假设H : (P->R)/\(Q->R)和h'' : Q
2. 你在第一个分支内部执行destruct H as [PthenR QthenR]，这意味着PthenR和QthenR仅存在于第一个分支的环境中。当处理完第一个分支进入第二个分支时，当前环境里根本没有QthenR——第二个分支从未执行过destruct H，自然不会生成这个变量。

方案一：提前拆分合取式（更简洁） #

把destruct H提到分支拆分前，让两个分支共享拆分后的变量：

Theorem choice_reverse : (P -> R) /\ (Q -> R)->((P \/ Q) -> R).
Proof.
intros H.
destruct H as [PthenR QthenR].
intros [h' |h''].
apply PthenR. assumption.
apply QthenR. assumption.
Qed.

方案二：在每个分支内拆分合取式 #

如果要保持原分支拆分顺序，需在每个分支内单独处理H，用_忽略不需要的变量：

Theorem choice_reverse : (P -> R) /\ (Q -> R)->((P \/ Q) -> R).
Proof.
intros H [h' |h''].
- destruct H as [PthenR _]. apply PthenR. assumption.
- destruct H as [_ QthenR]. apply QthenR. assumption.
Qed.

• 方案一的逻辑更清晰，因为(P->R)/\(Q->R)的拆分和后续的析取分支无关，提前拆分能减少重复操作。
• 方案二中用_占位可以避免生成无用的变量名，让证明更简洁。

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