相关疑难解决方法(0)

我想用这种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但我不明白这个程序.

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