1回答
Coq:列表对的证明
coq、coqide
我写了这个归纳谓词，并对其(强)规范进行了部分证明：| sp_base : SumPairs问题是，我不认为这个定理是正确的，因为Coq不接受像{n0 n1: nat | ...}这样的东西。有没有办法解决这个问题，还是我想错了？我认为谓词SumPairs是正确的，但由于我不确定，这里有一个它应该如何工作的示例:输入[(1,2),(3,4
浏览 13提问于2021-05-24得票数 2
回答已采纳
3回答
如何在Coq中对列表的长度进行归纳？
coq、induction
在纸上推理的时候，我经常用归纳的方式对某些列表的长度进行论证。我想用Coq将这些参数正规化，但似乎没有任何方法可以对列表的长度进行归纳。更具体地说，我试图证明。在理论上，我通过对w长度的归纳法证明了这一点。我的目标是在Coq中把这个证明正式化。
浏览 7提问于2017-08-25得票数 7
回答已采纳
1回答
如何设置Coq作为一阶逻辑的定理证明器
logic、computer-science、coq、coq-tactic、coq-plugin
据我所知，Coq有内置的一阶逻辑https://coq.inria.fr/tutorial/1-basic-predicate-calculus。但Coq不是定理证明者，Coq是证明助手，这意味着用户需要在每一步中提供一些提示，Coq应该选择什么规则/策略。存在更多的ore - lest组合启发式策略，但Coq仍然不是证明者。我听说过在证明<
浏览 21提问于2019-05-15得票数 3
回答已采纳
1回答
余弦中Prop，Set和Type_i的基数
coq、cardinality
我们可以将Coq中的分配给Prop、Set和每个Type_i吗？我只在Coq的库中看到了的定义，所以也许我们首先需要大基数的定义。根据证明无关的语义，例如暴露的，Set和Type_i形成一个递增的序列。这可以在Coq中得到证明吗？
由于不可预测性，Prop看起来更复杂。证明无关意味着我们识别同一P : Prop的所有证明，并将P
浏览 13提问于2018-08-28得票数 4
回答已采纳
2回答
我已经读过软件基础系列，并且对Coq基础有很好的理解。但是，任何非平凡的东西的证明都变得太冗长和乏味。
为熟悉基础知识的人编写易于管理的大型Coq证明的策略是什么？
浏览 3提问于2017-12-04得票数 1
2回答
可以用Coq编写C程序吗？
coq、coq-extraction
我知道可以将Coq程序提取到Haskell和OCaml程序中。有没有办法用C来做这件事？
我正在想象一个模拟C语言的库。也许这样的库会包含一组关于C结构如何与进程内存交互的公理，以及关于IEEE浮点数的公理和定理。然后，它就可以在Coq内建立一个C程序，以及关于这个程序的定理。比如说，我会使用这样一个库来构建一个C快速排序算法，该算法可以在GCC可编译的浮点数数组上工作。
浏览 6提问于2017-10-23得票数 8
回答已采纳
1回答
如何证明空列表的子序列为空？
coq、coq-tactic
我是coq的新手。我试图证明空列表的子序列是空的。 这是我正在研究的引理： Lemma sub_nil : forall l , subseq l nil <-> l=nil.我试着分开，这样我就可以 subseq l nil -> l = nil 和 l = nil -> subseq l nil 为了证明第一个问题，我尝试了对l进行归纳，但我在证明时受阻 subseq (
浏览 21提问于2020-10-11得票数 0
回答已采纳
2回答
Coq中普遍量化的方法
coq
我对Coq定理证明器很陌生。因此，我很可能已经错过了一些基本的东西，在阅读教程时。
在我提出我的问题之前，让我假设一些假设，并回顾一下我的想法。有了这些假设，就可以应用Consequent模型:可以根据Minor前提和Major前提构造推断Major的证明。这样的证明就是带有参数Minor的Minor函数的应用。那么，现在我想知道:在具有普遍量化命题的Co
浏览 4提问于2014-05-06得票数 0
5回答
认证计划的定义
coq、isabelle、agda、idris
我看到了几个不同的研究小组，至少有一本书，他们谈到了使用Coq来设计认证的程序。对认证课程的定义有共识吗？据我所知，它真正的意思是程序被证明是完全正确的。现在，程序的类型可能是一些非常奇特的东西，比如一个列表，证明它是非空的，排序的，所有元素都是>= 5的，等等。回到我最初的问题，什么是认证计划的
浏览 59提问于2014-01-24得票数 18
3回答
使用Coq证明助手证明(p->q)->(~q->~p)
logic、coq、theorem-proving
我是Coq的新手，正在尝试Ruth和Ryan的样例引理。使用自然演绎的证明非常简单，这就是我想用Coq来证明的。 assume ~q.有没有人能告诉我自然演绎和Coq关键字之间是否存在一对一的映射关系？
浏览 3提问于2013-02-01得票数 2
1回答
我是新来的科克。为了实现对列表和对列表的练习，我使用Coq列表库证明了一个简单的自然数定理。我试图证明自然数的简单性质：((a0*multiplier)=d1)+((a1*multiplier)=d2)+((我使用对列表(将a存储在一个列表中，
浏览 0提问于2018-02-08得票数 0
回答已采纳
1回答
Z3与coq的区别
z3、coq、theorem-proving
我想知道是否有人能告诉我Z3和coq之间的区别？在我看来，coq是一个证明助手，因为它要求用户填写证明步骤，而Z3没有这一要求。但似乎coq也有类似于Z3的自动策略？或者可能coq中的证明搜索能力没有Z3那么强大？
浏览 1提问于2012-07-18得票数 44
回答已采纳
2回答
Coq:证明‘P -> ~P -> Q’而不是‘矛盾’策略？
coq、coq-tactic
我正在学习Coq，我发现它是有建设性的。这是我可以证明“矛盾意味着一切”的一种方法，它起作用：
Theorem contradiction_implies_anything: forall P Q : Prop, P -> ~P -> Q.注意，没有Q是构造的，所以我假设contradiction是内置到Coq验证引擎中的。在我看来，如果不是这样，我们就得证明Q是如何构造的，而且不可能有任何Q，因此不能证明</em
浏览 4提问于2021-07-27得票数 1
回答已采纳
1回答
我正在考虑用Coq编写代码并提取这些代码，以便在一个大型Haskell项目中使用。我想在Coq中构建一个模块，证明属性，然后使用Haskell的模块系统来防止违反这些属性(通过智能构造函数)。我找不到任何迹象表明可以使用显式导出列表将Coq代码提取到Haskell模块中。似乎我必须手动修改提取的Coq代码，这不是什么大问题，但我想知道我是否正确。有没有人有替代方案？
浏览 3提问于2011-09-17得票数 5
回答已采纳
1回答
Coq中的反例证明
coq、proof、quantifiers、negation
在证明了命题和谓词演算中的数十个引理(有些比另一些更具有挑战性，但通常仍然可以在intro-apply-destruct自动驾驶仪上证明)之后，我碰到了一个起始w/ ~forall的引理，并立即陷入困境显然，我对Coq缺乏理解和知识。所以，我要求用一种低级的Coq技术来证明一般形式的语句。exists A [B].., ~(C -> D).
浏览 2提问于2016-03-01得票数 4
回答已采纳
1回答
我对Coq非常陌生，当我尝试使用作为一个证明时，我有一个错误。例如，考虑到以下情况：(就我现在而言，Coq.Init.Logic是自动加载的，所以这里没有必要，但是问题是相同的。)
浏览 5提问于2017-11-22得票数 1
回答已采纳
1回答
利用余弦证明有限集的幂集是有限的
math、coq、formal-verification、powerset
在试图证明一些事情时，我遇到了一个看起来很无辜的声明，但我在Coq中未能证明。我们的主张是，对于给定的有限集合，powerset也是有限的。该语句在下面的Coq代码中给出。我查阅了关于有限集的Coq文档以及关于有限集和幂集的事实，但我找不到可以将powerset解构为子集并集的东西(这样就可以使用Union_is_finite构造函数)。另一种方法可能是证明pow
浏览 28提问于2019-05-21得票数 5
1回答
在不指定Theorem定义的情况下，在Coq中进行交互式定理证明的最佳方法是什么？我想陈述一些初始假设和定义，然后交互式地探索转换，看看我是否可以在事先不知道的情况下证明任何有趣的定理。我希望Coq能帮助我跟踪转换后的假设，并检查我的重写是否有效，就像在交互模式下证明显式定理一样。Coq是否支持此用例？
浏览 3提问于2018-03-30得票数 2
2回答
Coq核的证明技术
coq
伊莎贝尔将其核心证明能力建立在与高阶统一相结合的分辨率上。命题作为类型可能会占用过多的空间；什么将取代Huet的高阶逻辑统一程序？。
浏览 3提问于2020-08-12得票数 1
回答已采纳
云服务器
对象存储
ICP备案
云点播
腾讯会议
腾讯云开发者
Copyright © 2013 - 2026 Tencent Cloud. All Rights Reserved. 腾讯云 版权所有
深圳市腾讯计算机系统有限公司 ICP备案/许可证号：粤B2-20090059 
粤公网安备44030502008569号
腾讯云计算（北京）有限责任公司 京ICP证150476号 | 京ICP备11018762号