(* Anomalies with taking the head or tail of a list *)

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

(* Remark: lists are defined in the standard library of
   Coq but that definition is polymorphic, ie. for every
   type 'A', 'list A' gives a type of lists with elements
   of type 'A'. *)

(* Now let us define the basic operations of head and tail *)
Definition tail (l : natlist) : natlist :=
  match l with
  | nil => nil
  | cons x xs => xs
  end.
(* Note that tail of nil is nil -- we have to choose _something_ *)
Definition head (l : natlist) : nat :=
  match l with
  | nil => 0
  | cons x xs => x
  end.
(* Note that head of nil is 0 -- we have to choose _something_ *)

(* Now let us prove how append works with empty lists *)

Lemma head_cons : forall x xs, head (cons x xs) = x.
Proof.
simpl.
auto.
Qed.

Lemma tail_cons : forall x xs, tail (cons x xs) = xs.
Proof.
simpl.
auto.
Qed.

Lemma cons_head_tail_firsttry : forall l, cons(head l)(tail l) = l.
Proof.
induction l.
simpl.
(* ??? *)
Admitted.

Lemma cons_head_tail : forall l, ~ l = nil -> cons(head l)(tail l) = l.
Proof.
induction l.
- intro Hnil.
  unfold not in Hnil.
  destruct Hnil.
  auto.
  (* Alternatively, "congruence." solves your goal
     congruence does a sequence of rewriting and uses that 
     - distinct constructors are unequal
     - t is not unequal to t
   *)
- intro H1.
  simpl.
  auto.
Qed.


(* The "option" type to deal with undefinedness *)

Print option.
(*
Inductive option (A:Type) : Type :=
Some : A -> option A
| None : option A.

a: A      --> Some a : option A
exception --> None : option A
*)

(* Now let us define the basic operations of head and tail again 
   otail : natlist -> option natlist
   ohead : natlist -> option nat
*)
Definition otail (l : natlist) : option natlist :=
  match l with
  | nil => None
  | cons x xs => Some xs
  end.
(* Now tail of nil is None *)

(** COMPLETE THE FOLLOWING **)

Eval compute in (otail nil).
Eval compute in (otail (cons 3 nil)).

Definition ohead (l : natlist) : option nat :=
  match l with
  | nil => None
  | cons x xs => Some x
  end.
(* Now head of nil is None *)

Eval compute in (ohead nil).
Eval compute in (ohead (cons 3 nil)).


(* We also define ocons *)
Definition ocons (n : option nat)(l : option natlist) : option natlist :=
match n with
 | None => None
 | Some p =>
        match l with
             None => None
            | Some k => Some (cons p k)
        end
end.

(* Lemma o_cons_head_tail : forall l, ocons(ohead l)(otail l) = l.
   Not well-typed ! *)

Lemma o_cons_head_tail1 : forall l, ocons(ohead l)(otail l) = None -> l = nil.
Proof.
induction l.
- simpl.
  intros.
  auto.
- simpl.
  intros.
  congruence.
Qed.

Lemma o_cons_head_tail2 : forall l k, ocons(ohead l)(otail l) = Some k -> l = k.
Proof.
induction l.
- simpl.
  intros.
  congruence.
- simpl.
  intros.
  congruence.
Qed.

(* Now redefine 
      otail : option natlist -> option natlist
      ohead : option natlist -> option nat
   so you can state and prove something like
      Lemma o_cons_head_tail : forall l, ocons(ohead l)(otail l) = l
*)

Definition ootail (x : option natlist) : option natlist :=
match x with
| None   => None
| Some nil => None
| Some(cons a l ) => Some l
end.

Definition oohead (x : option natlist) : option nat :=
match x with
| None   => None
| Some nil => None
| Some(cons a l ) => Some a
end.

(* Note that the Lemma
      forall l, ocons(oohead l)(ootail l) = l.
   is false: see the case for l=nil 
   So we have to rephrase it still *)

Lemma oo_cons_head_tail : forall l, l <> Some nil ->  ocons(oohead l)(ootail l) = l.
Proof.
intro l.
destruct l.
- destruct n.
  * simpl.
    intro H.
    congruence.
  * intros.
    simpl.
    auto.
- intros.
  simpl.
  auto.
Qed.

Lemma oo_cons_head_tail' : forall l, l = Some nil  ->  ocons(oohead l)(ootail l) = None.
Proof.
intros l Hl.
rewrite Hl.
simpl.
auto.
Qed.

(* Functions on types generalize to functions on option-types:
   if f : A -> B, then opt_fun f : option A -> option B
   similarly for f : A -> B -> C *)

Definition otp_fun (A B : Set)(f: A -> B) := 
fun x: option A =>
  match x with
     None => None
   | Some a => Some (f a)
  end.


Definition otp_fun2 (A B C: Set)(f: A -> B -> C) := 
fun (x : option A)(y:option B) =>
  match x, y with
     None  , _      => None
   |   _   , None   => None
   | Some a, Some b => Some (f a b)
  end.

(* Sometimes you know that one of the inputs is total. 
   Say we know that the first argument is really an a : A.
   Given f : A -> B -> C, define opt_fun2t f : A -> option B -> option C *)

Definition otp_fun2t (A B C: Set)(f: A -> B -> C) := 
fun (a : A)(y:option B) =>
  match y with
     None   => None
   | Some b => Some (f a b)
  end.