如何在Coq中使用归纳类型的案例 [英] How to do cases with an inductive type in Coq

问题描述

我想使用destruct策略来证明案件的陈述.我已经在线阅读了几个示例，我很困惑.有人可以更好地解释吗?

I wan to use the destruct tactic to prove a statement by cases. I have read a couple of examples online and I'm confused. Could someone explain it better?

这是一个小例子(有其他解决方法，但尝试使用destruct):

Here is a small example (there are other ways to solve it but try using destruct):

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

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

Now some examples online suggest doing the following:

intros. destruct a.

在这种情况下，我得到:

In which case I get:

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

______________________________________(2/3) 
one = two

______________________________________(3/3) 
two = two

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

So, I want to prove that the first two cases are impossible. But the machine lists them as subgoals and wants me to PROVE them... which is impossible.

摘要: 如何准确地丢弃不可能的情况?

Summary: How to exactly discard the impossible cases?

我已经看到一些使用inversion的示例，但是我不理解该过程.

I have seen some examples using inversion but I don't understand the procedure.

最后，如果我的引理取决于几种归纳类型，而我仍然想涵盖所有情况，会发生什么?

Finally, what happens if my lemma depends on several inductive types and I still want to cover ALL cases?

推荐答案

如何丢弃不可能的案例?好吧，确实不能证明前两个义务，但是请注意，它们有相互矛盾的假设(分别为zero <> zero和one <> one).因此，您可以使用tauto证明这些目标(如果您有兴趣的话，还有一些更原始的策略可以解决问题).

How to discard impossible cases? Well, it's true that the first two obligations are impossible to prove, but note they have contradicting assumptions (zero <> zero and one <> one, respectively). So you will be able to prove those goals with tauto (there are also more primitive tactics that will do the trick, if you are interested).

inversion是destruct的更高级版本.除了破坏"归纳法外，它有时还会产生一些相等性(您可能需要).它本身是induction的简单版本，它将另外为您生成归纳假设.

inversion is a more advanced version of destruct. Additional to 'destructing' the inductive, it will sometimes generate some equalities (that you may need). It itself is a simple version of induction, which will additionally generate an induction hypothesis for you.

如果您的目标中有几种归纳类型，则可以一个一个地destruct/invert归类.

If you have several inductive types in your goal, you can destruct/invert them one by one.

更详细的演练:

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.

这篇关于如何在Coq中使用归纳类型的案例的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！