coq 相关问题

Coq是一种形式化的证明管理系统，半交互式定理证明器和函数式编程语言。 Coq用于软件验证，编程语言的形式化，数学定理的形式化，教学等。由于Coq的交互性，如果认为合适，我们建议将问题链接到https://x80.org/collacoq/上的可执行示例。

在Coq中编写Ltac时，可能会试图用| - context [？x && true] => rewrite andb_true_r end编写try match目标，而不是尝试重写andb_true_r而不调用rewrite ...

coq coq-tactic

回答 2 投票 2

作为VST项目中的一个示例，reverse.c文件有一个如下链接列表：struct list {unsigned head; struct list * tail;}; unsigned sumlist（struct list * p）{unsigned s = 0;结构列表...

coq verifiable-c

回答 1 投票 1

（似乎我之前的问题有太多不相关的信息，所以我试图抽象出细节。我不确定它仍然是同一个问题，但是我会删除另一个问题，如果......

coq

回答 2 投票 3

作为通过有充分理由的关系理解递归的练习，我决定实现扩展的欧几里德算法。扩展的欧几里得算法适用于整数，所以我需要一些很好的...

recursion coq totality

回答 1 投票 5

我正在尝试使用Coq在正则表达式（RE）上形式化一些属性。但是，我有一些麻烦来证明一个相当简单的属性：对于所有字符串s，如果s是（epsilon）语言...

coq

回答 3 投票 4

我安装了带有opam的Coq，并希望制作一个Coq插件。我设法使用coq_makefile编译了一些插件示例，但是如果我可以在vim中使用merlin来获取类型信息和...

vim ocaml coq ocamlfind merlin

回答 3 投票 5

在像Coq这样的建设性环境中，我希望A / B的析取证明要么是A的证明，要么是B的证明。如果我在X的子集上重新拟定它，它说如果我有一个 ...

coq

回答 2 投票 2

我试图为某些特定的相互递归类型定义归纳原理，我有点困惑。使用Schema并没有真正解决我的问题，这就是我考虑定义原理的原因......

coq

回答 1 投票 0

平凡的，我试图将我自己的bool类型定义为：Inductive mybool：Type：= |是的|假。然后我做了一个“打印mybool”。但输出结果为：Inductive mybool：Set：= true：mybool | ...

coq

回答 1 投票 1

我有一个Coq函数，可以对素数进行分类。我将它导出到Haskell并进行测试;它工作正常。我想严格证明它确实对素数进行了分类，所以我试图证明以下内容......

primes coq

回答 1 投票 1