Coq基础(七)

递归命题

在前面有介绍过几种说明自然数n是一个偶数的方法，比如：

1. evenb n = true，或者
2. exists k, n = double k

现在，可以通过一条递归的规则来判断一个整数n是否是偶数：

• ev_0：数字0是偶数
• ev_SS：如果n是偶数，那么S(S n)也是偶数

根据上面规则可以将整数的偶数性定义为：

Inductive even : nat -> Prop :=
| ev_0 : even 0
| ev_SS (n : nat) (H : even n) : even (S (S n)).

Example ev_4 : even 4.
Proof. apply ev_SS. apply ev_SS. apply ev_0. Qed.

当然，如果假设中也用到了这个性质，那么同样也可以使用这些规则：

Theorem ev_plus4 : forall n, even n -> even (4 + n).
Proof.
  intros n. simpl. intros Hn.
  apply ev_SS. apply ev_SS. apply Hn.
Qed.

在证明中使用证据

上面所定义的递归类型的命题在coq中被称为证据(evidence)
而上面递归定义的声明不仅告诉Coq通过上面那两种方法可以构造出一个偶数n，并且声明了只能通过上面的两个构造器才能构造出一个整数
换句话说，如果给出一个假设E声称n是一个偶数，即even n，那么E必然是下面两种结构中的一种：

• E is ev_0(and n is 0)
• E is ev_SS n' E'(and n is S (S n)), E' is the evidence for even n'

[inversion]策略

由于这个特性，就和自然数一样，可以针对even类型的命题使用[destruct]策略

Theorem ev_inversion :
  forall (n : nat), even n ->
    (n = 0) / (exists n', n = S (S n') / even n').
