假设我在上下文中有两个假设,a_b : A -> B并且a : A.我应该能够申请a_b到a获得进一步的假设,b : B.
也就是说,给定以下状态:
1 subgoal
A : Prop
B : Prop
C : Prop
a_b : A -> B
a : A
______________________________________(1/1)
C
应该有一些策略,foo (a_b a)将其转换为以下状态:
1 subgoal
A : Prop
B : Prop
C : Prop
a_b : A -> B
a : A
b : B
______________________________________(1/1)
C
但我不知道是什么foo.
我能做的一件事是:
assert B as b.
apply a_b. …我想用这种destruct策略来证明案件的陈述.我在线阅读了几个例子,我很困惑.有人能更好地解释一下吗？
这是一个小例子(有其他方法可以解决它,但尝试使用destruct):
Inductive three := zero
| one
| two.
Lemma has2b2: forall a:three, a<>zero /\ a<>one -> a=two.
现在一些在线示例建议执行以下操作:
intros. destruct a.
在这种情况下,我得到:
3 subgoals H : zero <> zero /\ zero <> one
______________________________________(1/3)
zero = two
______________________________________(2/3)
one = two
______________________________________(3/3)
two = two
所以,我想证明前两种情况是不可能的.但机器将它们列为子目标,并希望我证明它们......这是不可能的.
摘要:如何准确丢弃不可能的案例？
我看过一些使用的例子,inversion但我不明白这个程序.
最后,如果我的引理依赖于几种归纳类型并且我仍想覆盖所有情况,会发生什么？
此问题与在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 (? …