我可以使用类型类型在Coq中天真地构建代数结构的层次结构.我在查找Coq语法和类型类语义方面遇到了一些麻烦.但是,我相信以下是半群,幺半群和交换幺半群的正确实现:
Class Semigroup {A : Type} (op : A -> A -> A) : Type := {
op_associative : forall x y z : A, op x (op y z) = op (op x y) z
}.
Class Monoid `(M : Semigroup) (id : A) : Type := {
id_ident_left : forall x : A, op id x = x;
id_ident_right : forall x : A, op x id = x
}.
Class AbelianMonoid `(M : Monoid) : Type := …上下文:我正在从事软件基础的练习.
Theorem neg_move : forall x y : bool,
x = negb y -> negb x = y.
Proof. Admitted.
Theorem evenb_n__oddb_Sn : forall n : nat,
evenb n = negb (evenb (S n)).
Proof.
intros n. induction n as [| n'].
Case "n = 0".
simpl. reflexivity.
Case "n = S n'".
rewrite -> neg_move.
在最后一行之前,我的子目标是这样的:
evenb (S n') = negb (evenb (S (S n')))
我想将其转化为:
negb (evenb (S n')) = evenb (S (S n'))
rewrite -> …
我正在学习Coq和我正在学习的书,(CPDT)大量使用auto证明.
因为我正在学习,所以我认为确切地看到auto引擎盖下的内容可能会有所帮助(早期越少越好).有没有办法强制它显示它用于计算证据的确切策略或技术？
如果没有,是否有一个地方详细说明了什么auto呢？
我是Coq的新手,并试图根据我的研究开发一个框架.我的工作非常沉重,而且由于Coq似乎对待集合而我编码很困难.
有Type和Set,他们称之为"排序",我可以用它们来定义一个新的集合:
Variable X: Type.
然后有一个库编码(子)设置为' Ensembles ',它们是从一些Type到另一个的函数Prop.换句话说,它们是对a的谓词Type:
Variable Y: Ensemble X.
Ensemble感觉更像是适当的数学集合.此外,它们是由许多其他图书馆建立的.我已经尝试过关注它们:定义一个通用集U: Set,然后将自己限制在(子)Ensemble上U.但不是.Ensembles不能用作其他变量的类型,也不能用于定义新的子集:
Variable y: Y. (* Error *)
Variable Z: Ensemble Y. (* Error *)
现在,我知道有几种方法可以解决这个问题.问题" 子集参数 "提供了两个.两者都使用强制.第一个坚持Sets.第二个基本上使用Ensembles(虽然不是名字).但两者都需要相当多的机器才能完成如此简单的事情.
问题:一致(优雅)处理集的推荐方法是什么？
示例:以下是我想要做的示例:假设设置DD.定义一对dm =(D,<),其中D是DD的有限子集,而<是D上的严格偏序.
我敢肯定,通过强制修改或其他结构,我可以完成它; 但不是特别易读; 并没有很好的直觉,如何进一步操纵结构.例如,以下类型检查:
Record OrderedSet {DD: Set} : Type := …我想考虑以下三个(相关的？)Coq定义.
Inductive nat1: Prop :=
| z1 : nat1
| s1 : nat1 -> nat1.
Inductive nat2 : Set :=
| z2 : nat2
| s2 : nat2 -> nat2.
Inductive nat3 : Type :=
| z3 : nat3
| s3 : nat3 -> nat3.
这三种类型都给出了归纳原则来证明一个命题.
nat1_ind
: forall P : Prop, P -> (nat1 -> P -> P) -> nat1 -> P
nat2_ind
: forall P : nat2 -> Prop,
P z2 -> (forall n : nat2, P n …当我用来Function在Coq中定义非结构递归函数时,在询问特定计算时,结果对象的行为很奇怪.实际上,Eval compute in ...指令不是直接给出结果,而是返回相当长的(通常为170 000行)表达式.似乎Coq无法评估所有内容,因此返回一个简化(但很长)的表达式而不仅仅是一个值.
这个问题似乎来自我证明所产生义务的方式Function.首先,我认为问题来自我使用的不透明术语,并且我将所有的引理转换为透明常量.那么,有没有办法列出一个术语中出现的不透明术语？或者任何其他方式将不透明的引理变成透明的引理？
然后我说,问题来自于所使用的订单有充分根据的证据.但我得到了奇怪的结果.
例如,我log2通过重复应用来定义自然数div2.这是定义:
Function log2 n {wf lt n} :=
match n with
| 0 => 0
| 1 => 0
| n => S (log2 (Nat.div2 n))
end.
我有两个证明义务.第一个检查n尊重lt递归调用中的关系,并且可以很容易地证明.
forall n n0 n1 : nat, n0 = S n1 -> n = S (S n1) -> Nat.div2 (S (S n1)) < S (S n1)
intros. apply Nat.lt_div2. apply le_n_S. apply …有没有办法一次简化一步？
假设您f1 (f2 x)可以通过单一依次简化这两者simpl,是否可以简化f2 x作为第一步,检查中间结果然后简化f1？
以例如定理为例:
Theorem pred_length : forall n : nat, forall l : list nat,
pred (length (n :: l)) = length l.
Proof.
intros.
simpl.
reflexivity.
Qed.
该simpl战术简化Nat.pred (length (n :: l))到length l.有没有办法将其分解为两步简化,即:
Nat.pred (length (n :: l)) --> Nat.pred (S (length l)) --> length l
与Agda不同,Coq倾向于将证明与功能分开.Coq提供的策略非常适合编写校样,但我想知道是否有办法复制一些Agda模式功能.
具体来说,我想:
?或Haskell的_,我可以在编写时省略函数的一部分,并且(希望)让Coq告诉我需要放在那里的类型?用一个函数填充一个块,它将?为所需的参数创建新块match在函数中执行时,让Coq自动写入扩展可能的分支(如Agda模式中的Cc Ca)这是可能的,在CoqIde或Proof General中？
I was wondering whether Coq defined the real numbers as Cauchy sequences or Dedekind cuts, so I checked Coq.Reals.Raxioms and... none of these two. The real numbers are axiomatized, along with their operations (as Parameters and Axioms). Why is it so?
Also, the real numbers tightly rely on the notion of subset, since one of their defining properties is that is every upper bounded subset has a least upper bound. The Axiom completeness encodes those subsets as Prop …
我试图看看是否可以evenb n = true <-> exists k, n = double k从https://softwarefoundations.cis.upenn.edu/lf-current/Logic.html证明,而不涉及奇数.我尝试过以下内容:
Theorem evenb_double_k : forall n,
evenb n = true -> exists k, n = double k.
Proof.
intros n H. induction n as [|n' IHn'].
- exists 0. reflexivity.
- (* stuck *)
但显然感应一次只能起作用一个自然数,exists k : nat, S n' = double k显然不可证明.
n' : nat
H : evenb (S n') = true
IHn' : evenb n' = true -> exists k : nat, …