有人可以给我一个关于Coq存在实例化和存在概括的简单例子吗？当我想要证明exists x, P,在P某些地方Prop使用时x,我经常想要命名x(作为x0或某些),并操纵P.这可能是Coq中的一个吗？
我正在尝试通过在线软件基础书籍来学习Coq:http://www.cis.upenn.edu/~bcpierce/sf/
我正在使用交互式命令行Coq解释器coqtop.
在归纳章节(http://www.cis.upenn.edu/~bcpierce/sf/Induction.html)中,我完全按照说明进行操作.我使用编译Basics.v coqc 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".
一切正常,直到最后一行,此时我收到以下错误:
Toplevel input, characters 5-15:
> Case "b = true".
> ^^^^^^^^^^
Error: No interpretation for string "b = true".
我对Coq太新了,开始解压为什么这不起作用.我在网上找到了一些建议我需要先做的事情Require String.,然而,这也没有用.有没有人通过这本书或遇到过这个问题？如何让代码正常工作？
这个Case关键字(战术？)似乎依赖于SF书不清楚的其他东西,但我无法弄清楚是什么.
在证明期间,我遇到了一个假设H.我有lemmas:H -> A和H -> B.
我怎样才能复制H以便推断两个假设A和B？
编辑:更确切地说,我有:
lemma l1: X -> A.
lemma l2: X -> B.
1 subgoals, subgoal 1 (ID: 42)
H: X
=========
Y
但是,我想得到:
1 subgoals, subgoal 1 (ID: 42)
H1: A
H2: B
=========
Y
假设我想证明以下定理:
Theorem succ_neq_zero : forall n m: nat, S n = m -> 0 = m -> False.
这个是微不足道的m,因为假设不能同时为后继和零.但是我发现证明这一点非常棘手,而且我不知道如何在没有辅助引理的情况下制作它:
Lemma succ_neq_zero_lemma : forall n : nat, O = S n -> False.
Proof.
intros.
inversion H.
Qed.
Theorem succ_neq_zero : forall n m: nat, S n = m -> 0 = m -> False.
Proof.
intros.
symmetry in H.
apply (succ_neq_zero_lemma n).
transitivity m.
assumption.
assumption.
Qed.
我很确定有更好的方法来证明这一点.最好的方法是什么？
我有一个Coq项目,其库被组织成子目录,如:
…/MyProj/Auxiliary/Aux.v
…/MyProj/Main/Main.v (imports Auxiliary/Aux.v)
当我编译文件时,我希望从工作目录MyProj(通过makefile)这样做.但是我也想使用Proof General/Coqtop来处理文件,在这种情况下,工作目录默认是文件所在的目录.
但这意味着两个上下文之间的LoadPath是不同的,因此库导入所需的逻辑路径是不同的.如何设置coqc调用,LoadPath和导入声明,以便它们在两个上下文中都能工作？
我尝试过的每种方法都出了问题.例如,如果我Aux.v通过调用编译
coqc -R "." "MyProj" Auxiliary/Aux.v
并将其导入Main.v为
Require Import MyProj.Auxiliary.Aux.
然后,当我编译时Main.v,这工作
coqc -R "." "MyProj" Main/Main.v
但在Coqtop失败了Error: Cannot find library MyProj.Auxiliary.Aux in loadpath.另一方面,如果在Require Import我添加之前
Add LoadPath ".." as MyProj.
然后这在Coqtop中工作,但是失败coqc -R "." "MyProj" Main/Main.v了
Error: The file […]/MyProj/Auxiliary/Aux.vo contains library
MyProj.Auxiliary.Aux而不是库MyProj.MyProj.Auxiliary.Aux
我正在寻找一个对于与协作者共享的库(并希望最终与用户共享)的强大解决方案,因此特别是它不能使用绝对文件路径.我现在发现的最好的方法是在Proof General调用Coqtop时添加emacs局部变量来设置LoadPath:
((coq-mode . ((coq-prog-args . ("-R" ".." "MyProj" "-emacs")))))
但是这个(a)似乎有点hacky,而且(b)只适用于Proof General,而不适用于Coqide或普通的Coqtop.有更好的解决方案吗？
我看到很多Coq战术在功能上相互重叠.
例如,当你在设定确切的结论,您可以使用assumption,apply,exact,trivial,或者其他人.其他例子包括destruct和induction非感应类型(??).
我的问题是:
是否有一个最小的一套基本的策略(即不包括auto,其类似物)完成后,在这个意义上,这一套可以用来证明关于自然数的功能,任何勒柯克,可证明的定理？
这个最小完整集中的策略理想情况下是基本的,因此每个都只执行一个(或两个)函数,并且可以很容易地理解它的作用.
我在Linux(Ubuntu 17.04)中成功安装了Coq 8.6和CoqIDE.但是,我不知道为了将SSReflect和MathComp添加到此安装中而继续.我检查过的所有参考资料似乎都让我很困惑.有没有人有一个直接和简单的食谱？我确实安装了opam.
我试图这样做如下:
? (A : *) ->
? (B : (A -> *)) ->
? (t : (? (r : *) -> (? (x : a) -> (B x) -> r)) -> r) ->
(t (B (t A (? (x : A) -> ? (y : (B x)) -> x)))
(? (x : A) -> ? (y : (B x)) -> y))
请注意,由于该函数返回的值取决于sigma本身内部的值,因此我需要提取该值.此代码不会检查,因为,我认为,它无法将从Sigma中提取的类型与其中的类型统一起来.
有没有解决方法？
在Coq,......之间的区别是什么？
我基本上记住了一些常见的模式.我通常使用Require Import X来查看代码.然后是Import ListNotation.我只是注意到它也可以只写需要X.有什么区别？一些实际的例子将不胜感激.
在Agda中,可以使用PHOAS方便地表示λ项:
data Term (V : Set) : Set where
var : V ? Term V
abs : (V ? Term V) ? Term V
app : Term V ? Term V ? Term V
这种方法比Bruijn指数有几个好处,如"机械化语义的参数高阶抽象语法"中所述.据我所知,不能有一个eval : ? {V} -> Term V -> Term V函数,给定一个λ项,返回其正常形式 - 毕竟,Agda是完全的,而λ演算不是.但我想知道是否有可能eval为仿射λ项编写这样的函数; 即,绑定变量最多出现一次的那些.这种语言显然是完全的.