我在Aquamacs上使用Emacs中的Proof General,每次写一段时间(".")都会执行一切(直到那段时间).这似乎是一种电动行为,但事实并非如此.所有其他键表现正常.
我知道这是我偶然使用一些键绑定时开始的一些模式.如果我重新启动会话,效果将停止,但我想知道键绑定使其停止(或使其启动).
你知道这种模式叫什么吗？我甚至无法在网上找到它.
我在Coq试图证明这一点
Theorem evenb_n__oddb_Sn : ?n : nat,
evenb n = negb (evenb (S n)).
我正在使用感应n.基本案例是微不足道的,所以我处于归纳案例,我的目标看起来像:
k : nat
IHk : evenb k = negb (evenb (S k))
============================
evenb (S k) = negb (evenb (S (S k)))
当然,现在有一个断言的函数的基本公理
a = b -> f a = f b
适用于所有功能f : A -> B.所以我可以申请negb双方,这会给我
k : nat
IHk : evenb k = negb (evenb (S k))
============================
negb (evenb (S k)) = negb (negb (evenb (S …我无法理解Coq中类型类和依赖记录之间的区别.参考手册给出了类型类的语法,但没有说明它们到底是什么以及如何使用它们.一些思考和搜索揭示了类型类本质上是具有一些语法糖的依赖记录,允许Coq自动推断一些隐式实例和参数.当在任何给定的上下文中只有一个或多或少的一个可能的实例时,似乎类型类的算法工作得更好,但这不是一个大问题,因为我们总是可以将类型类的所有字段移动到它的参数,消除歧义.此Instance声明也会自动添加到Hints数据库中,这通常可以简化证明,但如果实例过于笼统并导致证据搜索循环或爆炸,有时也会破坏它们.还有其他我应该注意的问题吗？在两者之间进行选择的启发式是什么？例如,如果我只使用记录并尽可能将其实例设置为隐式参数,我会失去任何东西吗？
我是Coq的新用户.我已经定义了一些功能:
Definition p (a : nat) := (a + 1, a + 2, a + 3).
Definition q :=
let (s, r, t) := p 1 in
s + r + t.
Definition q' :=
match p 1 with
| (s, r, t) => s + r + t
end.
我试图将p的结果破坏成元组表示.然而,coqc抱怨q:
Error: Destructing let on this type expects 2 variables.
而q'可以通过编译.如果我改变p以返回一对(a + 1,a + 2),则相应的q和q'都可以正常工作.
为什么let-destruct只允许配对？或者我在语法上有任何错误？我已经检查过Coq手册,但没有发现任何线索.
谢谢!
作为Coq中的练习,我试图证明以下函数返回一对长度相等的列表.
Require Import List.
Fixpoint split (A B:Set)(x:list (A*B)) : (list A)*(list B) :=
match x with
|nil => (nil, nil)
|cons (a,b) x1 => let (ta, tb) := split A B x1 in (a::ta, b::tb)
end.
Theorem split_eq_len : forall (A B:Set)(x:list (A*B))(y:list A)(z:list B),(split A B x)=(y,z) -> length y = length z.
Proof.
intros A B x.
elim x.
simpl.
intros y z.
intros H.
injection H.
intros H1 H2.
rewrite <- H1.
rewrite <- H2.
reflexivity. …我正在阅读Mike Nahas的Coq教程,该教程说:
"ex_intro"的参数是:
- 谓词
- 证人
- 与证人一起打电话的证明
我查看了定义:
Inductive ex (A:Type) (P:A -> Prop) : Prop :=
ex_intro : forall x:A, P x -> ex (A:=A) P.
而我在解析它时遇到了麻烦.表达式的哪些部分forall x:A, P x -> ex (A:=A) P对应于这三个参数(谓词,见证和证明)？
我是依赖类型的新手(尽管他们有很大的不同,我正在尝试Idris和Coq).
我试图表达以下类型:给定类型T和k nats n1,n2,... nk的序列,由k个k序列组成的类型,其长度分别为n1,n2,... nk.
即,k个向量的向量,其长度由参数给出.这可能吗？
当我Extraction Language Haskell.在Coq文件中使用Coq提取/编译Coq到Haskell 并运行时coqtop -compile mymodule.v > MyModule.hs,我得到了一个以Haskell开头的模块module Main where.
是否可以选择设置生成的Haskell模块名称？
我目前管道像这样sed -
coqtop -compile mymodule.v | sed s/Main/MyModule/ > MyModule.hs
但我正在寻找一个更清洁的解决方案.
我想使用Program Fixpoint或Function在Coq中定义以下函数:
Require Import Coq.Lists.List.
Import ListNotations.
Require Import Coq.Program.Wf.
Require Import Recdef.
Inductive Tree := Node : nat -> list Tree -> Tree.
Fixpoint height (t : Tree) : nat :=
match t with
| Node x ts => S (fold_right Nat.max 0 (map height ts))
end.
Program Fixpoint mapTree (f : nat -> nat) (t : Tree) {measure (height t)} : Tree :=
match t with
Node x ts => Node (f x) (map …我正在从Coq提取到Haskell,需要在Haskell端导入几个模块.是否有任何Coq提取功能允许您自动执行此操作？我知道我可以写一个脚本来做这件事,但我宁愿不必重新发明轮子.