InductionProof by Induction

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

Use coqc from command line or Compile Buffer from CoqIDE to compile Basics.v into Basics.vo so it can be imported here...

Require Export Basics.

Naming Cases

From now on, we'll use the Case tactic to mark points in the proof script where we're dealing with different subgoals generated by destruct (and other tactics like induction, which we'll see shortly):

Theorem andb_true_elim1 : ∀b c : bool,
  andb b c = true → b = true.
Proof.
  intros b c H.
  destruct b.
  Case "b = true". (* <----- here *)
    reflexivity.
  Case "b = false". (* <---- and here *)
    rewrite ← H.
    reflexivity.
Qed.

Proof by Induction

We proved last time that 0 is a neutral element for + on the left using just reflexivity. The fact that it is also a neutral element on the right is a little harder to show:

Theorem plus_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, but in the branch where n = S n' for some n' we get stuck in exactly the same way. We could use destruct n' to get one step further, but since n can be arbitrarily large, if we try to keep on like this we'll never be done.

Theorem plus_0_r_secondtry : ∀n:nat,
  n + 0 = n.
Proof.
  intros n. destruct n as [| n'].
  Case "n = 0".
    reflexivity. (* so far so good... *)
  Case "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.

In Coq's "goal-directed" style of reasoning, we begin with the goal of proving P(n) for all n and break it down (by applying the induction tactic) into two separate subgoals: first showing P(O) and then showing P(n') → P(S n'). For example...

Theorem plus_0_r : ∀n:nat, n + 0 = n.
Proof.
  intros n. induction n as [| n'].
  Case "n = 0". reflexivity.
  Case "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.

Another result, which we'll need in a moment, that can be proved by induction (left as an exercise).

Theorem plus_comm : ∀n m : nat,
n + m = m + n.
Proof.
(* FILL IN HERE *) Admitted.

We've seen that there are goals that destruct can't solve but induction can. What about the other way around? Are there steps in a proof that can be solved by pure case analysis (destruct) but not using induction?

(1) No

(2) Yes

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).
    Case "Proof of assertion". reflexivity.
  rewrite → H.
  reflexivity. Qed.

Actually, assert will turn out to be handy in many sorts of situations. For example, suppose we want to prove that (n + m) + (p + q) = (m + n) + (p + q). The only difference between the two sides of the = is that the arguments m and n to the first inner + are swapped, so it seems we should be able to use the commutativity of addition (plus_comm) to rewrite one into the other. However, the rewrite tactic is a little stupid about where it applies the rewrite. There are three uses of + here, and it turns out that doing rewrite → plus_comm will affect only the outer one.

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)...
     it seems like plus_comm should do the trick! *)
  rewrite → plus_comm.
  (* Doesn't work...Coq rewrote the wrong plus! *)
Abort.

To get plus_comm to apply at the point where we want 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 this lemma 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).
    Case "Proof of assertion".
    rewrite → plus_comm. reflexivity.
  rewrite → H. reflexivity. Qed.

(* $Date: 2013-07-17 16:19:11 -0400 (Wed, 17 Jul 2013) $ *)