Coq学习笔记（未完待续）

这篇文章来自《Coq in a Hurry》¹的总结。

表达式和逻辑公式

编写正确的公式

使用Check命令能查看公式的类型：

> Check True.
True : Prop

> Check 3.
3 : nat

a: A可以表示a的类型是A，或者a是A的证明。它可以位于表达式中，显式指明表达式类型。

常见的类型有Prop表示命题，nat表示自然数。复杂的类型可以通过逻辑联结词（/\、\/）和诸如加、乘、对(a, b)（其类型为A * B）等等创建。使用fun能创建λ表达式（其类型为A -> B，右结合）、forall和exists创建量词：

> Check (fun x:nat => x = 3).
fun x : nat => x = 3 : nat -> Prop

> Check (forall x:nat, x < 3 \/ (exists y: nat, x = y + 3)).
forall x : nat, x < 3 \/ (exists y : nat, x = y + 3) : Prop

使用let .. in可以给表达式一个临时的名字，注意到函数应用不需要括号。

> Check (let f := fun x => (x * 3,x) in f 3).
(let f := fun x : nat => (x * 3, x) in f 3 : nat * nat

有些符号被重载了，比如*既表示数字的乘法，又表示笛卡尔积类型。使用Locate命令可以找到符号背后的函数。

> Locate "_ <= _".

项是合法的需要遵守：

1. 语法正确
2. 类型正确

而Check命令不仅进行了上面的检查，还给出了表达式的类型。

对表达式求值

使用Compute可以对表达式求值。

用Coq编程

Coq中的程序用函数表示，简单的程序可以被Coq执行，复杂的可以用Extraction命令转换为其他编程语言的。

定义新的常量

使用Definition关键字可以定义常量：

> Definition example1 := fun x : nat => x*x+2*x+1.

上面的形式等价于：

> Definition example1 (x : nat) := x*x+2*x+1.

定义完后，就可以在诸如Check和Compute的命令中使用。使用Reset后面跟一个名字可以清除该名字。可以使用Print命令查看一个对象的定义。

布尔条件表达式

Coq内置了布尔（bool）值true和false。为了使用它，你需要导入Bool库。

> Require Import Bool.

布尔值可以使用if ... then ... else ...。后者接受一个模式返回符合的；而后者接受一系列的模式，返回都符合的。

使用自然数计算

需要使用Arith库进行自然数的计算。自然数有两种形式，一种是0，另一种是S p，其中p是一个自然数。可以使用match ... with ... end进行模式匹配。第一个子句的|可省略。

Definition is_zero (n:nat) :=
    match n with
        0 => true
    | S p => false
    end.

如果要使用递归，可以使用Fixpoint关键字。Fixpoint必须遵守一个约束叫structural recursion，即递归只能作用在初始参数（上面的p）上。这个约束确保计算是可终止的。递归函数可以有多个参数，这时候structural recursion必须在一个参数上是成立的。

Coq还支持深模式匹配，Coq会检查是否所有的模式都匹配了：

Fixpoint evenb n :=
    match n with
            0 => true
    |       1 => false
    | S (S p) => evenb p
    end.

使用列表计算

需要导入List库。如果要将几个元素放入列表中，需要使用::，它将左边的元素添加到右边列表的头，用nil表示空列表：

Check 1::2::3::nil.

注意nil需要上下文确定其具体类型。可以使用类型注解表示其类型。

Check (nil : list nat)

有一些预定义的列表函数：

• app，别名++：链接列表。
• map：对列表的每个元素做映射。

列表也可以模式匹配为nil和a::tl（a是一个元素，tl是剩余的列表）。同样也可以递归，递归只能作用在剩余的列表上。

命题和证明

找到已有的证明

Search后面跟标识符可以搜索已有的证明。SearchPattern后面跟一个模式表达式（使用_表示一个不完整的子表达式）。SearchRewrite与SearchPattern类似，只是寻找的一定是个相等的谓词。SearchAbout搜索所有的与某个符号相关的证明。

构建新的证明

构建证明的通常方式是“目标导向的证明”：

1. 使用Theorem或者Lemma开始一个定理。
2. Coq显示需要证明的命题，已经可以用于该证明的上下文（上下文在=====上方，目标在下方）。
3. 用户输入命令，分解目标。
4. Coq显示还需要证明的命题。
5. 回到3。

步骤3称为tactics。某些tactics减少了目标的数量。当所有目标都解决，证明就完成了，这时候可以输入Qed.命令，该命令保存了证明。一个简单的证明如下：

Lemma example2 : forall a b: Prop, a /\ b -> b /\ a.
Proof.
    intros a b H.
    split.
        destruct H as [H1 H2].
            exact H2.
        intuition.
Qed.

上下文中的内容一般是a: type或者H: formula的形式，我们称为假设，它表示我们现在有的事实。destruct H as [H1 H2]在H为两个命题的合取时可以使用。它的作用是创建两个新的假设，名字为H1和H2。下表包含了常见的tactics。

当你在处理假设时，可以用Hypothesis那一列；处理结论时用conclusion那列。

我们用exact H表示我们要证明的结论就在上下文中，assumption可以做到类似的效果。intuition可以用于自动证明。

当使用elim或者case，会将事实放在结论处，其目标会成为蕴含的前件。这些前件稍后可被intros引入。因此有destruct可以同时完成这两件事。

所有的以假设作为参数的tactics都可以以定理作为参数。

用基本tactics的另一个例子

（未完待续）