我想用这种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和one <> one分别).因此,您将能够证明这些目标tauto(如果您感兴趣,还有更多原始战术可以解决这个问题).
inversion是一个更高级的破坏版本.除了"破坏"归纳法之外,它有时会产生一些平等(你可能需要).它本身就是一个简单版本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.
如果你看到一个不可能实现的目标,那么有两种可能性:你在证明策略中犯了错误(也许你的引理是错误的),或者假设是矛盾的.
如果您认为这些假设是矛盾的,那么您可以设定目标False,以避免一些复杂性.elimtype False实现了这一点.通常,你False通过证明一个命题P及其否定来证明~P; 这个策略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打破了证明分为两个subproofs,一个是n = 0和一个n = S m.如果n在其他假设中使用(即你有一个H : P n),你可能需要记住,n你已经破坏了n这些假设中使用的相同:case_eq n这样做.inversion对假设的类型进行案例分析.当假设的类型存在依赖性时会特别有用destruct.您通常会使用case_eq假设Set(相关性相关)和inversion假设Prop(具有非常依赖类型).这种inversion策略背后留下了许多平等,而且通常会subst简化假设.该inversion_clear策略是一个简单的替代inversion; subst,但失去的少量信息.induction意味着您将通过对给定假设的归纳(=递归)来证明目标.例如,induction nwhere 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不要担心目标,并且tauto没有第elimtype False一个(IIRC它没有在旧版本的Coq中没有写),它就开始工作了.你可以tauto通过写作来了解Coq正在采取的策略info 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 -> False.所以,False是的结论H0:
apply H0.
现在我们需要证明zero=zero,这是
reflexivity.
现在我们已经证明了我们的主张False.剩下的就是证明这False意味着我们的目标.嗯,False暗示任何目标,这是它的定义(False被定义为具有0个案例的归纳类型).
destruct F.