Coq 小技巧

我第一次听说 Coq 是在本科的时候。从那以后我就一直很想学 Coq，但是并不知道怎么开始。大部分的 Coq 教程都是在讲逻辑，我觉得并不是很有趣。

上个学期我选了 UW CSE505 这门课。Prof. Zach Tatlock 和 TA Talia Ringer 设计了一系列非常棒的作业来帮我们学习 Coq。在这个课里面，我们证明了一些更加实际的东西，包括一个简单的编程语言的解释器还有一个简单的正则表达式引擎。事实上，我发现我对在 Coq 里面写证明还蛮在行的（但是写规范就完全是另外一回事了），至少在做作业的时候我是这么觉得的。

如果你在自学 Coq，我推荐以下资源：

UW CSE505 的作业
Formal Reasoning About Programs 这本书是我们上课的教材。这本书很短，边距很大，空白很多，每一章附带了详细的 Coq 代码。这本书还自带了一个很好用的 Coq 库 frap。
Software Foundations 如果你真的对形式化验证很感兴趣的话。

我非常高兴我终于能把 Coq 从我的愿望单里面划掉了。不过我并不是形式化验证的狂热粉丝，我觉得我之后也不用用到 Coq。我决定趁我还没完全忘记 Coq，赶紧把我做作业时学会的 Coq 技巧写下来，万一以后哪天我又用到 Coq 了呢，希望也对读者有所帮助。

Tactics

虽然说我并不是很能理解 Coq 官方的文档，但是有问题的时候看看还是有帮助的：https://coq.inria.fr/refman/coq-tacindex.html.

`intros`

intros 从目标中按照顺序引入假设。每一次它会消耗 forall 里面的一个自由变量，或者是一个 -> 前面的命题（也就是前提条件）。举个例子：

Theorem Transform_transform:
  forall c1 c2,
    Transform c1 c2 ->
    transform c1 = c2.

intros c1 c2 H. 之后：

c1, c2 : cmd
H : Transform c1 c2
______________________________________(1/1)
transform c1 = c2

另外，你也可以用 intros. 来引入所有的假设，Coq 会自动给他们命名。

`simpl`

simpl. 能化简目标。 simpl in H. 化简假设 H. simpl in *. 化简所有的假设和目标。当你不知道证明下一步怎么走的时候，总是可以试试 simpl in *.，看有没有发生什么变化。

`simplify` (Frap Tactic)

simplify. 是 frap 库里面一个更强版本的 simpl in *.。我个人总是使用 simplify 来替代 simpl，如果有引入 frap 库的话。

`destruct`

假设 x 是一个归纳类型，当你 destruct x.，Coq 会为每一个构造函数生成一个小目标。换句话说，destruct 让你可以分类讨论所有可能的情况。

让我们先看一个简单的例子。假设我们有这么一个递归类型：

Inductive cmd :=
| Skip
| Assign (x : var) (e : arith)
| Sequence (c1 c2 : cmd)
| If (e : arith) (then_ else_ : cmd)
| While (e : arith) (body : cmd).

我们想要证明：

Theorem transform_Transform:
  forall c1 c2,
    transform c1 = c2 ->
    Transform c1 c2.

如果我们 destruct c2.，我们会看到 c2 被各个构造函数替换掉了:

5 subgoals
c1 : cmd
______________________________________(1/5)
transform c1 = Skip -> Transform c1 Skip
______________________________________(2/5)
transform c1 = (Assign x e) -> Transform c1 (Assign x e)
______________________________________(3/5)
transform c1 = (Sequence c2_1 c2_2) -> Transform c1 (Sequence c2_1 c2_2)
______________________________________(4/5)
transform c1 = (If e c2_1 c2_2) -> Transform c1 (If e c2_1 c2_2)
______________________________________(5/5)
transform c1 = (While e c2) -> Transform c1 (While e c2)

注意到，Coq 里面许多东西都是归纳类型，你可以用 destruct 来“打开”他们，比如这个例子：

H : exists a : Set, In a (wl ++ adjacent t g) /\ Reachable g a b

假设 H 告诉我们存在一个 a 能够使得后面的命题成立，但是我们如何把这个实例给取出来呢？如果我们关闭 Coq 的记号显示（notation display），我们可以看到 H 实际上是：

H : ex (fun a : Set => and (In a (app wl (adjacent t g))) (Reachable g a b))

然后如果你 Print ex.：

Inductive ex (A : Type) (P : forall _ : A, Prop) : Prop :=
    ex_intro : forall (x : A) (_ : P x), ex P

ex 也是一个归纳类型。所以说我们可以用 destruct H. 把这个实例取出来：

x : Set
H : In x (wl ++ adjacent t g) /\ Reachable g x b

现在我们有了这个实例，虽然说它叫做 x 而不是 a。然后我们现在怎么把 /\ 打开呢？再来一次 destruct H.：

x : Set
H : In x (wl ++ adjacent t g)
H1 : Reachable g x b

这是因为 and 也是一个归纳类型。你可以用 Print and. 验证一下:

Inductive and (A B : Prop) : Prop :=
| conj : A -> B -> A /\ B.

那 \/ 怎么样呢？Print or.：

Inductive or (A B : Prop) : Prop :=
| or_introl : A -> A \/ B
| or_intror : B -> A \/ B.

所以说你也一样可以用 destruct 打开一个 \/，然后它会变成两个小目标。这很合理，从逻辑上来说，当你知道 A \/ B 成立，你需要讨论两个情况：A 成立以及 B 成立.

`induction`

induction 是总重要的招数之一。你可以 induction 一个归纳类型（inductive type），会产生和这个归纳类型的构造函数数量一样多的小目标。如果构造函数里面用到了这个归纳类型本身，那么在归纳的过程中会产生相应的归纳假设。

一开始的时候，我把 induction 和数学归纳法搞混了。要用数学归纳法证明一个命题 P，你需要先证明一个基础步骤 P(0)，然后在 P(n) 成立的情况下证明一个递推步骤 P(n+1)。但是在 induction 里面没有“基础步骤”和“递推步骤”之分，甚至 induction 产生的小目标的数量都不一定等于2。

