如何定义一般参数N:nat,N个元素的有限集合,$ A_ {0},... A_ {N-1} $？是否有一种优雅的方式通过递归定义来做到这一点？有人能指出我对这种结构进行推理的好例子吗？
我一直认为已经证明,pred对于任何数据类型的编码,在构造微积分的不变时间内都无法表达.现在,请注意nats的这种编码:
S0 : ? (r : *) . (r -> r) -> r -> r
S0 = ? s z . z
S1 : ? (r : *) (((? (r : *) . (r -> r) -> r -> r) -> a) -> (a -> a)))
S1 = ? s z . (s (? s z . z))
S2 : (? (r : *) . ((? (r : *) . ((? (r : *) . (r -> r) …我是使用Coq的新手.我想问一下我是否想要定义一个集合
A = {x | f(x) = 0},我怎么能这样做？我写的东西像:
Definition f0 := nat->nat.
Definition A : Set :=
forall x, f0 x -> 0.
他们没有按预期工作.
非常感谢.
出于这个问题的目的,假设我有:
Parameter eq_bool : forall (A:Type), A -> A -> bool.
Arguments eq_bool {A} _ _.
Axiom eq_bool_correct : forall (A:Type) (x y:A),
eq_bool x y = true -> x = y.
Axiom eq_bool_correct' : forall (A:Type) (x y:A),
x = y -> eq_bool x y = true.
我有一个函数,给出两个值x y:A返回随时和否则的Some证明.此函数通过模式匹配来实现,以测试相等性,并使用convoy模式作为一种技巧,在代码中访问对应于匹配分支的相等性证明:x = yx = yNoneeq_bool x y
Definition test (A:Type) (x y:A) : option (x = y) :=
match eq_bool x y as …我正在使用带有术语,变量和nat文字的语言进行开发,其中语言的arity构造在预定义中:
Inductive sort : Set := TERM | VAR | NAT.
Inductive termArity : list sort -> Set :=
| Var : termArity [VAR]
| Let : termArity [VAR ; TERM ; TERM]
| Lam : termArity [VAR ; TERM]
| Ap : termArity [TERM ; TERM]
| NumLit : termArity [NAT]
| Plus : termArity [TERM ; TERM]
.
我想要使用的术语的定义包含一个在其arity规范中匹配每个类型的子项(hlist是来自CPDT的异构列表):
Inductive t : Type :=
| Node : forall (sorts : list sort) (code : termArity sorts),
hlist (fun …我首先定义一个辅助函数来构建Decidable P给定证明的实例{P} + {~P}:
Require Import Coq.Classes.DecidableClass.
Definition derive_decidable : forall P : Prop, {P} + {~P} -> Decidable P.
intros P H; destruct H;
[ apply (Build_Decidable P true) | apply (Build_Decidable P false) ];
intuition congruence.
Qed.
现在我定义一个愚蠢的类型并给它一个愚蠢的Decidable实例:
Inductive Color := red | green | blue.
Instance Color_eqdec (x y : Color) : Decidable (x = y).
apply derive_decidable; decide equality.
Qed.
现在我希望能够使用这个实例来证明关于颜色的命题,但是我得到了一个令人惊讶的结果.后
Lemma green_neq_blue : green <> blue.
apply (Decidable_complete_alt _ (Color_eqdec green …我理解使用这种inversion策略的防爆原理:
Theorem ex_falso_quodlibet : forall (P:Prop),
False -> P.
Proof.
intros P contra.
inversion contra. Qed.
但是,我不明白Coq为了做同样的证明所采取的步骤,而是使用destruct而不是inversion:
Theorem ex_falso_quodlibet' : forall (P:Prop),
False -> P.
Proof.
intros P contra.
destruct contra. Qed.
False归纳如何被破坏？它如何影响目标并完成证明？
我很好奇Coq实体的类型等同于逻辑中的连接词.为了特殊性,让我们说->和/\.如果->是一个神奇的非[第一类实体],那么让我们只使用它/\作为实体.我很好奇它的域名是Prop还是Set.
是否可以使用coqtop获取表达式的类型？
我想用ghci做类似于以下的事情.
> ghci
:GHCi, version 8.6.3: :? for help
Prelude> :t (**)
(**) :: Floating a => a -> a -> a
我正在尝试确保将Coq提取到Haskell时会丢弃无用的东西Prop。但是，当我使用以下示例时，我看到两者divides和prime都被提取为Haskell空类型。这是为什么？
(***********)
(* isPrime *)
(***********)
Fixpoint isPrime (p : nat) : bool :=
match p with
| 0 => false
| 1 => false
| S p' => (negb (helper p p'))
end.
(***********)
(* divides *)
(***********)
Definition divides (n p : nat) : Prop :=
exists (m : nat), ((mult m n) = p).
(*********)
(* prime *)
(*********)
Definition prime (p : nat) : Prop :=
(p > …这是一个基本的问题。Coq具有Gallina形式的规范语言。据我了解，Coq本身是用OCaml编写的。
我的问题是，Gallina什么时候起作用？它有什么用，为什么？我想我误解了规范语言和编程语言的使用。