(** * Some more List programming *)

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#<br># 
[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. simpl. 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 
   function mutually by recursion.*) 

Require Import Arith.
Check Nat.leb.
Print "<=?".

(** The following is not accepted by Rocq #<br>#
[Fixpoint merge (l k :natlist) : 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.eqb n m then cons n (merge l' k) else cons m (merge l k')
 end.]
*)

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