标签: coq

编辑4:事实证明,这实际上只是TTY输入的一个限制; 没有具体的OCaml,Coq或Emacs引起的问题.

我正在使用Emacs中的Proof General进行Coq程序,我发现输入的错误太长了.如果coqtop通过Proof General 提交的区域包含超过1023个字符,则Proof General(虽然不是Emacs)在等待响应时挂起,并且*coq*缓冲区包含一个^G超过1023的每个字符的额外字符.例如,如果是1025个字符区域被发送到coqtop,然后*coq*缓冲区将以两个额外的字符结束^G^G.我无法继续过去文件中这一点,我必须杀死coqtop过程(具有C-c C-x或kill/ killall从终端).

关于这种限制的事情coqtop本身就产生了.如果生成一个1024个字符或更长的字符串并将其输入,例如通过运行

perl -e 'print ("Eval simpl in " . (" " x 1024) . "1.\n")' | coqtop

一切正常.(同样,coqc工作正常.) 但是,如果我coqtop在终端中运行,我不能在一行上输入超过1024个字符,包括结束返回字符.因此,输入一个1023个字符的行然后点击返回工作; 但是在输入1024个字符后,点击任何键,包括返回(但不包括删除等),除了产生哔声之外什么都不做.事实证明ocaml(OCaml toplevel)具有相同的行为:

perl -e 'print ((" " x 1024) . "1;;")' | ocaml

工作正常,但如果ocaml从终端运行,我不能在一行上输入超过1024个字符.由于我的理解是coqtop依赖于OCaml顶级(更明显的是在运行时coqtop -byte),我想这是一个相关的限制. …

在OCaml邮件列表上窃听人们之前,我想我可能会在这里发布我的问题.我刚发现这个美女(链接到Concoqtion网站).Concoqtion是MetaOCaml的扩展,它允许索引类型(可能还有更多).有了它,很容易创建列表,其中包括列表的长度:

