我试图证明下面这个微不足道的引理： Lemma lt_or_ge: forall a b : nat,Proof.我需要这样的东西： ((a <? b) = false) -> (a >= b) 但似乎在Coq库中找不到它。感谢您的帮助，谢谢。
浏览 31提问于2020-02-01得票数 1
回答已采纳
我是Coq的新手，正在尝试Ruth和Ryan的样例引理。使用自然演绎的证明非常简单，这就是我想用Coq来证明的。 assume ~q.assume p. False.
therefore ~p.therefore ~q -> ~p</em
浏览 3提问于2013-02-01得票数 2
我试着用tatics的介绍，应用，假设，销毁，左，右，分裂来证明这个引理，但失败了。有人能教我怎么证明吗？proof.一般情况下，如何证明诸如false->P，P/~P等简单命题？
浏览 0提问于2012-10-03得票数 5
回答已采纳
我对coq编程完全陌生，不能证明下面的定理。我需要帮助的步骤如何解决下面的构造？我尝试了下面的证明方法。Theorem PeirceContra: forall (p q:Prop), ~ p -> ~((p</e
浏览 0提问于2019-04-15得票数 0
我想在Coq中证明或伪造forall (P Q : Prop), (P -> Q) -> (Q -> P) -> P = Q.。这是我的方法。我认为这可能是因为coq证明了独立性(我不是以英语为母语的人，我不知道确切的单词，请原谅我的无知)，coq使得证明</e
浏览 0提问于2014-10-26得票数 8
回答已采纳
我试图在coq中证明(~Q -> ~P) -> (P-> Q)，这是反正定理(P -> Q) (~Q -> ~P)的逆。目前我正在考虑使用同样的逻辑来证明反正定理，如下所示：
不展开。介绍A。B。C。也许我需要额外的公理来证明反正定理的逆。有谁可以帮我？
浏览 40提问于2021-05-12得票数 0
回答已采纳
我正在学习Coq，我发现它是有建设性的。这是我可以证明“矛盾意味着一切”的一种方法，它起作用： contradiction.注意，没有Q</e
浏览 4提问于2021-07-27得票数 1
回答已采纳
1回答
根据Coq的文件
我认为，在Coq实现的直观(或建设性)逻辑中，这已经是分离的一个属性。例如，要证明Coq中排除的中间p \/ ~p，必须做实际工作，这不是一个逻辑公理。因此，p \/ q的证明必须是p的</
浏览 2提问于2018-07-11得票数 5
回答已采纳
我对coq很陌生，所以如果你只说自我介绍的话。我不知道该介绍什么。所以要有针对性，比如。(简介p. q.)会很有帮助的。
浏览 7提问于2022-03-01得票数 0
作为coq的新手，我无法找到这个非常简单的问题的答案(我相当肯定没有被问到这个问题，因为它是多么的基本)。我正在做家庭作业，为此我需要用coq来证明：
这是一个足够简单的证明，我可以在纸上做，但我似乎不能得到coq来为我这样做。我的策略是假设P<
浏览 5提问于2012-09-23得票数 2
回答已采纳
1回答
我正试图证明Coq中的一个二分派：我写下了一个有这种结构的证据：<-> <-><->thus: P <-> Q
如何在Coq中模拟这个计算证明结构？
浏览 2提问于2015-11-20得票数 2
回答已采纳
我试图证明一个关于Prop的替换定理，但我失败得很痛苦。下面的定理能在coq中被证明吗?如果不能，为什么不能。Theorem prop_subst: (P <-> Q) -> ((f P) <-> (f Q))重点是，在逻辑上，证明是通过归纳的。
浏览 2提问于2012-06-17得票数 7
目前，我对如何证明以下定理感到困惑： (forall P Q : Prop, (P -> Q) -> (~P \/ Q)) -> (forallP, P \/ ~P).我被困在这里： (forall P Q : Prop, (<
浏览 4提问于2021-12-25得票数 0
回答已采纳
1回答
在惠誉中，我试图构造((p⇒q)⇒p)⇒p的一个形式证明。我知道这是真的，但我怎么证明呢？我只能使用和介绍，和Elim，或Inro，或Elim，Neg Intro，Neg Elim，Impl Intro，Impl Elim，Biconditional，和Biconditional Elim。
浏览 1提问于2017-03-16得票数 1
我试图用公理证明余式中的(p -> q) -> (~ p/ q)： Axiom tautology : forall P:Prop, P \/ ~ P.我正在尝试通过应用p -> q将~p/q转换为~p/p。所以这样做： Theorem Conversion: foral
浏览 19提问于2019-04-13得票数 0
回答已采纳
1回答
如何使用Coq证明以下几点？(q，V，p)∧(p，p，q) <-> (p，V，q) 我的尝试 Lemma work: (forall p q: Prop, (q \/ p)/\(~p -> q) <-> (p \/ q</em
浏览 8提问于2019-02-24得票数 0
回答已采纳
我试着做精益文档中的一章，但我很难理解所有的术语，因为我几乎不知道如何写校样。我想了解更多，但需要一些帮助。我一直在尝试和错误地尝试解决这个例子：不知道从哪里开始。有没有我在解释中遗漏的答案？
浏览 22提问于2020-05-13得票数 0
回答已采纳
1回答
Coq中的反例证明
、、、
在证明了命题和谓词演算中的数十个引理(有些比另一些更具有挑战性，但通常仍然可以在intro-apply-destruct自动驾驶仪上证明)之后，我碰到了一个起始w/ ~forall的引理，并立即陷入困境显然，我对Coq缺乏理解和知识。所以，我要求用一种低级的Coq技术来证明一般形式的语句。exists A [B].., ~(C -> D).总之，我希望有一个
浏览 2提问于2016-03-01得票数 4
回答已采纳
1回答
我想在Coq中证明以下逻辑等价性。以下是我的尝试。我怎么才能解决这个问题？Lemma work : (forall p q : Prop, (p->q)->(~q->~p)).Proof.intros p_impl
浏览 0提问于2019-02-21得票数 0
回答已采纳
扫码
添加站长 进交流群
领取专属 10元无门槛券
手把手带您无忧上云
相关资讯
热门标签
云服务器
ICP备案
对象存储
腾讯会议
云直播活动推荐
腾讯云开发者
