Coq中文手册

Coq Hand Book

CCNT Lab

Zhiling Luo

指令：

Require Import libs

Libs:

Arith 自然数数学库(默认)

ZArith 整数数学库

Logic 命题逻辑库(默认)

Bool 布尔库

Ensembles 集合库

Strings 字符串库

List 列表库

Reals 实数库

Open Scope lib_scope

lib_scope:

nat_scope 自然数数学库符(默认)

Z_scope 整数数学库符

String_scope 字符串库符

R_scope 实数库符

Section sec End sec

由 section 和 End 包围的是一个段，sec 为段名。

Example：

Section Loc. End

Loc.

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. Variable

husky: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 库

证明策略：

intros/intro 用于 goal 里面有 forall,~,P‐> intros P H0.

intros.

unfold 展开非递归函数 unfold is_ture.

unfold is_true in H.

rewrite H 将 H 的右边当作左边带入 goal

或者指定的目标 rewrite H. rewrite

H in H0.

rewrite <‐ H 将 H 的左边当作右边带入 goal

或指定目标 rewrite <‐ H. rewrite

<‐ H in H0.

exists X 向 goal 或指定的目标指定

exist x:T 的目标 exists X in H0.

exists X.

subst 在指定地方或 goal 里面删去可去的参数或者指定的参数 subst. subst i.

subst i in goal.

symmetry 换位，将 goal 的等号两边换位置，用于将 a=b 变成 b=a symmetry.

reflexivity 自反，用于证明 a=a reflexivity.

simpl 规约 goal 或者指定的目标 simpl.

simpl in H.

discriminate 从已知式子中导出矛盾 discriminate.

destruct 拆掉指定假设中的或和与，当

H 含 forall 时加上一个对象

p。 destruct H as [H1 H2].

destruct H as [H1 | H2].

destruct (H p).

split 拆分 goal 中间的与 split.

left 指证 goal 中间的与的左边 left.

right 指证 goal 中间的与的右边 right.

apply H 应用指定假设到 goal 或者指定位置 apply. apply

H in H0.

eapply H 自动选择参数应用指定假设 eapply H. omega 需要 omega 库，自动证明加法和不等式 omega.

generalize H 将 H 返回到 goal 中，产生

forall generalize H.

inversion H 指出 H 的构造子 inversion H.

induction n 在 n 上使用归纳法 induction n.

case n 将 goal 中的 n 分构造子讨论 case n.

auto 自动证明 auto.

auto with arith.

tauto 自动证明布尔逻辑命题 tauto.

assert 指定一个新的假设 assert (H:P‐>Q).

高级技法： 证明即程序：

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 := match

half n with existT p _ => p end.