Coq证明#Coq
Coq证明#Coq
提问于 2022-01-01 03:53:55
我试图解决这个证据，但我找不到它的方法。我有两个子目标，但我甚至不知道它是否正确。
这里是我试图解决的引理，但我被困住了：
2个次级目标
a，b: Nat
H: Equal (leB a，b) True
______________________________________(1/2)
等匹配b与
Z => False
S‘=> leB a m’
结束(leB A b) /相等(leB b (S a)) (leB A b)
______________________________________(2/2)
相等(leB (S ) b)真/等(leB b (S ))真
Inductive Bool : Type :=
True : Bool | False : Bool.
Definition Not(b : Bool) : Bool :=
Bool_rect (fun a => Bool)
False
True
b.
Lemma classic : forall b : Bool, Equal b (Not (Not b)).
Proof.
intro.
induction b.
simpl.
apply refl.
simpl.
apply refl.
Qed.
Definition Equal(T : Type)(x y : T) : Prop :=
forall P : T -> Prop, (P x) -> (P y).
Arguments Equal[T].
(* Avec certaines versions Arguments Equal[T] *)
Lemma refl : forall T : Type, forall x : T, Equal x x.
Proof.
intros.
unfold Equal.
intros.
assumption.
Qed.
Fixpoint leB n m : Bool :=
match n, m with
| Z, _ => True
| _, Z => False
| S n', S m' => leB n' m'
end.回答 1
Stack Overflow用户
回答已采纳
发布于 2022-01-02 08:59:38
首先，不要在intros开头引入所有变量。你会得到一个太弱的归纳假说。只需介绍一下a。
然后，在每个分支中，用b策略考虑不同的destruct情况。它将简化您的目标，您可以看到目标的左边或右侧是真的，并使用您的refl引理来完成目标。
最后一种情况要求您使用您的归纳假设，在这里，重要的是它适用于所有的b，而不仅仅是一个特定的b。
另外，您没有为您的Nat类型提供定义，我想是这样的：
Inductive Nat := Z | S (n:Nat).这是一个证据。
Lemma Linear : forall a b, (Equal (leB a b) True) \/ (Equal (leB b a) True).
Proof.
induction a.
- intros b. destruct b; simpl.
+ left. apply refl.
+ left. apply refl.
- intros b. destruct b; simpl.
+ right. apply refl.
+ destruct (IHa b) as [Hleft | Hright].
++ left. apply Hleft.
++ right. apply Hright.
Qed.虽然它可能不那么有洞察力，但你也可以使用策略尝试这些步骤，以获得一个较短的证据。
induction a; destruct b; firstorder.也会证明你的引理。
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/70548700
复制相关文章
相似问题
腾讯云哪里有金融云服务器？申请流程是什么？
请问腾讯金融云在金融机构的业务场景？
腾讯云怎样进行移动金融？
为什么我的金融服务里面的云支付是404？
借助小程序·云开发制作校园导览？
添加站长 进交流群
领取专属 10元无门槛券
AI混元助手 在线答疑
关注 腾讯云开发者公众号
洞察 腾讯核心技术
剖析业界实践案例
腾讯云开发者
