我有一个参数集:
Parameter Q:Set.
现在我想定义另一个参数,它是Q的一个子集.类似于:
Parameter F: subset Q.
我该如何定义？我想我可以稍后将限制添加为公理,但似乎更自然地直接在F的类型中表达它.
我在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 …我试图写一个假设规则,在match建构的帮助下制定:
Goal forall x:nat, (match x with | 1 => 5 | _ => 10 end = 5 -> x = 1)%nat.
intros.
x : nat
H : match x with
| 0%nat => 10%nat
| 1%nat => 5%nat
| S (S _) => 10%nat
end = 5%nat
============================
x = 1%nat
我怎么能匹配这样的假设？以下直接方法失败:
match goal with
|[H:match ?e with | ?a => ?x | ?b => ?y | ?c => ?z end = ?b] => idtac
end.
> …我是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. …我正在使用CoqIDE完成关于Coq的软件基础书中的练习.我可以成功编译Basics.v,在我的目录中生成Basics.vo和Basics.glob.当我尝试运行Induction.v时,它可以工作.当我尝试编译它时,它会抱怨大量缺少的引用,例如evenb和negb_involutive.如果我将Basics.v内容复制到Induction.v中,它会编译,但显然这不是要走的路.
这不是问题的重复Coq错误:在当前环境中找不到引用evenb,因为我已经完成了这些事情:
编译Basics.v.检查Basics.vo是否在目录中.现在编译Induction.v.最后一步失败了.
他们似乎服务于类似的目的.到目前为止我注意到的一个区别是,虽然Program Fixpoint会接受一个复合测量{measure (length l1 + length l2) },但Function似乎拒绝这个并且只会允许{measure length l1}.
是否Program Fixpoint比Function它们更强大,或者它们更适合不同的用例？
我正在从Coq提取到Haskell,需要在Haskell端导入几个模块.是否有任何Coq提取功能允许您自动执行此操作？我知道我可以写一个脚本来做这件事,但我宁愿不必重新发明轮子.
无论如何，在将Coq提取到Haskell时是否要保留评论？理想情况下，我希望机器生成的Haskell文件不受人类的影响，因此提取注释的动机很明显。但是，我找不到该怎么做的，我想知道这是否完全可能（？）。这是一个示例Coq文件：
(*************)
(* factorial *)
(*************)
Fixpoint factorial (n : nat) : nat :=
match n with
| 0 => 1
| 1 => 1 (* this case is redundant *)
| S n' => (mult n (factorial n'))
end.
Compute (factorial 7).
(********************************)
(* Extraction Language: Haskell *)
(********************************)
Extraction Language Haskell.
(***************************)
(* Extract to Haskell file *)
(***************************)
Extraction "/home/oren/Downloads/RPRP/output.hs" factorial.
当我将其提取到Haskell时，除了析因内的注释丢失之外，其他所有功能都正常运行：
$ coqc ./input.v > /dev/null
$ cat ./output.hs
module Output where
import qualified Prelude …