Require Export Basics.
(** ** Last lecture:
- Introductions
- Logistics
- Piazza
- First homework due today (!)
- Functional programming
- [Inductive] type definitions
- pattern matching
- recursive functions
- Basic Coq tactics
- [simpl]
- [reflexivity]
- [intros]
- [rewrite]
- [destruct]
- Induction
- On recursively defined functions (e.g., over booleans)
- On natural numbers (type nat)
- [induction] tactic
*)
(** 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.
Proof. admit. Qed.
(** What about the next one?
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: forall b, (orb true b) = true.
Proof. admit. Qed.
(** What if we change the order of the arguments of [orb]?
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: forall b, (orb b true) = true.
Proof. admit. Qed.
(** What about this one?
(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 : forall n : nat, 0 + n = n.
Proof. admit. Qed.
(** What about this?
(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 : forall n : nat, n + 0 = n.
Proof. admit. Qed.
(** We went over this in class last time. Let's do it again
now, to get the hang of using induction and the other
tactics. *)
Theorem plus_n_O : forall n:nat, n = n + 0.
Proof. admit. Qed.
(** Here's another inductive proof we can try. *)
Theorem leb_refl : forall n:nat,
true = leb n n.
Proof.
(* FILL IN HERE *) Admitted.
(** ********************************************************************** *)
(** 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' : forall n m : nat,
(0 + n) * m = n * m.
Proof.
intros n m.
assert (H: 0 + n = n). { reflexivity. }
rewrite -> H.
reflexivity. Qed.
Theorem plus_comm : forall n m : nat,
n + m = m + n.
Proof.
intros n m. induction m as [| m' IHm'].
- (* m = 0 *)
simpl. rewrite <- plus_n_O. reflexivity.
- (* m = S m' *)
simpl. rewrite <- IHm'. rewrite <- plus_n_Sm.
reflexivity. Qed.
(** The [assert] tactic is 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 : 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)...
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 to, 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.