Proof.
  intros n E.
  destruct E as [ | n' E'].
  - (* E = ev_0 : even 0 *)
    left. reflexivity.
  - (* E = ev_SS n' E' : even (S (S n')) *)
    right. ∃n'. split. reflexivity. apply E'.
Qed.

然而[destruct]策略在下面这种情况下便行不通了：

Theorem evSS_ev : forall n,
  even (S (S n)) -> even n.
Proof.
  intros n E.
  destruct E as [| n' E'].
  - (* E = ev_0. *)
    (* We must prove that n is even from no assumptions! *)
Abort.

但是上面的定理还是可以使用前面证明过的inversion引理直接进行证明：

Theorem evSS_ev : forall n, even (S (S n)) -> even n.
Proof. intros n H. apply ev_inversion in H. destruct H.
 - discriminate H.
 - destruct H as [n' [Hnm Hev]]. injection Hnm.
   intro Heq. rewrite Heq. apply Hev.
Qed.

Coq中还存在着一种证明策略[inversion]，它的作用就和前面所证明的inversion引理一样，有时还会实现更多的功能
[inversion]策略可以检测出第一种情况(n=0)不适用：

Theorem evSS_ev' : forall n,
  even (S (S n)) -> even n.
Proof.
  intros n E.
  inversion E as [| n' E'].
  (* We are in the E = ev_SS n' E' case now. *)
  apply E'.
Qed.

[inversion]策略可以直接对一些明显的不成立的假设使用前面所说过的“矛盾原则”
有时候[inversion]策略会有更大的功能，当在等式证明中使用[inversion]策略时，相当于同时使用[discriminate]策略和[injection]策略，如下：

Theorem inversion_ex1 : forall (n m o : nat),
  [n; m] = [o; o] ->
  [n] = [m].
Proof.
  intros n m o H. inversion H. reflexivity. Qed.

[induction]策略

和前面介绍[induction]策略时的处境一样，当使用[destruct]策略进行case analysis无法解决问题时，那么首选的解决方法就是[induction]策略
在证据上面使用[induction]策略和在数据上面使用[induction]策略的效果是一样的，如下：

Lemma ev_even : forall n,
  even n -> exists k, n = double k.
Proof.
  intros n E.
  induction E as [|n' E' IH].
  - (* E = ev_0 *)
    exists 0. reflexivity.
  - (* E = ev_SS n' E'
       with IH : exists k', n' = double k' *)
    destruct IH as [k' Hk'].
    rewrite Hk'. ∃(S k'). reflexivity.
Qed.

递归关系

用数字(例如偶数)参数化的命题可以被看作是一种属性，即，定义了nat的一个子集，即命题可证明的那些数字。同样地，一个二元命题可以被认为是一种关系，即，定义了一组可证明命题的对。
一个有用的例子就是“小于等于”关系：

Module Playground.
Inductive le : nat → nat → Prop :=
  | le_n n : le n n
  | le_S n m (H : le n m) : le n (S m).
Notation "m <= n" := (le m n).
Theorem test_le1 :
  3 <= 3.
Proof.
  (* WORKED IN CLASS *)
  apply le_n.  Qed.

Theorem test_le2 :
  3 <= 6.
Proof.
  (* WORKED IN CLASS *)
  apply le_S. apply le_S. apply le_S. apply le_n.  Qed.

Theorem test_le3 :
  (2 <= 1) -> 2 + 2 = 5.
Proof.
  (* WORKED IN CLASS *)
  intros H. inversion H. inversion H2.  Qed.

(** The "strictly less than" relation [n < m] can now be defined
    in terms of [le]. *)

End Playground.

同样的，也可以对关系证明一些定理：

Lemma le_trans : forall m n o, m <= n -> n <= o -> m <= o.
Proof.
intros n m o Hnm Hmo.
  induction Hmo.
  - (* le_n *) apply Hnm.
  - (* le_S *) apply le_S. apply IHHmo. apply Hnm.
Qed.

Theorem O_le_n : forall n,
  0 <= n.
Proof.
intros n. induction n as [|n' IHn'].
-apply le_n.
-apply le_S. apply IHn'.
Qed.

Theorem n_le_m__Sn_le_Sm : forall n m,
  n <= m -> S n <= S m.
Proof.
intros n m E1.
induction E1 as [n0|n' m' H' IHE1'].
-apply le_n.
-apply le_S. apply IHE1'.
Qed.

Theorem Sn_le_Sm__n_le_m : forall n m,
  S n <= S m -> n <= m.
Proof.
intros n m E. inversion E as [n1|n' m' H' IHE'].
-apply le_n.
-apply (le_trans n (S n) m).
  +apply le_S. apply le_n.
  +apply H'.
Qed.

Theorem le_plus_l : forall a b,
  a <= a + b.
Proof.
intros a b. induction a as [|n' IHn'].
-simpl. apply O_le_n.
-simpl. apply n_le_m__Sn_le_Sm. apply IHn'.
Qed.

正则表达式

even属性提供了一个简单的例子来说明归纳定义和推理的基本技巧，但这些定理都是一些比较简单并且不是实用的
然而Coq中的递归证明的功能远不止如此，现在展示如何使用递归定义来建模计算机科学中的一个经典概念:正则表达式
正则表达式是一种用来描述字符串和集合的简单语言，其语法定义如下：

Inductive reg_exp {T : Type} : Type :=
  | EmptySet
  | EmptyStr
  | Char (t : T)
  | App (r1 r2 : reg_exp)
  | Union (r1 r2 : reg_exp)
  | Star (r : reg_exp).

通过以下规则连接正则表达式和字符串，这些规则定义了正则表达式何时匹配某个字符串:

• 表达式EmptySet不匹配任何字符串。
• 表达式EmptyStr匹配空字符串[]。
• 表达式Char x匹配一个字符的字符串[x]。
• 如果re1匹配s1, re2匹配s2，则App re1 re2匹配s1 ++ s2。
• 如果re1和re2中至少有一个匹配s，则Union re1 re2匹配s。
• 最后，如果我们可以把一些字符串s写成一个字符串序列s = s_1 ++…++ s_k，表达式re匹配每个字符串s_i，然后* re匹配s。作为一个特例，字符串序列可能是空的，不论re是怎么样的，* re总是和空字符串匹配

根据上面的规则，可以定义一个函数如下：

Inductive exp_match {T} : list T -> reg_exp -> Prop :=
  | MEmpty : exp_match [] EmptyStr
  | MChar x : exp_match [x] (Char x)
  | MApp s1 re1 s2 re2
             (H1 : exp_match s1 re1)
             (H2 : exp_match s2 re2) :
             exp_match (s1 ++ s2) (App re1 re2)
  | MUnionL s1 re1 re2
                (H1 : exp_match s1 re1) :
                exp_match s1 (Union re1 re2)
  | MUnionR re1 s2 re2
                (H2 : exp_match s2 re2) :
                exp_match s2 (Union re1 re2)
  | MStar0 re : exp_match [] (Star re)
  | MStarApp s1 s2 re
                 (H1 : exp_match s1 re)
                 (H2 : exp_match s2 (Star re)) :
                 exp_match (s1 ++ s2) (Star re).

Notation "s =~ re" := (exp_match s re) (at level 80).