如何在 Coq 中使用归纳类型处理案例

Posted 2023-05-08

【中文标题】如何在 Coq 中使用归纳类型处理案例

【英文标题】：How to do cases with an inductive type in Coq

【发布时间】：2011-10-12 23:47:23

【问题描述】：

我想使用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的例子，但我不明白这个过程。

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

【参考方案1】：

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

inversion 是更高级的 destruct 版本。除了“破坏”归纳之外，它有时还会产生一些等式（您可能需要）。它本身就是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.

【讨论】：

您介意向我展示另一种无需 tauto 即可证明目标的方法吗？如果您不介意发布一段代码，那就太好了。

我编辑了答案以包含完整的低级证明。这种低级的东西对学习很有用，但通常你会用tauto或firstorder之类的策略来消除它

【参考方案2】：

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

如果您认为假设相互矛盾，您可以将目标设置为False，以消除一些复杂性。 elimtype False 实现了这一点。通常，您通过证明命题P 及其否定~P 来证明False；策略absurd P 从P 和~P 推断出任何目标。如果有一个特定的假设是矛盾的，contradict H 会将目标设置为~H，或者如果假设是一个否定~A，那么目标将是A（比~ ~A 更强，但通常更方便） .如果某个特定假设明显矛盾，contradiction H 或只是contradiction 将证明任何目标。

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

destruct 只是将假设分解为几个部分。它丢失了有关依赖关系和递归的信息。一个典型的例子是destruct H，其中H是一个连词H : A /\ B，它将H拆分成两个独立的假设类型A和B；或双重destruct H，其中H是析取H : A \/ B，它将证明分成两个不同的子证明，一个带有假设A，一个带有假设B。 case_eq 类似于 destruct，但保留了假设与其他假设的联系。例如，destruct n 其中n : nat 将证明分为两个子证明，一个用于n = 0，一个用于n = S m。如果在其他假设中使用了n（即您有一个H : P n），您可能需要记住，您已破坏的n 与这些假设中使用的n 相同：case_eq n 就是这样做的。 inversion 对假设的类型进行案例分析。当destruct 会忘记的假设类型存在依赖关系时，它特别有用。您通常会在Set 中的假设上使用case_eq（平等是相关的），在Prop 中的假设上使用inversion（具有非常依赖的类型）。 inversion 策略留下了很多相等性，并且通常紧随其后的是 subst 以简化假设。 inversion_clear 策略是 inversion; subst 的简单替代方案，但会丢失一些信息。 induction 表示您将通过对给定假设的归纳（=递归）来证明目标。例如，induction n 其中n : 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. 之后。 （a 是 one 的情况是对称的；最后一种情况，a 是 two，通过自反性很明显。）

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

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

elimtype False. tauto.

事实上，tauto 可以工作，即使你没有先告诉 Coq 不要担心目标并在没有 elimtype False 的情况下写tauto（IIRC 在旧版本的 Coq 中没有）。您可以通过编写 info tauto 来了解 Coq 对 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) 又被定义为含义zero=zero -> False。所以False是H0的结论：

apply H0.

现在我们需要证明zero=zero，即

reflexivity.

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

destruct F.