(** * Some List programming and the Option type *)

(** ** More list functions *)
Inductive natlist : Set :=
  | nil : natlist
  | cons : nat -> natlist -> natlist.

Fixpoint append (l m : natlist) {struct l} : natlist :=
  match l with
  | nil => m
  | cons x xs => cons x (append xs m)
  end.
  
(** We define how to map a function over a list. 
   This is Exercise 2 in the file [list_ex.v] *)

Fixpoint map (f : nat -> nat)(l: natlist) {struct l} : natlist :=
  match l with
  | nil => nil
  | cons x xs => cons (f x) (map f xs)
  end.

Lemma map_commutes_with_append : forall (f : nat->nat)(l k : natlist),
  map f (append l k) = append (map f l)(map f k).
Proof.
intros.
induction l.
- simpl. auto.
- simpl. rewrite IHl. auto.
Qed.

(** We define how to fold a function over a list.
    Exercise 1 in the file [list_ex.v] is an instance 
    of this where [f = plus] and [n = 0]*) 

Fixpoint fold (f : nat -> nat -> nat)(n:nat)(l: natlist) {struct l} : nat :=
  match l with
  | nil => n
  | cons x xs => f x (fold f n xs)
  end.

(** We ask ourselves how [fold] and [append] commute #<br># 
You may try to prove
<<
Lemma fold_commutes_with_append : forall (f : nat->nat->nat)(n:nat)(l k : natlist),
  fold f n (append l k) = fold f (fold f n l) k.
>>
and note that you can't prove that. And if you think about it, you note that it's not true. #<br>#
This is the correct statement about how [fold] and [append] commute. *)

Lemma fold_commutes_with_append : forall (f : nat->nat->nat)(n:nat)(l k : natlist),
  fold f n (append l k) = fold f (fold f n k) l.
Proof.
intros.
induction l.
- simpl. auto.
- simpl. rewrite IHl. auto.
Qed.

Check max.

Definition list_max := fold max 0.

Eval compute in (list_max (cons 4 (cons 8 (cons 0 (cons 7 nil))))).

(** Something that Rocq will not accept is the direct definition of [merge], 
   because the recursive argument is not clear. A solution is to define two 
   functions mutually by recursion.*) 

Require Import Arith.
Check Nat.leb.
Print Nat.leb.

Fixpoint natleb (n m : nat) : bool :=
  match n, m with
  | 0, _ => true
  | S n', 0 =>  false
  | S n', S m' => natleb n' m'
 end.

Print natleb.

Print "<=?".

Search Nat.leb.

(** The following is not accepted by Rocq. Try it out. 
    The call to [l] in the last line is not structurally smaller
<<
Fixpoint merge (l k :natlist) {struct l} : natlist :=
 match l, k with
  | nil       , nil       => nil
  | cons n l' , nil       => cons n l'
  | nil       , cons m k' => cons m k'
  | cons n l' , cons m k' => 
       if Nat.leb n m then cons n (merge l' k) else cons m (merge l k')
 end.
>>
*)


(** This is how to define [merge] using the auxiliary [merge_aux] *)
Fixpoint merge (l k :natlist){struct l} : natlist := 
 let fix merge_aux k :=
 match l, k with
  | nil       , nil       => nil
  | cons n l' , nil       => cons n l'
  | nil       , cons m k' => cons m k'
  | cons n l' , cons m k' => 
       if Nat.leb n m then cons n (merge l' k) else cons m (merge_aux k')
 end
 in merge_aux k.

Eval compute in (merge (cons 4 (cons 8 nil)) (cons 0 (cons 7 nil))).

(** ** The Option type *)

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

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.

(** An improved statement *)
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 speaking, [option A] is the disjoint union of [A] and [{None}] 
*)

(** Now we 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))).

(** *** Exercise: Complete the following *)

Definition ohead (l : natlist) : option nat := None.
(** Fill in the correct function body in place of [None] *) 

(** Check that [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.

(** This can be shortened as follow *)
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.]
   This is not well-typed!
   But we do have the following. Fill in the proofs. *)

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.