Require Import Arith.
Require Import List.

Fixpoint pr (g:nat -> nat) (h:nat -> nat -> nat -> nat)
            ( x y:nat) :=
  match x with
    0 => (g y)
  | (S x) => (h x y (pr g h x y))
  end.

Lemma pr0 : forall (g:nat -> nat) (h:nat -> nat -> nat -> nat) (y:nat),
    (pr g h 0 y) = (g y).
Proof.
  trivial.
Qed.

Lemma prS : forall (g:nat -> nat) (h:nat -> nat -> nat -> nat) (x y:nat),
    (pr g h (S x) y) = (h x y (pr g h x y)).
Proof.
  trivial.
Qed.

Definition addpr :=
  let g x := x in
  let h x y r := (S r) in
    (pr g h).

Lemma add_is_pr : forall (x y:nat), (addpr x y) = (x + y).
Proof.
  induction x.
  - trivial.
  - intro. 
    unfold addpr. simpl. rewrite IHx.
    trivial.
Qed.

Definition mulpr :=
  let g x := 0 in
  let h x y r := y + r in
    (pr g h).

Lemma mul_is_pr : forall (x y:nat),
    (mulpr x y) = (x * y).
Proof.
  induction x.
  - trivial.
  - intro.
    unfold mulpr. simpl. rewrite IHx.
    trivial.
Qed.

Fixpoint plustr (x y:nat) : nat :=
  match x with
    0 => y
  | (S x) => (plustr x (S y))
  end.
Print pr.
Print nat_rect.
Print Nat.add.

Inductive btree (A:Type) : Type :=
  Empty : (btree A)
| Node : (btree A) -> A -> (btree A) -> (btree A).

Arguments Empty {A}.
Arguments Node [A] _ _ _.

Fixpoint pr_btree {A B C:Type}
         (g : B -> C) (h: (btree A) -> A -> (btree A) -> B -> C -> C -> C)
         (bt:btree A) (y:B) :=
  match bt with
    Empty => (g y)
  | Node bt1 x bt2 =>
    (h bt1 x bt2 y (pr_btree g h bt1 y) (pr_btree g h bt2 y))
  end.
Print pr_btree.

Print nat_rect.

Fixpoint div2 (n:nat) : nat :=
  match n with
    0 => 0
  | 1 => 0
  | S (S n) => S (div2 n)
  end.

Fixpoint list_pairing {A:Type} (xs : (list A)) : (list (A * A)) :=
  match xs with
    nil => nil
  | (x::nil) => nil
  | (x1::(x2::xss)) =>
       ((x1,x2)::(list_pairing xss))
  end.         

