Coq中文手册.docx
Coq中文手册Coq Hand BookCCNT LabZhiling Luo指令：Require Import libsOpen Scope lib_scopeSection sec End sec由section 以及End 包抄的是一个段，sec 为段名。Example：Section Loc. EndLoc.Print ident挨印界说，ident 能够是本段界说的任何对于象，范例和本段所包含的库中界说的对于象以及范例。Example:Print R.Check ident反省范例，check 能够反省本段界说的对于象以及范例。Example:Variable tab:Type.Check tab.Definition ident :type := define界说一个对于象，能够取舍性申明其范例，可是必需要有界说体，即:=后的内容。Example:Definition setiod:=nat.Variable ident :type申明一个全部变量，只要给出范例，没有必要界说体。当出有section 包抄时，顶级的全部变量等价于齐局变量。Example:Variable ck: nat.Parameter ident :type申明一个齐局变量，只要给出范例，没有必要界说体。Example:Parameter ck:nat.Inductive ident :type :=| constru : type1>typ2>type| .界说一个回纳体，能够包孕多少个机关子（constru），可是每一个机关子的范例的最初必需是回纳体范例。Example:Inductive expr : Type :=| Evar : ident > expr| Econst : Z > expr| Eadd : expr > expr > expr| Esub : expr > expr > expr.Lemma em:type界说一个料想，其范例为type。一般必要给出证实Example:Lemma not_all_not_ex :forall P:U >Prop, (forall n:U, P n)> exists n :U, P n.Fixpoint fun (A:type)(B:type):type:= tail.fixpoint 能够界说递回函数，个中括号中的是传进参数。正在tail 中常利用match 布局能够对于回纳布局举行拆分。Example:Fixpoint tail_plus n m:nat:=match n with| 0=>m| S n=>tail_plus n (S m) end.Compute expr回纳演算expr 的值。Example:Compute 1+1.Structure exp := dom1:typ1;dom2:typ2;dom3:typ3:=value界说布局体，能够包孕多少个域，域的名字没有能反复，经由过程dom1 exp 去会见域的值，使用Build_exp 去机关。Example:Structure person:=name:string;age:nat.Coercion Rela: typ1>>typ2创建从typ1 到typ2 的强迫子范例束缚，Rela 是以前界说的转换闭系。Example:Variable dog:Type. Variablehusky:Type.Variable belong:husky>dog.Coercion belong:husky>>dog.Search keyword搜刮闭键字的界说Example:Search nat.SearchAbout keyword搜刮一切闭键字相干的界说Example:SearchAbout nat.SearchPattern exp搜刮指定情势的界说式。Example:SearchAbout ( _ > nat).特别库的利用String:挨开字符串库符以后字符串的表述：“Ser” Example:Check “Ds”.List机关子有nil 以及n:l 两个，可用+毗连两个列表。Ensemble必要先界说元素范例，而后能够申明散开。Example:Variable I:Type.Variable set1:Ensemble I.Check Union I set1 set2.Check Intersection I set1 set2证实相干Proof.入手下手证实Qed.证实停止Hint Resolve lem 将lem 减进auto 库证实战略：下级技法：证实即步伐：Definition half(n:nat):p:nat & n = 2*p +n = S(2*p). induction n.exists 0;left;auto.destruct IHn as x Hx | Hx.exists x;right;auto.exists (S x);left;auto.Require Import Arith.rewrite Hx; ring.Defined.Print sigT.Compute half 3.Check existT.Definition half(n: nat): nat := matchhalf n with existT p _ => p end.附录1：Ensemble 界说：Library Coq.Sets.EnsemblesSection Ensembles.Variable U : Type.Definition Ensemble := U > Prop.Definition In (A:Ensemble) (x:U) : Prop := A x.Definition Included (B C:Ensemble) : Prop := forall x:U, In B x > In C x.Inductive Empty_set : Ensemble :=.Inductive Full_set : Ensemble :=Full_intro : forall x:U, In Full_set x.NB: The following definition buildsin equality of elements in U as Leibniz equality.This may have to be changed if we replace U by a Setoid on U with its own equality eqs, with In_singleton: (y: U)(eqs x y) > (In (Singleton x) y).Inductive Singleton (x:U) : Ensemble :=In_singleton : In (Singleton x) x.Inductive Union (B C:Ensemble) : Ensemble :=| Union_introl : forall x:U, In B x > In (Union B C) x| Union_intror : forall x:U, In C x > In (Union B C) x.Definition Add (B:Ensemble) (x:U) : Ensemble := Union B (Singleton x).Inductive Intersection (B C:Ensemble) : Ensemble :=Intersection_intro :forall x:U, In B x > In C x > In (Intersection B C) x.Inductive Couple (x y:U) : Ensemble :=| Couple_l : In (Couple x y) x| Couple_r : In (Couple x y) y.Inductive Triple (x y z:U) : Ensemble :=| Triple_l : In (Triple x y z) x| Triple_m : In (Triple x y z) y| Triple_r : In (Triple x y z) z.Definition Complement (A:Ensemble) : Ensemble := fun x:U => In A x.Definition Setminus (B C:Ensemble) : Ensemble :=fun x:U => In B x / In C x.Definition Subtract (B:Ensemble) (x:U) : Ensemble := Setminus B (Singleton x). Inductive Disjoint (B C:Ensemble) : Prop :=Disjoint_intro : (forall x:U, In (Intersection B C) x) > Disjoint B C.Inductive Inhabited (B:Ensemble) : Prop :=Inhabited_intro : forall x:U, In B x > Inhabited B.Definition Strict_Included (B C:Ensemble) : Prop := Included B C / B Definition Same_set (B C:Ensemble) : Prop := Included B C / Included C B. Extensionality AxiomAxiom Extensionality_Ensembles : forall A B:Ensemble, Same_set A B > A = B. End Ensembles.Hint Unfold In Included Same_set Strict_Included Add Setminus Subtract: setsv62.Hint Resolve Union_introl Union_intror Intersection_intro In_singletonCouple_l Couple_r Triple_l Triple_m Triple_r Disjoint_intro Extensionality_Ensembles: sets v62.
