大佬教程收集整理的这篇文章主要介绍了Rbar / Rbar_le / coquelicot 引理,大佬教程大佬觉得挺不错的,现在分享给大家,也给大家做个参考。
我正在通过 Coq 8.12.0 参考手册学习 Coq,但无法证明以下引理。
From Coq require import lia Reals Lra List.
Lemma lemma1 : forall (x y:rbar),Rbar_le x 0 -> Rbar_le y 0
-> Rbar_le (Rbar_plus x y) 0.
Proof.
destruct x ; destruct y ; simpl ; intuition.
destruct H.
destruct H0.
unfold Rle.
auto with real.
right.
...
然后我被困在完成证明过程中。有什么想法吗?
当您输入策略 right
时,您在证明中做出了没有被假设中的事实证实的选择。您应该删除这一行,并尝试找到另一种方法来证明您最初的猜想,这似乎确实可以证明。
实际上,如果您开始展开 Rle
的定义并使用 destruct
,您会进入太多细节。 ...; intuition
之后的目标如下:
1 subgoal (ID 207)
r,r0 : R
H : r <= 0
H0 : r0 <= 0
============================
r + r0 <= 0
这是简单线性算术的目标(因为我们只将变量加在一起并使用简单的比较)。这可以通过一种名为 lra
的强大策略来解决。就叫它。证明的完整脚本在这里:
Lemma lemma1 : forall (x y:rbar),Rbar_le x 0 -> Rbar_le y 0
-> Rbar_le (Rbar_plus x y) 0.
Proof.
destruct x ; destruct y ; simpl ; intuition.
lra.
Qed.
以上是大佬教程为你收集整理的Rbar / Rbar_le / coquelicot 引理全部内容,希望文章能够帮你解决Rbar / Rbar_le / coquelicot 引理所遇到的程序开发问题。
如果觉得大佬教程网站内容还不错,欢迎将大佬教程推荐给程序员好友。
本图文内容来源于网友网络收集整理提供,作为学习参考使用,版权属于原作者。
如您有任何意见或建议可联系处理。小编QQ:384754419,请注明来意。