Set Implicit Arguments.

Require Export List.
Open Scope list_scope.
Require Export Arith.

Module Type Order.
Variable A:Type.
Variable le:A->A->Prop.
Hypothesis le_refl : forall x, le x x.
Hypothesis le_trans : forall x y z, 
     le x y -> le y z -> le x z.
Variable le_total : forall x y, {le x y}+{le y x}.
End Order.

Module SortedList (X:Order).
Export X.

Definition le_list a l := forall k, In k l -> le a k.
Hint Unfold le_list.

Inductive sorted : list A -> Prop := 
       sort_nil : sorted nil
    | sort_cons : forall a l, le_list a l -> sorted l -> sorted (a::l).
Hint Constructors sorted.

Lemma sort_singl : forall a, sorted (a::nil).
intros; apply sort_cons; auto.
red; simpl; intuition.
Save.
Hint Resolve sort_singl.

Lemma sort_cons_cons : 
   forall a b l, le a b -> sorted (b::l) -> sorted (a::b::l).
intros; apply sort_cons; auto.
red; simpl; intuition.
subst; auto.
inversion_clear H0.
red in H1; apply le_trans with b; auto.
Save.

Hint Resolve sort_cons_cons.

Lemma insert0 : 
   forall a l, sorted l -> 
   {m : list A | sorted m /\ forall k, In k m <-> In k l \/ k=a}.
induction l.
exists (a::nil); simpl; intuition.
intro; case (le_total a a0); intro.
exists (a::a0::l); simpl; intuition.
case IHl.
inversion H; trivial.
intros m (Sm,Em).
exists (a0::m); split; intros.
apply sort_cons; auto.
inversion_clear H; red; intros.
case (Em k); intros H2 _.
case H2; intros; auto.
subst k; trivial.
case (Em k); simpl; intuition.
Defined.

Require Import Coq.Program.Utils.

Program Fixpoint insert (a:A) (l :list A) (_:unit | sorted l) {struct l} 
         : {m| sorted m /\ forall k, In k m <-> In k l \/ k=a} := 
match l with nil => (a::nil) 
                | (b::m) => if le_total a b then (a::l) 
                                  else (b::insert a (l:=m) tt)
end.
Next Obligation.
intuition.
Defined.
Next Obligation.
intuition.
Defined.
Next Obligation.
inversion H1; trivial.
Defined.
Next Obligation.
destruct_call insert; simpl.
subst l; inversion_clear H1.
case a0; clear a0; split.
apply sort_cons; auto.
red; intros; case (H4 k); intuition.
subst k; auto.
intro; case (H4 k); intuition.
simpl; auto.
case H9; auto.
Defined.

Program Fixpoint isort (l :list A) {struct l} 
         : {m| sorted m /\ forall k, In k l <-> In k m} := 
match l with nil => nil | (b::m) => insert b (l:=isort m) tt end.
Next Obligation.
destruct_call isort; simpl; intuition.
Defined.
Next Obligation.
destruct_call insert; simpl; subst l.
case a; clear a; split; auto.
generalize H0; clear H0.
destruct_call isort; simpl.
case a; intros.
case (H1 k); case (H2 k); intuition.
Defined.