Coq是一种形式化的证明管理系统，半交互式定理证明器和函数式编程语言。 Coq用于软件验证，编程语言的形式化，数学定理的形式化，教学等。由于Coq的交互性，如果认为合适，我们建议将问题链接到https://x80.org/collacoq/上的可执行示例。
在下面的示例中，统一（不出所料）不会推断规范结构：结构Pn：= sr {gs：nat}。规范结构Pn_1：Pn：= sr 1.规范结构Pn_2：Pn：= sr 2. ...
Coq 8.7集成了流行的Ssreflect库。因此可以通过以下方式导入其库：从Coq需要导入ssreflect ssrfun ssrbool。但是，当我尝试导入ssrnat时......
我想将以下PVS翻译成Coq：其中type trans的类型为env - > env - > bool，我按如下方式编写Coq代码：定义trans：= env - > env - > bool。定义dseq（P Q：......
在Coq中编写Ltac时，可能会试图用| - context [？x && true] => rewrite andb_true_r end编写try match目标，而不是尝试重写andb_true_r而不调用rewrite ...
作为VST项目中的一个示例，reverse.c文件有一个如下链接列表：struct list {unsigned head; struct list * tail;}; unsigned sumlist（struct list * p）{unsigned s = 0;结构列表...
Coq无法使用Fix定义有根据的定义，但如果使用Program Fixpoint定义则可以
作为通过有充分理由的关系理解递归的练习，我决定实现扩展的欧几里德算法。扩展的欧几里得算法适用于整数，所以我需要一些很好的...
我正在尝试使用Coq在正则表达式（RE）上形式化一些属性。但是，我有一些麻烦来证明一个相当简单的属性：对于所有字符串s，如果s是（epsilon）语言...
我安装了带有opam的Coq，并希望制作一个Coq插件。我设法使用coq_makefile编译了一些插件示例，但是如果我可以在vim中使用merlin来获取类型信息和...
平凡的，我试图将我自己的bool类型定义为：Inductive mybool：Type：= |是的|假。然后我做了一个“打印mybool”。但输出结果为：Inductive mybool：Set：= true：mybool | ...
我有一个Coq函数，可以对素数进行分类。我将它导出到Haskell并进行测试;它工作正常。我想严格证明它确实对素数进行了分类，所以我试图证明以下内容......