Proof By Simplification

之前的代码中出现过

Proof. simpl. reflexivity. Qed.

simpl是将方程的两边简化，reflexivity使用自反性检查两边是否包含相同的值
例如：

Theorem plus_0_n:forall n:nat,0+n=n.
Proof.
intros n. simpl. reflexivity. Qed.

实际上自反性可以在检查两边式子的时候自动实现一些简化，我们可以省略simpl的过程（simpl相当于将中间过程展示了出来）

Theorem plus_O_n' : ∀n : nat, 0 + n = n.
Proof.intros n. reflexivity. Qed.

以上的证明过程使用了Theorem引出需要证明的结论（实际上和exmaple差不多）

intros n. simpl. reflexivity.

以上是一个tatics的例子，tatics后续会详细介绍，这里我们只需要知道intro n.是将forall一般化

Proof By Rewriting

Theorem plus_id:forall n m:nat,n=m->n+n=m+m.

上述定理描述只有在n=m时，后续的定理才成立，并且需要对m和n一般化，intro. 可以实现上述三个目标
由于n和m是任意数，我们不能用simpl直接简化，需要利用条件n=m，将所有的n用m替换，再证明式子，这个过程用rewrite实现（是不是很像命题逻辑中的替换和代入规则）

Theorem plus_id:forall n m:nat,n=m->n+n=m+m.
Proof.
intros n m. 
intros H. (*将前提引入到证明环境中*)
rewrite->H. 
reflexivity. 
Qed.

rewrite->H.代表将前提从左到右重写，n->m说明将n全部用m代替，也可以写成rewrite<-H,表示n<-m将m全部替换为n
在这里插入图片描述

Proof by Case Analysis

然而在一些未知条件过多的证明中，仅仅使用上述策略无法实现证明

Theorem plus_1_neq_0_firsttry : ∀n : nat,(n + 1) =? 0 = false.
Proof.intros n.simpl. (* does nothing! *)
Abort.

原因是n+1=0无法再进行简化
那样我们就需要考虑所有n的情况，利用枚举法证明结论

destruct

我们提到了关于表示出n所有可能性的想法，coq中用destruct函数来实现列举可能的情况

例1

Theorem plus_1_neq_0 : ∀n : nat,eqb (n + 1)  0 = false.
Proof.intros n. destruct n as [| n']- reflexivity.- reflexivity. Qed.

ps:我没找到coq里面关于eqb函数的notation，这里直接用函数表示了

destruct函数为我们生成两个子目标：n=O，n=S n’，我们需要分别证明其正确性
destruct n as [| n']表示对每种情况需要引入的变量名，在这个证明中coq不会自动分类，需要根据引入的变量名修改子目标，[ ]表示一个参数列表，参数之间用“|”分割
我们使用“-”来使代码的分类证明更加有序

例2

我们也可以利用析构函数的策略证明相关的布尔表达式

Theorem negb_involutive:forall b:bool,negb (negb b)=b.
Proof.intros b.destruct b.
- reflexivity.
- reflexivity. Qed.

多重析构

有时我们需要对子目标继续进行析构，这时我们需要用不同的项目符号标记目标

Theorem andb_communtive:forall b c,(andb b c)=(andb c b).
(*定律描述*)
Proof.intros b c.destruct b.- destruct c.+ reflexivity.+ reflexivity.- destruct c.+ reflexivity.+ reflexivity.
Qed.

遇到三重以上证明时，可以用*作为第三层析构
我们也可以用括号包含析构内容，使代码更清晰

Theorem andb_commutative' : ∀b c, andb b c = andb c b.
Proof.intros b c. destruct b eqn:Eb.{ destruct c eqn:Ec.{ reflexivity. }{ reflexivity. } }{ destruct c eqn:Ec.{ reflexivity. }{ reflexivity. } }
Qed.

参考书目练习答案

basic部分

EX5:standard (plus_id_exercise)

Theorem plus_id_exercise : forall n m o : nat,n = m -> m = o -> n + m = m + o.
Proof.
intros n m o.
intros H1 H2.
rewrite->H1.
rewrite<-H2.reflexivity. Qed.
Theorem mult_0_plus : forall n m : nat,(0 + n) * m = n * m.
Proof.intros n m.rewrite -> plus_O_n.reflexivity. Qed.

//其中第二个证明展示了用已知结论重写待证明的式子

EX6:standard (mult_S_1)

Theorem mult_S_1 : forall n m : nat,m = S n -> m * (1 + n) = m * m.
Proof.
intros n m.
intros H.
rewrite->H.
reflexivity.
Qed.

注意这里不能用<-，因为无法找到需要被代替的S n

EX7:standard (andb_true_elim2)

Theorem andb_true_elim2 : forall b c : bool,andb b c = true -> c = true.
Proof.intros b c.destruct b.-destruct c.+ simpl.intros H.reflexivity.+ simpl.intros H.rewrite->H.reflexivity.-destruct c.+ simpl. intros H.reflexivity.+ simpl.intros H.rewrite->H.reflexivity.
Qed.

有几步不太好想，关键是把明确什么时候引入前提，什么时候结论为真不需要证明，什么时候结论为假需要说明前提也为假（利用替换）

EX8:standard (zero_nbeq_plus_1)

Fixpoint eqb (n m:nat):bool:=
match n with
|O=>match m with |O=>true|S m'=>falseend
|S n'=>match m with|O=>false|S m'=>(eqb n' m')end
end.Theorem zero_nbeq_plus_1 : forall n : nat,eqb 0 (n + 1) = false.
Proof.intros n.destruct n as [|n'].- reflexivity.- reflexivity.
Qed.

More exercise答案
1 indentity_fn_applied_twice

Theorem identity_fn_applied_twice :forall(f : bool -> bool),(forall(x : bool), f x = x) ->forall(b : bool), f (f b) = b.
Proof.intros f.destruct b.(*如果不将x进行析构和引入，x代表任意数，可以直接代换*)- rewrite H. rewrite H. reflexivity.- rewrite H. rewrite H. reflexivity. Qed.

2 (negation_fn_applied_twice）

Theorem negation_fn_applied_twice:
forall (f: bool->bool),(forall x:bool,f x=negb x)->forall b,f(f b)=b.
Proof.intros f.destruct b.- rewrite H. rewrite H. reflexivity. - rewrite H. rewrite H. reflexivity. 
Qed.

3 andb_eq_orb

Theorem andb_eq_orb :forall (b c : bool),(andb b c = orb b c) ->b = c.
Proof.intros b.destruct b.-simpl. intros c. intros H. rewrite->H. reflexivity.-simpl. intros c. intros H. rewrite->H. reflexivity.
Qed.