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.