(** * Induction: Proof by Induction *)
(* ################################################################# *)
(** * Review *)
(* QUIZ
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.
*)
(* QUIZ
What about the next one?
Theorem review2: forall 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.
*)
(* QUIZ
What if we change the order of the arguments of [orb]?
Theorem review3: forall 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.
*)
(* QUIZ
What about this one?
Theorem review4 : forall 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.
*)
(* QUIZ
What about this?
Theorem review5 : forall 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 *)
(** (We need to first use [coqc] 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 proved in the last chapter that [0] is a neutral element
for [+] on the left using just [reflexivity]. The proof that it
is also a neutral element on the _right_ is trickier... *)
Theorem plus_n_O_firsttry : forall n:nat,
n = n + 0.
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 plus_n_O_secondtry : forall n:nat,
n = n + 0.
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 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.
(** Let's try this one together: *)
Theorem minus_diag : forall 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 : forall n m : nat,
n + m = m + n.
Proof.
(* FILL IN HERE *) Admitted.
(* ################################################################# *)
(** * 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' : forall 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 : forall 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 : 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.
(* ################################################################# *)
(** * Formal vs. Informal Proof *)
(** "_Informal proofs are algorithms; formal proofs are code_." *)
(** An unreadable formal proof: *)
Theorem plus_assoc' : forall 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 plus_assoc'' : forall 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_. *)
(* ################################################################# *)
(** * More Exercises *)
(* These additional exercises will be used in later chapters. We
don't need to work them in class. *)
(** **** Exercise: 3 stars, standard, recommended (mult_comm)
Use [assert] to help prove [plus_swap]. You don't need to
use induction yet. *)
Theorem plus_swap : forall n m p : nat,
n + (m + p) = m + (n + p).
Proof.
(* FILL IN HERE *) Admitted.
(** Now prove commutativity of multiplication. You will probably
want to define and prove a "helper" theorem to be used
in the proof of this one. Hint: what is [n * (1 + k)]? *)
Theorem mult_comm : forall m n : nat,
m * n = n * m.
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!) *)
Check leb.
Theorem leb_refl : forall n:nat,
true = (n <=? n).
Proof.
(* FILL IN HERE *) Admitted.
Theorem zero_nbeq_S : forall n:nat,
0 =? (S n) = false.
Proof.
(* FILL IN HERE *) Admitted.
Theorem andb_false_r : forall b : bool,
andb b false = false.
Proof.
(* FILL IN HERE *) Admitted.
Theorem plus_ble_compat_l : forall n m p : nat,
n <=? m = true -> (p + n) <=? (p + m) = true.
Proof.
(* FILL IN HERE *) Admitted.
Theorem S_nbeq_0 : forall n:nat,
(S n) =? 0 = false.
Proof.
(* FILL IN HERE *) Admitted.
Theorem mult_1_l : forall n:nat, 1 * n = n.
Proof.
(* FILL IN HERE *) Admitted.
Theorem all3_spec : forall b c : bool,
orb
(andb b c)
(orb (negb b)
(negb c))
= true.
Proof.
(* FILL IN HERE *) Admitted.
Theorem mult_plus_distr_r : forall n m p : nat,
(n + m) * p = (n * p) + (m * p).
Proof.
(* FILL IN HERE *) Admitted.
Theorem mult_assoc : forall n m p : nat,
n * (m * p) = (n * m) * p.
Proof.
(* FILL IN HERE *) Admitted.
(** [] *)
(** **** Exercise: 2 stars, standard, optional (eqb_refl) *)
Theorem eqb_refl : forall n : nat,
true = (n =? n).
Proof.
(* FILL IN HERE *) Admitted.
(** [] *)