Assignment03.v

(** **** SNU 4190.310, 2016 Spring *)

(** Assignment 03 *)
(** Due: 2016/04/03 23:59 *)

(* Important: 
   - Do NOT import other files.

   - You are NOT allowed to use the [admit] tactic.

   - You are NOT allowed to use the following tactics.
     [tauto], [intuition], [firstorder], [omega].

   - Just leave [exact GIVEUP] for those problems that you fail to prove.
*)

Require Export Basics.

Definition GIVEUP {T: Type} : T.  Admitted.

(*** 
   See the chapter "Lists" for explanations of the following.
 ***)

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

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

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

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

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

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

Fixpoint snoc (l:natlist) (v:nat) : natlist := 
  match l with
  | nil    => [v]
  | h :: t => h :: (snoc t v)
  end.

Fixpoint rev (l:natlist) : natlist := 
  match l with
  | nil    => nil
  | h :: t => snoc (rev t) h
  end.

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

Definition option_elim (d : nat) (o : natoption) : nat :=
  match o with
  | Some n' => n'
  | None => d
  end.

(*=========== 3141592 ===========*)

(** **** Problem #1 : 2 stars (list_funs) *)
(** Complete the definitions of [nonzeros], [oddmembers] and
    [countoddmembers] below. Have a look at the tests to understand
    what these functions should do. *)

Fixpoint nonzeros (l:natlist) : natlist :=
  GIVEUP.

Example test_nonzeros:            nonzeros [0;1;0;2;3;0;0] = [1;2;3].
Proof. exact GIVEUP. Qed.

(*-- Check --*)

Check test_nonzeros:            nonzeros [0;1;0;2;3;0;0] = [1;2;3].

(*=========== 3141592 ===========*)

(** **** Problem #2 : 3 stars, advanced (alternate) *)
(** Complete the definition of [alternate], which "zips up" two lists
    into one, alternating between elements taken from the first list
    and elements from the second.  See the tests below for more
    specific examples.

    Note: one natural and elegant way of writing [alternate] will fail
    to satisfy Coq's requirement that all [Fixpoint] definitions be
    "obviously terminating."  If you find yourself in this rut, look
    for a slightly more verbose solution that considers elements of
    both lists at the same time.  (One possible solution requires
    defining a new kind of pairs, but this is not the only way.)  *)

Fixpoint alternate (l1 l2 : natlist) : natlist :=
  GIVEUP.

Example test_alternate1:        alternate [1;2;3] [4;5;6] = [1;4;2;5;3;6].
Proof. exact GIVEUP. Qed.
Example test_alternate2:        alternate [1] [4;5;6] = [1;4;5;6].
Proof. exact GIVEUP. Qed.
Example test_alternate3:        alternate [1;2;3] [4] = [1;4;2;3].
Proof. exact GIVEUP. Qed.
Example test_alternate4:        alternate [] [20;30] = [20;30].
Proof. exact GIVEUP. Qed.

(*-- Check --*)

Check 
(conj test_alternate1
(conj test_alternate2
(conj test_alternate3
(test_alternate4))))
:
alternate [1;2;3] [4;5;6] = [1;4;2;5;3;6] /\
alternate [1] [4;5;6] = [1;4;5;6] /\
alternate [1;2;3] [4] = [1;4;2;3] /\
alternate [] [20;30] = [20;30].

(*=========== 3141592 ===========*)

(** **** Problem #3 : 3 stars (list_exercises) *)
(** More practice with lists. *)

Theorem app_nil_end : forall l : natlist, 
  l ++ [] = l.   
Proof.
  exact GIVEUP.
Qed.  

(*-- Check --*)
Check app_nil_end : forall l : natlist, 
  l ++ [] = l.   

(*=========== 3141592 ===========*)

(** Hint: You may need to first state and prove some lemma about snoc and rev. *)
Theorem rev_involutive : forall l : natlist,
  rev (rev l) = l.
Proof.
  exact GIVEUP.
Qed.

(*-- Check --*)

Check rev_involutive : forall l : natlist,
  rev (rev l) = l.

(*=========== 3141592 ===========*)

(** 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 app_assoc4 : forall l1 l2 l3 l4 : natlist,
  l1 ++ (l2 ++ (l3 ++ l4)) = ((l1 ++ l2) ++ l3) ++ l4.
Proof.
  exact GIVEUP.
Qed.

(*-- Check --*)

Check app_assoc4 : forall l1 l2 l3 l4 : natlist,
  l1 ++ (l2 ++ (l3 ++ l4)) = ((l1 ++ l2) ++ l3) ++ l4.

(*=========== 3141592 ===========*)

Theorem snoc_append : forall (l:natlist) (n:nat),
  snoc l n = l ++ [n].
Proof.
  exact GIVEUP.
Qed.

(*-- Check --*)

Check snoc_append : forall (l:natlist) (n:nat),
  snoc l n = l ++ [n].

(*=========== 3141592 ===========*)

Theorem distr_rev : forall l1 l2 : natlist,
  rev (l1 ++ l2) = (rev l2) ++ (rev l1).
Proof.
  exact GIVEUP.
Qed.

(*-- Check --*)

Check distr_rev : forall l1 l2 : natlist,
  rev (l1 ++ l2) = (rev l2) ++ (rev l1).

(*=========== 3141592 ===========*)

(** An exercise about your implementation of [nonzeros]: *)
Theorem nonzeros_app : forall l1 l2 : natlist,
  nonzeros (l1 ++ l2) = (nonzeros l1) ++ (nonzeros l2).
Proof.
  exact GIVEUP.
Qed.

(*-- Check --*)

Check nonzeros_app : forall l1 l2 : natlist,
  nonzeros (l1 ++ l2) = (nonzeros l1) ++ (nonzeros l2).

(*=========== 3141592 ===========*)

(** **** Problem #4 : 2 stars (beq_natlist) *)
(** Fill in the definition of [beq_natlist], which compares
    lists of numbers for equality.  Prove that [beq_natlist l l]
    yields [true] for every list [l]. 

    You can use [beq_nat] from Basics.v
*)

Check beq_nat.

Fixpoint beq_natlist (l1 l2 : natlist) : bool :=
  GIVEUP.

Example test_beq_natlist1 :   beq_natlist nil nil = true.
Proof. exact GIVEUP. Qed.
Example test_beq_natlist2 :   beq_natlist [1;2;3] [1;2;3] = true.
Proof. exact GIVEUP. Qed.
Example test_beq_natlist3 :   beq_natlist [1;2;3] [1;2;4] = false.
Proof. exact GIVEUP. Qed.

(** Hint: You may need to first prove a lemma about reflexivity of beq_nat. *)
Theorem beq_natlist_refl : forall l:natlist,
  beq_natlist l l = true.
Proof.
  exact GIVEUP.
Qed.
  
(** [] *)

(*-- Check --*)

Check
(conj test_beq_natlist1
(conj test_beq_natlist2
(test_beq_natlist3)))
:   
beq_natlist nil nil = true /\
beq_natlist [1;2;3] [1;2;3] = true /\
beq_natlist [1;2;3] [1;2;4] = false.

(*-- Check --*)

Check beq_natlist_refl : forall l:natlist,
  beq_natlist l l = true.

(*=========== 3141592 ===========*)

(** **** Problem #5  : 4 stars, advanced (rev_injective) *)

(** Hint: You can use the lemma [rev_involutive]. *)
Theorem rev_injective: forall l1 l2 : natlist, 
  rev l1 = rev l2 -> l1 = l2.
Proof.
  exact GIVEUP.
Qed.

(*-- Check --*)

Check rev_injective: forall l1 l2 : natlist, 
  rev l1 = rev l2 -> l1 = l2.

(*=========== 3141592 ===========*)

(** **** Problem #6 : 2 stars (hd_opt) *)
(** Using the same idea, fix the [hd] function from earlier so we don't
   have to pass a default element for the [nil] case.  *)

Definition hd_opt (l : natlist) : natoption :=
  GIVEUP.

Example test_hd_opt1 : hd_opt [] = None.
Proof. exact GIVEUP. Qed.
Example test_hd_opt2 : hd_opt [1] = Some 1.
Proof. exact GIVEUP. Qed.
Example test_hd_opt3 : hd_opt [5;6] = Some 5.
Proof. exact GIVEUP. Qed.


(** This exercise relates your new [hd_opt] to the old [hd]. *)
Theorem option_elim_hd : forall (l:natlist) (default:nat),
  hd default l = option_elim default (hd_opt l).
Proof.
  exact GIVEUP.
Qed.

(*-- Check --*)

Check
(conj test_hd_opt1
(conj test_hd_opt2
(test_hd_opt3)))
:
hd_opt [] = None /\
hd_opt [1] = Some 1 /\
hd_opt [5;6] = Some 5.

(*-- Check --*)

Check option_elim_hd : forall (l:natlist) (default:nat),
  hd default l = option_elim default (hd_opt l).