破坏假设：一般情况

Question

如果 H 包含合取或析取，destruct 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 策略，因为它允许您从右到左或从左到右重写。

破坏假设：一般情况

Destruct hypothesis: general case

coq

ltac