Coq:修复递归表示法
Coq是一种交互式定理证明工具，它基于计算机辅助证明（Computer-Aided Proof）的思想，用于开发和验证数学定理和软件系统。Coq的核心是一种强大的编程语言和一个丰富的证明环境，它可以帮助开发人员构建形式化的证明，并通过机器验证来确保其正确性。
修复递归表示法是Coq中的一个概念，用于处理递归定义和证明中的问题。在Coq中，递归定义是通过递归函数来实现的，而递归证明是通过递归的方式来构建证明的。
修复递归表示法的主要目的是解决递归定义和证明中可能出现的问题，例如无限递归、不可达代码、不完全性等。通过修复递归表示法，可以确保递归定义和证明的正确性和完整性。
Coq提供了一些工具和技术来修复递归表示法，例如归纳法、递归方程、递归函数等。这些工具可以帮助开发人员在递归定义和证明中避免常见的问题，并提供一种形式化的方法来验证递归定义和证明的正确性。
Coq在实际应用中具有广泛的应用场景，包括但不限于以下领域：
- 数学证明：Coq可以用于开发和验证数学定理和证明，帮助数学家们进行形式化的证明工作。
- 软件验证：Coq可以用于验证软件系统的正确性，包括算法、协议、编译器等。通过形式化的证明，可以确保软件系统的正确性和安全性。
- 语言设计：Coq可以用于设计和验证编程语言的语法和语义，帮助语言设计者构建可靠的编程语言。
- 硬件验证：Coq可以用于验证硬件系统的正确性，包括电路设计、处理器设计等。通过形式化的证明，可以确保硬件系统的正确性和可靠性。
腾讯云提供了一些与Coq相关的产品和服务，例如云服务器、云数据库、云存储等。这些产品可以帮助用户在腾讯云上搭建和运行Coq相关的应用和系统。具体的产品介绍和链接地址可以参考腾讯云官方网站。
相关·内容
1回答
Coq:修复递归表示法
、、、、
下面是一个半工作的简单递归表示法：
Universe ARG. Definition ARG := Type@{ARG}.
Parameter X: ARG.
Notation A := (fun x:ARG->ARG => fun y:x X => y).
Parameter P: ARG -> ARG.
Parameter s: P X.
Notation "[ x .. z u ]" := (x P .. (z P u) .. ) (at level 5, z, u at next level).
Check (A P (A P (A P s)))
浏览 2提问于2017-06-28得票数 0
回答已采纳
我试图定义一个新的表示法范围，并在Coq中添加表示法。我正在遵循Coq手册()中这个页面的指导。
我定义了我的新范围
Declare Scope myHoTT_scope.
Delimit Scope myHoTT_scope with my.
稍后，我想将"*“作为infix操作符添加到作用域中。我做这件事
Infix "*" := concat (at level 40 , left associativity) : myHoTT_scope.
其中，concat是一个已经定义的函数。Coq接受所有这些。它不会引发错误或警告。但是，如果我跑
Locate "
浏览 13提问于2022-01-29得票数 1
回答已采纳
1回答
我正在正式化一个支持元组和nat作为函数输入的系统。但是，我对Coq中的对类型有一些问题。
根据我对Coq的了解，对被定义为左联想。也就是说，(1, 2, 3)和((1, 2), 3)具有相同的nat * nat * nat类型。有时，它可以被视为一个三元组的nat。另一方面，(1, (2, 3))有nat * (nat * nat)类型，它是一对nat和对偶(或二元组)。
理想上，我希望有一个允许对nat和元组以及对元组和nat的系统。也就是说，(1, (2, 3))和((1, 2), 3)都不同于(1, 2, 3)。对于这样的模型，Coq中是否有任何建议的数据类型？
浏览 8提问于2021-06-28得票数 2
回答已采纳
1回答
我希望使用这些符号来表示谓词测试，如下所示：
Variable A B : Type.
Inductive test : A -> B -> A -> B -> Prop :=
| test1 : forall a1 a2 b1 b2,
a1 \ b1 || a2 \ b2
where "c1 '\' st '||' c2 '\' st'" := (test c1 st c2 st')
.
但是，Coq有一个错误：
为什么这个表示法在Coq中不能被接受？
浏览 0提问于2018-02-02得票数 2
回答已采纳
1回答
如何将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".
浏览 2提问于2015-09-22得票数 1
回答已采纳
在Coq中导入QArith之后
Require Import Coq.QArith.QArith_base.
我想定义一个产品类型
Parameter T : Type.
Definition TT : Type := T * T.
但是*是在QArith中重新定义的，我得到了错误消息
Error: The term "T" has type "Type" while it is expected to have type "Q".
如何使用原始*
浏览 1提问于2017-10-25得票数 2
回答已采纳
我想把list of integer转换成list of nat。下面是我在Coq中返回的函数。
Fixpoint list_int_to_nat (l : list integer) : list nat :=
match l with
| nil => nil
| x :: l' => let i := Z.to_nat x in
list_int_to_nat l'
end.
您能否帮助我将列表integer的每个元素转换为nat的列表，因为在我的函数中，我没有使用第一个元素i？非常感谢你的帮助。
浏览 0提问于2013-06-06得票数 1
回答已采纳
我看到了“计算为”的Coq表示法定义如下：
Notation "e '||' n" := (aevalR e n) : type_scope.
我试图将符号'||'更改为其他东西，因为||经常用于逻辑or。然而，我总是会犯错误
A left-recursive notation must have an explicit level
例如，当我将'||'更改为：
'\|/'，'\||/'，'|_|'，'|.|'，'|v|'或'|_'。
浏览 2提问于2015-11-26得票数 6
回答已采纳
1回答
假设我想在coq中创建一个自然数矩阵。
我有内置的coq列表，为了创建一个自然数列表，我只编写了list nat。
为了创建一个二维列表(即矩阵)，我需要编写list (list nat)。
我的问题是:我不写list (list nat)，我该怎么做才能让coq完全理解matrix这个词，就好像它是list (list nat)一样。
我试过Notation "matrix" := list (list nat)，Notation "(matrix nat)" := (list (list nat))等，但是似乎没有什么效果。
浏览 2提问于2018-11-04得票数 5
回答已采纳
我有以下Ltac (来自)，它以前在CoQ8.4pl6上工作，但它不在CoQ8.5beta 3上工作：
Ltac maybe_intro_sym A B :=
match goal with
|[H:B=A|-_] => fail 1
|[H:A=B|-_] => assert (B=A) by auto
end.
Ltac maybe_intro_sym_neg A B :=
match goal with
|[H:B<>A|-_] => fail 1
|[H:A<>B|-_] => assert
浏览 1提问于2015-12-02得票数 1
回答已采纳
1回答
我想为几种判断创建符号，例如打字和子类型关系：
Reserved Notation "Г '⊢' t '∈' T" (at level 40).
Reserved Notation "Г '⊢' T '<:' U" (at level 40).
Inductive typing_relation : context -> term -> type -> Prop := ...
where "Γ '⊢' t '∈' T" :=
浏览 0提问于2017-05-03得票数 3
回答已采纳
3回答
我想要我自己的作用域，来处理长的发行版。
Declare Scope my_scope.
Delimit Scope my_scope with my.
Open Scope my_scope.
Definition f (x y a b : nat) : nat := x+y+a+b.
Notation "x < y * a = b" := (f x y a b)
(at level 100, no associativity) : my_scope.
Check (1 < 2 * 3 = 4)%my.
如何创建一个新的作用域？
编辑:我选择了"x
浏览 1提问于2013-02-23得票数 1
我想要像Coq中的"x∈{x }“这样的标准表示法。但也有一些问题：
1)花括号在Coq中有特殊的含义，因此发生以下情况：
Notation " x ∈ y " :=(tin x y) (at level 50).
Notation " { x } ":=(Sing x).
Check fun x => (x ∈ { x }).
(*error: Unknown interpretation for notation "_ ∈ { _ }". *)
如何正确定义这个符号？
2)如果第一个问题不能解决，还有另一个问题。(在这里，我决定
浏览 1提问于2018-11-03得票数 3
回答已采纳
1回答
所以我对coq，函数式编程非常陌生，我试图表达coq中连续性的拓扑定义。我使用这个在coq中定义了一个拓扑。我最好的表达连续性的方法是，
Definition Continuous (X:Type)(TX:Topology X)(Y:Type)(TY:Topology Y)(f:X->Y):=
forall V, exists U, all y:V, some x:U, f x = y.
我搞错了
"f x“一词为"Y”型，而“f x”则为"Prop“型。
不知道该做什么，任何帮助都是值得感激的。
浏览 5提问于2016-05-19得票数 1
回答已采纳
1回答
Coq手册()声明
由于保留符号，归纳，共归纳，记录，递归和共递归定义可以使用定制的符号.
我想定义一下
Reserved Notation "A +' B" (at level 80).
Record foo T :=
{ add : T -> T ->T;
commute a b : a +' b = b +' a
where "a +' b" := (add a b)
}.
但我得到
Error: Unknown interpretation for notation
浏览 1提问于2020-07-30得票数 1
2回答
对于我感兴趣的属性，我有一个简单的搜索函数，并证明该函数是正确的。我想评估函数，并使用正确性证明来获得原始性质的定理。不幸的是，coq中的计算非常慢。作为一个简单的例子，考虑寻找平方根：
(*
Coq 8.4
A simple example to demonstrate searching.
Timings are rough and approximate.
*)
Require Import Peano_dec.
Definition SearchSqrtLoop :=
fix f i n := if eq_nat_dec (i * i) n
then i
else ma
浏览 1提问于2013-11-03得票数 4
构造器策略允许您通过自动应用构造函数来完成一个目标，即归纳数据类型。然而，在Coq中，定义等式并不是一个归纳积。那为什么Coq会接受这个证据呢？
Example zeqz : 0 = 0. constructor.
浏览 1提问于2021-01-29得票数 1
回答已采纳
我试图在Coq中使用更大的数字，而在Coq中，内置Nat类型是不合适的。所以我试图用正型或N型来建立特定的值。
根据BinNums的标准库文档：
正数也将用十进制表示法表示；例如，6%的正数将缩写为xO (xI xH)，N中的数字也将用小数表示法表示；例如，6%的N将缩写Npos (xO (xI xH))。
但我的Coq代码仍在给我Nat输入的数字：
From Coq
Require Import BinNums.
Definition sixp := 6%positive.
Definition sixn := 6%N.
Check sixp.
Check sixn.
结果：
s
浏览 5提问于2020-12-02得票数 2
回答已采纳
我正在处理一个给出的例子
Notation step_normal_form := (normal_form step).
Definition stuck (t:tm) : Prop :=
step_normal_form t /\ ~ value t.
Example some_term_is_stuck :
exists t, stuck t.
我在第1步(Coq 8.4pl6)的定义unfold-ing step_normal_form上遇到了麻烦。我可以在Check CoqIDE中获取它的内容：
normal_form
: relation ?23 -> ?
浏览 5提问于2015-12-13得票数 1
在定义Coq中的整数时，我遵循的回答，但当试图在其上定义加法时，总是会出现错误“无法猜测递减参数”。我尝试过多种不同的定义，似乎总是会发生这种情况。有办法证明Coq的论点正在减少吗？或者我错过了一些明显的方法来定义加法。
Inductive nat : Type := (*Natural numbers*)
| O
| S (n : nat).
Fixpoint plus (n:nat) (m:nat) : nat := (*Addition of natural numbers*)
match n with
| O => m
| S(n') => S(plus n
浏览 2提问于2020-09-24得票数 1
回答已采纳
我正在尝试将Coq术语直译为精益术语，但我意识到我不知道如何翻译Coq原语fix，如下所示： Definition Fac : nat -> nat :=
fix f (n:nat) : nat :=
match n with
| 0 => 1
| S p => S p * f p
end. 我不是问如何在归纳类型上定义递归函数，这在精益文档中有很好的解释，但我问的是如何定义“递归let”，即其主体调用自身的lambda抽象。我假设Lean中存在一个等价的原语。 谢谢。
浏览 27提问于2020-03-29得票数 0
回答已采纳
我试图通过在线软件基金会书籍：来学习Coq。
我正在使用交互式命令行Coq解释器coqtop。
在归纳章节()中，我完全按照指示行事。我使用coqc Basics.v编译Basics.v。然后启动coqtop并准确地键入：
Require Export Basics.
Theorem andb_true_elim1 : forall b c : bool,
andb b c = true -> b = true.
Proof.
intros b c H.
destruct b.
Case "b = true".
所有操作直到最后一行，此时我得到以下错误：
浏览 1提问于2013-10-06得票数 10
回答已采纳
我试图编写一个非常简单的程序，将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
浏览 7提问于2022-03-19得票数 2
回答已采纳
在证明了一个存在性陈述之后，通常为这个定理的某些证明人引入一个常数符号是不方便的。
作为一个简单的例子，编写(用典型的数学表示法)要简单得多。
∀x. ∅ ⊆ x.
而不是写
∀x. ∃y. empty(y) and y ⊆ x.
我希望在Coq中复制这一效果。下面是我遇到的基本场景和我的尝试，这会导致一个错误(现在在实际Coq代码中)：
Variable A:Type.
Hypothesis inhabited: exists x:A, x=x.
Definition inhabitant:A.
destruct inhabited.
(*Error: Case analysi
浏览 5提问于2015-02-27得票数 5
回答已采纳
我正在尝试使用HoTT一书中的类型构造器/消除器来证明各种deMorgans法则。我从中挑选了相关的东西，并将其全部转储到一个.v文本文件中。我需要产品的消除/引入规则，联合产品和一种建立否定的方法。到目前为止，
Definition idmap {A:Type} (x:A) : A := x.
Inductive prod {A B:Type} : Type := pair : A -> B -> @prod A B.
Notation "x * y" := (prod x y) : type_scope.
Section projections.
Co
浏览 1提问于2017-10-08得票数 0
在我的证明中，这是可行的
induction H1 as [ | | | | | | | | | ].
但是，当我把它换成
dependent induction H1 as [ | | | | | | | | | ].
我得到了"Error:语法错误: tactic:ltac_use_default预期在之后“。
在进行依赖归纳时，您能认真地选择变量的名称吗？这太疯狂了；我真的希望我只是语法错误。
谢谢。
浏览 0提问于2020-08-15得票数 1
回答已采纳
我定义了一个符号来模拟命令式编程
Notation "a >> b" := (b a) (at level 50).
然而，在此之后，所有函数应用程序表达式都被表示为'>>‘样式。例如，在Coq Toplevel的证明模式中，我可以看到
bs' : nat >> list
其实应该是
bs' : list nat
为什么Coq会积极地将所有函数应用程序样式的表达式重写到我的自定义' >>‘表示中？如何将一切恢复正常，我的意思是我希望看到'a >> b’被解释为'b‘，&#
浏览 5提问于2015-05-18得票数 10
回答已采纳
我发现自己被Coq证明卡住了。
初步定义：
Require Import Coq.Bool.Bool.
Require Import Coq.Arith.Arith.
Require Import Coq.Arith.EqNat.
Require Import Coq.omega.Omega.
Require Import Coq.Lists.List.
Require Export Coq.Strings.String.
Import ListNotations.
Definition total_map (A:Type) := string -> A.
Definition st
浏览 2提问于2020-11-12得票数 0
回答已采纳
我正在尝试为lambda演算编写一个替换函数，在递归调用e上的替换之前，如果是lambda抽象(\x.e)，我必须在e中重命名变量。我如何在Coq中表示这种逻辑？
下面是一个最小的例子，对于这个例子，Coq给出了它不能猜测递减参数的错误。在简化的替换中，为什么Coq不能得到相同感应大小的e余量？
Fixpoint replace (x: nat) (y: nat) (e: exp): exp := e.
Fixpoint substitute (x: nat) (t: exp) (body: exp): exp :=
match body with
| Abs xp e => Abs
浏览 17提问于2017-12-23得票数 3
回答已采纳
1回答
我在Coq中有一个证明，其中一个假设是：
H : m = pred q * n + (r + n)
我有一个证明了的引理，它说：
Lemma suma_conmutativa: forall m, forall n, m + n = n + m.
其中+是我定义的一个名为suma的函数的符号：
Fixpoint suma (m:nat) (n:nat) : nat :=
match m with
| 0 => n
| S k => S (suma k n)
end.
Notation "m + n" := (suma m n).
由于某些原因，当我尝试重写
浏览 2提问于2015-11-25得票数 0
1回答
Coq初学者在这里，我最近独自完成了前7章的"“。
我正试图在∀ n>= 3, 2n+1 < 2^n的Coq中通过归纳来创建一个证明。
我从destruct开始，去掉错误的假设直到到达n=3。然后，我在n上进行归纳，n=3的情况很简单，但是，，如何证明归纳步骤？？。
我看得出来目标还在。我可以通过使用destruct进行案例分析来证明它，但是，它还不能以一般的形式显示出来。
。
到目前为止我的证据：
(* n>=3, 2n+1 < 2^n *)
Theorem two_n_plus_one_leq_three_lt_wo_pow_n : forall n:nat
浏览 0提问于2018-09-17得票数 2
考虑关系的自反传递闭包：
Inductive star {A : Type} (r : A -> A -> Prop) : A -> A -> Prop :=
| star_refl x : star r x x
| star_step x y z : r x y -> star r y z -> star r x z.
如何在Coq中给出表示法，以便编写x ->* y，或者添加一个下标来表示关系->__r。这在伊莎贝尔身上是可能的。在Coq有干净的方法吗？
浏览 1提问于2020-04-02得票数 2
回答已采纳
我安装了Coqide8.5w/ nix。不幸的是，所有面板的文本都是blakc；没有任何类型的语法突出显示(否则，8.5似乎比我安装的8.4有很大的改进)。我还得到以下信息：
(coqide:17272): GtkSourceView-WARNING **: Unknown parent scheme 'classic' in scheme 'coq_style'
(coqide:17272): GtkSourceView-WARNING **: Failed to load '/nix/store/2sxcqfc4q3ls4g2q13n1zwfhny
浏览 4提问于2016-06-18得票数 2
回答已采纳
1回答
我试图用Coq编写一个程序来解析一个相对简单的上下文无关语法(一种括号)，而我的一般算法是解析器可能返回字符串的其余部分。例如，解析"++]>><<"应该返回CBTerminated [Incr Incr] ">><<"，然后，假设解析"++>><<“的解析器能够获取">><<”并继续进行。
所以很明显，字符串较小，但令人信服的Coq则是另一回事。它给了我错误
parseHelper的递归定义是不正确的...。递归调用parseHelper的主体参数
浏览 4提问于2016-05-26得票数 5
回答已采纳
我很好奇在逻辑中等效于连接词的Coq实体的类型。为了具体起见，让我们假设->和/\。如果->是一个神奇的非头等实体，那么让我们使用/\作为实体。我很好奇它的域名是Prop还是Set。
是否可以使用coqtop获取表达式的类型？
我想用ghci做一些类似于下面的事情。
> ghci
:GHCi, version 8.6.3: :? for help
Prelude> :t (**)
(**) :: Floating a => a -> a -> a
浏览 0提问于2019-01-08得票数 1
回答已采纳
我在一些教程中读到if a then b else c代表match a with true => b | false => c end。但是，前者非常奇怪地不检查a的类型，而后者当然确保a是一个布尔值。例如,
Coq < Check if nil then 1 else 2.
if nil then 1 else 2
: nat
where
?A : [ |- Type]
Coq < Check match nil with true => 1 | false => 2 end.
Toplevel input, characters 33-
浏览 1提问于2017-12-25得票数 4
回答已采纳
如果x<5 (X)=1在Coq中，我如何定义像f(x)=0这样的函数？
如果我做了像OСaml这样的事，
Definition test (i:nat):nat :=
if i < 5 then 0 else 1.
它抱怨说
错误:术语i < 5有Prop类型，它不是(共同)归纳类型.
浏览 3提问于2017-09-24得票数 0
回答已采纳
我想知道是否有一种简洁的写作方式，即Coq中存在唯一的东西(即写唯一的存在量词)？
例如，要说存在一个x s.t。2 + x = 4
Goal exists x, 2 + x = 4.
如何编写存在具有相同属性的唯一 x？
我知道我可以在s.t.部分中复制谓词，如下所示：
Goal exists x, 2 + x = 4 /\ forall y, 2 + y = 4 -> y = x.
但总的来说，这是大量的重复，是否有一种方法可以对一个新的量词进行编码，并编写：
Goal exists1, 2 + x = 4.
表达同样的目标？
浏览 3提问于2016-09-07得票数 7
回答已采纳
在几个符号中使用了|-。例如，在中
Reserved Notation "Gamma '|-' t '\in' T" (at level 40).
这会干扰Ltac匹配结构。例如，这是：
Ltac test :=
match goal with
H: _ |- _ => idtac
end.
在Stlc之外工作很好，但是一旦定义了这个表示法，它就会失败，因为：
Toplevel input, characters 43-44:
Syntax error: "\in" expected after [cons
浏览 4提问于2015-04-17得票数 1
回答已采纳
我对add的定义如下：
Fixpoint add n m :=
match n with
| 0 => m
| S p => add p (S m)
end.
在后面的文件中，我试图证明以下目标：add (S n) 0 = S n
我调用simpl命令，期望它减少
add (S n) 0到add n (S 0)。
相反，它减少了
add (S n) 0到add n 1
我怀疑simpl命令只要能够执行就会执行多个步骤。
我的问题：是否有一个命令可以使一个步骤减少，减少
add (S n) 0 = S n
至
add n (S 0) = S n
浏览 4提问于2020-06-12得票数 0
回答已采纳
我有一个关于证明函数nat -> QArith.Q (作为Coq的标准库的有理数)是单调(总是非递减)的问题，这是关于在Coq中使用有理数的练习的一部分。问题是我被困在证明过程的归纳步骤中。假设我按如下方式定义了一个函数。
Definition silly (n:nat) : QArith_base.Q :=
match n with
| 0 => 1#1
| 1 => 2#1
| 2 => 3#1
| 3 => 4#1
| 4 => 5#1
| 5 => 6#1
| S n =>
浏览 2提问于2019-04-10得票数 1
1回答
我正在尝试使用Coq中的以下函数实现一个函数来构建一个包含n个元素的Braun树，但Coq给我的错误是它无法猜测fix的递减参数：
Fixpoint copy (x : V) (n : nat) : BraunTree :=
let
fix copy2 (a : V) (i : nat) : (BraunTree * BraunTree) :=
match i with
| 0 => (T a E E,E)
| _ => match Nat.odd i with
| true => let m := ((i - 1) /
浏览 27提问于2019-05-14得票数 1
回答已采纳
1回答
我想用coq编写一个安全的zip函数，它接受参数长度相等作为参数。
Fixpoint zip {b a:Type} (proof : length l1 = length l2) (l1 : list a) (l2 : list b) : list (a * b) :=
match l1,l2 with
| nil,nil => nil
| cons a a',cons b b' => cons (a,b) (zip a' b')
| _,_ => (* never reached *)
end.
解决这类问题的一般方法是什
浏览 6提问于2021-02-05得票数 1
回答已采纳
2回答
我试图在Coq中定义一个幂函数，但我似乎找不到要导入的相关模块：
Require Import Coq.Numbers.NatInt.NZPow.
Definition func (a b : nat) : nat := a+b*2^a.
给出以下错误：
Unknown interpretation for notation "_ ^ _".
我有点困惑，因为在中，我看到了以下描述：
幂函数的接口，然后它对自然的规范
此外，这也是：
Module Type PowNotation (A : Typ)(Import B : Pow A).
Infix "^
浏览 2提问于2020-05-08得票数 3
回答已采纳
1回答
动力塔
、
我想定义一个类型为PowersetTower : Type -> nat -> Type的家族，以便：
PowersetTower A 0 = APowersetTower A (n+1) = Ensemble (PowersetTower A n) (即PowersetTower A n -> Prop) )
这有可能吗？一种想法是
Inductive PowersetTower : Type -> nat -> Type :=
| base : forall (A : Type), PowersetTower A 0
| step : forall (A :
浏览 4提问于2021-04-08得票数 1
回答已采纳
正如标题所述，Coq可以用作模型检查器吗？我能把模型检查和Coq证明混在一起吗？这很平常吗？谷歌谈论的是“微积分”，有没有人有类似的经验？是否建议以这种方式使用Coq，还是应该寻找另一个工具？
浏览 3提问于2014-03-15得票数 25
回答已采纳
对于coq，我们是非常初级的。下面是Basic.v中的代码
1 Set Implicit Arguments.
2
3 (* Pretty-print for if-then-else expressions on informative types *)
4
5 Notation "'If' c1 'then' c2 'else' c3" :=
6 match c1 with
7 | left _ => c2
8 | right _ => c3
9 end (at level 200).
10
11
浏览 5提问于2021-07-21得票数 1
我在如何在BNF中表达一些递归的东西时遇到了麻烦。在我的例子中，'term‘可以由一个值，乘法和除法组成(如图所示)，我想出了以下方法：
<term> ::= <value>
| <value> “*”
| <value> “/”
浏览 3提问于2015-10-20得票数 1
2回答
我对Coq非常陌生，但是对于我的项目，我必须使用Coq中的联合查找数据结构。Coq中是否有联合查找(不相交集)数据结构的任何实现？
如果没有，有人能提供一个实现或一些想法吗？不一定要很有效率。(不需要进行路径压缩或所有花哨的优化)我只需要一个可以容纳任意数据类型(或者nat (如果太难)并执行：、union、和find )的数据结构。
提前感谢
浏览 5提问于2021-03-14得票数 3
扫码
添加站长 进交流群
领取专属 10元无门槛券
手把手带您无忧上云
相关资讯
热门标签
云服务器
ICP备案
实时音视频
对象存储
即时通信 IM活动推荐
腾讯云开发者
