2

对不起，过于复杂的例子。我有

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。

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

4

2 回答 2

4

让我们从你的第一个问题开始。实际上，之后生成的两个目标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 为您选择假设的名称，因为这会导致无法维护的证明脚本（请参阅此处）。只要有可能，您应该使用诸如destruct H as [H1 | H2]代替的形式destruct H。

于 2021-11-28T07:33:24.130 回答
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包），在那里我可以使用 case splits onx和y+z计算来检查引理是否成立。发现当他们三个是false目标减少到时false，我有我的反例，然后简单地把它变成一个命题反例。

于 2021-11-29T13:17:25.770 回答