(* coqc Basics.v *) 

Require Export Basics.

Module Exercises.

Inductive list (X:Type) : Type :=
  | nil : list X
  | cons : X -> list X -> list X.

Check nil.
Check cons.

Check (cons nat 2 (cons nat 1 (nil nat))).

Fixpoint length (X:Type) (l:list X) : nat := 
  match l with
  | nil => 0
  | cons h t => S (length X t)
  end.

Check (cons _ 2 (cons _ 1 (nil _))).

Implicit Arguments nil [[X]].
Implicit Arguments cons [[X]].

Check (cons 2 (cons 1 nil)).

Fixpoint length' {X:Type} (l:list X) : nat := 
  match l with
  | nil => 0
  | cons h t => S (length' t)
  end.

Fixpoint app {X : Type} (l1 l2 : list X) 
                : (list X) := 
  match l1 with
  | nil => l2
  | cons h t => cons h (app t l2)
  end.

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

Definition tl {X:Type} (l:list X) : list X :=
  match l with
  | nil => nil 
  | h :: t => t
  end.


Theorem tl_length_pred : forall X:Type, forall l:list X,
  pred (length' l) = length' (tl l).
Proof.
  Admitted.

Theorem app_ass : forall X:Type, forall l1 l2 l3 : list X, 
  (l1 ++ l2) ++ l3 = l1 ++ (l2 ++ l3).
Proof.
  Admitted.

Theorem app_length : forall X:Type, forall l1 l2 : list X,
  length' (l1 ++ l2) = (length' l1) + (length' l2).
Proof.
  Admitted.

Fixpoint snoc {X:Type} (l:list X) (v:X) : list X := 
  match l with
  | nil => [v]
  | h :: t => h :: (snoc t v)
  end.

Fixpoint rev {X:Type} (l:list X) : list X := 
  match l with
  | nil => nil
  | h :: t => snoc (rev t) h
  end.

Theorem rev_involutive : forall X:Type, forall l : list X,
  rev (rev l) = l.
Proof.
  Admitted.

(**************** The apply tactic ***************)

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.

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

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

Fixpoint map {X Y:Type} (f:X->Y) (l:list X) 
             : (list Y) := 
  match l with
  | [] => []
  | h :: t => (f h) :: (map f t)
  end.

Theorem map_rev : forall {X Y : Type} (f : X -> Y) (l : list X),
  map f (rev l) = rev (map f l).
Proof.
  Admitted.

(******************* The unfold tactic *********************)

(* Read about this in the textbook *)

(******************* The inversion tactic *********************)

Theorem eq_add_S : forall (n m : nat),
     S n = S m ->
     n = m.
Proof.
  intros n m eq. inversion eq. reflexivity.
Qed.

Theorem silly4 : forall (n m : nat),
     [n] = [m] ->
     n = m.
Proof.
  Admitted.

Theorem silly7 : forall (n m : nat),
     false = true ->
     [n] = [m].
Proof.
  Admitted.

Theorem beq_nat_eq : forall n m,
  true = beq_nat n m -> n = m.
Proof.
  intros n. induction n as [| n'].
  Admitted.

Theorem beq_nat_0_l : forall n,
  true = beq_nat 0 n -> 0 = n.
Proof.
  Admitted.

Theorem double_injective : forall n m,
     double n = double m ->
     n = m.
Proof.
  Admitted.

(*********** ...in H ....  ***************)

Theorem S_inj : forall (n m : nat) (b : bool),
     beq_nat (S n) (S m) = b ->
     beq_nat n m = b.
Proof.
  intros n m b H. simpl in H. apply H.
Qed.

Theorem silly3' : forall (n : nat),
  (beq_nat n 5 = true -> beq_nat (S (S n)) 7 = true) ->
     true = beq_nat n 5 ->
     true = beq_nat (S (S n)) 7.
Proof.
  intros n eq H.
  symmetry in H. apply eq in H. symmetry in H.
  apply H.
Qed.

(*************** destruct on compound expressions **************)

Definition sillyfun (n : nat) : bool :=
  if beq_nat n 3 then false
  else if beq_nat n 5 then false
  else false.

Theorem sillyfun_false : forall (n : nat),
  sillyfun n = false.
Proof.
  intros n. unfold sillyfun.
  destruct (beq_nat n 3).
    Case "beq_nat n 3 = true". reflexivity.
    Case "beq_nat n 3 = false". destruct (beq_nat n 5).
      SCase "beq_nat n 5 = true". reflexivity.
      SCase "beq_nat n 5 = false". reflexivity.
Qed.

(*************** remember **************)

Definition sillyfun1 (n : nat) : bool :=
  if beq_nat n 3 then true
  else if beq_nat n 5 then true
  else false.

Theorem sillyfun1_odd_FAILED : forall (n : nat),
     sillyfun1 n = true ->
     oddb n = true.
Proof.
  intros n eq. unfold sillyfun1 in eq.
  destruct (beq_nat n 3).
  (* stuck... *)
  Admitted.

Theorem sillyfun1_odd : forall (n : nat),
     sillyfun1 n = true ->
     oddb n = true.
Proof.
  intros n eq. unfold sillyfun1 in eq.
   remember (beq_nat n 3) as e3.
   (* At this point, the context has been enriched with a new
      variable e3 and an assumption that e3 = beq_nat n 3.
      Now if we do destruct e3... *)
   destruct e3.
   (* ... the variable e3 gets substituted away (it
     disappears completely) and we are left with the same
      state as at the point where we got stuck above, except
      that the context still contains the extra equality
      assumption -- now with true substituted for e3 --
      which is exactly what we need to make progress. *)
     Case "e3 = true". apply beq_nat_eq in Heqe3.
       rewrite -> Heqe3. reflexivity.
     Case "e3 = false".
      (* When we come to the second equality test in the
        body of the function we are reasoning about, we can
         use remember again in the same way, allowing us
         to finish the proof. *)
       remember (beq_nat n 5) as e5. destruct e5.
         SCase "e5 = true".
           apply beq_nat_eq in Heqe5.
           rewrite -> Heqe5. reflexivity.
         SCase "e5 = false". inversion eq.
Qed.

(************************ challenge **********************)

Fixpoint fold {X Y:Type} (f: X->Y->Y) (l:list X) (b:Y) : Y :=
  match l with
  | nil => b
  | h :: t => f h (fold f t b)
  end.

Definition fold_length {X : Type} (l : list X) : nat :=
  fold (fun _ n => S n) l 0.

Theorem fold_length_correct : forall X (l : list X),
  fold_length l = length' l.
Proof.
  Admitted.


End.