之后，我发现你可以把 induction 理解成数学归纳法的一种扩展。数学归纳法是作用在自然数上面的，而自然数是一种递归定义的归纳类型：

Inductive nat : Set :=
| O : nat
| S : nat -> nat.

所以说当你在 induction 一个 nat 的时候，你实际上就是在进行数学归纳法。另外一方面，你也可以把 induction 想成作用在结构上面。

先举一个例子：

Lemma len_repeat:
  forall s n,
    String.length (repeat s n) = n * String.length s.

在 induction 一个变量的时候，Coq intros 直到这个变量出现在假设中。所以说我们可以直接 induction n.，这等同于 intros s n. induction n.。

s : var
______________________________________(1/2)
String.length (repeat s 0) = 0 * String.length s
______________________________________(2/2)
String.length (repeat s (S n)) = S n * String.length s

你可以看到这里变成了两个小目标。一个是 0，另一个是 S n。注意到在第一个小目标里面没有归纳假设，因为 O 不是递归定义的。完成了第一个小目标之后，我们可以看到第二个小目标：

s : var
n : nat
IHn : String.length (repeat s n) = n * String.length s
______________________________________(1/1)
String.length (repeat s (S n)) = S n * String.length s

因为 S 是递归定义的，所以这里就出现了归纳假设 IHn。

让我们再看另一个例子：

Inductive Transform  : cmd -> cmd -> Prop :=
| TransformSkip: 
    Transform Skip Skip
| TransformAssign: forall v e,
    Transform (Assign v e) (Assign v e)
| TransformSeq: forall c1 c2 tc1 tc2,
    Transform c1 tc1 ->
    Transform c2 tc2 ->
    Transform (Sequence c1 c2) (Sequence tc1 tc2)
| TransformIf: forall e then_ else_ tthen telse,
    Transform then_ tthen ->
    Transform else_ telse ->
    Transform (If e then_ else_) (If e telse tthen)
| TransformWhile: forall e body tbody,
    Transform body tbody ->
    Transform (While e body) (While e tbody).

Theorem Transform_transform:
  forall c1 c2,
    Transform c1 c2 ->
    transform c1 = c2.

我们可以用 induction 1. 来开始证明。induction n 会不断地 intros 直到第 n 个命题已经引入到了假设里面，然后对这个命题进行归纳。在这个例子里面，induction 1. 和 intros c1 c2 H. induction H. 是一样的效果。然后我们可以看到：

5 subgoals
______________________________________(1/5)
transform Skip = Skip
______________________________________(2/5)
transform (Assign v e) = Assign v e
______________________________________(3/5)
transform (Sequence c1 c2) = Sequence tc1 tc2
______________________________________(4/5)
transform (If e then_ else_) = If e telse tthen
______________________________________(5/5)
transform (While e body) = While e tbody

对于每一个 Transform 的构造函数，我们都有一个对应的小目标。让我们看一下第四个小目标：

e : arith
then_, else_, tthen, telse : cmd
H : Transform then_ tthen
H0 : Transform else_ telse
IHTransform1 : transform then_ = tthen
IHTransform2 : transform else_ = telse
______________________________________(1/1)
transform (If e then_ else_) = If e telse tthen

我们可以看到这里有两个归纳假设（IHTransform1 和 IHTransform2），因为构造函数 TransformIf 有两个递归定义的前提条件。

`inversion`

在我看来，inversion 是最常用最强大的招数之一。我对 inversion H. 的理解是，它让 Coq 找出来要让 H 成立还有哪些事情要成立。它有可能会添加新的假设，也可能会添加新的小目标。

一个常见的用途是说明一个等式两边的构造函数里面的对应的部分是相同的。你也可以把 inversion 理解成“打开盒子”。举个例子，这里 If 是一个归纳类型的构造函数：

H : If e (transform c1_2) (transform c1_1) = If e0 c2_1 c2_2
______________________________________(1/1)
Transform (If e c1_1 c1_2) (If e0 c2_1 c2_2)

在 inversion H. 之后变成:

H : If e (transform c1_2) (transform c1_1) = If e0 c2_1 c2_2
H1 : e = e0
H2 : transform c1_2 = c2_1
H3 : transform c1_1 = c2_2
______________________________________(1/1)
Transform (If e0 c1_1 c1_2) (If e0 (transform c1_2) (transform c1_1))

Coq 为我们找到了三个非常有用的关系。顺带一提，inversion 和 subst 搭配使用效果更佳，因为 subst 可以把 inversion 发现的等式带入并化简，让假设看起来更加清楚。另外，如果在 inversion H; subst. 之后你发现假设列表里面唯一的变化就是多了一条和 H 一模一样的假设，那么你就知道说这个时候 inversion H. 完全没有作用。

实际上，= 没有任何特殊之处，因为它只不过是一个叫做 eq 的归纳类型。让我们看看一个稍微复杂一点的例子：

Inductive Transform  : cmd -> cmd -> Prop :=
| TransformSkip: 
    Transform Skip Skip
| TransformSeq: forall c1 c2 tc1 tc2,
    Transform c1 tc1 ->
    Transform c2 tc2 ->
    Transform (Sequence c1 c2) (Sequence tc1 tc2)
| TransformIf: forall e then_ else_ tthen telse,
    Transform then_ tthen ->
    Transform else_ telse ->
    Transform (If e then_ else_) (If e telse tthen)
(* Other constructors omitted *).
    
Inductive step_buggy : valuation * cmd -> valuation * cmd -> Prop :=
| StepBuggySeq1 : forall v c1 c2 v' c1',
    step_buggy (v, c1) (v', c1')
    -> step_buggy (v, Sequence c1 c2) (v', Sequence c1' c2)
| StepBuggySeq2 : forall v c2,
    step_buggy (v, Sequence Skip c2) (v, c2)
(* Other constructors omitted *).

假设我们有：

1 subgoal
v : valuation
c2, c1', c2' : cmd
H : Transform (Sequence Skip c2) c1'
H0 : step_buggy (v, c1') (v, c2')
______________________________________(1/1)
Transform c2 c2'

