(* Lists and higher-order functions
   Version of 1/21/2009
*)

(* This line imports all of our definitions from Basics.v.
For it to work, you need to compile Basics.v into
Basics.vo.  (This is like making a .class file from a
.java file, or a .o file from a .c file.)

Here are two ways to compile your code:

  - CoqIDE

    1. Open Basics.v.
    2. In the "Compile" menu, click on "Compile Buffer".

  - Command line

    1. Run: coqc Basics.v

*)
Require Export Basics.

(* ----------------------------------------------------------------------- *)
(* Administrivia *)

(* Is everyone on the course mailing list? *)

(* Remember: This homework due Monday, not Wednesday *)

(* ----------------------------------------------------------------------- *)
(* Formal vs. informal proof *)

(* An unreadable formal proof *)
Theorem plus_assoc' : forall n m p : nat,
  plus n (plus m p) = plus (plus n m) p.
Proof. intros n m p. induction n as [| n']. reflexivity. 
simpl. rewrite -> IHn'. reflexivity. Qed.

(* A careful informal proof of the same theorem:

   By induction on n.
     - First, suppose n = 0.  We must show
         plus 0 (plus m p) = plus (plus 0 m) p.
       This follows directly from the definition of plus.
     - Next, suppose n = S n', with
         plus n' (plus m p) = plus (plus n' m) p.
       We must show
         plus (S n') (plus m p) = plus (plus (S n') m) p.
       By the definition of plus, this follows from
         S (plus n' (plus m p)) = S (plus (plus n' m) p),
       which is immediate from the induction hypothesis.
*)

(* As an exercise, try translating this solution from last week into
   an informal proof: *)
Theorem plus_comm' : forall n m : nat,
  plus n m = plus m n.