(* Version non acceptée

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

Fixpoint fib (n:nat) : nat :=
  match n with
    0 => 1
  | (S n1) => (
      match n1 with
        0 => 1
      | (S n2) => (fib n2) + (fib n1)
      end
    )
  end.

Fixpoint shuffle {A:Type}
         (xs ys : (list A)) : (list A) :=
  match xs, ys with
    nil, _ => ys
  | _, nil => xs
  | (x::xs), (y::ys) => (x::(y::(shuffle xs ys)))
  end.
Print shuffle.

(* Version non acceptée

Fixpoint merge (xs ys:(list nat)) : (list nat) :=
  match xs, ys with
    nil, _ => ys
  | _, nil => xs
  | x::xs', y::ys' =>
    if (x <=? y) then x::(merge xs' ys)
    else y::(merge xs ys')
  end.
 *)

Definition merge :=
  (fix loop1 (xs ys:(list nat)) :=
     match xs with
       nil => ys
     | x::xs' =>
       (fix loop2 (ys:(list nat)) :=
          match ys with
            nil => xs
          | y::ys' =>
            if (x <=? y) then x::(loop1 xs' ys)
            else y::(loop2 ys')
          end)
         ys
     end).
Print merge.
Compute (merge (1::3::5::7::nil) (2::4::6::nil)).
Reset merge.
Fixpoint merge (xs ys:(list nat)) : (list nat) :=
  let fix merge_aux ys :=
      match xs, ys with
      | nil, _ => ys
      | _, nil => xs
      | x::xs', y::ys' =>
        if (x <=? y) then x::(merge xs' ys)
        else y::(merge_aux ys')
      end
  in (merge_aux ys).

(*
Fixpoint sum (ns:(list nat)) : nat :=
  match ns with
    nil => 0
  | n1::ns1 =>
    match ns1 with
      nil => n1
    | n2::ns2 => (sum ((n1+n2)::ns2))
    end
  end.
 *)

Definition sum (ns:(list nat)) : nat :=
  let fix loop (b:nat) (ns:(list nat)) :=
      match b with
        0 => 0
      | (S b') =>
        match ns with
          nil => 0
        | n::nil => n
        | n1::n2::ns' => (loop b' ((n1+n2)::ns'))
        end
      end
  in (loop (length ns) ns).

Lemma sum_eq1 : (sum nil) = 0.
Proof.
  auto.  
Qed.

Lemma sum_eq2 : forall (n:nat), (sum (n::nil)) = n.
Proof.
  auto.
Qed.

Lemma sum_eq3 : forall (n1 n2:nat) (ns:list nat),
  (sum (n1::n2::ns)) = (sum ((n1+n2)::ns)).
Proof.
  auto.
Qed.

Reset sum.

Require Import Coq.Program.Wf.

Program Fixpoint sum (ns:(list nat)) {measure (length ns)} :=
  match ns with
    nil => 0
  | n::nil => n
  | n1::n2::ns' => (sum ((n1+n2)::ns'))
  end.


(* Versions non acceptées

Fixpoint concat {A:Type} (xss:(list (list A))) : (list A) :=
  match xss with
    nil => nil
  | nil::xss' => (concat xss')
  | (x::xs')::xss' => x::(concat (xs'::xss'))
  end.

Fixpoint concat {A:Type} (xss:(list (list A))) : (list A) :=
  match xss with
    nil => nil
  | xs::xss' =>
    match xs with
      nil => (concat xss')
    | x::xs' => x::(concat (xs'::xss'))
    end
  end.
 *)

Fixpoint deep_length {A:Type} (xss:(list (list A))) : nat :=
  match xss with
    nil => 0
  | xs::xss => 1+(length xs)+(deep_length xss)
  end.
 
Program Fixpoint concat {A:Type} (xss:(list (list A)))
        {measure (deep_length xss)}: (list A) :=
  match xss with
    nil => nil
  | nil::xss' => (concat xss')
  | (x::xs')::xss' => x::(concat (xs'::xss'))
  end.

Definition lt2 (xy1:(nat*nat)) (xy2:(nat*nat)) : Prop :=
  match xy1,xy2 with
    (x1,y1),(x2,y2) => (x1 < x2) \/ ((x1 = x2) /\ (y1 < y2))
  end.

Lemma Acc_lt2 : forall (x y:nat), (Acc lt2 (x,y)).
Proof.
  induction x.
  - induction y.
    + apply Acc_intro.
      intros.
      destruct y.
      elim H.
      * intro. inversion H0.
      * intro. elim H0.
        intros. inversion H2.
    + apply Acc_intro.
      intros.
      destruct y0.
      elim H.
      * intro. inversion H0.
      * intro. elim H0.
        intros. rewrite H1.
        inversion H2.
        -- assumption.
        -- apply Acc_inv with (x:=(0,y)).
           ++ assumption.
           ++ right. split.
              ** trivial.
              ** auto with arith.

  - induction y.
    + apply Acc_intro.             
      intros.
      destruct y.
      elim H.
      * intro.
        inversion H0.
        -- apply IHx.
        -- apply Acc_inv with (x:=(x,n0)).
           ++ auto.
           ++ left. auto with arith.
      * intro. elim H0. intros.   
        inversion H2.
    + apply Acc_intro.
      destruct y0.
      intro.
      elim H.
      * intro. apply Acc_inv with (x:=(S x,y)).
        -- assumption.
        -- left. assumption.
      * intro. elim H0. intros.
        rewrite H1. inversion H2.
        -- assumption.
        -- apply Acc_inv with (x:=(S x,y)).     
           ++ assumption.
           ++ right. split.
              ** trivial.
              ** auto with arith.
Qed.

Theorem wf_lt2 : (well_founded lt2).
Proof.
  unfold well_founded. destruct a. apply Acc_lt2.
Qed.

Lemma lt2_wf_ind : forall (P: (nat*nat) -> Prop),
    (forall (xy:nat*nat), (forall (xy':nat*nat), (lt2 xy' xy) -> (P xy')) -> (P xy))
      -> forall (xy:nat*nat), (P xy).
Proof.
  intros. apply well_founded_ind with (R:=lt2).
  - apply wf_lt2.
  - auto. 
Qed.
    
Program Fixpoint ack (xy:nat*nat) {wf lt2 xy} : nat :=
  match xy with
    (0, y) => (S y)
  | (S x, 0) => ack (x, S 0)
  | (S x, S y) => ack (x, ack (S x, y))
  end.

Obligation 3 of ack.
injection Heq_xy.
intros.
left.
rewrite <- H0.
auto with arith.
Qed.

Obligation 4 of ack.
unfold Wf.MR. apply wf_lt2.
Qed.

Fixpoint size {A:Type} (bt:btree A) : nat :=
  match bt with
    Empty => 0
  | Node bt1 _ bt2 => S(size bt1 + size bt2)
  end.

Definition size2 {A:Type} (bt:btree A) : nat*nat :=
  match bt with
    Empty => (0,0)
  | Node bt1 _ _ => (size bt, size bt1)
  end.

Definition lt_btree {A:Type} (bt1 bt2:btree A) : Prop :=
  lt2 (size2 bt1) (size2 bt2).

Lemma Acc_lt_btree_eq : forall (A:Type) (xy:nat*nat),
    forall (bt:btree A), xy=(size2 bt) -> (Acc lt_btree bt).
Proof.
  induction xy using lt2_wf_ind.
  intros. apply Acc_intro. intros.
  apply H with (xy':=(size2 y)).
  - rewrite H0. assumption.
  - trivial.
Qed.

Lemma Acc_lt_btree : forall (A:Type) (bt:btree A), (Acc lt_btree bt).
Proof.
  intros. apply Acc_lt_btree_eq with (xy:=(size2 bt)).
  trivial.
Qed.

Lemma wf_lt_btree {A:Type} : well_founded (fun (bt1 bt2:btree A) => lt_btree bt1 bt2).
Proof.
  unfold lt_btree. unfold well_founded.
  apply Acc_lt_btree.
Qed.

Variable A:Type.
Program Fixpoint list_of_btree (bt:btree A)
        {wf lt_btree bt}: (list A) :=
  match bt with
    Empty => nil
  | Node Empty x bt' => x::(list_of_btree bt')
  | Node (Node bt1 x1 bt2) x2 bt3 
    => (list_of_btree (Node bt1 x1 (Node bt2 x2 bt3)))
  end.

Obligation 3 of list_of_btree. 
unfold Wf.MR. apply wf_lt_btree.
Qed.

Obligation 1 of list_of_btree.
unfold lt_btree. simpl. unfold lt2. 
destruct bt'.
- simpl size2.
  left. auto with arith.
- simpl size2.
  left. auto with arith.
Qed.

Obligation 2 of list_of_btree.
unfold lt_btree. simpl. right. split.
- rewrite Nat.add_succ_r. auto with arith.
- auto with arith.
Qed.