coq 相关问题

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

如何证明一阶语言的条款是否有充分根据？

目前，我已经开始在Coq（VerifiedMathFoundations）中证明有关一阶逻辑的定理。我已经证明了演绎定理，但后来因为正确定理而陷入引理1 ......

coq

回答 1 投票 0

如何在coq中证明ListMap的递归函数定理？

我正在尝试学习在Coq中使用ListMap模块。当ListMap由递归函数创建时，我真的不确定如何证明ListMap中的键或值的属性。我觉得 ...

coq coq-tactic

回答 1 投票 3

Coq：如何在目标中更深入地应用公理？

试图用MT1（或MT1bis）证明MT1A，但Coq无法统一：需要导出Classical_Prop。需要导出Classical_Pred_Type。变量MT：类型。参数NIL：MT。变量a b e：MT - ＆...

coq

回答 1 投票 1

如何将“Zneq_bool a b = true”转换为Coq中“a <> b”的见证人？

我试图证明以下定理：定理Zeq_to_eq：forall（a b：Z），Zneq_bool a b = true - > a <> b。证明。介绍一下b。介绍neq。重写Zeq_bool_neq。录取。我明白了......

coq coq-tactic

回答 1 投票 1

使用Coq中无限表示的有限子集进行计算

我有一个函数Z - > Z - >无论我将其视为从（Z，Z）到任何地图的一种映射，让我们输入它作为FF。无论是从nix还是inj_whatever构造的简单总和。 ...

coq

回答 2 投票 0

如何从Coq假设'd = d + 1'证明`false`和扩展？

目标forall（d：nat），d + 1 = d - > False。证明。介绍d H. Abort。如何从H证明假？反演H只是复制它。

coq

回答 2 投票 0

坚持证明posets中null元素的唯一性

我试图通过在Posets上实施事实来学习COQ。在证明我的第一个定理时，我被困在这里。类Poset {A：Type}（leq：A - > A - > Prop）：Prop：= {reflexivity：forall x y ...

coq

回答 1 投票 1

证明依赖类型实例之间的相等性

当试图形成对应于代数结构的类（例如所有幺半群的类）时，自然设计是创建一个类型monoid（a：Type）作为产品类型......

coq

回答 1 投票 1

如何在Coq中编写一个函数，给定一个列表返回列表中不存在的最小nat？

Coq拒绝接受以下函数，因为没有参数正在减少，但我怎么能说服它因为fvs的长度是有限的，函数会终止？ Fixpoint generate_unique_name（fvs：...

coq

回答 1 投票 2

在Coq中，“if then else”允许非布尔第一个参数？

我在一些教程中读到，如果a，则b表示匹配a与true => b | false => c结束。然而前者非常奇怪的是没有检查a的类型，而后者当然......

if-statement types coq

回答 1 投票 2

如何让Coq接受以下Fixpoint？

我试图为lambda演算编写替换函数，并且在递归调用e上的替换之前，在lambda抽象（\ x.e）的情况下，我必须重命名e中的变量。我怎么能够 ...

coq

回答 1 投票 3

证明唯一的零长度向量是零

我有一个定义为归纳位的类型：nat - > Set：= | bitsNil：位0 | bitsCons：forall {l}，bool - > bits l - > bits（S l）。我试图证明：Lemma emptyIsAlwaysNil：forall {...

coq dependent-type

回答 2 投票 3

如何在Coq中有选择地重写？

a：nat fvs：list nat H：a = max（maxNum fvs）a + 1 H1：max（maxNum fvs）a> = a在H1中执行重写H，替换为as而我只想重写a on RHS。可以吗？一世 ...

coq

回答 1 投票 1

是否有布尔版的`

就像beq_nat返回bool进行eq比较那么<或<=？

coq

回答 1 投票 1

通过归纳证明两个固定点功能

我正在努力寻找看似简单的引理，它涉及2个定点定义。以下两个是CoLoR库的轴向定义：来自Coq Require Import Vector Program。导入...

coq induction

回答 1 投票 2

Coq推理行为

我正在尝试在Coq中编写以下Agda代码段。 open import Data.Fin using（Fin; suc; zero）open import Data.Nat using（ℕ; suc; zero）thin：{n：ℕ} - > Fin（suc n） - > Fin n - > Fin（.. 。

types coq agda dependent-type

回答 2 投票 2

Coq中的“true = false”是什么意思？

[我不确定这是否适合堆栈溢出，但是这里还有很多其他Coq问题，所以也许有人可以提供帮助。]我正在从http://www.cis.upenn.edu/来完成以下工作......

logic coq

回答 3 投票 25

程序修复点：在“let”中递归调用和义务的假设

假设我有以下程序修复点：来自Coq需要导入列表程序。导入ListNotations。程序Fixpoint f l {measure（length l）}：list nat：= let f_rec：=（f（tl l））in match ...

coq totality

回答 1 投票 2

如何划分Coq代码以提供Coq ideslave（XML协议）？

我认为Coq ideslave（也称为Coq XML协议）的“添加”调用一次只占用一块代码，用句点（。）分区。在大多数情况下，我仍然相信这是真的。例如， ...

coq coqide

回答 1 投票 2

如何处理Coq中Program Fixpoint生成的非常大的术语？

我试图在Coq中定义和证明一个有效区分两个排序列表的函数。因为它并不总是在一个结构较小的术语上递归（第一个或第二个列表是...

coq

回答 2 投票 4

coq 相关问题

最新问题