(* 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.
(* This is just WRONG!  ??? *)
Abort.

Lemma cons_head_tail : forall l, ~ l = nil -> cons(head l)(tail l) = l.
Proof.
induction l.
- intro Hnil.
  simpl.
  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.

Idea: 
 + if a: A, then Some a : option A, meaning that "a is a proper value of type A"
 + None : option A, the "undefined element" of A
roughly: option A is the disjoint union of A and {None} 
*)

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

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

(** COMPLETE THE FOLLOWING **)

Definition ohead (l : natlist) : option nat := None.
(** FILL IN THE CORRECT FUNCTION BODY **) 

(* Now head of nil is None *)

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

Definition ocons' (n : option nat)(l : option natlist) : option natlist :=
match n, l with
 | None, _        => None
 | _, None        => None
 | Some p, Some k => Some (cons p k)
end.

(*
Lemma o_cons_head_tail : forall l, ocons(ohead l)(otail l) = l.
   Not well-typed !
   But we do have the following *)

Lemma o_cons_head_tail1 : forall l, ocons(ohead l)(otail l) = None -> l = nil.
Proof.
Admitted.

Lemma o_cons_head_tail2 : forall l k, ocons(ohead l)(otail l) = Some k -> l = k.
Proof.
Admitted.

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


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