Require Import Coq.subtac.Utils.
Require Export insertion.
Module SortProg (O:OrdSet).
Import O.
Module SP := Sort O.
Import SP.

Program Fixpoint insert (a:A) (l :list A) (_:unit | sorted l) {struct l} 
         : {m| sorted m /\ permut (a::l) m} := 
match l with nil => (a::nil) 
                | (b::m) => if le_total a b then (a::l) 
                                  else (b::insert a m tt)
end.
Next Obligation.
inversion s; auto.
Defined.
Next Obligation.
destruct_call insert; simpl; intuition.
apply sorted_le_list; auto.
apply le_list_permut with (a::m); auto.
apply le_list_cons; auto.
subst l; auto.
apply permut_trans with (b::a::m); auto.
subst l; auto.
Defined.

Program Fixpoint isort (l :list A) {struct l} 
         : {m| sorted m /\ permut l m} := 
match l with nil => nil | (b::m) => insert b (isort m) tt end.
Next Obligation.
destruct_call isort; simpl; intuition.
Defined.
Next Obligation.
destruct_call insert; simpl; intuition.
generalize H1; clear H1; destruct_call isort; simpl; intuition.
subst l; auto.
apply permut_trans with (b::x0); auto.
Defined.