我想使用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但我不明白这个程序。
最后，如果我的引理取决于几种归纳类型并且我仍然想涵盖所有情况，会发生什么？
如何排除不可能的情况？嗯，确实前两项义务无法证明，但请注意它们有相互矛盾的假设（zero <> zero and 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.
本文内容由网友自发贡献，版权归原作者所有，本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容，请联系:hwhale#tublm.com(使用前将#替换为@)
