Coq基础(五)

在前面的Proof in Coq中介绍了几种简单的证明方法以及常用的策略(tactics)，而这里则是介绍几种更为复杂的证明策略:

[apply]策略

在进行证明的时候经常遇到这样的情况，即要证明的目标与上下文中的某个假设或某个先前已证明的引理完全相同。
有时候可以使用[rewrite]然后在使用[reflexivity]来完成证明，如：

Theorem silly1 : forall (n,m,o,p:nat), n=m -> [n;o] = [n;p] -> [n;o] = [m;p].
intros n,m,o,p eq1 eq2. 
rewrite <- eq1.
rewrite eq2. reflexivity.
Qed.

但也可以使用[apply]策略一步完成证明：

Theorem silly1 : forall (n,m,o,p:nat), n=m -> [n;o] = [n;p] -> [n;o] = [m;p].
intros n,m,o,p eq1 eq2. 
rewrite <- eq1.
apply eq2.
Qed.

[apply]策略也适用于条件假设和引理:如果所应用的语句是一个蕴涵，那么这个蕴涵的前提将被添加到需要证明的子目标列表中。
如下，下面的证明中的第二个假设是一个蕴含语句：

Theorem silly2 : forall (n m o p:nat), n = m -> (forall (q r:nat), q=r -> [q;o]=[r;p]) -> [n;o] = [m;p].
Proof.
intros n m o p eq1 eq2.
apply eq2. apply eq1. Qed.

通常，当我们使用[apply H]时，而语句H是以关键字forall开始的，也就是说语句H绑定了一些通用的变量。当Coq根据H的结论匹配当前目标时，它将尝试为这些变量找到合适的值。例如，在上面的例子中使用语句[apply eq2]时，eq2中的通用变量q用n实例化，r用m实例化。

需要注意的一点是，要使用[apply]策略，所应用的事实(结论)必须与目标完全匹配—例如，如果等式的左右两边交换，apply将不起作用，这个时候就需要使用关键字[symmetry]将等式的两边进行交换：

Theorem silly3 : forall n:nat, true = (n=?5) -> (S(S n)) =? 7 = true.
Proof.
intros n H.
symmetry in H. (*将H中的等式两边进行交换*)
simpl.
apply H.
Qed.

[apply with]策略

[apply with]和[apply]其实没有太大区别，只不过[apply with]允许指定用上下文中的变量代替引用的假设或者结论中的绑定变量。
先看一个例子：

Example tras_eq_example : forall (a b c d e f : nat),[a;b] = [c;d] -> [c;d] = [e;f] -> [a;b] = [e;f].
Proof.
intros a b c d e f eq1 eq2. rewrite eq1. rewrite eq2. reflexivity. Qed.

因为这是一个常见的语句，可以尝试想把它作为引理记录，因为等价是具有传递性的。如下：

Theorem tras_eq : forall {X:Type} (n m o:X),n=m -> m=o -> n=o.
Proof.
intros X n m o eq1 eq2. rewrite eq1. rewrite eq2. reflexivity. Qed.

Example tras_eq_example' : forall (a b c d e f : nat),[a;b] = [c;d] -> [c;d] = [e;f] -> [a;b] = [e;f].
Proof.
intros a b c d e f eq1 eq2. apply traas_eq with (m:=[c;d]). apply eq1. apply eq2. Qed.

不过在使用[apply with]策略的时候需要注意避免上下文中的变量名称和引理中的绑定变量的名称重复的情况。
还有一点是，在前面介绍[rewrite]策略时，提到过可以指定上下文中的变量作为重写的参数。在这里，对于[apply]策略也同样适用：

Example trans_eq_example'' : forall (a b c d e f : nat),
     [a;b] = [c;d] ->
     [c;d] = [e;f] ->
     [a;b] = [e;f].
Proof.
intros a b c d e f eq1 eq2.
apply (trans_eq [a;b] [c;d] [e;f]).
apply eq1. apply eq2.
Qed.

[injection]和[discriminate]策略

回顾之前定义自然数的语句：

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

