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

然后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 : 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

然后你做了 destruct H as [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.

Answer 2

这不仅仅是关于策略或理解 Coq 工作原理的问题：您的目标是错误的，如下所示。

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 H.
  specialize (H False False False).
  firstorder.
Qed.

换句话说，如果x、y和z被认为是False，那么你引理的所有前提都是有效的，但它的结论确实不是。

[编辑：我是如何发现这一点的] 我首先尝试了 firstorder 策略（针对此类一阶目标的决策程序），发现它并没有终止，这让我产生了怀疑。然后我转向相应的目标布尔值（使用 ssreflect/ssrbool 包），我可以在 x、y 和 z 上使用大小写拆分 +检查引理是否成立的计算。发现当他们三个是 false 时，目标减少到 false，我有我的反例，然后简单地把它变回一个命题反例。

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

Coq: a vicious circle with two identical subgoals

coq

propositional-calculus