10

我想用这种destruct策略来证明一个案例。我在网上阅读了几个例子，我很困惑。有人可以更好地解释吗？

这是一个小例子（还有其他方法可以解决它，但请尝试使用destruct）：

 Inductive three := zero 
                  | one 
                  | two.
 Lemma has2b2: forall a:three, a<>zero /\ a<>one -> a=two.

现在一些在线示例建议执行以下操作：

intros. destruct a.

在这种情况下，我得到：

3 subgoals H : zero <> zero /\ zero <> one
______________________________________(1/3) 
zero = two

______________________________________(2/3) 
one = two

______________________________________(3/3) 
two = two

所以，我想证明前两种情况是不可能的。但是机器将它们列为子目标并希望我证明它们……这是不可能的。

摘要：如何准确丢弃不可能的情况？

我看过一些例子，inversion但我不明白这个过程。

最后，如果我的引理依赖于几种归纳类型并且我仍然想涵盖所有情况会发生什么？

4

2 回答 2

10

如何丢弃不可能的情况？好吧，前两个义务确实无法证明，但请注意它们的假设相互矛盾（zero <> zero和one <> one，分别）。因此，您将能够证明这些目标tauto（如果您有兴趣，还有更原始的策略可以解决问题）。

inversion是更高级的破坏版本。除了“破坏”归纳之外，它有时还会产生一些等式（您可能需要）。它本身是 的一个简单版本induction，它还会为您额外生成一个归纳假设。

如果您的目标中有几种归纳类型，则可以destruct/invert一一进行。

更详细的演练：

Inductive three := zero | one | two .

Lemma test : forall a, a <> zero /\ a <> one -> a = two.
Proof.
  intros a H.
  destruct H. (* to get two parts of conjunction *)
  destruct a. (* case analysis on 'a' *)
(* low-level proof *)
  compute in H. (* to see through the '<>' notation *)
  elimtype False. (* meaning: assumptions are contradictory, I can prove False from them *)
  apply H.
  reflexivity.
(* can as well be handled with more high-level tactics *)
  firstorder.
(* the "proper" case *)
  reflexivity.
Qed.
于 2011-07-26T10:10:14.800 回答
10

如果你看到一个不可能的目标，有两种可能性：要么你的证明策略有误（也许你的引理是错误的），要么假设是矛盾的。

如果您认为假设是矛盾的，您可以将目标设置为False，以消除一些复杂性。elimtype False实现了这一点。通常，您False通过证明一个命题P及其否定来证明~P；该策略从和absurd P推断出任何目标。如果有一个特定的假设是矛盾的，则将目标设置为 如果一个特定的假设显然是矛盾的，或者只是将证明任何目标。P~Pcontradict H~H~AA~ ~Acontradiction Hcontradiction

有许多策略涉及归纳类型的假设。弄清楚使用哪一个主要是经验问题。以下是主要的（但您很快就会遇到此处未涉及的情况）：

  • destruct简单地将假设分解为几个部分。它丢失了有关依赖关系和递归的信息。一个典型的例子是destruct Hwhere His 一个连词H : A /\ B，它分裂成两个独立的类型和H假设；或者对偶where是析取，它将证明分成两个不同的子证明，一个带有假设，一个带有假设。ABdestruct HHH : A \/ BAB
  • case_eq类似于destruct，但保留了假设与其他假设的联系。例如，destruct nwheren : nat将证明分为两个子证明，一个 forn = 0和一个 for n = S m。如果n用于其他假设（即您有 a H : P n），您可能需要记住，n您已破坏的 与n这些假设中使用的相同：case_eq n这样做。
  • inversion对假设的类型进行案例分析。当假设类型中存在destruct会忘记的依赖关系时，它特别有用。您通常会case_eq在假设中使用Set（平等相关）和inversion假设中Prop（具有非常依赖的类型）。该inversion策略留下了很多平等，并且通常遵循subst简化假设。该inversion_clear策略是一种简单的替代方法，inversion; subst但会丢失一些信息。
  • induction意味着您将通过对给定假设的归纳（=递归）来证明目标。例如，induction nwheren : nat表示您将执行整数归纳并证明基本情况（n替换为0）和归纳情况（n替换为m+1）。

你的例子很简单，你可以证明它“通过案例分析很明显a”。

Lemma has2b2: forall a:three, a<>zero/\a<>one ->a=two.
Proof. destruct a; tauto. Qed.

但是让我们看一下该destruct策略产生的案例，即intros; destruct a.. （is 的情况a是one对称的；最后一种情况aistwo是自反性显而易见的。）

H : zero <> zero /\ zero <> one
============================
 zero = two

这个目标看起来是不可能的。我们可以将这一点告诉 Coq，在这里它可以自动发现矛盾（zero=zero很明显，其余的是该策略处理的一阶重言式tauto）。

elimtype False. tauto.

事实上tauto，即使你不告诉 Coq 不要担心目标并且在tauto没有第一个目标的情况下编写elimtype False（IIRC 在旧版本的 Coq 中没有），实际上也是有效的。您可以tauto通过编写info tauto. Coq 会告诉你该tauto策略生成了什么证明脚本。这不是很容易理解，所以让我们看一下这个案例的手动证明。首先，让我们将假设（即合取）一分为二。

destruct H as [H0 H1].

我们现在有两个假设，其中之一是zero <> zero。这显然是错误的，因为它的否定zero = zero显然是正确的。

contradiction H0. reflexivity.

我们可以更详细地了解该contradiction策略的作用。（info contradiction会揭示场景下发生的事情，但同样对新手不友好）。我们声称目标是正确的，因为假设是矛盾的，所以我们可以证明任何事情。因此，让我们将中间目标设置为False。

assert (F : False).

跑去red in H0.看看那zero <> zero是真正的符号~(zero=zero)，它又被定义为含义zero=zero -> False。False的结论也是如此H0：

apply H0.

zero=zero现在我们需要证明

reflexivity.

现在我们已经证明了我们的断言False。剩下的就是证明这False意味着我们的目标。好吧，False意味着任何目标，这就是它的定义（False定义为 0 case 的归纳类型）。

destruct F.
于 2011-07-26T18:40:00.940 回答