3回答
我想证明一些简单的事情，比如对于每个自然数n，都存在一个自然数k，使得：如何进行这样的证明呢？当n是奇数或偶数时，我想把它分成几种情况，但我不知道如何在Coq中这样做。另外，在Coq中有内置的幂(指数)运算符吗？
浏览 11提问于2018-01-24得票数 2
1回答
: Tipe______________________________________(1/1)
False (其中TApp是一个构造函数) 在Idris中，可以用\Refl => impossible来证明这一点，但我还没有设法在Coq中为它编写任何证明。有没有简单的方法来证明这一点？
浏览 16提问于2019-04-01得票数 1
回答已采纳
1回答
我理解Coq和Idris这样的语言是如何被用来证明用这些语言编写的程序的特性的(从我在这个主题上的一点经验来判断)，但是我想知道是否有一种可以在已经存在的代码基上进行外部操作的平易近人的方法。有没有一种方法可以使用像Coq这样的工具或者其他一些专门的工具来证明用C++编写<e
浏览 2提问于2014-12-14得票数 14
回答已采纳
2回答
我是Coq的初学者。 虽然计算机为我验证了证明是令人满意的，但对于人类来说，满足Coq的证明是出了名的难以阅读。下面是一个简单的例子，假设你没有看到任何评论： Theorem add_comm : forall n m : nat,Proof.老实说，没有注释我无法阅读校样，如果我想向不了解Coq的观众展示它，就更不用说了。 手动编写</
浏览 27提问于2021-09-06得票数 3
是否有可能以及如何在前向链接模式中将Coq用作计算器或规则引擎？Coq脚本通常需要声明可以找到证据的目标。但是，是否有可能在其他方向上进行，例如，计算由某些规则限定的一些结果的集合，例如，通过一些步骤。我对全一阶逻辑的序列演算特别感兴趣。我猜(但我不知道)有一些一阶逻辑的序列演算的实现或包，但它是用于定理证明的。我喜欢用这样的顺序演算来推导出一些有指导的顺序<em
浏览 1提问于2019-09-08得票数 0
1回答
我正在尝试证明以下关于自然数的平凡抵消定理： forall i, j, k in nat .((i+j) = (i+k)) -> (j = k) 下面是我用Coq编写的代码 Theorem cancel : forall (i j k : nat),
((add i j) = (add i之后，Coq试图证明归纳的基础，这是微不足道的： j = k -> j = k 几乎所有的Coq
浏览 11提问于2019-01-16得票数 0
回答已采纳
我正在考虑用Coq编写代码并提取这些代码，以便在一个大型Haskell项目中使用。我想在Coq中构建一个模块，证明属性，然后使用Haskell的模块系统来防止违反这些属性(通过智能构造函数)。我找不到任何迹象表明可以使用显式导出列表将Coq代码提取到Haskell模块中。似乎我必须手动修改提取的Coq代码，这不是什么大问题，但我想知道我是否正确。有没有人有替代方案？
浏览 3提问于2011-09-17得票数 5
回答已采纳
1回答
定义和Coq中的“让”有什么区别？为什么有些定义需要证明？就像。这是群论中g1.v的一段代码。
Definition exp : Z -> U -> U.这个证据的目的是什么？
浏览 3提问于2015-02-11得票数 5
回答已采纳
1回答
我想知道是否有人能告诉我Z3和coq之间的区别？在我看来，coq是一个证明助手，因为它要求用户填写证明步骤，而Z3没有这一要求。但似乎coq也有类似于Z3的自动策略？或者可能coq中的证明搜索能力没有Z3那么强大？
浏览 1提问于2012-07-18得票数 44
回答已采纳
1回答
类似Agda的Coq/编程？
、、、、
与Agda不同，Coq倾向于将证明与函数分开。Coq给出的策略非常适合编写证据，但我想知道是否有一种方法可以复制Agda模式的功能。
相当于Agda模式下的C- C -r (reify)，在这里您用函数
浏览 6提问于2017-01-24得票数 10
回答已采纳
2回答
如何找到像intros或destruct这样的东西的确切含义，比如查找一个实现(或者如果不可能的话，一个定义)？怎样才能有效地做到这一点？
浏览 4提问于2020-09-10得票数 2
回答已采纳
我刚刚从CMU讲座中了解到，虽然Check Type以Coq格式返回Type : Type，但左、右的Types被不同的数字隐式索引，因为如果它们是相同的，就会导致类似Burali-Forti悖论的类型理论模拟如果您试图实现这样一个悖论，Coq将拒绝编译。
我很好奇Coq脚本中这个悖论是什么样子，但是找不到任何代码。一些讨论提到了B.Barras的“coq中的Burali-Forti悖论的形式化”，
浏览 2提问于2015-08-13得票数 2
回答已采纳
2回答
我知道可以将Coq程序提取到Haskell和OCaml程序中。有没有办法用C来做这件事？
我正在想象一个模拟C语言的库。也许这样的库会包含一组关于C结构如何与进程内存交互的公理，以及关于IEEE浮点数的公理和定理。然后，它就可以在Coq内建立一个C程序，以及关于这个程序的定理。比如说，我会使用这样一个库来构建一个C快速排序算法，该算法可以在GCC可编译的浮点数数组上工作。
浏览 6提问于2017-10-23得票数 8
回答已采纳
在Coq中，命题是类型，证明是值。例如，我们可以写一个这样的简单证明，它证明了0=0。eq_reflwhere?x : [ |- ?A]
这意味着eq_refl的所有参数都是隐式的。在Coq中，除非使用@
浏览 8提问于2018-02-13得票数 4
回答已采纳
我已经读过软件基础系列，并且对Coq基础有很好的理解。但是，任何非平凡的东西的证明都变得太冗长和乏味。
为熟悉基础知识的人编写易于管理的大型Coq证明的策略是什么？
浏览 3提问于2017-12-04得票数 1
在不指定Theorem定义的情况下，在Coq中进行交互式定理证明的最佳方法是什么？我想陈述一些初始假设和定义，然后交互式地探索转换，看看我是否可以在事先不知道的情况下证明任何有趣的定理。我希望Coq能帮助我跟踪转换后的假设，并检查我的重写是否有效，就像在交互模式下证明显式定理一样。Coq是否支持此用例？
浏览 3提问于2018-03-30得票数 2
1回答
我有点搞不懂Coq 中关于自然数定义的后继函数的内射性是否是公理？，根据，它是公理(7)。但令我困惑的是，在这一页的顶部写着：
这句话有点模棱两可不是吗？
浏览 3提问于2019-01-16得票数 5
回答已采纳
Require Import Coq.Reals.Reals.我不知道怎么证明。Euc 0不是一种归纳类型，所以我不能使用destruct t或induction t。
请告诉我如何证明。
浏览 1提问于2020-09-07得票数 2
回答已采纳
扫码
添加站长 进交流群
领取专属 10元无门槛券
手把手带您无忧上云
相关资讯
热门标签
云服务器
ICP备案
云直播
对象存储
实时音视频活动推荐
腾讯云开发者