在 inversion H; subst. 之后:

v : valuation
c2, c2', tc1, tc2 : cmd
H : Transform (Sequence Skip c2) (Sequence tc1 tc2)
H0 : step_buggy (v, (Sequence tc1 tc2)) (v, c2')
H3 : Transform Skip tc1
H5 : Transform c2 tc2
______________________________________(1/1)
Transform c2 c2'

让我来解释一下发生了什么。H 匹配上了 TransformSeq 构造函数，所以我们多了两个假设，也就是 TransformSeq 的两个前提条件（H3 和 H5）。从这个构造函数里面，我们还知道了 c1' 一定也是一个 Sequence，所以说这里 c1' 被替换成了 (Sequence tc1 tc2)。现在，让我们进入下一步，inversion H3; subst.：

v : valuation
c2, c2', tc2 : cmd
H : Transform (Sequence Skip c2) (Sequence Skip tc2)
H0 : step_buggy (v, (Sequence Skip tc2)) (v, c2')
H3 : Transform Skip Skip
H5 : Transform c2 tc2
______________________________________(1/1)
Transform c2 c2'

我们可以看到 tc1 被替换成了 Skip，因为我们知道 H3 : Transform Skip tc1 成立，而唯一能匹配的就是 TransformSkip 构造函数，从这里面我们可以知道 tc1 就是 Skip。现在让我们 inversion H0; subst.：

v : valuation
c2, tc2, c1' : cmd
H : Transform (Sequence Skip c2) (Sequence Skip tc2)
H0 : step_buggy (v, (Sequence Skip tc2)) (v, (Sequence c1' tc2))
H2 : step_buggy (v, Skip) (v, c1')
H3 : Transform Skip Skip
H5 : Transform c2 tc2
______________________________________(1/2)
Transform c2 (Sequence c1' tc2)
______________________________________(2/2)
Transform c2 c2'

因为这里有两个 step_buggy 构造函数能匹配上 H0，所以这两个情况我们都需要讨论，所以说这里产生了两个小目标。这种分类讨论的感觉就有点像 destruct。

那如果一个构造函数都匹配不上呢？比方说下面这个例子：

H : None = Some true

这个时候 inversion H. 就能结束证明，因为这种情况根本不可能出现。

`f_equal`

当目标是一个归纳类型的构造函数等于同一个构造函数的时候，你可以用 f_equal. 转换成证明其中对应的部分是相同的。比方说，

v : valuation
e : arith
body, tbody : cmd
______________________________________(1/1)
Sequence (transform body) (While e (transform body)) =
Sequence tbody            (While e tbody)

在 f_equal. 之后会变成：

v : valuation
e : arith
body, tbody : cmd
______________________________________(1/2)
transform body = tbody
______________________________________(2/2)
While e (transform body) = While e tbody

显然，如果你在第二个小目标里面运行 f_equal.，它会进一步变成：

______________________________________(1/1)
transform body = tbody

注意到，尽管 f_equal 可以把目标转化成更小的问题，但是在使用的时候你一定要确信其中对应的部分是相等的，不然你会产生错误的结论，比方说这个例子：

s : var
______________________________________(1/1)
String.length (reverse s) = String.length s

在这个例子里面，我们想要证明一个字符串翻转过来之后的长度和原来的长度是一样的。如果我们用 f_equal.：

s : var
______________________________________(1/1)
reverse s = s

目标变成了证明一个任意的字符串翻转过来和原字符串是一样的，这完全讲不通。

`assumption`

如果目标已经出现在假设里面了，你可以用 assumption. 来结束证明。另外，你也可以使用 auto 或者 exact。

`constructor`

当目标是一个归纳类型的时候，结束证明的方法一般来说是用构造函数。constructor. 会按照定义的顺序逐个尝试这个归纳类型的构造函数，直到第一个匹配上的为止。因为 constructor. 用的是第一个匹配上的构造函数，所以并不一定是正确的，如果遇到了这种情况，你需要使用 apply。

举一个简单的例子，假设我们有这么一个归纳类型：

Inductive eval_unop : op1 -> val -> val -> Prop :=
| eval_neg : forall i,
    eval_unop Oneg (Vint i) (Vint (Z.opp i))
| eval_not : forall b,
    eval_unop Onot (Vbool b) (Vbool (negb b)).

现在我们有：

b : bool
v' : val
______________________________________(1/1)
eval_unop Onot (Vbool b) (Vbool (negb b))

现在我们用 consturctor.， Coq 会匹配上第二个构造函数 eval_not。

`apply`

apply 也可以用来应用构造函数。实际上，你可以 apply 任何定理，你可以认为构造函数就是一种定理。比方说，在前面 constructor 的例子里面，你也可以 apply eval_not. 来代替 constructor.。

让我来用一个稍微复杂一点的例子来讲解 apply，假设我们有这么一个归纳类型和一个定理：

Inductive eval_e (s : store) (h : heap) :
  expr -> val -> Prop :=
(* Omitted *).

Inductive eval_s (env : env) :
  store -> heap -> stmt -> store -> heap -> Prop :=
| eval_ifelse_t :
    forall s h e p1 p2 s' h',
      eval_e s h e (Vbool true)                  ->
      eval_s  env  s h p1                  s' h' ->
      eval_s  env  s h (Sifelse e p1 p2)   s' h'
| eval_ifelse_f :
    forall s h e p1 p2 s' h',
      eval_e s h e (Vbool false)                 ->
      eval_s  env  s h p2                  s' h' ->
      eval_s  env  s h (Sifelse e p1 p2)   s' h'
| eval_seq :
    forall s1 h1 p1 s2 h2 p2 s3 h3,
      eval_s  env  s1 h1 p1             s2 h2 ->
      eval_s  env  s2 h2 p2             s3 h3 ->
      eval_s  env  s1 h1 (Sseq p1 p2)   s3 h3.

Lemma interp_e_eval_e :
  forall s h e v,
    interp_e s h e = Some v ->
    eval_e s h e v.

现在我们有：

IHfuel : forall (env : env) (s : store) (h : heap) (p : stmt) (s' : store) (h' : heap),
         interp_s fuel env s h p = Some (s', h') ->
         eval_s env s h p s' h'
Heqo : interp_e s h e = Some (Vbool true)
H : interp_s fuel env s h p1 = Some (s', h')
______________________________________(1/1)
eval_s env s h (Sifelse e p1 p2) s' h'

在构造函数里面有一些 ->，如果你是第一次接触 Coq 的话，这看起来很吓人，不过一旦你理解了 apply 和 constructor 的原理，事情就很容易了。

在这个例子里面，我们想要用构造函数 eval_ifelse_t。为什么呢？首先，看一下目标，这是一个 eval_s 所以我们要找找 eval_s 的构造函数。我们怎么知道要的不是构造函数 eval_seq 呢？因为我们的目标从结构上匹配不上 eval_seq。但是 eval_ifelse_t 和 eval_ifelse_f 的结论有完全一样的形式 eval_s env s h (Sifelse e p1 p2) s' h'，要用哪个呢，以及要怎么处理这些前提条件呢？

从逻辑上来说，要使用 eval_ifelse_t 的话，我们需要证明它的前提条件。实际上，如果你 constructor. 或者 apply eval_ifelse_t.，就会变成两个小目标，这符合逻辑，因为这里有两个前提条件：

______________________________________(1/2)
eval_e s h e (Vbool true)
______________________________________(2/2)
eval_s env s h p1 s' h'

其实第二个小目标是显然的，你可以用 apply IHfuel. assumption. 解决掉它。让我再讲解一遍这个显然的情况，加深对 apply 的理解。IHfuel 的最后一个命题的形式（eval_s env s h p s' h'）能匹配上第二个小目标的形式（eval_s env s h p1 s' h'）。注意到在 IHfuel 里面有一个 forall，在 apply IHfuel. 的时候，Coq 能自己搞清楚这些自由变量是什么。所以说第二个小目标变成了 interp_s fuel env s h p1 = Some (s', h')，这就是 Heqo.

我说第二个小目标是显然的，因为你也可以 auto. 而不用 apply IHfuel. assumption.。甚至更简单地，如果你一开始就 constructor; auto. 或者 apply eval_ifelse_t; auto.，第二个小目标根本就不会出现。

至于第一个小目标，我们可以用 apply interp_e_eval_e. assumption. 来完成证明。想想这是为什么。其实是一样的。

除了转化目标以外，apply 也可以作用在假设上面，只要你加上 in H。比方说：

Theorem Transform_transform:
  forall c1 c2,
    Transform c1 c2 ->
    transform c1 = c2.

现在我们有：

H : Transform (Assign x e) c1'

apply Transform_transform in H. 可以把 H 变成：

H : transform (Assign x e) = c1'

`exists`

证明全称量词的一个方法是直接告诉 Coq 这些变量到底是什么。举个例子：

H3 : String a s1 =~ EmptySet
H4 : s2 =~ re1
H0 : String a s1 ++ s2 = String a (s1 ++ s2)
______________________________________(1/1)
exists s0 s3 : string, s1 ++ s2 = s0 ++ s3 /\
  (String a s0 =~ EmptySet) /\ s3 =~ re1

我们可以告诉 Coq exists s1, s2.：

H3 : String a s1 =~ EmptySet
H4 : s2 =~ re1
H0 : String a s1 ++ s2 = String a (s1 ++ s2)
______________________________________(1/1)
s1 ++ s2 = s1 ++ s2 /\ (String a s1 =~ EmptySet) /\ s2 =~ re1

然后一个 first_order 就能结束证明。

`reflexivity`

正如这个名字本身的含义，当目标类似 x = x 的形式，使用 reflexivity. 就能结束证明。

`discriminate`

如果有一个假设是一个等式，但是等式两边结构不同，可以使用 discriminate. 来结束证明，无论要证明的结论是什么，因为逻辑上一个错误的假设可以推导出任何结论。举个例子，

H : None = Some v'
______________________________________(1/1)
eval_unop Oneg (Vbool b) v'

discriminate. 就能结束证明。

再来一个例子：

c1_1, c1_2, c2 : cmd
H : Sequence (transform c1_1) (transform c1_2) = c2
______________________________________(1/1)
Transform (Sequence c1_1 c1_2) c2

这里 cmd 是一个归纳类型，Sequence 是其中的一个构造函数。显然，c2 也必须是一个 Sequence. 如果你运行 destruct c2; try discriminate.：

c1_1, c1_2, c2_1, c2_2 : cmd
H : Sequence (transform c1_1) (transform c1_2) = Sequence c2_1 c2_2
______________________________________(1/1)
Transform (Sequence c1_1 c1_2) (Sequence c2_1 c2_2)

这就符合我们的预期。这个效果类似于 inversion H; subst.。

`congruence`

我发现 congruence 好像是一个更强版本的 discriminate。前面 discriminate 的两个例子都可以用 congruence. 替代。但是 congruence 可以做更多的事情，比方说：

H : x1 <> x1
______________________________________(1/1)
Some t2 = Some t1

在这个例子里面，congruence. 可以发现 H 不成立，所以证明就结束了，但是 discriminate. 就不能。

`auto`

我一开始的时候以为 auto 是一个非常强力的招数，但是后来我发现其实它只能解决一些简单的情况。我对它的理解就是把它当做自动地尝试 assumptions、 reflexivity、 congruence，以及尝试应用假设里面的定理。

`econstructor` / `eapply` / `eauto` / `edestruct` / `eexists`

带有 e 版本的这些招数做的事情和不带 e 的版本一样，只不过当找不到某些变量的时候，带 e 的版本会引入像未知数一样的变量，而不是直接失败。而后随着证明的推进，Coq 有可能会自动地搞清楚这些引入的变量是什么。

`rewrite`

如果你有一个等式，你可以用它来转化其他假设或者目标。rewrite H. 把等式 H 左边的表达式替换成等式右边的。如果要反过来，你可以使用 rewrite <- H.。如果你想要改变一个假设 H1 而不是目标，使用 rewrite H in H1.。如果你想要改变所有的假设和目标，使用 in *.

举个例子：

H1 : length h = length ht
______________________________________(1/1)
length h < length (snoc ht t0)

在 rewrite H1. 之后：

H1 : length h = length ht
______________________________________(1/1)
length ht < length (snoc ht t0)

再举一个例子：

H1 : length h = length ht
H8 : nth (length ht) (snoc ht t0) TBool = t0

在 rewrite <-H1 in H8. 之后：

H1 : length h = length ht
H8 : nth (length h) (snoc ht t0) TBool = t0

另外，如果你不确定应该用哪边替换另一边，就带和不带 <- 两个都试一下，总有一个是对的。

`unfold`

有时候一个命题里面包含了抽象的定义，要把这层抽象去掉，可以用 unfold。举个例子：

1 subgoal
______________________________________(1/1)
derives derive

面对这个目标，我们并没有任何的招式可用。但是在 unfold derives. 之后：

______________________________________(1/1)
forall (a : ascii) (re : reg_exp), is_der re a (derive a re)

现在看来就好多了，我们可以进一步 unfold is_der.：

______________________________________(1/1)
forall (a : ascii) (re : reg_exp) (s : string),
String a s =~ re <-> s =~ derive a re

现在我们就可以对它进行变换了（intros. split.）。

和 rewrite 类似, unfold 默认应用到目标上。要应用到一个假设 H 上，使用 in H。要应用到所有假设和目标，用 in *。

`specialize`

如果有个假设以 forall 开头，你可以用 specialize 来代入这些自由变量。

如果有个假设是若干个命题用 -> 连接起来的，而这些前提条件又正好都在你的假设里面，那你就可以用 specialize 把这个假设里面的这些前提条件去掉。

举个例子：

IHstep : forall c1' : cmd,
         c1' = c1' ->
         Transform c1 c1' ->
         exists c2' : cmd, step_buggy (v, c1') (v', c2')
H3 : Transform c1 tc1

在 specialize (IHstep tc1). 之后：

IHstep : tc1 = tc1 ->
         Transform c1 tc1 ->
         exists c2' : cmd, step_buggy (v, tc1) (v', c2')
H3 : Transform c1 tc1

如果你转而使用 specialize (IHstep tc1 (eq_refl tc1) H3). 就会有如下结果：

IHstep : exists c2' : cmd, step_buggy (v, tc1) (v', c2')
H3 : Transform c1 tc1

`pose proof`

pose proof 可以做 specialize 能做的事情，但有一点点不同。pose proof 会添加一个新的假设，而 specialize 则是原地修改原来假设。

因为 pose proof 能够添加新的假设，所以它可以做更多的事情。特别地，你可以使用一个引理来添加一个假设。

下面是两个例子：

pose proof (IHstep tc1 (eq_refl tc1) H3).
pose proof (step_step_buggy p1 p2 H c1' H0).

`split`

如果目标是若干个命题 /\ 连起来的，也就是一个和取范式，那你可以使用 split. 把它们拆开变成若干个小目标。

如果目标是一个当且仅当 iff，你也可以使用 split. 来把它拆成两个方向。

`left` / `right`

另外一方面，如果目标是一个析取范式，使用 left. 或者 right. 来选择你要证明哪一边。

`exact`

如果你的目标已经在假设里面了，你可以用 exact 来结束证明。另外，你也可以用 exact 来替代 pose proof 和 assumption 的组合。

两个例子：

exact H7.
exact (ReachRefl g b).

`assert`

assert 可以往假设里面添加一个命题，当然你要证明它。assert P. 会产生两个小目标：一个是给定当前已知的假设，证明 P；另一个是给定当前已知的假设和 P，证明原来的目标。

这么做的动机可能是因为你想要复制一份现有的假设，因为你后面打算对它进行修改。还有一个常见的情况就是你看出来一些假设是成立的，但是 Coq 没有。

几个例子：

assert (H8 := Heqo0).
assert (a < length h); try omega.
assert ("" = "" ++ ""). equality.
assert (~ free e1 x).

`first_order`

first_order 可以用来打开假设和目标中的 /\、\/、->、<-> 以及很多其他东西。

举个例子：

H : ("" =~ re1) /\ String a s =~ re2 \/
    (exists s0 s1 : string, s = s0 ++ s1 /\
    (String a s0 =~ re1) /\ s1 =~ re2)
H0 : "" =~ re1 <-> true = true
______________________________________(1/1)
s =~ Union (derive a re2) (App (derive a re1) re2)

first_order 会把复杂的 H and H0 打开。因为 H 里面有一个 \/，所以会变成两个小目标：

H1, H : "" =~ re1
H2 : String a s =~ re2
H0 : true = true
______________________________________(1/1)
s =~ Union (derive a re2) (App (derive a re1) re2)

以及

H1 : "" =~ re1
x, x0 : string
H : s = x ++ x0
H2 : String a x =~ re1
H3 : x0 =~ re2
H0 : true = true
______________________________________(1/1)
s =~ Union (derive a re2) (App (derive a re1) re2)

再举一个例子：

H4 : heap_typ_extends x ht /\ typed E0 x e' t0 /\ heap_typed x h'
______________________________________(1/1)
heap_typ_extends x ht /\ typed E0 x (ref e') (TRef t0) /\ heap_typed x h'

在 first_order 之后会变成：

H4 : heap_typ_extends x ht
H7 : typed E0 x e' t0
H8 : heap_typed x h'
______________________________________(1/1)
typed E0 x (ref e') (TRef t0)

尽管原先的目标由三个命题组成，但是 first_order 之后依然只有一个目标而不是三个，这是因为另外两个命题已经在假设 H4 里面了。顺带一提，first_order 会进一步把 heap_typed 的前提条件拆出来，但是我这里为了简单就假装没有发生。

`admit`

在有多个小目标的情况下，有时候你想要跳过其中的几个小目标。这可能是因为你暂时不知道怎么证明；有可能是因为你觉得这太简单现在不想证；也有可能你不确定现在走的这条路对不对，想要先看一眼后面的其他几个小目标。

这时候，你可以用 admit. 来跳过当前的小目标。当然了，一旦你有了一个 admit.，你这个证明就不能 Qed.，你只能 Admitted.

`symmetry`

如果目标是一个等式，而且你想要翻转它，你可以使用 symmetry.。举个例子：

______________________________________(1/1)
env2 x = Some t

在 symmetry 之后：

______________________________________(1/1)
Some t = env2 x

`revert`

revert 可以把你之前 intros 引入的假设放回去。为什么放回去？因为有时候你需要把归纳假设变得更强一些。比方说：

Lemma extends_lookup :
  forall h h' a,
    a < length h ->
    heap_typ_extends h' h ->
    lookup_typ h' a = lookup_typ h a.

如果我们直接 induction a; intros.，第二个小目标会是这样的：

h : list typ
h' : heap_typ
a : nat
IHa : a < length h ->
      heap_typ_extends h' h ->
      lookup_typ h' a = lookup_typ h a
H : S a < length h
H0 : heap_typ_extends h' h
______________________________________(1/1)
lookup_typ h' (S a) = lookup_typ h (S a)

然而，如果我们 intros h h' a. revert h h'. induction a; intros.，我们的第二个小目标会变成这样：

a : nat
IHa : forall (h : list typ) (h' : heap_typ),
      a < length h ->
      heap_typ_extends h' h ->
      lookup_typ h' a = lookup_typ h a
h : list typ
h' : heap_typ
H : S a < length h
H0 : heap_typ_extends h' h
______________________________________(1/1)
lookup_typ h' (S a) = lookup_typ h (S a)

可以看到，后面这个版本里面的归纳假设 IHa 比没有 revert 的那个版本的更强。如果不 revert 的话，IHa 就不足以证明这个命题（我当时浪费了很长时间在这个上面）。

所以怎么知道要不要 revert 呢？我觉得我们可以先想简单一点，不要 revert。当你发现你的归纳假设不够强之后，再来想想 revert。

`remember`

我遇到的关于 induction 的另一个问题是这样的：

a : ascii
s : string
re : reg_exp
H : String a s =~ Star re
______________________________________(1/1)
exists s0 s1 : string, s = s0 ++ s1 /\ (String a s0 =~ re) /\ s1 =~ Star re

这里 =~ 只是一个归纳类型的记号，x =~ y 的意思是 exp_match x y。尽管直觉上我们知道我们需要对 H 进行归纳，但如果我们直接 induction H，我们会得到一大堆无法证明的东西：

8 subgoals
a : ascii
s : string
re : reg_exp
______________________________________(1/8)
exists s0 s1 : string, s = s0 ++ s1 /\ (String a s0 =~ re) /\ s1 =~ EmptyStr
______________________________________(2/8)
exists s0 s1 : string, s = s0 ++ s1 /\ (String a s0 =~ re) /\ s1 =~ Char x
______________________________________(3/8)
exists s0 s1 : string, s = s0 ++ s1 /\ (String a s0 =~ re) /\ s1 =~ Dot
______________________________________(4/8)
exists s0 s3 : string, s = s0 ++ s3 /\ (String a s0 =~ re) /\ s3 =~ App re1 re2
______________________________________(5/8)
exists s1 s2 : string, s = s1 ++ s2 /\ (String a s1 =~ re) /\ s2 =~ Union re1 re2
______________________________________(6/8)
exists s1 s2 : string, s = s1 ++ s2 /\ (String a s1 =~ re) /\ s2 =~ Union re1 re2
______________________________________(7/8)
exists s0 s1 : string, s = s0 ++ s1 /\ (String a s0 =~ re) /\ s1 =~ Star re0
______________________________________(8/8)
exists s1 s2 : string, s = s1 ++ s2 /\ (String a s1 =~ re) /\ s2 =~ Star re0

我听说这是因为当构造函数的参数不是变量的时候，induction 就会表现得很糟糕。这个例子里面 String a s and Star re 都是表达式，不是变量。

在这种情况下，我们可以使用 remember (String a s). remember (Star re). 来把这两个表达式替换成变量：

a : ascii
s : string
re : reg_exp
s0 : string
Heqs0 : s0 = String a s
r : reg_exp
Heqr : r = Star re
H : s0 =~ r
______________________________________(1/1)
exists s1 s2 : string, s = s1 ++ s2 /\ (String a s1 =~ re) /\ s2 =~ r

现在我们就可以 induction H; try discriminate.，现在就只剩下一个可以证明的目标了：

a : ascii
s : string
re : reg_exp
s0, sk : string
Heqs0 : sk ++ s0 = String a s
re0 : reg_exp
Heqr : Star re0 = Star re
H : s0 =~ Star re0
H0 : sk =~ re0
IHexp_match1 : s0 = String a s ->
               Star re0 = Star re ->
               exists s0 s1 : string, s = s0 ++ s1 /\ (String a s0 =~ re) /\ s1 =~ Star re0
IHexp_match2 : sk = String a s ->
               re0 = Star re ->
               exists s0 s1 : string, s = s0 ++ s1 /\ (String a s0 =~ re) /\ s1 =~ re0
______________________________________(1/1)
exists s1 s2 : string, s = s1 ++ s2 /\ (String a s1 =~ re) /\ s2 =~ Star re0

`induct` (Frap Tactic)

induct 是 frap 库里面一个更强版本的 induction。你不需要使用 remember，而且甚至可以得到更强的结论。比如上面的例子，如果我们直接 induct H.，我们就会有：

re : reg_exp
s0, sk : string
H : s0 =~ Star re
H0 : sk =~ re
IHexp_match1 : forall (a : ascii) (s : string) (re0 : reg_exp),
               s0 = String a s ->
               Star re = Star re0 ->
               exists s0 s1 : string, s = s0 ++ s1 /\ (String a s0 =~ re0) /\ s1 =~ Star re0
IHexp_match2 : forall (a : ascii) (s : string) (re0 : reg_exp),
               sk = String a s ->
               re = Star re0 ->
               exists s0 s1 : string, s = s0 ++ s1 /\ (String a s0 =~ re0) /\ s1 =~ Star re0
a : ascii
s : string
x : sk ++ s0 = String a s
______________________________________(1/1)
exists s1 s2 : string, s = s1 ++ s2 /\ (String a s1 =~ re) /\ s2 =~ Star re

这里的归纳假设比原来更强了。所以说如果有可能的话，我都会使用 induct 来替代 induction。

Vernacular Commands

`Print`

你可以用 Print 来检查定义。比方说 Print or.：

Inductive or (A B : Prop) : Prop :=
| or_introl : A -> A \/ B
| or_intror : B -> A \/ B.

`Search`

要想找到一个你想要的 Coq 内置的定理是很难的。有一次我遇到了一个情况，我需要翻转一个不等于关系：

H1 : x1 <> x2
H5 : x2 <> x1 -> ~ free e1 x2

虽然说这个对人类来说非常的显然，但是对 Coq 来说并不是。后来，我发现，只要我知道怎么表达我需要的定理，我就可以用 Search 来找到它。在这个例子里面，我想要的定理是这样的：

Search (forall a b, a <> b -> b <> a).

然后 Coq 就会神奇般地告诉我：

not_eq_sym: forall (A : Type) (x y : A), x <> y -> y <> x

再举一个我遇到的情况：

IHtyped : E0 = E0 ->
          heap_typed ht h ->
          (exists (e' : expr) (h' : heap), h; e ==> h'; e') \/ isValue e

我怎么才能告诉 Coq 所有东西都会等于自身呢？

Search (forall x, x = x).

于是我知道了：

eq_refl: forall (A : Type) (x : A), x = x

不过有时候你不确定怎么表达一个定理（比方说，我就不知道怎么表达“x = y 和 x <> y 两者必有一个成立”），在这种情况下，你可以尝试搜索名字，比方说 Search "eq".。Coq 会告诉你所有沾有 eq 两字的定理，然后你就可以一条条地看过去。

Tricks

对什么进行归纳？

归纳一般来说会反映定义。比方说：

Lemma len_app_plus:
  forall s1 s2,
    String.length (s1 ++ s2) = String.length s1 + String.length s2.

要证明 len_app_plus ，就对 s1 进行归纳，因为 String.length 在每次迭代中会消耗字符串的第一个字符。当你对 s1 进行归纳的时候，第二个情况会是 s1 = String ch s，也就是一个字符后面跟着一个字符串，这就对应了 String.length 的定义，所以说我们就可以应用归纳假设。

再举一个例子：

Lemma len_repeat:
  forall s n,
    String.length (repeat s n) = n * String.length s.

类似地，要证明 len_repeat，我们就要对 n 进行归纳，因为 repeat 是定义在 n 上的一个递归。

缩进和子弹点

我不确定 Coq 社区是如何看待缩进的，但是我来自一个很强的编程背景，所以我就会希望我的证明也能有缩进来反映证明的结构。

Coq 会忽略空白字符和空行，但是 Coq 提供了子弹点来区分不同的小目标：+、-、*、以上符号的重复（++、***、……）以及一对 {}。所以你可以这么写证明：

Proof.
tactic.             (* become two subgoals after this *)
+ tactic.           (* enter "+", level 1, focus only one subgoal *)
  tactic.           (* become three subgoals after this *)
  - tactic.         (* enter "-", level 2, focus only one subgoal, and prove it *)
  - tactic.         (* focus another level 2 subgoal, and prove it *)
  - tactic.         (* focus another L2 subgoal, become two subgoals after this *)
    * tactic.       (* enter "*", level 3, focus only one subgoal *)
      tactic.       (* become two subgoals after this *)
      { tactic.     (* enter "{}", level 4, focus only one subgoal *)
        tactic.     (* become two subgoals after this *)
        - tactic.   (* enter "-" inside "{}", level 5, focus only one subgoal *)
          tactic.
          + tactic. (* level 6 *)
          + tactic.
        - tactic. } (* prove another "-" inside "{}" and finish the first "{}" *)
      { tactic.     (* enter another "{}" subgoal *)
        tactic. }   (* finish the subgoal *)
    * tactic.
+ tactic.           (* come back to the very first level *)
Qed.

虽然说不用子弹点也能完成证明，但是我发现子弹点可以帮助我们追踪证明的结构。在你进入了一个子弹点之后，目标就会变成只有一个。在你结束了这个小目标之后，Coq 会告诉你还有多少这个级别的小目标要证。

另外，我个人喜欢避免在简单的情况分叉，不然的话这个证明就会看起来往一边偏：

+ tactic.
+ tactic.
  - tactic.
  - tactic.
    * tactic.
    * tactic.
      ++ tactic.
      ++ tactic.
         ** tactic.
         ** tactic.
            -- tactic.
            -- tactic.
               { tactic. }
               { tactic.
                 + tactic.
                 + tactic.
                   - tactic.
                   - tactic. }

要避免这种无意义的分叉有若干种办法：

如果有若干个情况，但是只有一个是有意义的
- 用 ; 和 try，比方说 destruct c2; try discriminate.
如果恰好只有两个情况
- 如果显然的情况是在第一个，那就直接证明，不要用子弹点
- 如果显然的情况是在第二个，可以用 2: 跳到第二个情况，比方说 destruct s2. 2: inversion x. 还有 cases (ascii_dec a0 a0). 2: congruence.

在一行里面写多个招式

我发现把紧密相关的几句话写在一行里面实际上会让证明看起来更清楚。比方说：

inversion H. subst.
cases (ascii_dec a0 a0). 2: congruence.
econstructor; eauto.

看起来就比下面这个好：

inversion H.
subst.
cases (ascii_dec a0 a0).
2: congruence.
econstructor.
eauto.

尤其是当证明很长、子弹点很多的时候。

向前证明和向后证明

有两种证明的风格，向前和向后。向前证明就是一直加入假设，直到目标已经在假设里面了。向后证明就是一直对目标进行变换，直到目标已经在假设里面了。

一般来说这两者会混着来，因为有时候 pose proof 更容易，有时候 apply 定理更容易，或者用 e 系列的招数让 Coq 自动把问题解决。

显示记号

一开始看到 Coq 里面奇奇怪怪的符号的时候非常吓人，但其实他们一般来说就只是记号（notation）而已，并不是什么特殊的东西，你甚至可以为你自己的归纳类型添加记号。

但是当记号妨碍你理解的时候，你可以选择不显示它们。在 CoqIDE 里面，这个选项是在 View / Display notations。

FAQ

已知 `Some x = Some y`，怎么变成 `x = y`？

inversion.

求证 `Some x = Some y`，怎么转变成证明 `x = y`？

f_equal.

已知 `x <> y`，怎么变成 `y <> x`？

Search (forall a b, a <> b -> b <> a).

not_eq_sym: forall (A : Type) (x y : A), x <> y -> y <> x

怎么说明要么 `x = y`，要么 `x <> y`？

一般来说这个是叫做 _dec，比方说：

ascii_dec
string_dec
Nat.eq_dec

你可以用 destruct (string_dec x y). 来分类讨论这两种情况。

我的假设里面有 `/\` 或 `\/` 怎么办？

first_order 或者 destruct。

我的目标里面有 `/\` 或 `<->` 怎么办？

first_order 或者 split。

我的目标里面有 `\/` 怎么办？

用 left. 或者 right. 来证明两者中的其中一个。

怎么样复制一份假设？

assert。

怎么样把一个命题加到假设里面？

assert。

我的假设里面有矛盾怎么办？

比方说现在有一个 H : False 或者任何能被转化成 False 的假设（比方说 Some x = None、1 = 2 或者 True = False），那么恭喜，试试看 discriminate. 或者 congruence.，这个证明就结束了。

这是因为从逻辑上说，一个假的命题可以推导出任何东西。

我的假设里面的前提条件有矛盾怎么办？

比方说现在有一个 H : Some x = None -> P，那么现在你就只能 clear H. 把它删掉了，因为你永远没有办法使用 H。这跟前面的条件不一样，因为你没办法证明 Some x = None 所以你没办法去掉 H 里面的前提条件，所以 P 无法成立。

目标是个矛盾怎么办？不可证怎么办？

如果你的目标是 False 或者 Some x = None 或者任何类似的不可证的东西，别慌张，先检查一下假设里面有没有任何能导出矛盾的地方，因为假命题可以推导出任何东西，包括假命题。

如果所有的假设都很合理，那就说明你在之前的步骤中做错了事情。把它找出来，改掉。

目标里面有 `->` 怎么办？

intros。

目标以 `forall` 开头怎么办？

intros。

目标以 `exists` 开头怎么办？

一般来时我会用 exists 告诉 Coq 这些变量是什么，但是你也可以用 eexists. 向前推进证明，然后到某个时刻 Coq 会自动推导出来这个变量是什么。

我的假设以 `forall` 开头怎么办？

specialize 或者 pose proof。

我的假设以 `exists` 开头怎么办？

destruct 来把这个变量取出来。

我的假设里面有 `->` 怎么办？

specialize 或者 pose proof。

怎么样才能跳过这个小目标去证下一个？

admit。

Tactics

intros

simpl

simplify (Frap Tactic)

destruct

induction

inversion

f_equal

assumption

constructor

apply

exists

reflexivity

discriminate

congruence

auto

econstructor / eapply / eauto / edestruct / eexists

rewrite

unfold

specialize

pose proof

split

left / right

exact

assert

first_order

admit

symmetry

revert

remember

induct (Frap Tactic)

Vernacular Commands

Print

Search

Tricks

对什么进行归纳？

缩进和子弹点

在一行里面写多个招式

向前证明和向后证明

显示记号

FAQ

已知 Some x = Some y，怎么变成 x = y？

求证 Some x = Some y，怎么转变成证明 x = y？

已知 x <> y，怎么变成 y <> x？

怎么说明要么 x = y，要么 x <> y？

我的假设里面有 /\ 或 \/ 怎么办？

我的目标里面有 /\ 或 <-> 怎么办？

我的目标里面有 \/ 怎么办？

怎么样复制一份假设？

怎么样把一个命题加到假设里面？

我的假设里面有矛盾怎么办？

我的假设里面的前提条件有矛盾怎么办？

目标是个矛盾怎么办？不可证怎么办？

目标里面有 -> 怎么办？

目标以 forall 开头怎么办？

目标以 exists 开头怎么办？

我的假设以 forall 开头怎么办？

我的假设以 exists 开头怎么办？

我的假设里面有 -> 怎么办？

怎么样才能跳过这个小目标去证下一个？

`intros`

`simpl`

`simplify` (Frap Tactic)

`destruct`

`induction`

`inversion`

`f_equal`

`assumption`

`constructor`

`apply`

`exists`

`reflexivity`

`discriminate`

`congruence`

`auto`

`econstructor` / `eapply` / `eauto` / `edestruct` / `eexists`

`rewrite`

`unfold`

`specialize`

`pose proof`

`split`

`left` / `right`

`exact`

`assert`

`first_order`

`admit`

`symmetry`

`revert`

`remember`

`induct` (Frap Tactic)

`Print`

`Search`

已知 `Some x = Some y`，怎么变成 `x = y`？

求证 `Some x = Some y`，怎么转变成证明 `x = y`？

已知 `x <> y`，怎么变成 `y <> x`？

怎么说明要么 `x = y`，要么 `x <> y`？

我的假设里面有 `/\` 或 `\/` 怎么办？

我的目标里面有 `/\` 或 `<->` 怎么办？

我的目标里面有 `\/` 怎么办？

目标里面有 `->` 怎么办？

目标以 `forall` 开头怎么办？

目标以 `exists` 开头怎么办？

我的假设以 `forall` 开头怎么办？

我的假设以 `exists` 开头怎么办？

我的假设里面有 `->` 怎么办？