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.