Coq:一个有两个相同子目标的恶性循环

Question

对于过于复杂的示例，我们深表歉意。我有

Lemma test : forall x y z : Prop,
 (
     (((x → (y ∨ z)) → (x ∨ y)) ↔ (x ∨ y))
   ∧ (((y → (x ∨ z)) → (x ∨ y)) ↔ (x ∨ y))
   ∧  ((y → (x ∨ z)) → (x ∨ (x → (y ∨ z))))
   ∧  ((x → (y ∨ z)) → (y ∨ (y → (x ∨ z))))
  )  → ((x → (y ∨ z)) → (y ∨ z)).

做

Proof.
  intros.
  destruct H.
  destruct H1.
  destruct H2.
  pose proof (H3 H0).

给予

1 goal
x, y, z : Prop
H : ((x → y ∨ z) → x ∨ y) ↔ x ∨ y
H1 : ((y → x ∨ z) → x ∨ y) ↔ x ∨ y
H2 : (y → x ∨ z) → x ∨ (x → y ∨ z)
H3 : (x → y ∨ z) → y ∨ (y → x ∨ z)
H0 : x → y ∨ z
H4 : y ∨ (y → x ∨ z)
______________________________________(1/1)
y ∨ z

然后我执行 destruct H4. 这给出了

2 goals
x, y, z : Prop
H : ((x → y ∨ z) → x ∨ y) ↔ x ∨ y
H1 : ((y → x ∨ z) → x ∨ y) ↔ x ∨ y
H2 : (y → x ∨ z) → x ∨ (x → y ∨ z)
H3 : (x → y ∨ z) → y ∨ (y → x ∨ z)
H0 : x → y ∨ z
H4 : y
______________________________________(1/2)
y ∨ z
______________________________________(2/2)
y ∨ z

我已经不明白了:为什么有两个相同的目标？？ 然后我执行 left. 并获得

2 goals
x, y, z : Prop
H : ((x → y ∨ z) → x ∨ y) ↔ x ∨ y
H1 : ((y → x ∨ z) → x ∨ y) ↔ x ∨ y
H2 : (y → x ∨ z) → x ∨ (x → y ∨ z)
H3 : (x → y ∨ z) → y ∨ (y → x ∨ z)
H0 : x → y ∨ z
H4 : y
______________________________________(1/2)
y
______________________________________(2/2)
y ∨ z

然后假设。给出

1 goal
x, y, z : Prop
H : ((x → y ∨ z) → x ∨ y) ↔ x ∨ y
H1 : ((y → x ∨ z) → x ∨ y) ↔ x ∨ y
H2 : (y → x ∨ z) → x ∨ (x → y ∨ z)
H3 : (x → y ∨ z) → y ∨ (y → x ∨ z)
H0 : x → y ∨ z
H4 : y → x ∨ z
______________________________________(1/1)
y ∨ z

然后做

pose proof (H3 H0).
destruct H5.
left.
assumption.

再次介绍两个相同的目标，并把我带到

1 goal
x, y, z : Prop
H : ((x → y ∨ z) → x ∨ y) ↔ x ∨ y
H1 : ((y → x ∨ z) → x ∨ y) ↔ x ∨ y
H2 : (y → x ∨ z) → x ∨ (x → y ∨ z)
H3 : (x → y ∨ z) → y ∨ (y → x ∨ z)
H0 : x → y ∨ z
H4, H5 : y → x ∨ z
______________________________________(1/1)
y ∨ z

除了我现在有两个相同的前提 y → x ∨ z 之外，这与之前的状态相同。

我卡住了。显然我做错了什么，但是什么？

Answer 1

让我们从您的第一个问题开始。实际上，destruct 之后生成的两个目标不是一样的。他们的结论确实都是y\/z，但是他们的前提不同:第一个有H4 : y，而第二个有H4 : y -> x\/z。更一般地说，如果你有一个形式的目标

(* ... *)
H : A \/ B
------------
 C

然后你将H分解为[H1 | H2].，你生成子目标

(* ... *)
H1 : A
-----------
  C

和

(* ... *)
H2 : B
------------
  C

得出相同的结论。

关于你的第二个问题，问题可能是你调用了两次pose proof (H3 H0)。如果您浏览脚本，您会注意到该策略引入的假设在两次调用中都是相同的:y\/(y -> x\/z)。我怀疑你应该在第二次调用时使用 H2 H4 而不是 H3 H0，但我还没有检查过。

最后的评论:您应该让 Coq 为您选择假设的名称，因为这会导致无法维护的证明脚本(参见 here)。只要有可能，您应该使用诸如 destruct H as [H1 | H2] 而不是 destruct H。