2

这很清楚destruct HifH包含合取或析取。但我无法弄清楚它在一般情况下的作用。它做了一些奇怪的事情，尤其是如果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。

4

1 回答 1

2

您所指的案例分为两类。如果H : AandA是归纳或协归纳定义的（例如，合取和析取），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 会为该类型的每个构造函数生成一个案例。但是该类型只有一个构造函数：eq_refl. 在考虑这种情况时，Coq 还会自动用 LHS 替换出现的破坏相等的 RHS（因为对于该构造函数，两边都是相等的）。在您的第一个和第三个示例中，这导致将目标中的 4 替换为x.

大多数时候，您不想破坏等式假设，因为这种替换行为不是很有用。通常最好使用该rewrite策略，因为它允许您从右到左或从左到右重写。

于 2021-08-18T20:04:51.623 回答