我想在coq中声明一个结构,它表示一个着色良好的有向图。如果我没有条件的话,我声明了一个coq接受的寄存器。但是,我尝试了许多方法,用coq编写条件wellColored,而没有退出。每次我收到一条新的错误消息:
The condition wellColored is the following:
for every pair of vertices $v1$, $v2$ and every edge $e$, if the source of $e$ is $v1$,
the target of $e$ is $v2$ and the color of $v1$ is $a$ then
当我在下面运行Coq脚本时(对原始脚本的简化):
Inductive w (g: nat): nat -> Prop:=
| z: w g 0.
Lemma x:
forall (i j: nat), w i j -> (forall k: nat, k <= k).
Proof.
Admitted.
Lemma y:
forall (m n: nat),
w m n -> w m n.
Proof.
intros m n H.
apply x in H.
在最后一行中,我得到以下错误消息:
错误:找不到变量k的实例。
有人能向我解释
我想证明莱玛·RnP_eq。 From mathcomp Require Import ssreflect.
Require Import Coq.Program.Equality.
Definition func {n m l o:nat}
(I:t R 0 -> t R m -> t R l)(J:t R n -> t R l -> t R o):=
(fun (x:t R n)(a:t R m) => J (snd (splitat 0 x)) (I (fst (splitat 0 x)) a)).
Lemma deriveP_eq (n
我有点搞不懂Coq 中关于自然数定义的后继函数的内射性是否是公理?,根据,它是公理(7)。当我查看手册页面时,我会看到以下内容:
定义eq_add_S n m (H: S=S):n=m := f_equal pred H.
提示立即eq_add_S: core。
它看起来像一个公理(?)但令我困惑的是,在这一页的顶部写着:
它描述了关于自然数的各种引理和定理,包括Peano的算术公理(在Coq中,这些定理是可证明的)。
这句话有点模棱两可不是吗?
我有个公理
Parameter set : Type.
Parameter IN : set->set->Prop.
Axiom AXIOM_OF_SUBSETS :
forall prop x, exists y, forall u,
IN u y <-> IN u x /\ (prop u)
.
现在我想用它来构建一个空的集合,就像
Definition EMPTYSET : set.
Check (AXIOM_OF_SUBSETS (fun _ : set => False) x).
检查结果如下:
AXIOM_OF_SUBSETS (f
在Coq中,我可以编写 Variable A : False.
Axiom B : False. 假设False的名字分别是A和B。这两个陈述在证明中都有效,所以我可以 Theorem nothing_makes_sense : forall (a : Type), a.
destruct true; exfalso.
* apply A.
* apply B.
Qed. 实际的区别是什么?什么时候我应该使用一个而不是另一个?
如何让Coq识别出两种类型,每种类型都是从使用相同参数从模块函子创建的模块中导入的,但出现在不同的模块中,它们实际上是相同的类型?
极小例子
Module Type S.
End S.
Module F (s : S).
Inductive foo : Type := a.
End F.
Module G (s : S).
Include F s.
End G.
Module H (s : S).
Include F.
End H.
Module I (s : S).
Module G := G s.
Module H := H s.
(* This is a type error
考虑以下几行( Coq):
Variable A : Type.
Variable f g : A -> A.
Axiom Hfg : forall x, f x = g x.
Variable a b : A.
Axiom t : g a = g b.
Goal f a = g b.
战术refine (eq_trans (Hfg _) t)解决了目标。也就是说,Coq可以在不需要帮助的情况下用a替换这个孔。但是战术refine (eq_trans (Hfg a) _)用g a = g b代替了上面的目标。
但是,Coq无法单独找到t。战术refine (eq_trans (Hfg
从Coq中提取的Ocaml代码包括(在某些情况下)定义如下的类型__和函数__:
type __ = Obj.t
let __ = let rec f _ = Obj.repr f in Obj.repr f
文档说,在过去,这种类型被定义为unit (因此__可以被视为()),但是存在(很少)将__类型的值应用于__类型的值的情况。
__使用了OCaml中未记录的Obj模块函数,但似乎定义的函数本质上是一个完全多态的函数,它会吃掉所有参数(不管它们的数量是多少)。
有没有一些关于__不能被消除的情况以及这种类型的值被应用到相同类型的值的情况的文档,无论是从理论上(构造不可能消除的Coq项)还
你如何解释归纳谓词?它们是用来干什么的?他们背后的理论是什么?它们只存在于依赖型系统中,还是在其他系统中?它们在某种程度上与GADT有关吗?在Coq中,为什么默认情况下它们是真的?
这是Coq的一个例子:
Inductive even : nat -> Prop :=
| even0 : even 0
| evens : forall p:nat, even p -> even (S (S P))
你将如何使用这个定义?这是一种数据类型还是一个命题?
我正在学习Coq语言,并试图证明以下说法:
Lemma ex4: forall (X : Set) (P : X -> Prop), ~(forall x, ~ (P x)) -> (exists x, (P x)).
在我的证据开始时:
Proof.
intros X P A.
我到达了我有假设的那一刻
X : Set
P : X -> Prop
A : ~ (forall x : X, ~ P x)
现在我想在A上应用德摩根定律来得到一个假设
B : exists x : X, ~ (~ P x) (*** Or something similar ***)
但我找不
我想定义一个类型为PowersetTower : Type -> nat -> Type的家族,以便:
PowersetTower A 0 = APowersetTower A (n+1) = Ensemble (PowersetTower A n) (即PowersetTower A n -> Prop) )
这有可能吗?一种想法是
Inductive PowersetTower : Type -> nat -> Type :=
| base : forall (A : Type), PowersetTower A 0
| step : forall (A :
考虑以下大小列表的类型定义:
Inductive listn: nat -> Type -> Type :=
| nil: forall {A: Set}, listn 0 A
| cons: forall {n: nat} {A: Set}, A -> listn n A -> listn (S n) A.
这本质上是Idris中的类型。
我试图为init定义listn函数,它删除了最后一个元素。
我尝试的实现实际上与Idris中init的定义完全相同。这是在伊德里斯:
init : Vect (S len) elem -> Vect len elem
init
我对Coq很陌生,并尝试通过来学习它。在“Coq中的逻辑”一章中,我完成了一个练习not_exists_dist (通过猜测),但不理解:
Theorem not_exists_dist :
excluded_middle →
∀ (X:Type) (P : X → Prop),
¬ (∃ x, ¬ P x) → (∀ x, P x).
Proof.
intros em X P H x.
destruct (em (P x)) as [T | F].
- apply T.
- destruct H. (* <-- This ste
我想知道是否有一种系统的方法来解释Coq定义为agda程序。我正在翻译部分编程基础,无法让tUpdate函数在下面工作。为什么这个失败。对coq代码进行注释。
--Definition total_map (A : Type) := string -> A.
totalMap : Set → Set
totalMap A = String → A
-- Definition t_empty {A : Type} (v : A) : total_map A :=
-- (fun _ => v).
tEmpty : {A : Set} (v : A) → totalMap A
t
我在一些教程中读到if a then b else c代表match a with true => b | false => c end。但是,前者非常奇怪地不检查a的类型,而后者当然确保a是一个布尔值。例如,
Coq < Check if nil then 1 else 2.
if nil then 1 else 2
: nat
where
?A : [ |- Type]
Coq < Check match nil with true => 1 | false => 2 end.
Toplevel input, characters 33-
下面的证明是在Coq中给出的。
Fixpoint add n m := match n with 0 => m | S p => add p (S m) end.
Lemma exercise6 : forall n m, add n (S m) = S (add n m).
Proof.
induction n; intros m; simpl.
reflexivity.
rewrite IHn; reflexivity.
Qed.
我试着一步一步地写这篇文章来理解正在发生的事情,但是在解决了基本案例之后,归纳假设就不一样了!因此,战术失败:
Lemma exer
我正在用Coq阅读/测试一个证据。
Theorem ceval_step__ceval: forall c st st',
(exists i, ceval_step st c i = Some st') -> c / st || st'.
特定的函数/定义并不重要,因为它们不被使用。经过几步之后,定理被转换成一种形式,在这种形式中,内部存在量词被转换成一个通用的:
1 subgoals
______________________________________(1/1)
forall (c : com) (st st' : state) (
我尝试从列表中删除所有大于7的整数,如下所示 filter (fun n => n > 7). 但是,我得到了以下错误 The term "n > 7" has type "Prop" while it is expected to have type "bool". 我是Coq新手,我该如何修复它?
假设我有这样一个假设:
FooProp a b
我想把假设改为这种形式:
exists a, FooProp a b
我该怎么做?
我知道我可以做assert (exists a, FooProp a b) by eauto,但是我正在试图找到一个解决方案,它不需要我显式地写下整个假设;这对自动化是不好的,当假设不是微不足道的时候,这通常是一个令人头痛的问题。理想情况下,我希望指定intro_exists a in H1或其他什么;它确实应该是那么简单。
编辑:为什么?因为我有这样一个引理:
Lemma find_instr_in:
forall c i,
In i c <-