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
From LF Require Export Basics.
Proof by Induction
Theorem plus_n_O_firsttry : ∀n:nat,
n = n + 0.
Proof.
intros n.
simpl. (* Does nothing! *)
Abort.
n = n + 0.
Proof.
intros n.
simpl. (* Does nothing! *)
Abort.
Theorem plus_n_O_secondtry : ∀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.
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.
- 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 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.
Theorem minus_diag : ∀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 plus_comm : ∀n m : nat,
n + m = m + n.
Proof.
(* FILL IN HERE *) Admitted.
n + m = m + n.
Proof.
(* FILL IN HERE *) Admitted.
Proofs Within Proofs
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.
(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 plus_comm should do the trick! *)
rewrite → plus_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 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.
(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."
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.
n + (m + p) = (n + m) + p.
Proof. intros n m p. induction n as [| n' IHn']. reflexivity.
simpl. rewrite → IHn'. reflexivity. Qed.
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.
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 fromS (n' + (m + p)) = S ((n' + m) + p),which is immediate from the induction hypothesis. Qed.
- First, suppose n = 0. We must show