从Coq中的定义返回记录

假设我有一个包含两个nats的record。 num1 : nat;}.我想构建一个定义，给定两个nats，返回一个包含这两个nats的record。*)谢谢

浏览 0提问于2017-08-12得票数 3

回答已采纳

1回答

如何使Coq形式化可重用？

我在研究一种算法的Coq形式化。但是这个算法的组件(一些函数和引理)可以在不同类型上“重载”(在Haskell意义上)。我的目的是避免代码重复。我知道Coq有模块(如ML)和类型类(如Haskell)。实现引理和函数定义的可重用性的最佳方法是什么?它可以在不同类型上进行参数化？

浏览 2提问于2015-09-30得票数 2

回答已采纳

1回答

Coq :>符号

、、

这可能非常琐碎，但我在Coq中找不到关于':>‘符号的任何信息。U:类型和W :>类型有什么区别？

浏览 0提问于2018-07-18得票数 6

回答已采纳

1回答

关于通配符"_“匹配失败的问题

我正在从软件基金会提供的资源中学习coq。在证明鸽子洞原理的过程中，我试图定义一个函数，从列表中提取子序列，这样里面就没有重复的元素。以下是我的定义： match l with |然而，coq返回消息： Pattern "_&q

浏览 8提问于2022-11-25得票数 0

1回答

从Coq中提取Ocaml中的__

、

从Coq中提取的Ocaml代码包括(在某些情况下)定义如下的类型__和函数__：let __ = let rec f _ = Obj.repr f in Obj.reprf 文档说，在过去，这种类型被定义为unit (因此__可以被视为())，但是存在(很少)将__类型的值应用于__类型的值的情况。__使用了OCaml中未记录的Obj模块函数，但似

浏览 1提问于2013-04-05得票数 6

2回答

在Coq中添加新表示法的问题

我试图定义一个新的表示法范围，并在Coq中添加表示法。我正在遵循Coq手册()中这个页面的指导。Declare Scope myHoTT_scope.其中，concat是一个已经定义的函数。Coq接受所有这些。它不会引发错误或警告。但是，如果我跑唯一返回的是type_scope和nat_scope

浏览 13提问于2022-01-29得票数 1

回答已采纳

1回答

用于定义引理的Coq语法

我可以看到Coq用于定义引理的不同语法。例如，Lemma plus_n_O: forall n:nat, n = n + 0.和Lemma plus_n_O n: n = n + 0.都定义了零与任意数字之和等于该数字。这些定义有何不同？或者，这是Coq的一个新特性，可以从定义中删除forall量词。

浏览 81提问于2019-06-13得票数 2

回答已采纳

1回答

在尝试构建coq源代码时，如何安装dllcoqrun.so？

我正在尝试从源代码构建coq-8.4pl4，我遇到一个错误，说“致命错误:无法加载共享库dllcoqrun原因: dllcoqrun.so:无法打开共享目标文件:没有这样的文件或目录”。我使用的是ubuntu 18.04、ocaml-4.00.0和camlp5-rel707 COQMKTOP -o bin/coqtop.byte File "lib/lib.cma(Errors)",

浏览 19提问于2019-05-21得票数 1

回答已采纳

1回答

来自Coq中空集的函数

我是Coq的新手。我注意到可以使用以下命令在Coq中定义空集 Inductive Empty_set : Set :=. 是否也可以将函数从空集定义到另一个通用集/类型？如果是这样的话，是怎么做的？

浏览 7提问于2020-11-04得票数 2

1回答

`coqc -Q`returns "coqc：-Q:没有这样的文件或目录“

LF编译文件时，我得到了错误： coqc: -Q: no such file or directory coqc信息： The Coq Proof Assistant, version 8.4pl6 (December 2020) compiled on Dec 02 2020 23:06:36 with OCaml 4.02.0 奇怪的是，它以前对我是有效的。我格式化了我的磁盘到相同的操作系统，安装了相同的opam，但我得到了一个错误，我以前没有。出于遗留原因，也使用8.4.6。

浏览 41提问于2020-12-03得票数 0

回答已采纳

1回答

在非归纳类型的类型上相等

我想在Coq中考虑实数上的相等。但是Coq.Reals.Reals.中的R不是归纳类型，所以我不能定义像Nat.eqb这样的函数。如何在Coq中定义实数上的等式？

浏览 7提问于2020-10-11得票数 3

回答已采纳

1回答

如何导入Coq库？

我想在Coq中使用&&作为andb的infix形式。官方文档告诉我，&&是在Coq.Init.Datatypes模块中定义的。我试过这个：Import Coq.Init.Datatypes.Coq仍然给出了错误：在Coq中包含Std库的正确

浏览 7提问于2017-09-03得票数 3

回答已采纳

1回答

这个符号`:>`在Coq中是什么意思？

我看到在record数据类型定义中使用了:>表示法。不确定这是一个标准符号，还是在我正在查看的文件中定义的。

浏览 13提问于2019-04-25得票数 0

回答已采纳

1回答

我们能在Coq中定义递归定义吗？

、、

我知道Coq允许定义相互递归的归纳类型。但是有没有一种方法可以用Coq编写递归定义呢？例如，我想将一个定义写为： Definition myDefinition A := forall B C, (myDefinition B) \/ (A = C).上述定义中的重要部分是myDefinition B，它在另一个参数上递归调用相同的定义。在Coq中可以这

浏览 5提问于2020-11-04得票数 1

1回答

记录是道具吗？

我刚刚了解到'record‘关键字可以用来定义一个Prop类型，例如： Record Equivalence (A : Type) (R : relation A) : Prop := Build_EquivalenceReflexive R; Equivalence_Transitive : Transitive R } 但是当我尝试使用记录来定义一个命题时我通过Coq得到以下消息： proprecord is defin

浏览 20提问于2020-09-02得票数 1

回答已采纳

1回答

如何证明或伪造“`forall (P，q:支柱)，(P -> Q) -> (Q -> P) -> P=q.”？

、、、、

我想在Coq中证明或伪造forall (P Q : Prop), (P -> Q) -> (Q -> P) -> P = Q.。这是我的方法。我认为这可能是因为coq证明了独立性(我不是以英语为母语的人，我不知道确切的单词，请原谅我的无知)，coq使得证明1=2 ->假是不可能的。但是，如果是这样的话，为什么还要消除证据的内容呢？没有上面的命题，我就无法证明下面的命题或它们的否定。 Le

浏览 0提问于2014-10-26得票数 8

回答已采纳

2回答

为什么Coq中的所有数字文字都显示nat类型？

我试图在Coq中使用更大的数字，而在Coq中，内置Nat类型是不合适的。所以我试图用正型或N型来建立特定的值。根据BinNums的标准库文档：正数也将用十进制表示法表示；例如，6%的正数将缩写为xO (xI xH)，N中的数字也将用小数表示法表示；例如，6%的N将缩写Npos (xO (xI xH))。但我的Coq代码仍在给我Nat输入的数字

浏览 5提问于2020-12-02得票数 2

回答已采纳

2回答

为什么实数在Coq中公理化？

、

我想知道Coq是把实数定义为Cauchy序列还是Dedekind割集，所以我检查了Coq.Reals.Raxioms和.这两个人都没有。实数是公理化的，以及它们的操作(如Parameters和Axioms)。为什么会这样呢？而且，实数严格依赖于子集的概念，因为它们的一个定义性质是，每个上有界子集都有一个最小的上界。我的印象是，这些Prop只构成了reals的可定义子集。那么<em

浏览 0提问于2018-08-20得票数 13

回答已采纳

1回答