此问题与在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字形替换它们,但我不确定.有人可以帮我解释一下吗？
我试图在Coq中定义Ackermann-Peters函数,我收到一条我不明白的错误消息.正如你所看到的,我把a, bAckermann 的论据打包成一对ab; 我提供了一个定义参数的排序函数的排序.然后我使用Function表单来定义Ackermann本身,为它提供ab参数的排序函数.
Require Import Recdef.
Definition ack_ordering (ab1 ab2 : nat * nat) :=
match (ab1, ab2) with
|((a1, b1), (a2, b2)) =>
(a1 > a2) \/ ((a1 = a2) /\ (b1 > b2))
end.
Function ack (ab : nat * nat) {wf ack_ordering} : nat :=
match ab with
| (0, b) => b + 1
| (a, 0) => ack (a-1, 1)
| (a, b) => ack (a-1, …这是我对回文的归纳定义:
Inductive pal { X : Type } : list X -> Prop :=
| pal0 : pal []
| pal1 : forall ( x : X ), pal [x]
| pal2 : forall ( x : X ) ( l : list X ), pal l -> pal ( x :: l ++ [x] ).
我想从Software Foundations中证明这个定理:
Theorem rev_eq_pal : forall ( X : Type ) ( l : list X ),
l = rev l -> …我正在尝试compile_correct从依赖类型的认证编程的第一章做一个修改过的证明.在我的版本中,我试图利用progDenote折叠的事实,并在证明主要引理的证据中使用较弱的归纳假设compile_correct.
与本书相同的代码是:
Require Import Bool Arith List.
Set Implicit Arguments.
Inductive binop : Set := Plus | Times.
Inductive exp : Set :=
| Const : nat -> exp
| Binop : binop -> exp -> exp -> exp.
Definition binopDenote (b : binop) : nat -> nat -> nat :=
match b with
| Plus => plus
| Times => mult
end.
Fixpoint expDenote (e : exp) : nat :=
match …有喜欢的战术什么simpl的Program FixpointS'
特别是,如何证明以下琐碎的陈述？
Program Fixpoint bla (n:nat) {measure n} :=
match n with
| 0 => 0
| S n' => S (bla n')
end.
Lemma obvious: forall n, bla n = n.
induction n. reflexivity.
(* I'm stuck here. For a normal fixpoint, I could for instance use
simpl. rewrite IHn. reflexivity. But here, I couldn't find a tactic
transforming bla (S n) to S (bla n).*)
显然,Program Fixpoint这个玩具示例没有必要,但我在一个更复杂的设置中面临同样的问题,我需要证明Program Fixpoint手动终止.
理论上可以将任何Coq证明转换为Idris还是有任何限制？更抽象的问题:Idris类型系统在lambda多维数据集上的位置是什么？
这些问题的原因在于我试图了解Idris类型系统如何(和如果)与Coq类型系统相媲美.
我对Coq解析器的实现方式感到非常惊讶.例如
https://www.cis.upenn.edu/~bcpierce/sf/current/Imp.html#lab321
通过给出notation命令并且后续解析器能够解析任何表达式,解析器似乎可以接受任何lexeme.所以这意味着语法必须是上下文敏感的.但这非常灵活,绝对超出了我的理解范围.
关于这种解析器在理论上如何可行的任何指针？它应该如何工作？任何材料或知识都可行.我只是试着了解一下这种类型的解析器.谢谢.
请不要让我自己阅读Coq的来源.我想检查一般的想法,但不是具体的实现.
在一些Cedille源中使用以下Nats编码:
cNat : ?
cNat = ? X : ? . X ? (? R : ? . (R ? X) ? R ? X) ? X
cZ : cNat
cZ = ? X . ? z . ? s . z
cS : ? A : ? . (A ? cNat) ? A ? cNat
cS = ? A . ? e . ? d . ? X . ? z . ? s . s · A (? …在证明期间,我遇到了一个假设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
在Coq中,我遇到了rewrite在以下情况下应用策略的问题:
Section Test.
Hypothesis s t : nat -> nat.
Hypothesis s_ext_eq_t : forall (x : nat), s x = t x.
Definition dummy_s : nat -> nat :=
fun n => match n with
| O => 42
| S np => s np
end.
Definition dummy_t : nat -> nat :=
fun n => match n with
| O => 42
| S np => t np
end.
Goal forall (n : nat), dummy_s n = …