type ('n:'(nat),'a) listl =
   | Nil : ('(0),'a) listl
   | Cons of let 'm:'(nat) in 'a * ('(m),'a) listl : ('(m+1),'a) listl

这(m+1)是在类型级别完成的.井井有条.

但是,最后一个版本是2007年(OCaml 3.08).有谁知道为什么这个项目被取消,或者今天OCaml有类似的东西？

我正在通过阅读"使用依赖类型的认证编程"一书来学习Coq,而我在学习forall语法方面遇到了麻烦.

作为一个例子让我们考虑这种互感的数据类型:(代码来自书中)

Inductive even_list : Set :=
| ENil : even_list
| ECons : nat -> odd_list -> even_list

with odd_list : Set :=
| OCons : nat -> even_list -> odd_list.

这个相互递归的函数定义:

Fixpoint elength (el : even_list) : nat :=
  match el with
  | ENil => O
  | ECons _ ol => S (olength ol)
  end

with olength (ol : odd_list) : nat :=
  match ol with
  | OCons _ el => S (elength el)
  end.

Fixpoint …

我无法理解Coq中类型类和依赖记录之间的区别.参考手册给出了类型类的语法,但没有说明它们到底是什么以及如何使用它们.一些思考和搜索揭示了类型类本质上是具有一些语法糖的依赖记录,允许Coq自动推断一些隐式实例和参数.当在任何给定的上下文中只有一个或多或少的一个可能的实例时,似乎类型类的算法工作得更好,但这不是一个大问题,因为我们总是可以将类型类的所有字段移动到它的参数,消除歧义.此Instance声明也会自动添加到Hints数据库中,这通常可以简化证明,但如果实例过于笼统并导致证据搜索循环或爆炸,有时也会破坏它们.还有其他我应该注意的问题吗？在两者之间进行选择的启发式是什么？例如,如果我只使用记录并尽可能将其实例设置为隐式参数,我会失去任何东西吗？

假设我有两个归纳定义的数据类型:

Inductive list1 (A : Type) : Type :=
 | nil1 : list1 A
 | cons1 : A -> list1 A -> list1 A.

和

Inductive list2 (A : Type) : Type :=
 | nil2 : list2 A
 | cons2 : A -> list2 A -> list2 A.

对于任何P (list1 a)我应该能够以构造P (list2 a),通过施加予用于构造完全相同的方法P (list1 a),只是用nil1与nil2,list1与list2和cons1用cons2.类似地,任何list1 a作为参数的函数都可以扩展为a list2 a.

是否有类型系统允许我以这种方式说两个具有相同形状的数据类型(具有相同形状的构造函数),并证明 …

Coq的文档带有一般警告,不依赖于内置命名机制,而是选择自己的名称,以免命名机制中的更改过去证明​​无效.

在考虑表单的表达式时remember Expr as v,我们将变量v设置为表达式Expr.但是假设的名称是自动选择的,就像这样Heqv,我们有:

Heqv: v = Expr

我怎样才能选择自己的名字而不是Heqv？我总是可以使用rename命令将它重命名为我喜欢的任何内容,但这并不能保证我的证明不依赖于Coq中内置命名机制的假设未来变化.

在coq中,该destruct策略有一个变体接受"连接析取引入模式",允许用户为引入的变量分配名称,即使在解包复杂的归纳类型时也是如此.

coq中的Ltac语言允许用户编写自定义策略.我想写(实际上,维持)一种策略,在将控制权交给之前做一些事情destruct.

我希望我的自定义策略允许(或要求,更容易)用户提供我的策略可以提供的介绍模式destruct.

Ltac语法实现了什么？

以下定理在Coq中可证明吗？如果没有,有没有办法证明它不可证明？

Theorem not_for_all_is_exists:
    forall (X : Set) (P : X -> Prop), ~(forall x : X, ~ P x) -> (exists x: X, P x).

我知道这种相关关系是真的:

Theorem forall_is_not_exists : (forall (X : Set) (P : X -> Prop), (forall x, ~(P x)) -> ~(exists x, P x)).
Proof.
  (* This could probably be shortened, but I'm just starting out. *)
  intros X P.
  intros forall_x_not_Px.
  unfold not.
  intros exists_x_Px.
  destruct exists_x_Px as [ witness proof_of_Pwitness].
  pose (not_Pwitness := forall_x_not_Px witness). …

我正在尝试编写一个函数,它接受一个自然数列表并返回其中不同元素的数量作为输出.例如,如果我有列表[1,2,2,4,1],我的函数DifElem应该输出"3".我尝试了很多东西,我得到的最接近的是:

Fixpoint DifElem (l : list nat) : nat :=
   match l with
   | [] => 0
   | m::tm => 
   let n := listWidth tm in
   if (~ In m tm) then S n else n
end.

我的逻辑是:如果m不在列表的尾部,那么将一个添加到计数器.如果是,不要添加到计数器,所以我只计算一次:它是最后一次出现.我收到错误:

Error: The term "~ In m tm" has type "Prop"
which is not a (co-)inductive type.

In是Coq列表标准库的一部分Coq.Lists.List.它定义为:

Fixpoint In (a:A) (l:list A) : Prop :=
   match l with
   | [] => False
   | b :: m => b = a …

我很好奇discriminate战术背后的策略是如何运作的.因此我做了一些实验.

首先是一个简单的归纳定义:

Inductive AB:=A|B.

然后是一个简单的引理,可以通过discriminate策略证明:

Lemma l1: A=B -> False.
intro.
discriminate.
Defined.

让我们看看证明的样子:

Print l1.

l1 = 
fun H : A = B =>
(fun H0 : False => False_ind False H0)
  (eq_ind A
     (fun e : AB => match e with
                    | A => True
                    | B => False
                    end) I B H)
     : A = B -> False

这看起来相当复杂,我不明白这里发生了什么.因此,我试图更明确地证明相同的引理:

Lemma l2: A=B -> False.
apply (fun e:(A=B) => match e with end).
Defined. …