Proof.
  intros n m. induction m as [| m'].
  Case "m = 0".
    simpl. rewrite -> plus_n_O. reflexivity.
  Case "m = S m'".
    simpl. rewrite <- IHm'. rewrite <- plus_n_Sm.
    reflexivity.
Qed.

(* Informal proof:
Theorem: plus is commutative.
Proof:
   (* EXERCISE... *)
   Let natural numbers n and m be given.  We show plus n m = plus m n
   by induction on m.
     - First, suppose m = 0.  By the definition of plus, plus 0 n = 0.
       More, we have already shown (lemma plus_n_0) that plus n 0 = 0.
       Thus, plus n 0 = plus 0 n.

     - Next, suppose m = S m' for some m' such that plus n m' = plus m' n.
       By the definition of plus and the inductive hypothesis, 
       plus (S m') n = S (plus m' n) = S (plus n m').  It
       remains to show plus n (S m') = S (plus n m') as well, but
       this is precisely lemma plus_n_Sm.
   (* ...TO HERE *)
*)

(* Exercise: write a formal proof of the following theorem, using
   the provided informal proof as a guide

Theorem : For any n, true = beq_nat n n
Proof :
   By induction on n.
     - First, suppose n = 0.  We must show
         true = beq_nat n n.
       This follows directly from the definitions of beq_nat.
     - Next, suppose n = S n', with
         true = beq_nat n' n'.
       We must show
         true = beq_nat (S n') (S n')
       This follows directly from the IH and with the
       definition beq_nat.
*)

Theorem beq_nat_refl : forall n : nat,
  true = beq_nat n n.
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

(* -------------------------------------------------------------- *)
(* Pairs of numbers *)

(* Technical note: Here, we again use the Module feature
   to wrap all of the definitions for pairs and lists of
   numbers in a module so that, later, we can use the same
   names for the generic ("polymorphic") versions of the
   same operations. *)
Module NatList.

Inductive natprod : Set :=
  pair : nat -> nat -> natprod.

Definition fst (p : natprod) : nat := 
  match p with
  | pair x y => x
  end.
Definition snd (p : natprod) : nat := 
  match p with
  | pair x y => y
  end.

Notation "( x , y )" := (pair x y).

Eval simpl in (fst (3,4)).

Definition fst' (p : natprod) : nat := 
  match p with
  | (x,y) => x
  end.
Definition snd' (p : natprod) : nat := 
  match p with
  | (x,y) => y
  end.

Definition swap_pair (p : natprod) : natprod := 
  match p with
  | (x,y) => (y,x)
  end.

(* Let's try and prove a few simple facts about pairs.
   If we state the lemmas in a particular way, we can prove them
   with just partial evaluation
 *)
Theorem surjective_pairing' : forall (n m : nat),
  (n,m) = (fst (n,m), snd (n,m)).
Proof.
  reflexivity.
Qed.

(* But that's not enough if we state the lemma in a more natural way: *)
Theorem surjective_pairing_stuck : forall (p : natprod),
  p = (fst p, snd p).
Proof.
  simpl. (* Doesn't reduce anything! *)
Admitted.

(* We have to expose the structure of p so that simple can perform
   the pattern match in fst and snd.

   Notice that, unlike for nats, destruct doesn't generate
   an extra subgoal here.  That's because natprods can
   only be constructed in one way.  
*)
Theorem surjective_pairing : forall (p : natprod),
  p = (fst p, snd p).
Proof.
  intros p.  destruct p as (n,m).  simpl.  reflexivity.
Qed.
(* Notice that Coq allows us to use the notation we
   introduced for pairs in the "as..." pattern telling it
   what variables to bind. *)

Theorem snd_fst_is_swap : forall (p : natprod),
  (snd p, fst p) = swap_pair p.
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

Theorem fst_swap_is_snd : forall (p : natprod),
  fst (swap_pair p) = snd p.
Proof.
  (* OPTIONAL EXERCISE *) Admitted.

(* -------------------------------------------------------------- *)
(* Lists of numbers *)

Inductive natlist : Set :=
  | nil : natlist
  | cons : nat -> natlist -> natlist.

Definition l123 := cons 1 (cons 2 (cons 3 nil)).

Notation "x :: l" := (cons x l) (at level 60, right associativity).
Notation "[ ]" := nil.
Notation "[ x , .. , y ]" := (cons x .. (cons y nil) ..).

Definition l123'   := 1 :: (2 :: (3 :: nil)).
Definition l123''  := 1 :: 2 :: 3 :: nil.
Definition l123''' := [1,2,3].

Fixpoint repeat (n count : nat) {struct count} : natlist := 
  match count with
  | O => nil
  | S count' => n :: (repeat n count')
  end.

Fixpoint length (l:natlist) {struct l} : nat := 
  match l with
  | nil => O
  | h :: t => S (length t)
  end.

Definition hd (l:natlist) : nat :=
  match l with
  | nil => 0  (* arbitrarily *)
  | h :: t => h
  end.

Definition tl (l:natlist) : natlist :=
  match l with
  | nil => nil  
  | h :: t => t
  end.

Fixpoint app (l1 l2 : natlist) {struct l1} : natlist := 
  match l1 with
  | nil    => l2
  | h :: t => h :: (app t l2)
  end.

Notation "x ++ y" := (app x y) 
                     (right associativity, at level 60).

Example test_app1:             [1,2,3] ++ [4,5] = [1,2,3,4,5].
Proof. reflexivity. Qed.
Example test_app2:             nil ++ [4,5] = [4,5].
Proof. reflexivity. Qed.
Example test_app3:             [1,2,3] ++ nil = [1,2,3].
Proof. reflexivity. Qed.

(* -------------------------------------------------------------- *)
(* Exercise: Bags via lists *)
Definition bag := natlist.  

(** <<
Fixpoint count (v:nat) (s:bag) {struct s} : nat := 
  FILL IN HERE (OPTIONALLY)

Example test_count1:              count 1 [1,2,3,1,4,1] = 3.
Proof. reflexivity. Qed.
Example test_count2:              count 6 [1,2,3,1,4,1] = 0.
Proof. reflexivity. Qed.

Definition union := 
  FILL IN HERE (OPTIONALLY)

Example test_union1:              count 1 (union [1,2,3] [1,4,1]) = 3.
Proof. reflexivity. Qed.

Definition add (v:nat) (s:bag) : bag := 
  FILL IN HERE (OPTIONALLY)

Example test_add1:                count 1 (add 1 [1,4,1]) = 3.
Proof. reflexivity. Qed.
Example test_add2:                count 5 (add 1 [1,4,1]) = 0.
Proof. reflexivity. Qed.

Definition member (v:nat) (s:bag) : bool := 
  FILL IN HERE (OPTIONALLY)

Example test_member1:             member 1 [1,4,1] = true.
Proof. reflexivity. Qed.
Example test_member2:             member 2 [1,4,1] = false.
Proof. reflexivity. Qed.

Fixpoint remove_one (v:nat) (s:bag) {struct s} : bag :=
  FILL IN HERE (OPTIONALLY)

Example test_remove_one1:         count 5 (remove_one 5 [2,1,5,4,1]) = 0.
Proof. reflexivity. Qed.
Example test_remove_one2:         count 5 (remove_one 5 [2,1,4,1]) = 0.
Proof. reflexivity. Qed.
Example test_remove_one3:         count 4 (remove_one 5 [2,1,4,5,1,4]) = 2.
Proof. reflexivity. Qed.
Example test_remove_one4: 
  count 5 (remove_one 5 [2,1,5,4,5,1,4]) = 1.
Proof. reflexivity. Qed.

Fixpoint remove_all (v:nat) (s:bag) {struct s} : bag :=
  FILL IN HERE (OPTIONALLY)

Example test_remove_all1:          count 5 (remove_all 5 [2,1,5,4,1]) = 0.
Proof. reflexivity. Qed.
Example test_remove_all2:          count 5 (remove_all 5 [2,1,4,1]) = 0.
Proof. reflexivity. Qed.
Example test_remove_all3:          count 4 (remove_all 5 [2,1,4,5,1,4]) = 2.
Proof. reflexivity. Qed.
Example test_remove_all4:          count 5 (remove_all 5 [2,1,5,4,5,1,4]) = 0.
Proof. reflexivity. Qed.

Fixpoint subset (s1:bag) (s2:bag) {struct s1} : bool :=
  FILL IN HERE (OPTIONALLY)

Example test_subset1:              subset [1,2] [2,1,4,1] = true.
Proof. reflexivity. Qed.
Example test_subset2:              subset [1,2,2] [2,1,4,1] = false.
Proof. reflexivity. Qed.
>> *)

(* ---------------------------------------------------------- *)
(* Reasoning about lists *)

(* Just like with numbers, we can do some proofs about
   lists using just "partial evaluation"... *)
Theorem nil_app : forall l:natlist,
  [] ++ l = l.
Proof.
   reflexivity.
Qed.

(* And, also like numbers, sometimes it helps to do case
   analysis on the structure of the list. Here, we give
   coq two names for the cons case - one for the first
   element of the list and the other for the tail of the
   list. *)
Theorem tl_length_pred : forall l:natlist,
  pred (length l) = length (tl l).
Proof.
  intros l. destruct l as [| n l'].
  Case "l = nil".
    reflexivity.
  Case "l = cons n l'".
    reflexivity.
Qed.
(* The [nil] case works because we've chosen (tl nil = nil). *)

(* ---------------------------------------------------- *)
(* Induction on lists *)

(* We can do induction on any inductively defined type,
   not just numbers: Coq generates an appropriate
   induction principle when it processes the [Inductive]
   declaration.

   Here is the induction principle for lists:

     If [P l] is some proposition involving a natlist l,
     and we want to show that P holds for all l, we can
     reason like this:
        - show that P [] holds
        - show that, for any element n:nat and any natlist
          l', if [P l'] holds, then so does [P (n::l')]
        - conclude that [P l] holds for all natlists l.
*)

Theorem ass_app : forall l1 l2 l3 : natlist, 
  l1 ++ (l2 ++ l3) = (l1 ++ l2) ++ l3.   
Proof.
  intros l1 l2 l3. induction l1 as [| n l1'].
  Case "l1 = nil".
    reflexivity.
  Case "l1 = cons n l1'".
    simpl. rewrite -> IHl1'. reflexivity.
Qed.

(* An exercise to be worked together: *)
Theorem app_length : forall l1 l2 : natlist,
  length (l1 ++ l2) = plus (length l1) (length l2).
Proof.
  (* OPTIONAL EXERCISE *) Admitted.

(* Exercises *)
(** <<
Fixpoint nonzeros (l:natlist) {struct l} : natlist :=
  FILL IN HERE

Example test_nonzeros:            nonzeros [0,1,0,2,3,0,0] = [1,2,3].
Proof. reflexivity. Qed.

Fixpoint oddmembers (l:natlist) {struct l} : natlist :=
  FILL IN HERE

Example test_oddmembers:            oddmembers [0,1,0,2,3,0,0] = [1,3].
Proof. reflexivity. Qed.

Fixpoint countoddmembers (l:natlist) {struct l} : nat :=
  FILL IN HERE

Example test_countoddmembers1:    countoddmembers [1,0,3,1,4,5] = 4.
Proof. reflexivity. Qed.
Example test_countoddmembers2:    countoddmembers [0,2,4] = 0.
Proof. reflexivity. Qed.
Example test_countoddmembers3:    countoddmembers nil = 0.
Proof. reflexivity. Qed.

Fixpoint alternate (l1 l2 : natlist) {struct l1} : natlist :=
  FILL IN HERE

Example test_alternate1:        alternate [1,2,3] [4,5,6] = [1,4,2,5,3,6].
Proof. reflexivity. Qed.
Example test_alternate2:        alternate [1] [4,5,6] = [1,4,5,6].
Proof. reflexivity. Qed.
Example test_alternate3:        alternate [1,2,3] [4] = [1,4,2,3].
Proof. reflexivity. Qed.
>> *)

(* snoc inserts an element at the end of a list *)
Fixpoint snoc (l:natlist) (v:nat) {struct l} : natlist := 
  match l with
  | nil    => [v]
  | h :: t => h :: (snoc t v)
  end.

(* We can use snoc to reverse a list *)
Fixpoint rev (l:natlist) {struct l} : natlist := 
  match l with
  | nil    => nil
  | h :: t => snoc (rev t) h
  end.

Example test_rev1:            rev [1,2,3] = [3,2,1].
Proof. reflexivity. Qed.
Example test_rev2:            rev nil = nil.
Proof. reflexivity. Qed.

(* Now some more list theorems using our newly defined snoc and rev.
   Let's try something a little more intricate: proving that reversing
   a list does not change its length.  Our first attempt at this proof
   gets stuck in the successor case... *)
Theorem rev_length_firsttry : forall l : natlist,
  length (rev l) = length l.
Proof.
  intros l. induction l as [| n l'].
  Case "l = nil".
    reflexivity.
  Case "l = cons".
    simpl. (* Here we get stuck: the goal is an equality
              involving [snoc], but we don't have any equations
              in either the immediate context or the global
              environment that have anything to do with
              [snoc]! *)
Admitted.

(* So let's take the equation about snoc that would have
   enabled us to make progress and prove it as a separate
   lemma. *)
Theorem length_snoc : forall n : nat, forall l : natlist,
  length (snoc l n) = S (length l).
Proof.
  intros n l. induction l as [| n' l'].
  Case "l = nil".
    reflexivity.
  Case "l = cons n' l'".
    simpl. rewrite -> IHl'. reflexivity.
Qed. 

(* Now we can complete the original proof. *)
Theorem rev_length : forall l : natlist,
  length (rev l) = length l.
Proof.
  intros l. induction l as [| n l'].
  Case "l = nil".
    reflexivity.
  Case "l = cons".
    simpl. rewrite -> length_snoc. rewrite -> IHl'. reflexivity.
Qed. 

(* ------------------------------------------------------- *)
(* A bunch of exercises... *)

Theorem app_nil_end : forall l : natlist, 
  l ++ [] = l.   
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

Theorem rev_involutive : forall l : natlist,
  rev (rev l) = l.
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

Theorem distr_rev : forall l1 l2 : natlist,
  rev (l1 ++ l2) = (rev l2) ++ (rev l1).
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

(* There is a short solution to the next exercise.  If you
   find yourself getting tangled up, step back and try to
   look for a simpler way... *)
Theorem ass_app4 : forall l1 l2 l3 l4 : natlist,
  l1 ++ (l2 ++ (l3 ++ l4)) = ((l1 ++ l2) ++ l3) ++ l4.
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

Theorem snoc_append : forall (l:natlist) (n:nat),
  snoc l n = l ++ [n].
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

Theorem append_snoc : forall l1 l2 : natlist, forall n : nat,
  ((snoc l1 n) ++ l2) = l1 ++ (n :: l2).
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

(* ------------------------------------------------------- *)
(* A couple more exercises *)

(* Design exercise: 
     - Write down a non-trivial theorem involving cons (::),
       snoc, and append (++).
     - Prove it. 

FILL IN HERE
*) 

(* An exercise about your implementation of nonzeros *)
(** <<
Lemma nonzeros_length : forall l1 l2 : natlist,
  nonzeros (l1 ++ l2) = (nonzeros l1) ++ (nonzeros l2).
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

>> *)

(* If you did the optional exercise about bags above, here
   are a couple of little theorems to prove about your
   definitions *)
(** <<
Theorem count_member_nonzero : forall (s : bag),
  ble_nat 0 (count 1 (1 :: s)) = true.
Proof.
  (* OPTIONAL EXERCISE *) Admitted.

(* The following lemma about ble_nat might help you below *)
Theorem ble_n_Sn : forall n,
  ble_nat n (S n) = true.
Proof.
  intros n. induction n as [| n'].
  Case "0".  
    simpl.  reflexivity.
  Case "S n'".
    simpl.  rewrite IHn'.  reflexivity.
Qed.

Theorem remove_decreases_count: forall (s : bag),
  ble_nat (count 0 (remove_one 0 s)) (count 0 s) = true.
Proof.
  (* OPTIONAL EXERCISE *) Admitted.

>> *)

(* -------------------------------------------------------------- *)
(* Options *)

Inductive natoption : Set :=
  | Some : nat -> natoption
  | None : natoption.  

Fixpoint index_bad (n:nat) (l:natlist) {struct l} : nat :=
  match l with
  | nil => 42  (* arbitrary! *)
  | a :: l' => match beq_nat n O with 
               | true => a 
               | false => index_bad (pred n) l' 
               end
  end.

Fixpoint index (n:nat) (l:natlist) {struct l} : natoption :=
  match l with
  | nil => None 
  | a :: l' => match beq_nat n O with 
               | true => Some a
               | false => index (pred n) l' 
               end
  end.

Example test_index1 :    index 0 [4,5,6,7]  = Some 4.
Proof. reflexivity. Qed.
Example test_index2 :    index 3 [4,5,6,7]  = Some 7.
Proof. reflexivity. Qed.
Example test_index3 :    index 10 [4,5,6,7] = None.
Proof. reflexivity. Qed.

Fixpoint index' (n:nat) (l:natlist) {struct l} : natoption :=
  match l with
  | nil => None 
  | a :: l' => if beq_nat n O then Some a else index (pred n) l'
  end.

(* This function pulls the nat out of a natoption,
   returning a supplied default in the None case. *)
Definition option_elim (o : natoption) (d : nat) : nat :=
  match o with
  | Some n' => n'
  | None => d
  end.

(* Using the same idea, fix the hd function from earlier so
   we don't have to return an arbitrary element *)
(** <<
Definition hd_opt (l : natlist) : natoption :=
  FILL IN HERE

Example test_hd_opt1 : hd_opt [] = None.
Proof. reflexivity. Qed.

Example test_hd_opt2 : hd_opt [1] = Some 1.
Proof. reflexivity. Qed.

Example test_hd_opt3 : hd_opt [5,6] = Some 5.
Proof. reflexivity. Qed.

(* An exercise relating your new hd_opt to the old hd *)
Theorem option_elim_hd : forall l:natlist,
  hd l = option_elim (hd_opt l) 0.
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

>> *)

(* Another functional programming exercise *)
(** <<
Fixpoint beq_natlist (l1 l2 : natlist) {struct l1} : bool :=
  FILL IN HERE

Example test_beq_natlist1 :   (beq_natlist nil nil = true).
Proof. reflexivity. Qed.
Example test_beq_natlist2 :   beq_natlist [1,2,3] [1,2,3] = true.
Proof. reflexivity. Qed.
Example test_beq_natlist3 :   beq_natlist [1,2,3] [1,2,4] = false.
Proof. reflexivity. Qed.

Theorem beq_natlist_refl : forall l:natlist,
  beq_natlist l l = true.
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

>> *)

(* ----------------------------------------------------- *)
(* The [apply] tactic *)

(* We often encounter situations where the goal to be proved
   is exactly the same as some hypothesis in the context or
   some previously proved lemma. *)
Theorem silly1 : forall (n m o p : nat),
     n = m 
  -> [n,o] = [n,p]
  -> [n,o] = [m,p].
Proof.
  intros n m o p eq1 eq2.
  rewrite <- eq1.
  (* At this point, we could finish with [rewrite ->
     eq2. reflexivity.] as we have done several times above.
     But we can achieve the same effect in a single step by
     using the [apply] tactic instead: *)
  apply eq2.
Qed.

(* The [apply] tactic also works with CONDITIONAL hypotheses
   and lemmas: if the statement being applied is an
   implication, then the premises of this implication will
   be added to the list of subgoals needing to be proved. *)
Theorem silly2 : forall (n m o p : nat),
     n = m 
  -> (forall (q r : nat), q = r -> [q,o] = [r,p])
  -> [n,o] = [m,p].
Proof.
  intros n m o p eq1 eq2.
  apply eq2. apply eq1.
Qed.
(* You may find it instructive to experiment with this proof
   and see if there is a way to complete it using just
   [rewrite] instead of [apply]. *)

(* Typically, when we use [apply H], the statement [H] will
   begin with a [forall] binding some "universal variables."
   When Coq matches the current goal against the conclusion
   of [H], it will try to find appropriate values for these
   variables.  For example, when we do [apply eq2] in in the
   following proof, the universal variable [q] in [eq2] gets
   instantiated with [(m,m)] and [r] gets instantiated with
   [(n,n)]. *)
Theorem silly2a : forall (n m : nat),
     (n,n) = (m,m) 
  -> (forall (q r : nat), (q,q) = (r,r) -> [q] = [r])
  -> [n] = [m].
Proof.
  intros n m eq1 eq2.
  apply eq2. apply eq1.
Qed.

(* Exercise: Complete the following proof without using
   [simpl]. *)
Theorem silly_ex : 
     (forall n, evenb n = true -> oddb (S n) = true)
  -> evenb 3 = true
  -> oddb 4 = true.
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

(* To use the [apply] tactic, the (conclusion of the) fact
   being applied must match the goal EXACTLY -- for example,
   [apply] will not work if the left and right sides of the
   equality are swapped. *)
Theorem silly3_firsttry : forall (n : nat),
     true = beq_nat n 5 
  -> beq_nat (S (S n)) 7 = true.
Proof.
  intros n H.
  simpl.
  (* here we are stuck *)
Admitted.

(* When you find yourself in such a situation, one thing
   to do is to go back and try reorganizing the statement
   of whatever you are trying to prove so that things
   appear the right way around when they are needed.  But
   if this is not possible or convenient, then the
   following lemma can be used to swap the sides of an
   equality statement in the goal so that some other lemma
   can be applied. *)
Theorem sym_eq_bool : forall (b c : bool),
  b = c -> c = b.
Proof.
  intros b c H. rewrite -> H. reflexivity.
Qed.

Theorem silly3 : forall (n : nat),
     true = beq_nat n 5 
  -> beq_nat (S (S n)) 7 = true.
Proof.
  intros n H.
  apply sym_eq_bool. (* NOTE that, just as with [rewrite],
                        we can [apply] a lemma, 
                        not just an assumption in the context *)
  simpl.             (* Actually, this line is unnecessary, since *)
  apply H.           (* [apply] will do a [simpl] step first. *)
Qed.

(* Here are two exercises for you *)

Theorem rev_exercise1 : forall (l l' : natlist),
     l = rev l'
  -> l' = rev l.
Proof.
  (* Remember you can use [apply] with previously defined lemmas, 
     not just hypotheses in the context. *)
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

(* This one is a little tricky.  The first line of the
   proof is provided, because it uses an idea we haven't
   seen before.  Notice that we don't introduce m before
   performing induction.  This leave it general, so that
   the IH doesn't specify a particular m, but lets us
   pick.  We'll talk more about this later in the course.
*)
Theorem beq_nat_sym : forall n m b,
  beq_nat n m = b -> beq_nat m n = b.
Proof.
  intros n. induction n as [| n'].
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

(* As an exercise, also provide an informal proof of this 
   lemma: 

   Informal proof of beq_nat_sym:
   Theorem:  For any nats n m and bool b, if beq_nat n m = b
   then beq_nat m n = b.

   Proof:
   (* EXERCISE... *)
   Let an arbitrary nat n be given.  We go by induction on
   n.

   For the base case, we have n = 0.  Let m and b be given
   and assume beq_nat 0 m = b.  Either m = 0 or not.  In
   the first case, we must show beq_nat 0 0 = b which is
   exactly the assumption.  In the second case, m = S m'
   for some m'.  By our assumption, it's enough to show
   beq_nat (S m') 0 = beq_nat 0 (S m'), and by the
   definition of beq_nat both are false.

   In the inductive case, we have n = S n' for some n'.
   Let m and b be given and assume beq_nat (S n') m = b.
   Our IH is that, for any m and b, beq_nat n' m = b ->
   beq_nat m n = b. We go by cases on m.

   Suppose first m = 0.  By the assumption, it's enough to
   show beq_nat 0 (S n') = beq_nat (S n') 0.  By the
   definition of beq_nat, both sides are false.

   Otherwise, m = S m' for some m'.  By the assumption,
   it's enough to show:
     beq_nat (S m') (S n') = beq_nat (S n') (S m')
   And, by the definition of beq_nat, this reduces to
   showing:
     beq_nat m' n' = beq_nat n' m'.

   Picking m = m' and b = beq_nat n' m' in the 
   inductive hypothesis gives:
     beq_nat n' m' = beq_nat n' m -> 
     beq_nat m' n' = beq_nat n' m'.
   The premise is trivial, and the conclusion is exactly
   what we wanted to show.
   (* ...TO HERE *)

 *)

(* Give an alternate proof of the associativity of ++ with
   a more general induction hypothesis.  Complete the
   following (leaving the first line unchanged). *)
Theorem ass_app' : forall l1 l2 l3 : natlist, 
  l1 ++ (l2 ++ l3) = (l1 ++ l2) ++ l3.   
Proof.
  intros l1. induction l1 as [ | n l1'].
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

End NatList.

(* Put beq_nat_sym into the top-level namespace, so that we can
   use it later even if we're not importing the Lists
   module. *)
Definition beq_nat_sym := NatList.beq_nat_sym.