(* coqc Basics.v *) 

Require Export Basics.

Module Exercises.

(* ###################################################### *)
(** * Lists of Numbers *)

(** An inductive definition of _polymorphic lists_ : *)

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

(* Use _ to infer the type parameters *)

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

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

(* ###################################################### *)
(** *** Implicit Arguments *)

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

(** Some notation for lists to make our lives easier: *)

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

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" := (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.

(* ###################################################### *)
(** * Reasoning About Lists *)

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

(* ###################################################### *)
(** ** Induction on Lists *)

(** Coq generates an induction principle for every [Inductive]
    definition, including lists. *)

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

(** Here is an informal proof of the same theorem. *)

(** _Theorem_: For all lists [l1], [l2], and [l3], 
   [(l1 ++ l2) ++ l3 = l1 ++ (l2 ++ l3)].

   _Proof_: By induction on [l1].

   - First, suppose [l1 = []].  We must show
[[
       ([] ++ l2) ++ l3 = [] ++ (l2 ++ l3),
]]
     which follows directly from the definition of [++].

   - Next, suppose [l1 = n::l1'], with
[[
       (l1' ++ l2) ++ l3 = l1' ++ (l2 ++ l3)
]]
     (the induction hypothesis). We must show
[[
       ((n :: l1') ++ l2) ++ l3 = (n :: l1') ++ (l2 ++ l3).
]]  
     By the definition of [++], this follows from
[[
       n :: ((l1' ++ l2) ++ l3) = n :: (l1' ++ (l2 ++ l3)),
]]
     which is immediate from the induction hypothesis.  []

  Here is an exercise to be worked together in class: *)

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.

SearchAbout rev.  (* then do C-c C-; to copy results here *)

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

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

(* Complete the following proof without using simpl. *)

(** Hint: you might like to use the [symmetry] tactic, which
    switches the left and right sides of an equality in the goal. *)
 
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 *********************)

(** Sometimes, a proof will get stuck because Coq doesn't
    automatically expand a function call into its definition.  (This
    is a feature, not a bug: if Coq automatically expanded everything
    possible, our proof goals would quickly become enormous -- hard to
    read and slow for Coq to manipulate!) *)

Definition plus3 := plus 3.

Theorem unfold_example_bad : forall m n,
  3 + n = m ->
  plus3 n + 1 = m + 1.
Proof.
  intros m n H.
  (* At this point, we'd like to do [rewrite -> H], since [plus3 n] is
     definitionally equal to [3 + n].  However, Coq doesn't
     automatically expand [plus3 n] to its definition. *)
  Admitted.

(** The [unfold] tactic can be used to explicitly replace a
    defined name by the right-hand side of its definition.  *)

Theorem unfold_example : forall m n,
  3 + n = m ->
  plus3 n + 1 = m + 1.
Proof.
  intros m n H.
  unfold plus3.
  rewrite -> H.
  reflexivity.  Qed.

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

(** Recall the definition of natural numbers:
[[
     Inductive nat : Type :=
       | O : nat
       | S : nat -> nat.
]]
    It is clear from this definition that every number has one of two
    forms: either it is the constructor [O] or it is built by applying
    the constructor [S] to another number.  But there is more here than
    meets the eye: implicit in the definition (and in our informal
    understanding of how datatype declarations work in other
    programming languages) are two other facts:

    - The constructor [S] is _injective_.  That is, the only way we can
      have [S n = S m] is if [n = m].

    - The constructors [O] and [S] are _disjoint_.  That is, [O] is not
      equal to [S n] for any [n]. *)

(** Similar principles apply to all inductively defined types: all
    constructors are injective, and the values built from distinct
    constructors are never equal.  For lists, the [cons] constructor is
    injective and [nil] is different from every non-empty list.  For
    booleans, [true] and [false] are unequal.  (Since neither [true]
    nor [false] take any arguments, their injectivity is not an issue.) *)

(** Coq provides a tactic, called [inversion], that allows us to
    exploit these principles in making proofs.
 
    The [inversion] tactic is used like this.  Suppose [H] is a
    hypothesis in the context (or a previously proven lemma) of the
    form
[[
      c a1 a2 ... an = d b1 b2 ... bm
]]
    for some constructors [c] and [d] and arguments [a1 ... an] and
    [b1 ... bm].

    Then [inversion H] instructs Coq to "invert" this equality to
    extract the information it contains about these terms:

    - If [c] and [d] are the same constructor, then we know, by the
      injectivity of this constructor, that [a1 = b1], [a2 = b2],
      etc.; [inversion H] adds these facts to the context, and tries
      to use them to rewrite the goal.

    - If [c] and [d] are different constructors, then the hypothesis
      [H] is contradictory.  That is, a false assumption has crept
      into the context, and this means that any goal whatsoever is
      provable!  In this case, [inversion H] marks the current goal as
      completed and pops it off the goal stack. *)

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 .... (using tactics in hypotheses) ***************)

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.

(** Note about Coq's conditionals: they are exactly like those found
    in any other language, with one small generalization.  Since the
    boolean type is not built in, Coq actually allows conditional
    expressions over _any_ inductively defined type with exactly two
    constructors.  The guard is considered true if it evaluates to the
    first constructor in the [Inductive] definition and false if it
    evaluates to the second. *)

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.

(* ### apply ... with ... ### see textbook *)

(* ################################################################## *)
(** * Review *)

(** We've now seen a bunch of Coq's fundamental tactics -- enough to
    do pretty much everything we'll want for a while.  We'll introduce
    one or two more as we go along through the next few lectures, and
    later in the course we'll introduce some more powerful
    _automation_ tactics that make Coq do more of the low-level work
    in many cases.  But basically we've got what we need to get work
    done.

    Here are the ones we've seen:

      - [intros]: 
        move hypotheses/variables from goal to context 

      - [reflexivity]:
        finish the proof (when the goal looks like [e = e])

      - [apply]:
        prove goal using a hypothesis, lemma, or constructor

      - [apply... in H]: 
        apply a hypothesis, lemma, or constructor to a hypothesis in
        the context (forward reasoning)

      - [apply... with...]:
        explicitly specify values for variables that cannot be
        determined by pattern matching

      - [simpl]:
        simplify computations in the goal 

      - [simpl in H]:
        ... or a hypothesis 

      - [rewrite]:
        use an equality hypothesis (or lemma) to rewrite the goal 

      - [rewrite ... in H]:
        ... or a hypothesis 

      - [unfold]:
        replace a defined constant by its right-hand side in the goal 

      - [unfold... in H]:
        ... or a hypothesis  

      - [destruct... as...]:
        case analysis on values of inductively defined types 

      - [induction... as...]:
        induction on values of inductively defined types 

      - [inversion]:
        reason by injectivity and distinctness of constructors

      - [remember (e) as x]:
        give a name ([x]) to an expression ([e]) so that we can
        destruct [x] without "losing" [e]

      - [assert (e) as H]:
        introduce a "local lemma" [e] and call it [H] 
*)

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