Coq证明时出现两个相同子目标陷入死循环，该如何解决？

解答 #

关于子目标重复的误解 #

执行destruct H4得到的两个子目标并不相同：

1. 第一个分支假设y成立，你执行left后目标缩小为y，和假设匹配，assumption后直接完成该分支
2. 第二个分支假设y → x ∨ z成立，目标仍为原始的y ∨ z，是需要继续处理的分支
   你是误把不同阶段的目标看成了重复项，destruct的行为完全符合析取拆分的逻辑。

死循环的原因 #

你在第二个分支中重复调用pose proof (H3 H0)，这个步骤和你之前得到H4的推导逻辑完全一致，相当于重复生成已经得到的结论，全程没有用到未使用的前提H2，自然会原地循环。

修正后的证明步骤 #

首先需要确认你使用的是经典逻辑环境，该引理在直觉主义逻辑下不可证，需要先导入经典库：

Require Import Classical.

当你进入只有H4: y → x ∨ z的剩余分支时，按以下步骤操作即可完成证明：

1. 调用之前未使用的前提H2，得到新的析取假设：

   pose proof (H2 H4). (* 得到 H5: x ∨ (x → y ∨ z) *)
   destruct H5.
   

2. 处理第一个子分支（假设x成立）：

   apply H0 in H5. (* 用H0: x→y∨z，直接得到y∨z *)
   exact H5.
   

3. 处理第二个子分支，用反证法推导即可：

   destruct (classic (y ∨ z)) as [Hz|Hnz].
   - exact Hz.
   - exfalso.
     apply Hnz.
     apply H0.
     destruct (H4 (fun y => Hnz (or_introl y))) as [Hx|Hz].
     + exact Hx.
     + contradiction.
   

内容的提问来源于stack exchange，提问作者მამუკა ჯიბლაძე