归纳证明

在证明过程中，特别是在使用formal method的证明过程中归纳法是特别重要的。 在这里暂且先略过Order Theory 和超限完全归纳等等的数学理论，因为我也没有搞的非常明白，还是单单从inFormal goal-oriented证明的角度来说一下吧。code没啥好多说的，最近感觉非形式化的证明过程必须搞明白。

0X00

归纳法(Induction)是我们初中就学过的基本数学工具，他在处理一些离散的东西，比如数列，多项式的时候非常的有效。 什么时候需要使用归纳证明？
比如希望证明等差数列的求和通项就是， S(n)是由一个比自己略微小一些的问题S(n-1)+n构成的，而我们知道自然数N是存在一个最小值的，也就是说n如果不断减小，总有一天是能减小到n=0这个base case的。

实际上如果定义有递归的部分，归纳都是常见的手法，不过在我们使用的函数式编程的语言中（比如sml）没有对于原始递归的要求(primitive recursion), 证明每次命题确实是在减小也是比较重要的（或者说测度在变小）。Coq的Gallina支持了Fixpoint Inductive, HOL里归纳定义也有对应的工具。ok，试着用在最简单的情况中吧。

0X01 对变量进行归纳

之前学过自然数可以表示为Peano 算术的形式，而在这个形式系统中是有归纳公理的， 所以对于自然数相关的命题自然是可以通过归纳法实现，比如证明0是+的右幺元(identity):

Theorem plus_n_O: ∀n:nat, n = n + 0.

Proof
对变量n进行归纳证明：
首先证明命题对于 n = O 时需要成立 ,有命题目标

O = O + O

根据加法的函数定义， 这种情况显然是成立的,0加上任何数n都是n。

fix add (n m : nat) {struct n} : nat :=
  match n with
  | 0 => m
  | S p => S (add p m)
  end

接下来我们需要证明在n = S n的情况下，原命题也成立，换句话说此时的goal为带入n = S n的命题。

S n = S n + O

而此时我们有归纳假设(Inductive Hypothesis), 也就是我们原来证的结论:

n = n + o

ok,我们再次使用加法的基本定义可以将goal转化为

S n = S (n + o)

此时归纳假设IH告诉我们， n = n + 0,故可以将命题中所有的n重写为n+0,之后，等号左右完全相等，命题得证。
宗上，根据归纳公理(Induction Axiom),0是自然数加法运算的右幺元。
Q.E.D.

0X02 对命题进行归纳

在证明一阶逻辑相关的命题的时候我们很多时候面对的对象不只是一个简单的逻辑变量，我们可能需要对类似 F(a)之类进行归纳，因为F(a)很可能就是递归的方式定义的， 比如如下定义：
n 是偶数

Inductive even : nat → Prop :=
  | ev_0 : even 0
  | ev_SS : ∀n, even n → even (S (S n)).

这是一个典型的递归定义， 初始0是偶数其他n+2都是偶数。
求证如下命题

Theorem ev_sum : ∀ n m, even n -> even m -> even (n+m).

非形式化的说，对于所有n,m,若n是偶数，且m也是偶数，那么（n+m）是偶数。

首先，这里如果我们直接对逻辑变量n做归纳，之后再展开偶数的定义当然是可以的，但是其实没有那么麻烦。一阶逻辑和命题逻辑最大的区别也就在于，在一阶逻辑中命题是可以被看作一个变量的！
因此不难猜测，此处如果直接对even n进行归纳可能是一种更加好的想法。
Proof
对even n进行归纳证明。
由even n的定义不难看出，base case应当为 even n = even o, 也就是n取0时的命题.此时代入原命题有如下goal:

even(0+m)

根据加法的定义化简后与条件m是偶数一致，得证。
对于"n+1"也就是 "even n = even (S (S n))" 换句话说 n = S (S n)的情况，代入得goal:

even (S (S n) + m)

并且此时有归纳假设IH(也就是原来的goal):

even (n + m)

根据加法的定义,我们不难化简goal得：

even (S S (n + m))

根据偶数定义的第二条ev_SS，我们可以推出，当前goal成立的前提条件是当 (n+m)是偶数，而这正是我们的归纳假设IH。故命题得证。
综上，原命题成立。
Q.E.D.

0x03 在归纳中使用泛化(generalizing)

那么在上面的归纳中有没有什么是被我们忽略的东西呢？
看如下证明：
根据自然数的定义，不难写一个double的函数

Fixpoint double (n : nat) : nat :=
  match n with
  | 0 => 0
  | S n' => S (S (double n'))
  end

求证double运算具有内射性(injective)

Theorem double_injective : 
    ∀n m,  double n = double m -> n = m.

这个结论看上去很好证明.
Proof
对变量n进行归纳证明

• 当 n = 0 时， 条件变为 0 = double m 此时根据自然数的定义，我们可以分情况讨论，m 如果是 O,那自然是相等， 如果形如S n', 那么代入double计算以后得条件变为 0=S (S double n') 这显然不可能。故base case证明完毕。
• 当 n = S n 时，有归纳假设

double n = double m -> n = m

和刚才一样我们对m分情况讨论m = O的情况，不可能，因为此n代入double以后的结果必然带有S。当m = S m时, 此时goal 和归纳假设如下

double (S n) = double (S m)
IH: 
double n = double (S m) -> n = S m
goal:
S n = S m

这时证明无法再进行下去了。。。。。。可以感觉到IH和结论存在明显的矛盾。
Failed.
那么错在哪里了呢？
在上面的证明过程中，我们在分情况讨论m的取值的时候，直接导致了IH中的m也被替换了，这里有一个隐藏的逻辑，在规模更加小一点的归纳假设当中，m的值必须要要和比他更大的goal中的一样。也就是说，在这种逻辑下面，所有的n都会被映射到同一个m! 这和我们的想要的并不相同，我们时为了证明一个n有且只有一个m，而至于等于什么并不重要，我们的归纳假设有问题，或者是分析替换有问题，因为IH和goal中的m可能是不一样的！

万幸在Coq定理证明器中，有generalize dependent这个策略可以帮我们把m恢复到 全称量词当中，这样在生成归纳假设是就不会出现上面的情况了
使用之后的IH：

 ∀ m , double n = double m-> n = m

完美，用IH就能结束证明
Q.E.D.

0X04 在程序验证过程中使用归纳定义和归纳证明

先放到smell-step和STLC里面吧，后面再回过头来总结。