(** * Recursion *)

(* ** Fibonacci *)

(** *** Straightforward definition *)

Fixpoint fib (n:nat) : nat := match n with 
    0 => 0 | 1 => 1 | S (S m as p) => fib m + fib p end.

Eval compute in fib 4.

(** *** Associated recursion principles *)
Section FibPrinciple.

Variable P : nat -> Type.
Variable P0: P 0.
Variable P1:P 1.
Variable Pr : forall n, P n -> P (S n) -> P (S (S n)).

Fixpoint Pfib1 (n:nat) : P n := 
    match n return P n with 
          0 => P0
     | S p => match p return P p -> P (S p) with 
         (* trick to have the right dependency and pass the guard condition *)
                       0 => fun _ => P1
                    | S m => Pr m (Pfib1 m) end
                    (Pfib1 p) 
     end.

Fixpoint Pfib2 (n:nat) : P n * P (S n) := 
    match n return P n * P (S n) with 
          0 => (P0,P1)
     | S p => match Pfib2 p with 
                      (Pp,PSp) => (PSp,Pr p Pp PSp)
                    end
    end.

Definition Pfib (n:nat) : P n := fst (Pfib2 n).

End FibPrinciple.

(** *** Definitions of Fibonacci *)

Definition fib1 : nat-> nat := Pfib1 (fun _ => nat) 0 1 (fun n p q => p+q).

Eval compute in fib1 4.

Definition fib2 : nat-> nat := Pfib (fun _ => nat) 0 1 (fun n p q => p+q).
Eval compute in fib2 4.

Extraction Inline Pfib1 Pfib Pfib2.
Extraction fib1.
Extraction fib2.

(** fib1 correspond to th eexponantial algorithm, while 
      fib2 is the linear version *)

(** ** Recursion over lists *)
Require Export List.
Parameter A : Type.
Fixpoint split (l:list A) : list A * list A := 
   match l with nil => (nil,nil)
                    | a::nil => (cons a nil,nil)
                    | a::b::m => let (l1,l2) := split m in 
                                         (a::l1,b::l2) 
   end.

(** Recusive principle associated to split *)
Section SplitInd.

Variables (P:list A -> Prop) 
   (Pnil : P nil) (Pone : forall a, P (a::nil)) 
   (Pr : forall a b l, P l -> P (a::b:: l)).

Fixpoint split_ind (l:list A) : P l := 
      match l return P l with
                      nil => Pnil
                    | a::nil => Pone a
                    | a::b::m => Pr a b m (split_ind m)
      end.
End SplitInd.

Lemma split_length_le : forall l, 
    length (fst (split l)) <= length l 
 /\ length (snd (split l)) <= length l.
intros; elim l using split_ind; simpl; intros; auto.
destruct (split l0); simpl in *; intuition.
Save.

Require Omega.

Lemma split_length_lt : forall l, 
   1 < length l ->    
    length (fst (split l)) < length l 
 /\ length (snd (split l)) < length l.
destruct l; simpl; intros; try omega.
destruct l; simpl in *; intros; try omega.
generalize (split_length_le l); case (split l); simpl in *; intuition.
Save.

Variable le : A -> A -> bool.

Fixpoint merge (l1 l2:list A) {struct l1} : list A := 
  match l1 with  nil  => l2 
  | a::m1 => (fix maux (m: list A) : list A := 
       match m with nil   => l1
              |b::m2 => if le a b then a::merge m1 m
                        else b::maux m2 end) l2 end. 

Require Export Arith.

Fixpoint sortn (l:list A) (n:nat) {struct n}: list A := 
  if le_lt_dec (length l) 1 then l else
      match n with 0 => nil 
            | S m => let (l1,l2) := split l in merge (sortn l1 m) (sortn l2 m) 
      end.

Lemma sortn_eq : forall (l:list A) (n:nat),
  sortn l n = 
  if le_lt_dec (length l) 1 then l else
      match n with 0 => nil 
            | S m => let (l1,l2) := split l in merge (sortn l1 m) (sortn l2 m) 
      end.
destruct n; trivial.
Save.

Lemma sortnS : forall l m, 
sortn l (S m) =  if le_lt_dec (length l) 1 then l 
      else let (l1,l2) := split l in merge (sortn l1 m) (sortn l2 m).
trivial.
Save.

Definition sort l := sortn l (length l).

Lemma sortn_stable
   : forall n m l, length l <= n -> length l <= m -> sortn l n = sortn l m.
intro n; induction n; intros.
simpl.
assert (l=nil).
destruct l; simpl; auto.
absurd (length (a :: l) <= 0); simpl; intuition.
subst l; simpl; auto.
case m; simpl; auto.

intros; rewrite sortnS.
rewrite (sortn_eq l m).
case (le_lt_dec (length l) 1); intros; auto.
generalize (split_length_lt l).
case (split l); simpl; intros; auto.
destruct m; auto.
absurd (1<0); intuition.
assert (length l1 <= n).
omega.
assert (length l2 <= n).
omega.
assert (length l1 <= m).
omega.
assert (length l2 <= m).
omega.
rewrite (IHn m l1) ; auto.
rewrite (IHn m l2) ; auto.
Save.

Lemma sortn_eq_sort : forall n l, length l <= n -> sortn l n = sort l.
intros; unfold sort; apply sortn_stable; auto.
Save.

Lemma sortn_fix : forall (l:list A),
  sort l = if le_lt_dec (length l) 1 then l 
              else let (l1,l2) := split l in merge (sort l1) (sort l2).
unfold sort at 1; intro; rewrite sortn_eq; case (le_lt_dec (length l) 1); intros; auto.
case_eq (length l); intros.
intros; absurd (1<length l); auto;omega.
generalize (split_length_lt l l0); auto.
case (split l); simpl; intros; repeat rewrite sortn_eq_sort; auto; omega.
Save.

(** ** Partial functions *)

Variables (t : A) (F : nat -> nat -> A -> A).

(** f n m = if n = m then t else F n m (f n (m-1)) *)
(** f defined on n m, s.t. n <= m, we can use the inductive definition of le *)

Lemma le_pred : forall n m, n <= m -> n <> m -> n <= pred m.
intros n m lenm; case lenm; intros.
(* proof by contradiction *)
case H; trivial.
exact H.
Defined.

Fixpoint f (n m:nat) (p:n <= m) {struct p} : A := 
    match eq_nat_dec n m with 
         left _ => t 
      | right H => F n m (f n (pred m) (le_pred n m p H))
    end.