(** * 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 *)

(* 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 *)

(* 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 *)

(* 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 *)

(* 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.
*)
(* /QUIZ *)

(* ################################################################# *)
(** * Separate Compilation *)

(** First type [coqc Datatypes.v] into the terminal to compile
    [Datatypes.v] into [Datatypes.vo] so it can be imported here. Note
    that you may need to remove the [From LF] from the following line:
    *)

From LF Require Export Datatypes.

(* ################################################################# *)
(** * Proof by Recursion *)

(** Clearly, for many proofs about infinite datatypes (natural numbers
    included) our existing tactics will be insufficient. Consider for
    instance the claim that that every number is either even or
    odd. Proving this by case analysis is clearly impossible: There
    are (countably) infinitely many natural numbers! Let's start by
    stating our desired theorem. *)

Inductive Even : nat -> Prop :=
| E_O : Even 0
| E_S : forall n, Odd n -> Even (S n)

with Odd : nat -> Prop :=
| O_S : forall n, Even n -> Odd (S n).

(** We just wrote a "mutually inductive" definition.  In short, it
    says that [O] is [Even], the successor of an [Odd] number is
    [Even] and then successor of an [Even] number is [Odd]. *)

(** So let's try proving our lemma! *)

Lemma Even_or_Odd : forall (n : nat), Even n \/ Odd n.
Proof.
  Abort.

(* But the proof of Even_or_Odd is actually quite easy to program! *)

Fixpoint Even_or_Odd (n : nat) : Even n \/ Odd n 
  (* WORK IN CLASS *). Admitted.

(** As we've seen, writing entire proofs in the programming language
    can be quite hard. Fortunately, there is a simply program that 
    makes these proofs easy. *)

Print nat_ind.

(** nat_ind takes three arguments:

    1) A proposition [P] over natural numbers
    2) A proof of [P O] 
    3) A proof that [P n -> P (S n)]. 

    and it constructs a recursive proof that for any n, P n. *)

(** Coq automatically generates these "induction schemes" whenever we
    define an [Inductive] type, and applies them when we use the
    keyword [induction]. Let's try using it to prove Even_Or_Odd
    again: **)

Lemma Even_or_Odd' (n : nat) : Even n \/ Odd n.
Proof.
  induction n.
  - apply or_introl.
    apply E_O.
  - destruct IHn as [He | Ho].
    + apply or_intror. apply O_S. apply He.
    + apply or_introl. apply E_S. apply Ho.
Defined.

(** Let's take a look at the generated term: *)

Print Even_or_Odd'.

Eval compute in Even_or_Odd'.

(* ################################################################# *)
(** * Proof by Induction *)

(** Let's jump to some less contrived examples of induction in general. 
    These will tend to use rewriting, so trying to write a fixpoint will
    get pretty hairy. Let's start with finally proving that 0 is a right 
    identity for addition. *)

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 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.

(** 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.

(* Of course, in this instance we can take a more direct 
   route by simply providing plus_comm with the desired 
   arguments: *)

Theorem plus_rearrange' : forall n m p q : nat,
  (n + m) + (p + q) = (m + n) + (p + q).
Proof.
  intros n m p q.
  rewrite (plus_comm m n).
  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 a bit 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_. *)


(* ################################################################# *)
(** * Homework *)

(** Let's define "Less than" as an inductive Prop on natural numbers *)

Inductive Lt : nat -> nat -> Prop :=
| lt01           : Lt 0 (S 0)
| ltS (m n : nat)  : Lt m n -> Lt m (S n)                   
| ltSS (m n : nat) : Lt m n -> Lt (S m) (S n).                   

Arguments ltS {m n}.
Arguments ltSS {m n}.

(** We can use this, for instance, to prove that 2 is less then 4 *)

Lemma Lt_2_4 : Lt 2 4.
Proof.
(* WORK IN CLASS *) Admitted.

(** **** Exercise: 3 stars (Lt_0_S)  *) 
(** Prove that 0 is less than the successor of any number recursively
    using Coq's programming language *)

Fixpoint Lt_0_S (n : nat) : Lt 0 (S n)
  (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.

(** [] *)

(** **** Exercise: 3 stars (Lt_0_S')  *) 
(** Now prove the same thing using the proof assistant *)
Lemma Lt_0_S' : forall n, Lt 0 (S n).
Proof.
  (* FILL IN HERE *) Admitted.

(** [] *)


(* ################################################################# *)
(** * More Exercises *)

(** **** Exercise: 3 stars, recommended (mult_comm)  *)
(** Hint: You shouldn't need to use induction on [plus_swap].  You may
          wish to use [assert] or rewrite using a lemma with arguments
          *)

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
    need to define and prove a separate subsidiary theorem to be used
    in the proof of this one.  You may find that [plus_swap] comes in
    handy.) *)

Theorem mult_comm : forall m n : nat,
  m * n = n * m.
Proof.
  (* FILL IN HERE *) Admitted.
(** [] *)

(** **** Exercise: 3 stars, 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, optional (eqb_refl)  *)
(** Prove the following theorem.  (Putting the [true] on the left-hand
    side of the equality may look odd, but this is how the theorem is
    stated in the Coq standard library, so we follow suit.  Rewriting
    works equally well in either direction, so we will have no problem
    using the theorem no matter which way we state it.) *)

Theorem eqb_refl : forall n : nat,
  true = (n =? n).
Proof.
  (* FILL IN HERE *) Admitted.
(** [] *)


(* NEW NAME *)
Notation zero_neqb_S := zero_nbeq_S (only parsing).
Notation S_neqb_0 := S_nbeq_0 (only parsing).
Notation plus_leb_compat_l := plus_ble_compat_l (only parsing).