Require Export List.

Module Type OrdSet.

Variable A : Set.

Variable le : A -> A -> Prop.

Hypothesis le_trans : forall x y z, le x y -> le y z -> le x z.
Hypothesis le_total : forall x y, le x y + le y x.

End OrdSet.

Module Sort (O:OrdSet).
Import O.

Inductive le_list (x:A) : list A -> Prop := 
    le_list_nil : le_list x nil
  | le_list_cons : forall a l, le x a -> le_list x l -> le_list x (a::l).

Hint Constructors le_list.

Lemma le_le_list_trans 
     : forall a b l, le a b -> le_list b l -> le_list a l.
induction 2; auto.
apply le_list_cons; auto.
apply le_trans with b; trivial.
Save.

Inductive sorted : list A -> Prop := 
    sorted_nil : sorted nil
  | sorted_singl : forall a, sorted (a::nil)
  | sorted_cons : forall a b l, sorted (b::l) -> le a b 
                         -> sorted (a::b::l).
Hint Constructors sorted.

Lemma le_list_sorted : forall l a, sorted (a::l) -> le_list a l.
induction l; intros; auto.
inversion_clear H; auto.
apply le_list_cons; auto.
apply le_le_list_trans with a; auto.
Save.
Hint Immediate le_list_sorted.

Lemma sorted_le_list : 
forall a l, sorted l -> le_list a l -> sorted (a::l).
induction 1; intros; auto.
inversion H; auto.
inversion_clear H1; auto.
Save.
Hint Resolve sorted_le_list.

Inductive permut : list A -> list A -> Prop := 
    permul_nil : permut nil nil
 | permut_cons : forall a l1 l2, 
            permut l1 l2 -> permut (a::l1) (a::l2)
 | permut_cons2 : forall a b l1 l2, 
            permut (a::l1) l2 -> permut (a::b::l1) (b::l2)
 | permut_trans : forall l1 l2 l3, 
            permut l1 l2 -> permut l2 l3 -> permut l1 l3.
Hint Constructors permut.

Lemma permut_refl : forall l, permut l l.
induction l; auto.
Save.
Hint Resolve permut_refl.

Lemma le_list_permut : forall a l m, permut l m 
   -> le_list a l -> le_list a m.
induction 1; intros; auto.
inversion H0; auto.
inversion_clear H0; auto.
inversion H2; auto.
Save.

Lemma insertion : forall a l, sorted l -> {m| sorted m /\ permut (a::l) m}.
induction l; intro.
exists (a::nil); auto.
case (le_total a a0); intro.
exists (a::a0::l); split; auto.
assert (sorted l).
inversion H; auto.
case (IHl H0); intros m (Hs,Hp).
exists (a0::m); split; auto.
apply sorted_le_list; auto.
apply le_list_permut with (a::l); auto.
Defined.


Lemma sort : forall l, {m| sorted m /\ permut l m}.
induction l.
exists (nil (A:=A)); auto.
case IHl; intros l1 (Hsl1,Hpl1).
case (insertion a l1 Hsl1); intros l2 (Hsl2,Hpl2).
exists l2; split; auto.
apply permut_trans with (a::l1); auto.
Defined.

(*
Extraction sort.
Extraction insertion. 
*)
End Sort.
Extraction Sort.
Extraction "inssort.ml" Sort.