是否可以在coq中打印未完成校样的部分定义？
在Coq中，可以使用Print命令来打印未完成校样的部分定义。Print命令用于显示当前环境中的定义、定理和引理等信息。
要打印未完成校样的部分定义，可以按照以下步骤操作：
- 打开Coq的交互式环境，例如CoqIDE或Coqtop。
- 在Coq中定义一个未完成校样的部分，例如一个函数或一个类型。
- 使用Print命令来打印该部分定义。例如，如果要打印一个函数的定义，可以使用以下命令：
- 使用Print命令来打印该部分定义。例如，如果要打印一个函数的定义，可以使用以下命令：
- 其中，function_name是要打印的函数的名称。
- Coq会显示该函数的定义信息，包括参数类型、返回类型和函数体等。
需要注意的是，打印未完成校样的部分定义只会显示已经定义的部分，而不会显示未完成的部分。这是因为Coq是一个交互式证明助理，它会根据已有的定义和定理来进行推理和证明，而未完成的部分无法进行推理和证明。
关于Coq的更多信息和使用方法，可以参考腾讯云的Coq产品介绍页面：Coq产品介绍。
相关·内容
3回答
我刚接触过Coq，从事集合论证明写作。
我意识到括号被省略了，这使我很难读懂公式。例如,
1 subgoal
A, B : {set T}
H : B \subset A
______________________________________(1/1)
A :\: A :|: A :&: B = B
但是我想让Coq打印(A :\: A) :|: (A :&: B) = B。上面的输出是由折叠代码获得的。
Require Import ssreflect ssrbool ssrnat fintype finset.
Theorem a_a_b__b' (A B :
浏览 3提问于2016-10-04得票数 9
1回答
我想知道是否有人能告诉我Z3和coq之间的区别？在我看来，coq是一个证明助手，因为它要求用户填写证明步骤，而Z3没有这一要求。但似乎coq也有类似于Z3的自动策略？或者可能coq中的证明搜索能力没有Z3那么强大？
浏览 1提问于2012-07-18得票数 44
回答已采纳
1回答
我从命令行对这个简单的输入文件调用Coq：
$ cat AddingZero.v
Theorem plus_O_n : (forall n, O + n = n).
Proof.
intros n.
simpl.
exact (eq_refl n).
Qed.
我是这样做的：
$ coqc ./AddingZero.v ; echo $?
0
当我看到0输出时，我知道一切正常，所以我尝试通过执行以下操作来检查Coq的输出：
$ vim ./AddingZero.vo
但是我得到了一些二进制的胡言乱语。我做错了什么？谢谢!
浏览 11提问于2018-08-09得票数 0
回答已采纳
我首先定义一个帮助器函数，用于构建给定{P} + {~P}证明的Decidable P实例
Require Import Coq.Classes.DecidableClass.
Definition derive_decidable : forall P : Prop, {P} + {~P} -> Decidable P.
intros P H; destruct H;
[ apply (Build_Decidable P true) | apply (Build_Decidable P false) ];
intuition congruence.
Qed.
现在我定义了一个愚蠢的
浏览 0提问于2018-01-22得票数 1
回答已采纳
2回答
我正在用emacs研究Coq。我垂直拆分emacs窗口，左边是文档，右边是代码编辑区。当我解释Coq程序时，结果将显示在左侧窗口并覆盖文档。这让我很困扰。是否有这样一种方式，我可以水平拆分代码编辑区，并在右下角显示解释结果？
浏览 2提问于2017-09-17得票数 1
1回答
这里我的意思是公理是我们可以用command中的Axiom关键字定义的，而不是通过传递给Coq的命令行参数来定义的。
我知道一些公理使得Coq不一致。然而，AFAIK他们并没有使Coq图灵完成。在我的粗略理解中，这是因为它们没有提供任何额外的计算行为。
是否有一个能使Coq变成完整的？如果没有，你能给出更具体的解释为什么这是不可能的吗？
浏览 5提问于2021-07-08得票数 3
回答已采纳
2回答
这是一个基本的问题。Coq有一种Gallina形式的规范语言。据我所知，Coq本身是用OCaml编写的。
我的问题是，Gallina什么时候开始发挥作用？它是用来做什么的，为什么？我想我误解了规范语言和编程语言的使用。
浏览 39提问于2019-08-14得票数 1
问题：
Coq中的类型相互排斥吗？
例如，在这个问题的公认答案中：
有人提到"Set <= Type_0“。(这是否意味着任何类型的集合也是类型的？)
另一方面，这个问题的公认答案是：
有人提到，“语言的每一个有效元素都有一种类型”。
My动机：
Coq中的关系(在Relations：中)定义为：
Variable A : Type.
Definition relation := A -> A -> Prop.
我的意图是表达对某种“较小的”B的关系的限制。如果这些类型是相互排斥的，那么它可能没有任何意义。
浏览 0提问于2018-06-22得票数 3
回答已采纳
是否每个属性都可以使用 在Coq中，通过对其中一个前提进行归纳，将其重构为使用以下条件的证明 我们在相同的前提下进行破坏？使用单独的命令来执行以下操作的意义是什么？ 和
浏览 28提问于2021-03-02得票数 1
回答已采纳
1回答
伊莎贝尔证明助手(2020)是否有办法检查预定义函数的定义，如div (或缩写和其他定义)？
在了解伊莎贝尔的过程中，我发现理解像div这样的函数是如何定义的很有帮助。我知道你可以打印或签入Coq，但无法理解伊莎贝尔的定义。
我试图将鼠标悬停在Isabelle/jEdit中的上下文菜单上，但什么也找不到。在互联网上搜索似乎也没有提供任何相关信息。
浏览 1提问于2021-01-04得票数 1
回答已采纳
我不太熟悉Coq中的模块，但它是在我最近提出的一个问题中提出的。我有下面的代码。
Module Type Sig.
Parameter n : nat.
Definition n_plus_1 := n + 1.
End Sig.
Module ModuleInstance <: Sig.
Definition n := 3.
End ModuleInstance.
Coq在尝试运行n_plus_1时抱怨End ModuleInstance的定义。我不确定这是否是使用模块的正确方式，但我希望它只使用签名中的定义，这是一个不需要任何附加信息的完整定义。有可能做到吗？
浏览 1提问于2018-03-15得票数 3
回答已采纳
1回答
Coq正在使用类似于OCaml的模块系统。在OCaml中，我们可以应用像Module_A.Module_B.Func这样的函数，并使用Module_A.Module_B来查找到Func的路径。
然而，我不能在Coq中做类似的事情。例如，如果我只运行Print Coq.Arith.Minus.minus_n_O.，Coq报告Coq.Arith.Minus.minus_n_O is not a defined object.
我必须先加载库，然后才能打印对象。在下面的例子中，它是成功的。
From Coq Require Export Arith.Minus.
Print Coq.Arith.Mi
浏览 6提问于2022-11-19得票数 0
回答已采纳
如何从外部软件中调用验证助理Coq？Coq有API吗？Coq命令行接口是否足够丰富，足以在文件中传递参数并在文件中接收响应？我对Java或C++桥感兴趣。
这是一个合理的问题。Coq并不是人们可以期望开发人员友好的API的通常业务软件。我对伊莎贝尔/霍尔也有类似的问题，这是合法的问题，有着不平凡的答案。
浏览 6提问于2017-09-04得票数 9
回答已采纳
1回答
在我的Coq研究中经常会出现这样的证明状态：
1 goal
n : nat
IHn : fib_v1 n <= fib_v1 (S n)
______________________________________(1/1)
fib_v1 (S n) <= fib_v1 (S (S n))
Coq抱怨说它不能把n和S n统一起来，S n和S (S n)不能统一。在纸和笔中，很容易在目标中引入象征性的操作，比如t = S n，甚至n = S n，那么归纳假设就会变得适用。在Coq看来不是这样的。在这样的情况下，一个人是如何前进的？
浏览 2提问于2022-04-27得票数 1
我使用Coq8.4pl6，希望在Coq中编译Logic.v ( Coq标准库)，并将其输出作为模块编译和打印的示例，但失败了。
更具体地说，Logic.v第107行的tauto失败了：
104 Theorem and_cancel_l : forall A B C : Prop,
105 (B -> A) -> (C -> A) -> ((A /\ B <-> A /\ C) <-> (B <-> C)).
106 Proof.
107 intros; tauto.
108 Qed.
我
浏览 2提问于2015-11-04得票数 2
我正在使用：
$ coqtop -v
The Coq Proof Assistant, version 8.4pl5 (February 2015)
compiled on Feb 06 2015 17:44:41 with OCaml 4.02.1
我定义了以下CoInductive类型，stream
$ coqtop
Welcome to Coq 8.4pl5 (February 2015)
Coq < CoInductive stream (A : Type) : Type :=
Coq < | Cons : A -> stream A -> stream A
浏览 2提问于2015-05-04得票数 3
回答已采纳
2回答
在大多数IDE或文本编辑器中，您可以右键单击某个术语，然后将其带到定义该术语的文件中。CoqIDE似乎没有，所以我一直在做coqdoc myfile.v --html，然后转到生成的HTML。但是该文件中唯一可点击的术语是用于Coq标准库的。例如，Terms定义的术语不可点击。
在Coq文件中定义了某个术语/标识符(以及它的源代码)，是否有一种快速查找的标准方法？无论是在CoqIDE中还是在emacs + ProofGeneral中(我正在使用CoqIDE，但是如果emacs/ProofGeneral有这种能力，我会切换)。
还是为您使用的每个Coq项目和依赖项生成文档的标准方法？
浏览 6提问于2015-07-18得票数 7
回答已采纳
在ocamltop中(加载我的文件之后)，我可以运行以下命令
#cd "/afs/csail.mit.edu/u/j/jgross/coq-HoTT/";;
#directory "/afs/csail.mit.edu/u/j/jgross/coq-HoTT/";;
#directory "/afs/csail.mit.edu/u/j/jgross/coq-HoTT/dev";;
#use "dev/include";;
#trace <some_function>
但是我不能跟踪未导出的函数，所以我想使用ocamld
浏览 0提问于2013-09-27得票数 0
1回答
我试图用一个构造函数定义一个数据类型，该构造函数接受一个列表，并包含有关这个列表的命题。
这样做很好：
Require Import Coq.Lists.List.
Import ListNotations.
Inductive Foo := MkFoo : list Foo -> Foo.
这也是如此：
Inductive Foo := MkFoo : forall (l : list Foo), Foo.
但这是失败的
Inductive Foo := MkFoo : forall (l : list Foo), l <> [] -> Foo.
使用
在&
浏览 0提问于2018-05-07得票数 2
回答已采纳
我正在使用proof-general来编写Coq证明。
在校样中使用C-c C-n时，光标将移动到下一行，但当前行未格式化。例如，如果我键入：
intros n. <C-c C-n>
我的光标移动到下一行，但intros n.保持不缩进。因此，我必须返回一行，转到行尾，然后点击<RET>来自动缩进coq语句。在这一点上，proof-general认为该语句发生了变化，我必须重新运行它。
理想情况下，我会在C-c C-n行中自动缩进它正在运行的行，而不是转到下一行。
我怎样才能做到这一点呢？
浏览 35提问于2021-10-02得票数 3
3回答
我试图在Coq (长故事：)中在pandoc中编写一个代码块。
$ pandoc --list-highlight-languages | grep coq | wc -l
0
由于它不存在，我想知道是否有一个选项可以编写我自己的用户定义的代码块语言？
浏览 14提问于2022-05-24得票数 1
回答已采纳
2回答
有没有一种方法可以像在Haskell中那样提供Coq类型分类方法的默认实现？我在Coq类型化文档中没有看到这一点。如果不存在这样的特性，那么是否有一种通用的模式来模拟这种行为？
浏览 10提问于2022-10-13得票数 0
回答已采纳
1回答
我的Coq证明有问题，希望能得到一些帮助和指导。我有以下定义的一部分：
Inductive Architecture : Set :=
| Create_Architecture (Arch_Name: string)(MyComponents: list Component)
(MyConnections: list Connector)
with
...
with
Connector : Set :=
| Create_Connector (Con_Name:string) (client: Component)(server:Component)
我想说的是“组件术语必须
浏览 2提问于2011-07-31得票数 1
我正在尝试使用这个库中的引理eqb_sym：https://coq.inria.fr/library/Coq.Structures.Equalities.html 我尝试了“需要导入Coq.Structures.Equalities”。和“要求导入BoolEqualityFacts”，但这两个都不让我使用引理eqb_sym。Coq抱怨它在当前环境中找不到引理。通常，当我在https://coq.inria.fr/library/的库中找到我想要使用的引理时，我在哪里找到要导入的正确模块，以及“是否需要导入模块名称”是正确的使用方法？
浏览 23提问于2019-03-07得票数 2
回答已采纳
你如何证明enumerateSingletonPowerset Require Import Coq.Sets.Ensembles.
Definition emptyOnly A := Singleton _ (Empty_set A).
Theorem enumerateSingletonPowerset A s (inc : Included _ s (emptyOnly A)):
Same_set _ s (Empty_set _) \/ Same_set _ s (emptyOnly A). 我使用Same_set来避免可扩展性。(任何一种方式都可以。) 从概念上讲，似乎很简
浏览 28提问于2021-08-15得票数 0
回答已采纳
2回答
是否有策略来重新排序Coq证明中假设的显示。通常在使用归纳法时(假设很长)，我想在顶部打印所有定义和所有其他方程。
浏览 22提问于2020-08-30得票数 0
回答已采纳
1回答
我很抱歉，如果这显然是张贴在某处，但我一直在尝试谷歌搜索，所以搜索，但没有发现这一点。
Part A.
在R^2和R^3中是否有定义坐标/矢量和点的标准库？我很想做一些标准的事情，比如添加向量，交叉产品，缩放等等。
如果没有，这是怎么开始的：
Require Import Coq.Reals.Reals.
Inductive Coordinate2 : Type := Point2: R -> R -> Coordinate2.
Definition R2plus (u:Coordinate2) (v:Coordinate2) : Coordinate2 :=
match u,
浏览 2提问于2013-11-05得票数 1
回答已采纳
我使用了从Coq到OCaml的提取，其中有Z、N、positive类型。
我不需要在int of OCaml中提取它。
那么提取后的类型是：
type positive =
| Coq_xI of positive
| Coq_xO of positive
| Coq_xH
type coq_N =
| N0
| Npos of positive
type coq_Z =
| Z0
| Zpos of positive
| Zneg of positive
我在OCaml中有一个程序，其中一些函数使用OCaml类型的string。
在我的OCaml程序中，我需要编写一些转换类型的函数：st
浏览 1提问于2014-09-02得票数 2
回答已采纳
2回答
我对Coq非常陌生，但是对于我的项目，我必须使用Coq中的联合查找数据结构。Coq中是否有联合查找(不相交集)数据结构的任何实现？
如果没有，有人能提供一个实现或一些想法吗？不一定要很有效率。(不需要进行路径压缩或所有花哨的优化)我只需要一个可以容纳任意数据类型(或者nat (如果太难)并执行：、union、和find )的数据结构。
提前感谢
浏览 5提问于2021-03-14得票数 3
我对coq很陌生，我试图使用ZArith.Int中的"int“类型，但是coq找不到它。
Require Export ZArith Int.
Open Scope Int_scope.
当我在定义(. -> int -> .)中使用"int“时，coq找不到它。如何将它与库的操作一起正确加载？
浏览 0提问于2014-05-04得票数 1
回答已采纳
2回答
什么是归纳谓词？
、、
你如何解释归纳谓词？它们是用来干什么的？他们背后的理论是什么？它们只存在于依赖型系统中，还是在其他系统中？它们在某种程度上与GADT有关吗？在Coq中，为什么默认情况下它们是真的？
这是Coq的一个例子：
Inductive even : nat -> Prop :=
| even0 : even 0
| evens : forall p:nat, even p -> even (S (S P))
你将如何使用这个定义？这是一种数据类型还是一个命题？
浏览 7提问于2014-04-11得票数 5
回答已采纳
我有一个具有list类型的dataframe列，但是列中的一些行丢失了数据，所以我想从列中删除丢失的数据行。
for i in range(len(data_Re)):
if type(data_Re.ix[i,'Actual CoQ Value1']) == float:
data_Re.ix[i,'Actual CoQ Value1'] = data_Re.ix[i,'Actual CoQ Value1'].drop(data_Re.ix[i,'Actual CoQ Value1'], a
浏览 0提问于2019-09-06得票数 0
2回答
我对Coq定理证明器很陌生。因此，我很可能已经错过了一些基本的东西，在阅读教程时。
在我提出我的问题之前，让我假设一些假设，并回顾一下我的想法。
Coq < Parameter Antecedent : Prop .
Coq < Parameter Consequent : Prop .
Coq < Conjecture Minor : Antecedent .
Coq < Conjecture Major : Antecedent -> Consequent .
有了这些假设，就可以应用Consequent模型:可以根据Minor前提和Major前提构造推断Ma
浏览 4提问于2014-05-06得票数 0
我只是想知道实数的“小于”关系是如何定义的。
我理解对于自然数(nat)，<可以递归地定义为一个数字是另一个数的(1+)继承者S。我听说很多关于实数的东西在Coq中都是公理的，不计算。
但我想知道，对于Coq中的实数是否有一组最小公理，根据这些公理可以导出其他性质/关系。(例如，认为Rplus_0_r : forall r, r + 0 = r.是一条公理，除其他外)
特别是，我感兴趣的是，是否可以在平等关系的基础上定义诸如<或<=之类的关系。例如，我可以想象在传统的数学中，给定两个数字r1 r2
r1 < r2 <=> exists s, s > 0
浏览 5提问于2015-12-21得票数 7
回答已采纳
Coq允许编写复杂的模式匹配，但随后对它们进行分解，以便其内核能够处理它们。
例如，让我们考虑以下代码。
Require Import List. Import ListNotations.
Inductive bar := A | B | C.
Definition f (l : list bar) :=
match l with
| _ :: A :: _ => 1
| _ => 2
end.
我们在列表和第二个元素上进行模式匹配。打印f显示Coq存储了一个更复杂的版本。
Print f.
(* f = fun l : list bar => matc
浏览 0提问于2019-09-17得票数 2
回答已采纳
1回答
有人能给我更多关于Coq中一级模块的信息吗？我知道Coq中的模块不是一流的。我想知道原因是什么？将来Coq中的模块有没有可能是一流的？
非常感谢
浏览 2提问于2013-04-11得票数 2
回答已采纳
1回答
假设我有这样的记录类型： Record myRec : Type := {
myNat : nat;
myProof : myNat > 0
}. 如何让Coq解析myRec类型的值的字段myProof，而不是直接打印(即隐藏 它可以在声明记录类型时设置吗？ 或者应该使用Notation命令和only printing语法修饰符来完成？
浏览 14提问于2021-10-07得票数 2
回答已采纳
1回答
我想在coq中制定一个Ltac策略，它可以接受1个或3个参数。我在模块中读过关于ltac_No_arg的文章，但如果我理解正确的话，我将不得不用以下命令调用我的策略：
Coq < mytactic arg_1 ltac_no_arg ltac_no_arg.
这不是很方便。
有没有办法得到这样的结果？：
Coq < mytactic arg_1.
Coq < mytactic arg_1 arg_2 arg_3.
浏览 8提问于2017-06-30得票数 6
回答已采纳
1回答
在ssreflect中的所有coq代码中都有这样一条语句
Import GroupScope.
什么是GroupScope？如果是另一个文件，我可以从哪里下载？
浏览 2提问于2015-02-18得票数 1
1回答
我注意到，我一直在为嵌套(有时相互)的归纳类型重新定义非常相似的归纳原则，因为Coq自动生成的归纳原则太弱了。下面是一个非常简单的示例：
Require Import Coq.Lists.List.
Inductive T : Set :=
| C1 : T
| C2 : list T -> T.
Section T_nested_ind.
Variable P : T -> Prop.
Hypothesis C1_case : P C1.
Hypothesis C2_case : forall l : list T, Forall P l -> P (C2
浏览 1提问于2017-11-03得票数 4
回答已采纳
有时我发现coq进入了一种状态，当我应用一种策略时，新的目标和假设不会自动打印出来。如何将其设置为在每次策略调用后打印出来。
这是coq 8.7.2，使用coqtop
浏览 0提问于2018-11-13得票数 1
1回答
我知道Coq允许定义相互递归的归纳类型。但是有没有一种方法可以用Coq编写递归定义呢？
例如，我想将一个定义写为：
Definition myDefinition A := forall B C, (myDefinition B) \/ (A = C).
上述定义中的重要部分是myDefinition B，它在另一个参数上递归调用相同的定义。在Coq中可以这样做吗？
浏览 5提问于2020-11-04得票数 1
我是一个程序员，但一个超新手对Coq，并试图找出教程，但没有多少成功。我的问题很简单:如何定义Coq中的有序对(自然数)？
以下是我的尝试：
Variable node1 : nat.
Variable node2 : nat.
Inductive edge : type := node1 -> node2.
(请注意，"edge“是我为有序对使用的名称。)第三行给出了一个语法错误，表明我需要一个“.”在某处的句子里。
该怎么办呢。任何帮助都会很好！(此外，是否有一个教程可以帮助您更好地教授非常基本的Coq概念，而不是Google搜索"Coq教程“时很容易看到的那些概念?
浏览 1提问于2013-10-02得票数 2
回答已采纳
正如标题所述，Coq可以用作模型检查器吗？我能把模型检查和Coq证明混在一起吗？这很平常吗？谷歌谈论的是“微积分”，有没有人有类似的经验？是否建议以这种方式使用Coq，还是应该寻找另一个工具？
浏览 3提问于2014-03-15得票数 25
回答已采纳
2回答
在coq中使用哪个向量库？
、、、、
我想知道，在coq中是否有一个常用的向量库，即按其类型的长度索引的列表。
有些教程引用了Bvector，但是当我试图导入它时却找不到它。
有Coq.Vectors.Vectordef，但是定义的类型是t，这让我觉得它是为内部使用的。
对于那些不想使用自己的库的人来说，什么是最好的或最常见的做法？标准库中的向量我错了吗？还是我又错过了另一个自由战士？还是人们只是使用列表，并与其长度的证据一起使用？
浏览 10提问于2017-02-17得票数 6
回答已采纳
考虑以下大小列表的类型定义：
Inductive listn: nat -> Type -> Type :=
| nil: forall {A: Set}, listn 0 A
| cons: forall {n: nat} {A: Set}, A -> listn n A -> listn (S n) A.
这本质上是Idris中的类型。
我试图为init定义listn函数，它删除了最后一个元素。
我尝试的实现实际上与Idris中init的定义完全相同。这是在伊德里斯：
init : Vect (S len) elem -> Vect len elem
init
浏览 6提问于2022-03-19得票数 1
回答已采纳
我有一个归纳定义--在计算之后--打印警告“忽略递归调用”。这个定义似乎运作得很好。不过，我仍然很好奇，为何要发出这个警告。下面是一个很小的例子。
Inductive testor :=
| Constr1 : list testor -> testor
| Constr2 : testor -> testor.
我认为罪魁祸首是第一个构造函数中的list testor。另一方面，如果没有第二个构造函数，则不会给出警告。
Q：为什么发出警告？这是否意味着对归纳定义施加限制？
我用的是Coq 8.5。
浏览 6提问于2016-06-02得票数 3
回答已采纳
编辑:我包含了证明。
我将一个证明(取自软件基金会的证明)从一个文件复制到另一个文件。在原始文件中，一切都编译得很好。在新文件中，错误：
Hs is used in hypothesis _the_hidden_goal_.
是由这条线引起的
rewrite H in Hs.
这是什么意思？在谷歌上搜索"_the_hidden_goal_“后，我找到的唯一信息是。根据该链接，我将有问题的行更改为
rewrite H in Hs *.
现在它可以编译了，但我不明白为什么。
谢谢。
编辑：
以下是包含*的情况下导致问题的证据。
Lemma eqb_string_true_iff : for
浏览 11提问于2020-05-19得票数 0
回答已采纳
1回答
我是Coq的新手。我正在尝试使用Coq的依赖类型。我想要做的是，简单地将一个偶数输入到一个函数中。例如，在伪代码中：
def next_even(n: {n: Integer | n is even}) :=
{
add n 2
}
然后我想使用带有不同参数的函数，例如(在伪代码中)：
next_even(1) // Coq should show an error
next_even(4) // Coq should compute 6
所以，在Coq中，我想做以下事情：
Compute (next_even 1).
Compute (next_even 4).
我该如何构建
浏览 8提问于2019-11-14得票数 1
扫码
添加站长 进交流群
领取专属 10元无门槛券
手把手带您无忧上云
相关资讯
热门标签
云服务器
ICP备案
对象存储
即时通信 IM
腾讯会议活动推荐
腾讯云开发者
