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.
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.
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.
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.
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.
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
From LF Require Export Basics.
Proof by Induction
Theorem add_0_r_firsttry : ∀ n:nat,
n + 0 = n.
n + 0 = n.
... gets stuck.
Proof.
intros n.
simpl. (* Does nothing! *)
Abort.
intros n.
simpl. (* Does nothing! *)
Abort.
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.
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.
- 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.
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.
Proof.
intros n. induction n as [| n' IHn'].
- (* n = 0 *) reflexivity.
- (* n = S n' *) simpl. rewrite → IHn'. reflexivity. Qed.
Theorem minus_n_n : ∀ n,
minus n n = 0.
Proof.
(* WORK IN CLASS *) Admitted.
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.
n + m = m + n.
Proof.
(* FILL IN HERE *) Admitted.
Exercise: 2 stars, standard (eqb_refl)
The following theorem relates the computational equality =? on nat with the definitional equality = on bool.
Theorem eqb_refl : ∀ n : nat,
(n =? n) = true.
Proof.
(* FILL IN HERE *) Admitted.
☐
(n =? n) = true.
Proof.
(* FILL IN HERE *) Admitted.
☐
Exercise: 2 stars, standard, optional (even_S)
Here's a useful theorem that proves n-1 is not even if n is 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.
☐
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.Proofs Within Proofs
Theorem mult_0_plus' : ∀ n m : nat,
(n + 0 + 0) × m = n × m.
Proof.
intros n m.
assert (H: n + 0 + 0 = n).
{ rewrite add_comm. simpl. rewrite add_comm. reflexivity. }
rewrite → H.
reflexivity. Qed.
(n + 0 + 0) × m = n × m.
Proof.
intros n m.
assert (H: n + 0 + 0 = n).
{ rewrite add_comm. simpl. rewrite add_comm. 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.
(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.
(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."
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.
n + (m + p) = (n + m) + p.
Proof. intros n m p. induction n as [| n' IHn']. reflexivity.
simpl. rewrite IHn'. reflexivity. Qed.
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.
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.
- First, suppose n = 0. We must show that
(* These additional exercises will be used in later chapters. We
don't need to work them in class. *)
don't need to work them in class. *)
Exercise: 3 stars, standard, especially useful (mul_comm)
Use assert to help prove add_shuffle3. You don't need to use induction yet.
Theorem add_shuffle3 : ∀ n m p : nat,
n + (m + p) = m + (n + p).
Proof.
(* FILL IN HERE *) Admitted.
n + (m + p) = m + (n + p).
Proof.
(* FILL IN HERE *) Admitted.
Now prove commutativity of multiplication. You will probably want
to look for (or define and prove) a "helper" theorem to be used in
the proof of this one. Hint: what is n × (1 + k)?
Theorem mul_comm : ∀ m n : nat,
m × n = n × m.
Proof.
(* FILL IN HERE *) Admitted.
☐
m × n = n × m.
Proof.
(* FILL IN HERE *) Admitted.
☐
Exercise: 2 stars, standard, optional (plus_leb_compat_l)
If a hypothesis has the form H: P → a = b, then rewrite H will rewrite a to b in the goal, and add P as a new subgoal. Use that in the inductive step of this exercise.
Check leb.
Theorem plus_leb_compat_l : ∀ n m p : nat,
n <=? m = true → (p + n) <=? (p + m) = true.
Proof.
(* FILL IN HERE *) Admitted.
☐
Theorem plus_leb_compat_l : ∀ n m p : nat,
n <=? m = true → (p + n) <=? (p + m) = true.
Proof.
(* FILL IN HERE *) Admitted.
☐
Exercise: 3 stars, standard, optional (more_exercises)
Take a piece of paper. For each of the following theorems, first think about whether (a) it can be proved using only simplification and rewriting, (b) it also requires case analysis (destruct), or (c) it also requires induction. Write down your prediction. Then fill in the proof. (There is no need to turn in your piece of paper; this is just to encourage you to reflect before you hack!)
Theorem leb_refl : ∀ n:nat,
(n <=? n) = true.
Proof.
(* FILL IN HERE *) Admitted.
Theorem zero_neqb_S : ∀ n:nat,
0 =? (S n) = false.
Proof.
(* FILL IN HERE *) Admitted.
Theorem andb_false_r : ∀ b : bool,
andb b false = false.
Proof.
(* FILL IN HERE *) Admitted.
Theorem S_neqb_0 : ∀ n:nat,
(S n) =? 0 = false.
Proof.
(* FILL IN HERE *) Admitted.
Theorem mult_1_l : ∀ n:nat, 1 × n = n.
Proof.
(* FILL IN HERE *) Admitted.
Theorem all3_spec : ∀ b c : bool,
orb
(andb b c)
(orb (negb b)
(negb c))
= true.
Proof.
(* FILL IN HERE *) Admitted.
Theorem mult_plus_distr_r : ∀ n m p : nat,
(n + m) × p = (n × p) + (m × p).
Proof.
(* FILL IN HERE *) Admitted.
Theorem mult_assoc : ∀ n m p : nat,
n × (m × p) = (n × m) × p.
Proof.
(* FILL IN HERE *) Admitted.
☐
(n <=? n) = true.
Proof.
(* FILL IN HERE *) Admitted.
Theorem zero_neqb_S : ∀ n:nat,
0 =? (S n) = false.
Proof.
(* FILL IN HERE *) Admitted.
Theorem andb_false_r : ∀ b : bool,
andb b false = false.
Proof.
(* FILL IN HERE *) Admitted.
Theorem S_neqb_0 : ∀ n:nat,
(S n) =? 0 = false.
Proof.
(* FILL IN HERE *) Admitted.
Theorem mult_1_l : ∀ n:nat, 1 × n = n.
Proof.
(* FILL IN HERE *) Admitted.
Theorem all3_spec : ∀ b c : bool,
orb
(andb b c)
(orb (negb b)
(negb c))
= true.
Proof.
(* FILL IN HERE *) Admitted.
Theorem mult_plus_distr_r : ∀ n m p : nat,
(n + m) × p = (n × p) + (m × p).
Proof.
(* FILL IN HERE *) Admitted.
Theorem mult_assoc : ∀ n m p : nat,
n × (m × p) = (n × m) × p.
Proof.
(* FILL IN HERE *) Admitted.
☐