如何在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屋!