标签: proof-general

与Agda不同,Coq倾向于将证明与功能分开.Coq提供的策略非常适合编写校样,但我想知道是否有办法复制一些Agda模式功能.

具体来说,我想:

• 一些相当于Agda ?或Haskell的_,我可以在编写时省略函数的一部分,并且(希望)让Coq告诉我需要放在那里的类型
• 相当于Agda模式下的Cc Cr(reify),?用一个函数填充一个块,它将?为所需的参数创建新块
• 当我match在函数中执行时,让Coq自动写入扩展可能的分支(如Agda模式中的Cc Ca)

这是可能的,在CoqIde或Proof General中？

此问题与在Emacs中的Proof General中配置Coq模式有关.

我正在尝试让Emacs使用相应的Unicode字形自动替换Coq中的关键字和符号.我设法定义fun为希腊小写lambdaλ,forall作为通用量词符号∀等.我没有问题定义单词的符号.

问题是,当我尝试定义操作符=>,->,<->等他们的Unicode符号⇒→↔,他们不是在勒柯克相应的Unicode字形所取代.但是,*scratch*当我测试它们时,它们会在缓冲区中被替换.我使用相同的机制将Unicode glyps与Coq表示法匹配:

(defun define-glyph (string char-info)
  (font-lock-add-keywords
   nil
   `((,(format "\\<%s\\>" string)
      (0 (progn
       (compose-region
        (match-beginning 0) (match-end 0)
        ,(apply #'make-char char-info))
       nil))))
   ))

我怀疑问题是Coq模式将某些标点符号标记为特殊标记,因此Emacs忽略了我的代码以用Unicode字形替换它们,但我不确定.有人可以帮我解释一下吗？

编辑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),我想这是一个相关的限制. …

我在Aquamacs上使用Emacs中的Proof General,每次写一段时间(".")都会执行一切(直到那段时间).这似乎是一种电动行为,但事实并非如此.所有其他键表现正常.

我知道这是我偶然使用一些键绑定时开始的一些模式.如果我重新启动会话,效果将停止,但我想知道键绑定使其停止(或使其启动).

你知道这种模式叫什么吗？我甚至无法在网上找到它.

我一直在努力学习虽然原则上我喜欢异步防爆检查的主意,用伊莎贝尔2016年,我不喜欢伊莎贝尔/ jEdit的为许多原因,其中最严重的是,它使用了太多的内存(为了我).

如果我可以使用Isabelle 2016中的旧版Proof General,那就太棒了.我将变量设置isa-isabelle-command为指向bin/isabelleIsabelle分发目录下的文件.当我使用Proof General的菜单启动Isabelle时,Emacs挂起,当我打断它时C-g,我在*isabelle*缓冲区中得到以下内容.

 > val it = (): unit
 ^BException- ERROR "Bad socket name: \"I\"" raised

我知道这个站点上的旧帖子表明,Proof General用来与定理证明者通信的Isabelle组件被删除了.这是(仍然)Isabelle 2016的真实情况吗？如何在较新版本的Isabelle中使用Proof General？

我正在尝试将coq与ProofGeneral一起使用，但是内置的Verilog模式遮盖了*.v文件类型识别。我可以以某种方式禁用它，让ProofGeneral将其重新映射到其CoQ模式吗？

在大多数IDE或文本编辑器中,您可以右键单击一个术语,它会将您带到定义该术语的文件中.CoqIDE似乎没有,所以我一直在做coqdoc myfile.v --html,然后去生成的HTML文档.但该文件中唯一可点击的术语是Coq标准库.由ssreflect定义的术语(例如)不可单击.

有没有一种标准的方法能够在Coq文件中快速查找定义某些术语/标识符(以及它的源代码)的位置？无论是在CoqIDE还是在emacs + ProofGeneral中(我使用的是CoqIDE,但如果emacs/ProofGeneral具备此功能,我会切换).

或者是为每个Coq项目和您使用的依赖项生成文档的标准方法？

可能是一个coq新手问题,但我找不到一个现成的解决方案,所以我会在这里请求参考.cocq版本是8.5pl2

我试着建立 coqfj.第一次make尝试失败,第37行出现了一些错误src/FJ/ClassTable.v.这个问题不是关于那个错误.

仔细看看,我打开ClassTable.v了emacs proofgeneral并按下C-c C-n,或者运行coqc src/FJ/ClassTable.v.结果是第1行出错:

File "./src/FJ/ClassTable.v", line 1, characters 15-23:
Error: Cannot find a physical path bound to logical path matching suffix FJ.

似乎导入require import FJ.Lists无法解决(尽管FJ用作前缀,而不是后缀).我注意到make已经创建了一个编译文件src/Lists.vo,应该由coqc选中.

如何告诉coqc它应该通过查看文件夹中的文件*.vo或*.v文件来解决这个"后缀" src？

我正在做软件基础练习，并且combine_split在尝试证明辅助引理时遇到了困难。

当在证明过程reflexivity中应用时assert，尽管方程显然(x, y) = (x, y)是正确的，但证明过程只是挂在那里。

这是实现

Theorem combine_split : forall X Y (l : list (X * Y)) l1 l2,
  split l = (l1, l2) ->
  combine l1 l2 = l.
Proof.
  intros X Y.
  intros l.
  induction l as [| n l' IHl'].
  - simpl. intros l1 l2 H. injection H as H1 H2. rewrite <- H1, <-H2. reflexivity.
  - destruct n as [n1 n2]. simpl. destruct (split l'). 
    intros …

当Isabelle在ProofGeneral中显示目标时,假设会围绕它们呈现括号,如下所示:

然而,在Isabelle/jEdit中,这似乎已经改为meta-implication箭头:

虽然我理解前者有点不标准,但我觉得它更容易阅读.有没有办法修改Isabelle/jEdit的行为以打印旧ProofGeneral风格的目标？

有人可以解释一下如何完成这个证明吗？（请不要给出实际答案，只是一些指导:)

练习来自 SF 第 1 卷，如标题所示，内容如下：

(** **** Exercise: 3 stars, standard (injection_ex3) *)
Example injection_ex3 : forall (X : Type) (x y z : X) (l j : list X),
  x :: y :: l = z :: j ->
  j = z :: l ->
  x = y.

现在，我在介绍所有术语后尝试通过injectionon来解决这个问题H0。injection经过重写后H2，我最终得到了以下目标，但我不知道如何前进。

1 subgoal (ID 174)
  
  X : Type
  x, y, z : X
  l, j : list X
  H2 : x = …