Induction

Seperate Compilation

Import all our definitions from the previous chapter Basics.v

Require let Coq find .vo (analogous to the .class for java and .o for C)

Create _CoqProject and organize the project.

Proof by Induction

Theorem plus_n_O_firsttry : forall n:nat,
  n = n + 0.

Easy on the left(by simplification) but hard on the right.

Actually I have tried an induction proof on plus_1_r.

(* I try the case analysis but it fails with destruct, i need induction *)
Theorem plus_1_r : forall n : nat, (n+1) = S n.
Proof.
  intros.
  simpl.
  induction n.                  (* induction *)
  - reflexivity.
  - simpl.
    rewrite -> IHn.
    reflexivity.
Qed.

This chapter we will deep inside proofs by induction.

We could use destruct to get one step further, but since n can be arbitrarily large, we'll never get all the there if we just go like this.

Powerful reasoning principle: induction

• show that [P(O)] holds;
• show that, for any [n'], if [P(n')] holds, then so does [P(S n')];
• conclude that [P(n)] holds for all [n].

Theorem plus_n_O : forall n:nat, n = n + 0.
Proof.
  intros n. induction n as [| n' IHn'].
  - (* n = 0 *)    reflexivity.
  - (* n = S n' *) simpl. rewrite <- IHn'. reflexivity.  Qed.

[IHn'] i.e. the Induction Hypothesis for [n']

What does [simpl] really do?

Theorem plus_n_Sm : forall n m : nat,
  S (n + m) = n + (S m).
Proof.
  intros n m.
  induction n as [| n' IHn'].
  - (* Case [n=0] *)
    Print plus.
    Print Nat.add.
    simpl. (* By the definition of Nat.add we can match 0 on both sides and drp the 0*)
    reflexivity.
  - (* Case [n=Sn'] *)
    (* We must show that [S (Sn' + m) = Sn' + Sm] *)
    Print Nat.add.
    (* Here as match with second rule in Nat.add simpl with unfold the S (n' m) on the left and S(n' + Sm)*)
    simpl.
    rewrite -> IHn'. reflexivity.
Qed.

So I manage to finish the plus_comm. At first I forget to use the plus_n_Sm as a Lemma to help me prove if and that is really terrible for such a beginner like me.

(* A little bit hard to be at first *)
Theorem plus_comm : forall n m : nat,
  n + m = m + n.
Proof.
  intros n m.
  induction n as [| n' IHn'].
  - (* Case [n=0] *)
    (* By the definition of plus simpl. match 0 so we can drop 0 on the left *)
    simpl.
    (* rewrite plus_n_0 as it gives n = n + 0 *)
    rewrite <- plus_n_O. reflexivity.
  - (* Case [n= Sn'] *)
    (* By the definition simpl. will unfold the left *)
    simpl.
    Print plus_n_Sm.
    (* plus_n_Sm tells forall n m in nat S (n + m) = n + S m *)
    rewrite -> IHn'.
    rewrite <- plus_n_Sm.
    reflexivity.
Qed.

When we need to search for some lemma/theorems, use [Search "string"].

According to the context, maybe it's better to [rewrite] before [simpl] as [simpl] will unfold the match. Like this

Theorem evenb_S : forall n : nat,
  evenb (S n) = negb (evenb n).
Proof.
  induction n as [| n' IHn'].
  - simpl. reflexivity.
  - rewrite -> IHn'.
    Print evenb.
    Print negb_involutive.
    simpl.
    (* By the definition of evenb S (S n') => evenb n' , so [simpl] will replace the left with evenb n'. As for the right we search for negb_invlutive.*)
    rewrite -> negb_involutive.
    reflexivity.
Qed.

Not begin with [simpl] always

In case [n = S n'], if we [simpl] before [rewrite -> IHn'], we will get the subgoal like this

n' : nat
IHn' : evenb (S n') = negb (evenb n')
============================
evenb n' = negb match n' with
                | 0 => false
                | S n'0 => evenb n'0
                end

Briefly explain the difference between the tactics [destruct] and induction

Destruct just split the proof into different case. Induction give an useful induction Hypothesis.

Both [destruct] and induction will consider all possible shapes that [x] can take. However, induction will also generate an induction hypothesis. This is useful for proving facts about inductive data types that have recursive definitions.

Proofs Within proofs

In Coq, as in informal mathematics, large proofs are often broken into a sequence of theorems. But sometimes, give a proof its own top-level name is trivial.

For convenience, simply state and prove the needed "sub-theorem" right at the point where it is used with tactic [assert].

[assert] introduces two sub-goals

• The first goal -> [H:] itself
• The second goal -> the origin goal at the point we invoke [assert]

Tell Coq where to rewrite

When the positions where we can use the same [rewrite] tactic appears more than once, the [rewrite] tactic is not very smart about where it applies the rewrite.

We can tell Coq with [assert] and sub-proof. Like this:

Theorem plus_rearrange : forall n m p q : nat,
  (n + m) + (p + q) = (m + n) + (p + q).
Proof.
  intros n m p q.
  assert (H: n + m = m + n).
  { rewrite -> plus_comm. reflexivity. }
  rewrite -> H. reflexivity.  Qed.

Use [replace] tactic to specify a particular subterm to rewrite and what you want it rewritten to. [replace (t) with u].

Formal vs. Informal Proof

"Informal proofs are algorithms; formal proofs are code."

A rough and ready definition of proof

A proof of a mathematical proposition [P] is a written (or spoken) text that instills in the reader or hearer the certainty that [P] is true -- an unassailable argument for the truth of [P]. That is, a proof is an act of communication.

Communication and readers

Acts of communication may involve different sorts of readers.

• program
  • Like Coq,Isabel...
  • Mechanically derived from a certain set of formal logic rules.
  • Formal proofs
• human being
  • in natural language
  • convince readers
  • Informal proofs

Differences

Coq has been designed so tha its induction tactic generates the same sub-goals, in the same order, as the bullet points that a mathematician would write.