mergesort.v

Require Export Coq.Lists.List.
Require Export Coq.Arith.Arith.
Require Import Program.Wf.

Program Fixpoint merge (x : list nat) (y : list nat) {measure (length x + length y)} : list nat :=
  match x with
  | x1 :: xs =>
    match y with
      | y1 :: ys => if x1 <=? y1
        then x1::(merge xs y)
        else y1::(merge x ys)
      | _ => x
    end
  | _ => y
  end.
Next Obligation.
  apply Nat.add_le_lt_mono; auto.
Qed.

Program Fixpoint mergesort (x : list nat) {measure (length x)}: list nat :=
  match x with
  | nil => nil
  | x :: nil => x :: nil
  | x :: y :: nil => if x <=? y
    then (x :: y :: nil)
    else (y :: x :: nil)
  | x :: y :: z :: rest => 
    let a := (x :: y :: z :: rest) in 
    let p := (Nat.div2 (length a)) in
    merge (mergesort (firstn p a)) (mergesort (skipn p a))
  end.
Next Obligation.
  rewrite firstn_length.
  simpl.
  apply lt_n_S.
  apply Nat.min_lt_iff.
  left.
  destruct (length rest).
  auto.
  apply lt_n_S.
  destruct n.
  auto.
  rewrite Nat.lt_div2.
  auto.
  apply Nat.lt_0_succ.
Qed.
Next Obligation.
  rewrite skipn_length.
  simpl.
  destruct (length rest).
  auto.
  destruct Nat.div2.
  auto.
  rewrite Nat.lt_succ_r.
  rewrite Nat.le_succ_r.
  left.
  rewrite Nat.le_succ_r.
  left.
  rewrite Nat.le_sub_le_add_r.
  apply le_plus_l.
Qed.

Lemma mergesort_1 : forall x, mergesort (x :: nil ) = x :: nil.
Proof.
intros.
 unfold mergesort;   unfold merge;  unfold merge_func;                                                                                                             
  rewrite Wf.WfExtensionality.fix_sub_eq_ext; simpl.
auto.
Qed. 

Lemma mergesort_nil : mergesort nil = nil.
Proof.
intuition.
Qed.

Lemma mergesort_merge : forall il ,  merge (mergesort (firstn (Nat.div2 (length il)) il))
    (mergesort (skipn  (Nat.div2 (length il)) il)) = mergesort il.
Proof.
destruct il.
intuition.

destruct il.
simpl.
intuition.

destruct il.
simpl.
repeat rewrite mergesort_1.
unfold mergesort;
  rewrite Wf.WfExtensionality.fix_sub_eq_ext; simpl.
 unfold merge; unfold merge_func;
    rewrite Wf.WfExtensionality.fix_sub_eq_ext; simpl.
remember ( n <=? n0 ).
destruct b; intuition.

simpl.
(* blocked here *)