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, 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.
What about this?
    Theorem review5 : ∀ n : nat, n = n + 0. (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

Coq will first need to compile Basics.v into Basics.vo so it can be imported here -- detailed instructions are in the full version of this chapter...
From LF Require Export Basics.

Proof by Induction

We can prove that 0 is a neutral element for + on the left using just reflexivity. But the proof that it is also a neutral element on the right ...
Theorem add_0_r_firsttry : ∀ n:nat,
  n + 0 = n.
Proof.
  intros n.
  simpl. (* Does nothing! *)
Abort.

And reasoning by cases using destruct n doesn't get us much further: the branch of the case analysis where we assume n = 0 goes through fine, but in the branch where n = S n' for some n' we get stuck in exactly the same way.
Theorem add_0_r_secondtry : ∀ n:nat,
  n + 0 = n.
Proof.
  intros n. destruct n as [| n'] eqn:E.
  - (* n = 0 *)
    reflexivity. (* so far so good... *)
  - (* n = S n' *)
    simpl. (* ...but here we are stuck again *)
Abort.

We need a bigger hammer: the principle of induction over natural numbers...
  • If P(n) is some proposition involving a natural number n, and we want to show that P holds for all numbers, we can reason like this:
    • show that P(O) holds
    • show that, if P(n') holds, then so does P(S n')
    • conclude that P(n) holds for all n.
For example...

Theorem add_0_r : ∀ n:nat, n + 0 = n.
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_n_n : ∀ 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 add_comm : ∀ n m : nat,
  n + m = m + n.
Proof.
  (* FILL IN HERE *) Admitted.

Exercise: 2 stars, standard, optional (even_S)

Here's a useful theorem that proves n-1 is not even. This will facilitate proofs by induction on n:
Theorem even_S : ∀ n : nat,
  even (S n) = negb (even n).
Proof.
  (* FILL IN HERE *) Admitted.
☐

Exercise: 1 star, standard, optional (destruct_induction)

Briefly explain the difference between the tactics destruct and induction.
(* FILL IN HERE *)
☐

Proofs Within Proofs

Here's a way to use 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.

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 add_comm should do the trick! *)
  rewrite add_comm.
  (* Doesn't work... Coq rewrites the wrong plus! :-( *)
Abort.

To use add_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 add_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 add_comm. reflexivity. }
  rewrite H. reflexivity. Qed.

Formal vs. Informal Proof

"_Informal proofs are algorithms; formal proofs are code."
An unreadable formal proof:
Theorem add_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 clearer...
Theorem add_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 that
              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 now show that
              (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.