我使用了从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
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
我不太熟悉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的定义。我不确定这是否是使用模块的正确方式,但我希望它只使用签名中的定义,这是一个不需要任何附加信息的完整定义。有可能做到吗?
在 coqtop 交互式终端中,如何删除已定义的名称?
例如,我可以用下面的代码定义一个bool类型。
Coq < Inductive my_bool : Type :=
Coq < | my_true : my_bool
Coq < | my_false : my_bool.
这是可行的,我得到了以下输出。
my_bool is defined
my_bool_rect is defined
my_bool_ind is defined
my_bool_rec is defined
但是,如果我想重新定义my_bool术语,我会得到Error: my_bool alread
我试图证明在Coq中最简单的事情:
Require Import Coq.Structures.OrdersFacts.
Require Import Coq.Structures.Orders.
Lemma easy: forall a b : nat, (a = b) -> (a <= b).
Proof.
intros.
apply le_lteq. (* doesn't work *)
apply LeIsLtEq.le_lteq. (* doesn't work *)
但我得到了以下错误:
The reference le_l
我试图检查Coq中两个整数之间的等价性,但我得到了这个错误:“术语"first = second”的类型是"Prop“,它不是一个(co-)归纳类型。”Coq中有没有提供等价性检查的库?下面是我的代码: Definition verify_eq (first : Z) (second : Z) : Z :=
if first = second then 0 else 1.
如何让Coq识别出两种类型,每种类型都是从使用相同参数从模块函子创建的模块中导入的,但出现在不同的模块中,它们实际上是相同的类型?
极小例子
Module Type S.
End S.
Module F (s : S).
Inductive foo : Type := a.
End F.
Module G (s : S).
Include F s.
End G.
Module H (s : S).
Include F.
End H.
Module I (s : S).
Module G := G s.
Module H := H s.
(* This is a type error
我正在编写我自己的第一个Coq文件,但是我在导出另一个用户定义的文件(由图书软件基金会定义)时遇到了困难。
问题是我当前的Coq文件有路径Coq/NWA.v,而我想导入的文件有路径Coq/SoftwareFoundations/lf/Rel.v。我尝试了以下语法:
From Coq/SoftwareFoundations/lf Require Import Rel.v
&
From Coq.SoftwareFoundations.lf Require Import Rel.v
&
From ./../SoftwareFoundations/lf Require Import R
我知道Coq允许定义相互递归的归纳类型。但是有没有一种方法可以用Coq编写递归定义呢?
例如,我想将一个定义写为:
Definition myDefinition A := forall B C, (myDefinition B) \/ (A = C).
上述定义中的重要部分是myDefinition B,它在另一个参数上递归调用相同的定义。在Coq中可以这样做吗?
我正在使用来自Coq标准库的ListSet扩展,以使用有限集作为类的属性: Require Import ListSet.
Class aux := {
attribute1: set;
attribute2: set -> set;
}. 但是我得到了这个错误: Error: In environment
aux : Type
The term "set" has type "Type -> Type" which should be Set, Prop or Type. 我不明白为什么会发生这种事。(我是Coq新手)
我想证明
Theorem T20d :forall (x y:R), (0<x /\ 0<y) -> 0 < Rmin x y.
使用
Lemma min_glb_lt n m p : p < n -> p < m -> p < min n m.
它在Coq.Structures.GenericMinMax中
我用Require导入的Coq.Structures.GenericMinMax
但是,当我尝试使用它时,还没有找到"reference min_glb_lt“吗?我怀疑我需要打开一个范围,但我不知道是哪个范围。
我对Coq非常陌生,当我尝试使用作为一个证明时,我有一个错误。例如,考虑到以下情况:
Require Import Coq.Init.Logic.
Lemma dummy: forall A B, (A <-> B) -> (~A <-> ~B).
Proof.
apply not_iff_compat.
Qed.
Coq告诉我:"Error: The reference not_iff_compat was not found in the current environment.“
(就我现在而言,Coq.Init.Logic是自动加载的,所以这里
如何将Coq中的nat转换为q (Rational)?
我想写这样的东西:
Require Import Coq.QArith.QArith.
Open Scope Q_scope.
Definition a := 2/3.
当我尝试这样做时,Coq告诉我:
Error: The term "2" has type "nat" while it is expected to have type "Q".
在我的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看来不是这样的。在这样的情况下,一个人是如何前进的?
在Coq中,Haskell的相当于什么?
一般来说,我发现Coq标准库中围绕排序混淆。
我本来希望排序列表的一些“公理化”,以及不同类型的可用性,我可以提供一个排序函数。
然而,情况似乎并非如此。
,它使用关系Variable R : A -> A -> Prop.,但对此R没有任何限制。我原以为这是一种命令,但不存在这样的事情。
还有一个带有"“的文件,它需要一个新的模块来传递。
没有提供像sortBy这样的帮助的“高级”版本。
我是否可以使用sortBy的某些实现,或者是否需要手动创建它?
我试图编写一个非常简单的程序,将nats合并到一个列表()中:
Fixpoint sum (l : list nat) : nat :=
match l with
| [] => 0
| x :: xs => x + sum xs
end.
但我当地的Coq和jsCoq抱怨道:
Syntax error: 'end' expected after [branches] (in [term_match]).
为什么会这样呢?(注意,我甚至没有实现这个,但是我的实现看起来几乎是一样的)
我以前实现过递归函数:
Inductive