Coq -将选择函数添加到上下文
Coq是一个交互式定理证明助理，它是一种基于计算机的形式化方法，用于开发和验证数学定理和软件系统。它提供了一种强大的证明语言和工具，可以帮助开发人员和数学家进行形式化证明。
Coq的主要特点包括：
- 交互式证明：Coq允许用户与证明交互，逐步构建证明过程。用户可以通过编写和应用证明策略来指导证明的进行。
- 形式化语言：Coq提供了一种严格的形式化语言，称为Gallina，用于编写数学定理和程序。这种语言具有严格的语法和语义，可以确保证明的正确性。
- 自动化证明：Coq还提供了自动化证明工具，如反演、自动化策略和决策过程。这些工具可以帮助用户自动化一些繁琐的证明步骤。
- 可扩展性：Coq是一个可扩展的系统，可以通过添加新的逻辑和推理规则来扩展其功能。这使得Coq可以适用于不同领域的证明和验证任务。
Coq的应用场景包括：
- 数学证明：Coq可以用于形式化数学定理的证明，包括代数、几何、逻辑等领域。
- 软件验证：Coq可以用于验证软件系统的正确性，包括程序的功能性和安全性。
- 证明助理：Coq可以作为一个交互式证明助理，帮助数学家和计算机科学家进行证明工作。
腾讯云提供了一些与Coq相关的产品和服务，包括：
- 腾讯云服务器（CVM）：腾讯云提供了可靠的云服务器实例，可以用于部署和运行Coq系统。
- 腾讯云数据库（TencentDB）：腾讯云提供了高性能和可扩展的数据库服务，可以用于存储Coq系统的数据。
- 腾讯云安全产品：腾讯云提供了一系列安全产品和服务，可以帮助保护Coq系统的安全性，包括DDoS防护、Web应用防火墙等。
更多关于腾讯云产品和服务的信息，请访问腾讯云官方网站：https://cloud.tencent.com/
相关·内容
我正在使用：
$ 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
回答已采纳
1回答
考虑下面的Coq程序： Inductive foo : nat -> Type :=
| nil : foo 0
| succ{n:nat} : foo n -> foo n.
Fixpoint bar {n:nat}(A:foo n)(B:foo n) : Prop :=
match B with
| nil => False
| succ C => bar A C
end. Coq抱怨bar的定义 In environment
bar : forall n : nat, foo n -> foo n -> Prop
n : nat
A
浏览 14提问于2021-03-31得票数 0
我正在用Coq开发一个谷歌库。到目前为止，这个项目进行得很顺利。然而，我有一个问题:我能在Coq中得到宇宙的继承者吗？
我可以通过lsuc在Agda中得到宇宙的继承者。Coq似乎是唯一的运算符max(_,_)。通过Print命令，我可以看到类似于Type@{(Top.9)+1}的东西，其中包括_+1，但是我不能使用这个符号。
浏览 4提问于2020-04-02得票数 2
回答已采纳
是否有可能以及如何在前向链接模式中将Coq用作计算器或规则引擎？Coq脚本通常需要声明可以找到证据的目标。但是，是否有可能在其他方向上进行，例如，计算由某些规则限定的一些结果的集合，例如，通过一些步骤。我对全一阶逻辑的序列演算特别感兴趣。我猜(但我不知道)有一些一阶逻辑的序列演算的实现或包，但它是用于定理证明的。我喜欢用这样的顺序演算来推导出一些有指导的顺序的结果。在Coq中这是可能的吗？
浏览 1提问于2019-09-08得票数 0
2回答
在我当前的项目中，我们使用Java和Coq。我们使用maven设置了一个连续的集成。我们想要检查coq文件作为它的一部分。也就是说，我们需要：
下载并在没有安装coq的情况下在本地安装coq(就像maven对gwt等框架所做的那样)
检查coq文件是否正确
有人试过设计这个吗？这是如何做到的呢？
浏览 1提问于2012-08-23得票数 5
有时我发现coq进入了一种状态，当我应用一种策略时，新的目标和假设不会自动打印出来。如何将其设置为在每次策略调用后打印出来。
这是coq 8.7.2，使用coqtop
浏览 0提问于2018-11-13得票数 1
我是Coq的新手。 在我们的项目中，我们切换到使用coq_makefile实用程序，并遇到了以下问题。 单步执行验证脚本将导致以下错误： Require Import comparable.
Error:
The file /Users/ayman/open-source/regex-reexamined-coq/comparable.vo contains library
Top.comparable and not library comparable 我们的_CoqProject文件非常简单(也许这就是问题所在)，它只列出了项目https://github.com/awaltersc
浏览 19提问于2020-05-02得票数 1
回答已采纳
我有一个简单的问题。 我想告诉Coq vec_assoc是存在的。 Require Import Coq.Vectors.Vector.
Lemma vec_assoc (A:Type)(a b c:nat): t A ((a+b)+c) = t A (a+(b+c)).
Proof.
f_equal. symmetry. apply Nat.add_assoc. Qed.
Variable a b c:nat.
Variable A B:Type.
Variable I : (t A ((a+b)+c) -> B).
Variable p:t A (a+(b+c)). Coq返
浏览 7提问于2020-10-08得票数 0
回答已采纳
我一直想使用，而且我已经安装好了。我可以从opam list确认这一点
ubuntu@ubuntu-xenial:~$ opam list
# Installed packages for system:
...
coq 8.6 Formal proof management system.
coq-vpl 0.2 Coq interface to VPL abstract domain of convex polyhedra.
coq-vpltactic 0.2 A Coq Tactic for Ar
浏览 34提问于2018-01-29得票数 1
回答已采纳
1回答
我想证明在Coq中减法不通勤，但我被卡住了。我相信我想在Coq里证明的声明是写在forall a b : nat, a <> b -> a - b <> b - a上的
到目前为止，这是我的证据。
Theorem subtraction_does_not_commute :
forall a b : nat, a <> b -> a - b <> b - a.
Proof.
intros a b C.
unfold not; intro H.
apply C.
我想我可以用C : a <> b来反驳a =
浏览 0提问于2017-05-18得票数 1
回答已采纳
我感兴趣的是依赖型定理证明器是如何在上下文中进行替换的。我在Coq中找到了一个叫做"intro ->“的东西，如下所述：
在这个例子中，它指出了目标：
x，y，z: nat
H:X=y
y=z -> x=z
会变成
x，z: nat H:x=z
x=z
在"intros ->“的应用程序之后。
我不知道将H:x =y替换成H:x =z的步骤是如何完成的，Coq的逻辑是根据什么规则进行的？这似乎是重写的一步，根据我目前的知识，大多数重写都是根据等式进行的，所以从H:x =y到H:x = z的替换应该来自类似于(H:x= y) =(H:x= z)
浏览 4提问于2021-06-28得票数 0
回答已采纳
1回答
是否有任何函数/命令来获取/检查一个自由变量(例如n:U )是否存在于一个术语/表达式e中，使用Coq？请分享。
例如，我想在Coq中声明这个"n不出现在e的自由名称中“。
谢谢,
威拉亚特
浏览 6提问于2012-07-16得票数 1
最近，我在Visual中调试C++ (使用VS2012)时发现了“步骤特定”选项，这非常有用，特别是在有许多构造函数、智能指针等的情况下。
但是，由于我主要是使用键盘(F9、F10、F11、Shift-F11)进行调试，我想知道是否可以以某种方式将此功能添加到键盘配置中？
或者，因为我通常对函数使用“步骤特定”命令，例如
void doSomethingInterestingWith(sharedPtrToDb->getEltFromDb(EltId(atoi(key))))
我想知道是否有可能创建一个直接进入外部函数(doSomethingInterestingWith())的快捷方
浏览 0提问于2016-09-09得票数 6
回答已采纳
我正在测试AAC战术库，以重写模块的结合性和交换性。根据，人们应该：
根据安装情况，可以修改以下两行，或者将它们添加到.coqrc文件中，替换“”。使用aac_tactics库的路径。
Add Rec LoadPath "." as AAC_tactics.
Add ML Path ".".
Require Import AAC.
Require Instances.
但我不知道如何找到通往aac_tactics库的路径，并使用“。没起作用。
我在Ubuntu 16.04 LTS下安装了Coq，大致如下：
opam repo add coq-releas
浏览 3提问于2016-06-24得票数 1
回答已采纳
我有时会在Coq中看到这个语法来表示某些类型/集，例如打印有关存在变量的信息：
?T : [ |- Set]
?T0 : [ x : ?T |- Set ]
我不知道如何搜索这个语法。
什么意思？
第一个是否与
? T : Set
浏览 1提问于2016-07-21得票数 3
回答已采纳
我们从类型的层次结构中了解到，Set是Type(0)，Type(i)的类型是Type(i+1)。因此，对于Type(i)的任何术语t，它也是Type(i+1)的术语。有没有可能在Coq中使用这个结构？例如，假设我们有
apple: Fruit, apple : Food
由于水果是食物，我想构造类型Fruit和Food，使得Fruit是Type(i)的，Food是Type(j)的，其中i<j，因此是Fruits : Food。在Coq中有这样的可能性吗?如果没有，有没有其他方法来形成这种结构？
浏览 1提问于2018-07-24得票数 0
1回答
我编写了一个解析器程序(用OCaml编写)，将输入作为xsd，然后将其生成为Coq文件。但在终端机上需要大量的时间(~：0m.0152)才能产生。我想知道一些建议，才能使推车跑得更快？例如，使程序变慢的原因是什么？这是我第一次面对这个运行时间问题。因此，我非常感谢您对此有任何建议/经验？
非常感谢
编辑:我可以尝试通过主文件解释：
open Libxml;; (*it is the library for xml file*)
open Error;; (* it is for the error message*)
let main () =
let xml = parse_
浏览 5提问于2013-10-21得票数 1
回答已采纳
我需要在Coq中证明，对于任何类型X和任何命题P(尽管我认为即使P是一个类型，它也应该是有效的)存在 trunc_impl：|| P-> X || -> (P-> ||X||) 其中，||_||是HoTT书中用来表示命题截断的符号。 我在类型论中证明了这一陈述:一是利用命题截断的归纳原理，假设一个H：|| P->X ||和一个p: p，H=|H'|，其中H'：P-> X，然后定义trunc_impl(p):= |H'(p)|。(|-|表示服务的构造函数，即|_|：一个-> ||A||)。 顺便说一下，我不能用Coq写它！任何帮助都将
浏览 14提问于2020-08-10得票数 0
2回答
我是Coq的初学者。 虽然计算机为我验证了证明是令人满意的，但对于人类来说，满足Coq的证明是出了名的难以阅读。下面是一个简单的例子，假设你没有看到任何评论： Theorem add_comm : forall n m : nat,
n + m = m + n.
Proof.
intros n m.
induction m as [|m Hm].
- (* n + 0 = 0 + n *)
simpl. (* n + 0 = n *)
浏览 27提问于2021-09-06得票数 3
2回答
我正在学习coq，不明白为什么重写不起作用。 我的代码如下所示： Inductive nat : Type :=
| zero
| succ (n : nat)
.
Fixpoint add (a b : nat) : nat :=
match b with
| zero => a
| succ b' => add (succ a) b'
end.
Theorem add_succ : forall a b : nat,
add a (succ b) = succ (add a b).
Proof.
induction b as
浏览 51提问于2021-09-28得票数 0
回答已采纳
1回答
对于这些简单的推理规则，我想要Ltac战术。
在Modus Ponens中，如果我有H:P->Q和H1:P，Ltac mp H H1将把Q添加到上下文中作为H2 : Q。
在ModusTol透镜中，如果我有H:P->Q和H1:~Q，那么Ltac mt H H1将向上下文中添加H2:~P。
我写了一封信给大家，但它在复杂的情况下行不通，因为先例也是一种暗示。
Ltac mp H0 H1 := let H := fresh "H" in apply H0 in H1 as H.
编辑:我在另一个看似无关的问题()中找到了对apply的答案，在这个问题中，apply的“哑
浏览 2提问于2018-10-22得票数 4
回答已采纳
我正在使用opam 安装coq，并收到了错误消息。
`No solution for coq: The following dependencies couldn't be met:
- coq → ocaml < 4.10
base of this switch (use '--unlock-base' to force)
我继续使用以下命令切换到ocaml 4.05.0
opam switch create with-coq 4.05.0
并且可以成功地安装Coq，但是我更愿意使用最新版本的ocaml。这是Coq
浏览 0提问于2020-04-04得票数 2
回答已采纳
1回答
我试图用Coq编写一个程序来解析一个相对简单的上下文无关语法(一种括号)，而我的一般算法是解析器可能返回字符串的其余部分。例如，解析"++]>><<"应该返回CBTerminated [Incr Incr] ">><<"，然后，假设解析"++>><<“的解析器能够获取">><<”并继续进行。
所以很明显，字符串较小，但令人信服的Coq则是另一回事。它给了我错误
parseHelper的递归定义是不正确的...。递归调用parseHelper的主体参数
浏览 4提问于2016-05-26得票数 5
回答已采纳
1回答
我一直在使用上的下载链接来安装Coq。但是，当我在终端或命令提示符上尝试coqc或coqtop时，我收到错误消息，指出找不到该命令。尽管如此，我仍然可以在Coq IDE上很好地运行Coq，但是当我编译buffer时，特别是来自的练习，我得到了以下消息。
Running: coqc -I '/Users/zhangsheng/Desktop/G/repos/Coqy/cis500' '/Users/zhangsheng/Desktop/G/repos/Coqy/cis500/Basics.v' 2>&1
据我所知，2>&1似乎是某种形式
浏览 17提问于2017-01-26得票数 2
回答已采纳
我如何在coq中写一个类似于这个开关状态的开关状态(在铁锈中)？特别是，我很好奇如何合并coq中的分支以产生相同的输出，并通过一些默认实现耗尽其余的分支。
type Voltages = u32; // in coq is similar to Definition Voltages := R.
type Timestamp = u32; // in coq is similar to Definition Timestamp := R.
const TD: Timestamp = 2; // dummy value cuz rust, in coq would be Variable TD
浏览 1提问于2022-04-24得票数 0
回答已采纳
我正在遵循一个coq教程，它需要一个基本的coq OPAM库coq:io:system。但我在使用OPAM时遇到了错误。(这是Ubuntu14.04，coq 8.4pl6和opam1.2.1)
我用谷歌搜索了一下，没有找到任何解决方案。
有没有人知道问题可能是什么以及如何修复这个错误？
谢谢。
=-=- Processing actions -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
∗ installed coq:function-ninjas.1.0.0
∗ installed coq:error-handlers.
浏览 1提问于2015-05-26得票数 1
我买了一台新机器(mac book m1，不确定这是否重要)，我注意到我没有Coq：
(base) brandomiranda~ ❯ coqc -v
zsh: command not found: coqc
因此，我按照说明下载coq ()。它的某些部分似乎起作用了：
(base) brandomiranda~ ❯ opam init
eval $(opam env)
<><> Required setup - please read <><><><><><><><>&l
浏览 5提问于2022-02-14得票数 0
2回答
考虑以下几行( Coq)：
Variable A : Type.
Variable f g : A -> A.
Axiom Hfg : forall x, f x = g x.
Variable a b : A.
Axiom t : g a = g b.
Goal f a = g b.
战术refine (eq_trans (Hfg _) t)解决了目标。也就是说，Coq可以在不需要帮助的情况下用a替换这个孔。但是战术refine (eq_trans (Hfg a) _)用g a = g b代替了上面的目标。
但是，Coq无法单独找到t。战术refine (eq_trans (Hfg
浏览 2提问于2015-02-12得票数 3
回答已采纳
我对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是自动加载的，所以这里
浏览 5提问于2017-11-22得票数 1
回答已采纳
1回答
据我所知，Coq有内置的一阶逻辑https://coq.inria.fr/tutorial/1-basic-predicate-calculus。但Coq不是定理证明者，Coq是证明助手，这意味着用户需要在每一步中提供一些提示，Coq应该选择什么规则/策略。存在更多的ore - lest组合启发式策略，但Coq仍然不是证明者。我听说过在证明助手中使用机器学习或其他启发式方法来自动化证明过程的努力(它们被命名为*hammer?)，其中一些趋势发表在http://ai4reason.org/activities.html上。 我的问题是- Coq能否被配置为与一阶逻辑的E-prover或Z3 p
浏览 21提问于2019-05-15得票数 3
回答已采纳
我正在编写我自己的第一个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
浏览 1提问于2020-06-12得票数 0
回答已采纳
我安装了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中讨论与记录相关的子类型的参考资料，但找不到。 我特别想知道Record _ : _ := { _ :> * }语法是什么意思，以及它是如何运行的。尤其是当一条记录有:>和:判断的混合时，我想所有的正常子类型关系(包括排列)都成立？ 请分享您认为相关的其他参考资料(键入规则、子类型在Coq中的实际用法等) 顺便说一句- Agda中有没有类似的机制，如果有的话，欢迎对这一点进行更多的参考。
浏览 26提问于2020-12-16得票数 1
在使用类型类时，Coq有时会出现分歧。在Proof General下发生这种情况时，Emacs也会挂起。
我所知道的最好的恢复方法是中断emacs (C-g)并重新启动Coq (C-c C-x)。但是，这并不是简单地终止Coq进程，而是将我置于Emacs再次挂起的模式中，并显示“正在收回缓冲区...”。相当长的一段时间(有时太长以至于我放弃了，只是开始一个全新的emacs!)。
为什么？
有没有更好的方法？(还有:当这种情况发生时，有没有一个简单的第一步来查看什么是不同的？)
浏览 0提问于2018-02-04得票数 3
当将(string) -s表达式解析为嵌套数组/表示AST的列表时，我遇到了一个意外的错误。S-表达式来自(SerAPI )，但在我看来很好：
sexp = b'(Answer 3(ObjList((CoqGoal((fg_goals(((name 3)(ty(App(Ind(((Mutind(MPfile(DirPath((Id Logic)(Id Init)(Id Coq))))(DirPath())(Id eq))0)(Instance())))((Ind(((Mutind(MPfile(DirPath((Id Datatypes)(Id Init)(Id Coq))))(Dir
浏览 2提问于2019-04-22得票数 0
回答已采纳
2回答
我试图证明自然数上的下列简单定理：
((i + j) = (i + k)) -> (j = k)
以下是我在Coq中的内容
Theorem cancel : forall (i j k : nat),
((add i j) = (add i k)) -> (j = k).
Proof.
intros i j k.
induction i.
simpl.
apply A_IMPLIES_A.
simpl.
在那之后，我有了一个子目标：
S (add i j) = S (add i k) -> j = k
所以我想我应该应用eq_add_S，它说明了S m = S n -&g
浏览 0提问于2019-01-16得票数 0
回答已采纳
我在开发Angular库时遇到了一个问题: angular-coq。
我正在尝试提供以下功能：
<div ng-controller="myController">
<form coq-model="team1">
<!-- Inputs will be automatically added to form (wrapped in <p>) -->
</form>
</div>
使用在作用域team1中公开的myController，一个具有2个属性的自定义
浏览 1提问于2014-06-13得票数 1
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
回答已采纳
1回答
在Coq中，我有两个假设-- H和H0，它们相互矛盾。问题是，它们只是在某些专业上互相矛盾，而在这个证明的时刻，上下文并不是那么专业。
此时，我的证明上下文如下所示：
color : Vertex -> bool
v : V_set
a : A_set
x0, x1 : Vertex
H : v x0 -> v x1 -> a (A_ends x0 x1) \/ a (A_ends x1 x0) -> color x0 <> color x1
H0 : v x0 -> v x1 -> a (A_ends x0 x1) \/ a (A_e
浏览 1提问于2017-09-11得票数 4
回答已采纳
我使用了从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 < 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
假设我们有：
Require Import ZArith Program.
Program Fixpoint range (from to : Z) {measure f R} : list :=
if from <? to
then from :: range (from + 1) to
else [].
我想让Coq相信这已经结束了--我试着用abs (to - from)来测量范围的大小。然而，这并不是很有效，因为一旦范围为空(即from >= to)，它就会再次开始增加。
我还尝试使用以下方法进行测量：
Definition get_range (from
浏览 2提问于2018-01-06得票数 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
回答已采纳
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 (suc n)
thin zero y = suc y
thin (suc x) zero = zero
thin (suc x) (suc y) = suc (thin x y)
我认为这可以直截了当地翻译为：
Inductive Fin : nat
浏览 5提问于2016-05-03得票数 2
回答已采纳
1回答
我试图在Coq中建立一种不那么天真的非决定论一元编码(比MonadPlus和公共列表更不天真)，这种编码经常在Haskell中使用；例如，对列表的编码如下所示
data List m a = Nil | Cons (m a) (m (List m a))
而Coq中相应的定义如下所示。
Inductive List (M: Type -> Type) (A: Type) :=
Nil: List M A
| Cons : M A -> M (List M A) -> List M A.
然而，这种定义在Coq中是不允许的，因为归纳数据类型是“严格正的”-conditi
浏览 0提问于2016-04-05得票数 5
回答已采纳
我目前使用的是我以标准方式安装的标准版本(可能是通过网站)。但我想使用。我相信我已经正确安装了它，因为我有一个bin文件，所有常见的Coq内容似乎都在那里：
pinno:~/gamepad/tcoq $ ls bin
coq-tex coqc coqchk.byte coqdep_boot coqmktop coqtop.byte coqworkmgr gallina
coq_makefile coqchk coqdep coqdoc coqtop coqwc fake_ide ocamllibdep
浏览 4提问于2019-01-28得票数 0
2回答
我试图在Coq中证明以下引理：
Lemma not_eq_S2: forall m n, S m <> S n -> m <> n.
这看起来很简单，但我不知道如何完成这个证明。有谁能帮帮我吗？
谢谢。
浏览 4提问于2015-12-02得票数 2
扫码
添加站长 进交流群
领取专属 10元无门槛券
手把手带您无忧上云
相关资讯
热门标签
云服务器
ICP备案
对象存储
实时音视频
即时通信 IM活动推荐
腾讯云开发者
