Require Compare.

Inductive list : Set :=
  nil : list
| cons : nat -> list -> list.

Inductive low [a:nat] : list -> Prop :=
 low_nil : (low a nil)
| low_cons : (l:list)(b:nat)(le a b)->
                         (low a (cons b l)).

Inductive sorted : list -> Prop :=
  sort_nil : (sorted nil)
| sort_cons : (l:list)(a:nat)(sorted l)->
                (low a l)->(sorted (cons a l)).


Inductive perm : list -> list -> Prop :=
  p_refl : (l:list)(perm l l)
| p_sym : (l1,l2:list)(perm l1 l2)->
            (perm l2 l1)
| p_trans : (l1,l2,l3:list)(perm l1 l2)->
              (perm l2 l3)->(perm l1 l3)
| p_cons : (a:nat)(l1,l2:list)(perm l1 l2)->
     (perm (cons a l1)(cons a l2))
| p_perm : (a,b:nat)(l:list)
      (perm (cons a (cons b l))
            (cons b (cons a l))).


Hints Resolve low_nil low_cons sort_nil 
      sort_cons p_refl.

Lemma ins : (l:list)(a:nat)(sorted l)->
    {l':list | (sorted l')
             /\(perm l' (cons a l))
             /\((b:nat)(le b a)->(low b l)->
                                     (low b l'))}.
Intros l a; Elim l.
Split with (cons a nil); Split; Auto; Split; Auto.

Clear l; Intros b l hl sl.
Elim (le_dec a b); Intro lab.
Split with (cons a (cons b l)); Split; Auto; Split; Auto.

Elim hl.
Intros x [sx [px hx]].
Split with (cons b x); Split; Auto.
Apply sort_cons; Auto.
Apply hx; Auto.
Inversion sl.
Auto.

Split; Auto.
Apply p_trans with (cons b (cons a l)).
Apply p_cons; Auto.

Apply p_perm.

Intro c; Intros; Apply low_cons.
Inversion H0.
Auto.

Inversion sl.
Auto.
Qed.

Extraction ins.


Lemma sort : (l:list){l':list |(sorted l')
                             /\(perm l l')}.
Induction l.
Split with nil; Split; Auto.

Clear l; Intros a l [l' [h1 h2]].
Elim (ins l' a).
Intros x [hx1 [hx2 hx3]]; Split with x; Split; Auto.
Apply p_sym.
Apply p_trans with (cons a l'); Auto.
Apply p_cons.
Auto.
Apply p_sym; Auto.

Auto.
Qed.