从定义的语句中很明显能够看出，每个自然数都只能是两种情况中的一种：要么是是由构造器O构成的，要么是由构造器S中构成的。这也是基础证明策略[destruct]和[induction]的基本原理。
然而还能够从自然数的定义语句中看出两外两点：
1.构造器S（可以视为一个从自然数映射到自然数的函数）是单射的，也就是说如果S n = S m，则 n = m
2.构造器O和构造器S是不相交的，也就是说对于任何的一个n，O不可能等于S n
这两条规则可以适用于任何一个递归定义的变量类型。
可以对构造器S的单射性进行证明：

Theorem S_injective : forall (n m:nat), S n = S m -> n = m.
Proof.
intros n m H1. assert (H2:n = pred (S n)). {reflexivity. }
rewrite H2. rewrite H1. reflexivity.
Qed.

这个定理也可以使用[injection]策略进行证明：

Theorem S_injective' : forall (n m:nat), S n = S m -> n = m.
Proof.
intros n m H. 
injection H. intros Hnm. apply Hnm.
Qed.

通过[injection H]语句，Coq会生成它可以依据构造函数的单射性推导出的所有方程。每一个这样的方程都是作为目标的前提加入的，而在这个例子中，添加了前提n=m。而这些前提也会成为后续证明的子目标。
此外，还可以使用关键字as引入一个变量来绑定这些前提，如：

Theorem injection_ex : forall (n m : nat), [n] = [m] -> n = m.
Proof.
intros n m H.
injection H as Hnm. apply Hnm.
Qed.

不相交原则是指两个变量以不同的构造函数(如[O]和[S]，或[true]和[false])永远不可能相等。这意味着，任何时候我们发现上下文中某个假设断言两个不同构造器的变量相等，那么就可以得到任何想要的结论，因为假设是不成立的。
[discriminate]策略具体化了这个原则，通常这个策略被用在某个断言两个不同构造器构造的变量相等的假设上，然后使用这个策略快速完成当前的目标。例如：

