InductionProof by Induction

Review


To prove the following theorem, which tactics will we need besides intros and reflexivity? (1) none, (2) rewrite, (3) destruct, (4) both rewrite and destruct, or (5) can't be done with the tactics we've seen.
    Theorem review1: (orb true false) = true.

What about the next one?
    Theorem review2: ∀ b, (orb true b) = true.
Which tactics do we need besides intros and reflexivity? (1) none (2) rewrite, (3) destruct, (4) both rewrite and destruct, or (5) can't be done with the tactics we've seen.

What if we change the order of the arguments of orb?
    Theorem review3: ∀ b, (orb b true) = true.
Which tactics do we need besides intros and reflexivity? (1) none (2) rewrite, (3) destruct, (4) both rewrite and destruct, or (5) can't be done with the tactics we've seen.

What about this one?
    Theorem review4 : ∀ n : nat, 0 + n = n.
(1) none, (2) rewrite, (3) destruct, (4) both rewrite and destruct, or (5) can't be done with the tactics we've seen.

What about this?
    Theorem review5 : ∀ n : nat, n + 0 = n.
(1) none, (2) rewrite, (3) destruct, (4) both rewrite and destruct, or (5) can't be done with the tactics we've seen.

Separate Compilation

First type coqc Datatypes.v into the terminal to compile Datatypes.v into Datatypes.vo so it can be imported here. Note that you may need to remove the From LF from the following line:
From LF Require Export Datatypes.

Proof by Recursion

Clearly, for many proofs about infinite datatypes (natural numbers included) our existing tactics will be insufficient. Consider for instance the claim that that every number is either even or odd. Proving this by case analysis is clearly impossible: There are (countably) infinitely many natural numbers! Let's start by stating our desired theorem.
Inductive Even : nat → Prop :=
| E_O : Even 0
| E_S : ∀ n, Odd n → Even (S n)

with Odd : nat → Prop :=
| O_S : ∀ n, Even n → Odd (S n).
We just wrote a "mutually inductive" definition. In short, it says that O is Even, the successor of an Odd number is Even and then successor of an Even number is Odd.
So let's try proving our lemma!
Lemma Even_or_Odd : ∀ (n : nat), Even n ∨ Odd n.
Proof.
  Abort.
(* But the proof of Even_or_Odd is actually quite easy to program! *)
Fixpoint Even_or_Odd (n : nat) : Even n ∨ Odd n
  (* WORK IN CLASS *). Admitted.
As we've seen, writing entire proofs in the programming language can be quite hard. Fortunately, there is a simply program that makes these proofs easy.
Print nat_ind.
nat_ind takes three arguments: 
    1) A proposition [P] over natural numbers
    2) A proof of [P O] 
    3) A proof that [P n -> P (S n)].
and it constructs a recursive proof that for any n, P n.
Coq automatically generates these "induction schemes" whenever we define an Inductive type, and applies them when we use the keyword induction. Let's try using it to prove Even_Or_Odd again:
Lemma Even_or_Odd' (n : nat) : Even n ∨ Odd n.
Proof.
  induction n.
  - apply or_introl.
    apply E_O.
  - destruct IHn as [He | Ho].
    + apply or_intror. apply O_S. apply He.
    + apply or_introl. apply E_S. apply Ho.
Defined.
Let's take a look at the generated term:
Print Even_or_Odd'.
Eval compute in Even_or_Odd'.

Proof by Induction

Let's jump to some less contrived examples of induction in general. These will tend to use rewriting, so trying to write a fixpoint will get pretty hairy. Let's start with finally proving that 0 is a right identity for addition.
Theorem plus_n_O : ∀ n:nat, n = n + 0.
Proof.
  intros n. induction n as [| n' IHn'].
  - (* n = 0 *) reflexivity.
  - (* n = S n' *) simpl. rewrite <- IHn'. reflexivity. Qed.

Let's try this one together:
Theorem minus_diag : ∀ n,
  minus n n = 0.
Proof.
  (* WORK IN CLASS *) Admitted.

Here's another related fact about addition, which we'll need later. (The proof is left as an exercise.)
Theorem plus_comm : ∀ n m : nat,
  n + m = m + n.
Proof.
  (* FILL IN HERE *) Admitted.

Proofs Within Proofs

Here's an alternate proof of mult_0_plus, using an in-line assertion instead of a separate lemma. New tactic: assert.
Theorem mult_0_plus' : ∀ n m : nat,
  (0 + n) * m = n * m.
Proof.
  intros n m.
  assert (H: 0 + n = n). { reflexivity. }
  rewrite → H.
  reflexivity.
Qed.

Another example of assert...
Theorem plus_rearrange_firsttry : ∀ n m p q : nat,
  (n + m) + (p + q) = (m + n) + (p + q).
Proof.
  intros n m p q.
  (* We just need to swap (n + m) for (m + n)... seems
     like plus_comm should do the trick! *)
  rewrite → plus_comm.
  (* Doesn't work...Coq rewrites the wrong plus! *)
Abort.

To use plus_comm at the point where we need it, we can introduce a local lemma stating that n + m = m + n (for the particular m and n that we are talking about here), prove this lemma using plus_comm, and then use it to do the desired rewrite.
Theorem plus_rearrange : ∀ 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.
(* Of course, in this instance we can take a more direct 
   route by simply providing plus_comm with the desired 
   arguments: *)
Theorem plus_rearrange' : ∀ n m p q : nat,
  (n + m) + (p + q) = (m + n) + (p + q).
Proof.
  intros n m p q.
  rewrite (plus_comm m n).
  reflexivity.
Qed.

Formal vs. Informal Proof

"Informal proofs are algorithms; formal proofs are code."
An unreadable formal proof:
Theorem plus_assoc' : ∀ n m p : nat,
  n + (m + p) = (n + m) + p.
Proof. intros n m p. induction n as [| n' IHn']. reflexivity.
  simpl. rewrite → IHn'. reflexivity. Qed.

Comments and bullets can make things a bit clearer...
Theorem plus_assoc'' : ∀ n m p : nat,
  n + (m + p) = (n + m) + p.
Proof.
  intros n m p. induction n as [| n' IHn'].
  - (* n = 0 *)
    reflexivity.
  - (* n = S n' *)
    simpl. rewrite → IHn'. reflexivity.
Qed.

... but it's still nowhere near as readable for a human as a careful informal proof:
  • Theorem: For any n, m and p,
       n + (m + p) = (n + m) + p.
    Proof: By induction on n.
    • First, suppose n = 0. We must show
        0 + (m + p) = (0 + m) + p.
      This follows directly from the definition of +.
    • Next, suppose n = S n', where
        n' + (m + p) = (n' + m) + p.
      We must show
        (S n') + (m + p) = ((S n') + m) + p.
      By the definition of +, this follows from
        S (n' + (m + p)) = S ((n' + m) + p),
      which is immediate from the induction hypothesis. Qed.

(* NEW NAME *)
Notation zero_neqb_S := zero_nbeq_S (only parsing).
Notation S_neqb_0 := S_nbeq_0 (only parsing).
Notation plus_leb_compat_l := plus_ble_compat_l (only parsing).