coq - 破坏假设 : general case

Question

这很清楚 destruct H如果 H包含连词或析取。但我无法弄清楚它在一般情况下的作用。它做了一些奇怪的事情，特别是如果 H: a -> b .
一些例子:

Lemma demo : forall (x y: nat), x=4 -> x=4.
Proof.
  intros. destruct H.

假设刚刚被破坏:

1 subgoal
x, y : nat
______________________________________(1/1)
x = x

另一个:

Lemma demo : forall (x y: nat), (x = 4 -> x=4) -> True.
Proof.
  intros. destruct H.

现在我有两个分支:

1 subgoal
x, y : nat
______________________________________(1/1)
x = 4

1 subgoal
x, y : nat
______________________________________(1/1)
True

第三个例子。这无法证明，但对我来说仍然没有意义:

Lemma demo : forall (x y: nat), (x = 4 -> x = 4) -> x = 4.
Proof.
  intros. destruct H.

现在我要证明 x = x在第二个分支!

2 subgoals
x, y : nat
______________________________________(1/2)
x = 4
______________________________________(2/2)
x = x

所以，我显然不明白 destruct H做。

Answer 1

您所指的案例分为两类。如 H : A和 A是归纳或共同定义的(例如，合取和析取)，然后 destruct H为该类型的每个构造函数生成一个子目标，附加假设由该构造函数的参数确定。另一方面，如果 H : A -> B ，然后 destruct H生成一个您必须证明的子目标 A ，然后继续递归，好像 H : B .这大致相当于以下调用:

assert (H' : A); [ |specialize (H H'); destruct H].

拼图的缺失部分是等式本身被定义为归纳类型:

Inductive eq (A : Type) (a : A) : A -> Prop :=
| eq_refl : eq A a a

当你破坏 x = 4 类型的东西时, Coq 为该类型的每个构造函数生成一个 case。但该类型只有一个构造函数: eq_refl .在考虑这种情况时，Coq 还会自动用 LHS 替换出现的破坏相等的 RHS(因为该构造函数的两边都是相等的)。在您的第一个和第三个示例中，这导致将目标中的 4 替换为 x .
大多数情况下，您不想破坏相等假设，因为这种替换行为不是很有用。通常最好使用 rewrite策略，因为它允许您从右到左或从左到右重写。