Theorem eqb_0_1 : forall n, 0 =? n = true -> n = 0.
Proof.
intros n.
destruct n as [| n'].
-reflexivity.
-simpl. intros H. discriminate H.
Qed.

可以将[discriminate]策略理解为：如果证明过程中某个荒谬的假设成立，那么推出的任何结论也是成立的，如：

Theorem bottom_implys_all : forall n : nat, S n = O -> 2 + 2 = 5.
Proof.
intros n contra. discriminate contra. Qed.

在假设中使用策略

Coq中使用策略时，都是默认作用在当前目标上，然而策略同样也可以作用到假设上，例如：

Theorem S_inj : forall (n m : nat) (b : bool), (S n) =? (S m) = b -> n =? m = b.
Proof.
intros n m b H. simpl in H. apply H. Qed.

需要注意的是，如果[apply]所使用的引理是条件语句(即形如X -> Y)，在当前子目标上使用[apply]时，如果当前子目标与 Y 匹配成功，那么当前子目标证明完成，但是同时会生成一个与 X 对应的子目标。而在假设 H 中使用[apply]时，如果假设中与 X 匹配成功，那么这个假设会直接重写为与 Y 对应的语句。
如下：

Theorem silly3' : forall n:nat, (n =? 5) = true -> (S (S n)) =? 7 = true) -> true = (n=?5) -> true = (n=?7).
Proof.
intros n H eq.
symmetry in eq. apply H in eq. symmetry in eq. apply eq.
Qed.

易变的归纳性假设

当在Coq中进行归纳性证明时，需要准确的控制当前的归纳假设。具体的来说，在调用[induction]策略之前，需要仔细考虑证明过程中(使用[intros]策略)将哪些假设从目标移动到上下文。
例如，想要证明double(n:nat, n => 2n)函数是一个单射的函数：
如果在开始证明的时候，就将 m 从目标移动到上下文中，即使用语句intros n m. 那么这个结论将无法得到证明：

Theorem double_injective_Failed : forall n m : nat, 
   double n = double m -> n = m.
Proof.
intros n m. induction n as [|n' IHn'].
-simpl. intros eq. destruct m as [|m'].
  +reflexivity.
  +discriminate eq.
-intros eq. destruct m as [|m'].
  +discriminate eq.
  +apply f_equal.
(*At this point, IHn' : double n' = double (S m') -> n' = S m', so the goal is not provable*)
Abort.

运行到这一步后，发现无法再继续进行证明了，证明不得不中止。
然而这并不是Coq本身的哪里出了问题，现在可以对上面的代码进行分析：
intros n m. 这一句就将[m]引入上下文中，也就是说，想在的证明目标是：对于某两个确定的[n]和[m]，"if double n = double m then n = m"
induction n. 这一句就是对[n]进行归纳证明，证明目标 Pn = "if double n = double m then n = m"
Basics : "if double 0 = double m, then 0 = m"
Inductive : "if double n = double m, then n = m" -> "if double S n = double m, then S n = m"
然而这个归纳得到的假设并不能对接下来的证明起到任何作用：
举一个更直观的列子，假设有两个命题：
Q := if double n = 10 then n = 5.
R := if double (S n) = 10 then (S n) =5
显然，如果需要证明命题[R]，那么命题[Q]就不能起到任何作用。
所以这个证明的主要问题是在开始证明的时候就将另外一个变量[m]给绑定了：

Theorem double_injective : forall n m : nat, 
   double n = double m -> n = m.
Proof.
intros n. induction n as [|n' IHn'].
-simpl. intros m eq. destruct m as [|m'].
  +reflexivity.
  +discriminate eq.
-simpl. intros m eq. destruct m as [|m'].
  +discriminate eq.
  +apply f_equal. apply IHn'. injection eq as goal. apply goal.
Qed.

所以在证明基于两个递归定义的变量的定理时，需要避免这样的问题。

[unfold]策略

有时在证明过程中需要手动展开一个已经被一个[Definition]所定义好的函数名称，以便更好操纵等式的右边。
例如，定义一个平方函数：

Definition square n := n * n.

然后基于这个定义进行以下证明：

Theorem square_mult : forall n m, square (n * m) = square n * square m.
Proof.
intros n m. (*Did nothing*)
unfold square.
rewrite mult_assoc.
assert (H : n * m * n = n * n * m). {rewrite mult_comm. apply mult_assoc. }
rewrite H. rewrite mult_assoc. reflexivity.
Qed.

在复合表达式中使用[destruct]策略

在之前所使用的[destruct]策略中，[destruct]一般都是用来进行case analysis。但有时也需要根据一些表达式的结果来进行推理，这时也可以使用[destruct]策略：

Definition sillyfun (n : nat) : bool :=
  if n =? 3 then false
  else if n =? 5 then false
  else false.
Theorem sillyfun_false : forall (n : nat),
  sillyfun n = false.
Proof.
  intros n. unfold sillyfun.
  destruct (n =? 3) eqn:E1.
    - (* n =? 3 = true *) reflexivity.
    - (* n =? 3 = false *) destruct (n =? 5) eqn:E2.
      + (* n =? 5 = true *) reflexivity.
      + (* n =? 5 = false *) reflexivity. Qed.

[destruct]策略中的"eqn:"部分是可选的，但大多数时候都会选择加上这个部分仅仅是为文档化，但是大多数的Coq证明都会忽略这个部分。
此外，需要注意的是，当对复合表达式使用[destruct]策略时，由eqn部分记录的信息有时会是决定性的：如果忽略这部分信息，那么[destruct]策略可能会删除掉在完整证明的过程中所需要的信息。
比如：

Definition sillyfun1 (n : nat) : bool :=
  if n =? 3 then true
  else if n =? 5 then true
  else false.
Theorem sillyfun1_odd_FAILED : ∀(n : nat),
     sillyfun1 n = true →
     oddb n = true.
Proof.
  intros n eq. unfold sillyfun1 in eq.
  destruct (n =? 3).
  (* stuck... *)
Abort.
Theorem sillyfun1_odd : ∀(n : nat),
     sillyfun1 n = true →
     oddb n = true.
Proof.
  intros n eq. unfold sillyfun1 in eq.
  destruct (n =? 3) eqn:Heqe3.
  (* Now we have the same state as at the point where we got
     stuck above, except that the context contains an extra
     equality assumption, which is exactly what we need to
     make progress. *)
    - (* e3 = true *) apply eqb_true in Heqe3.
      rewrite → Heqe3. reflexivity.
    - (* e3 = false *)
     (* When we come to the second equality test in the body
        of the function we are reasoning about, we can use
        eqn: again in the same way, allowing us to finish the
        proof. *)
      destruct (n =? 5) eqn:Heqe5.
        + (* e5 = true *)
          apply eqb_true in Heqe5.
          rewrite → Heqe5. reflexivity.
        + (* e5 = false *) discriminate eq. Qed.