Require Import List.

Section Selsort.

Variable A:Set.
Variable lt : A -> A -> Prop.
Let le x y := lt x y  \/ x=y.

Hint Unfold le.

Notation "a < b" := (lt a b).
Notation "a > b" := (lt b a).

Notation "a <= b" := (le a b).
Notation "a >= b" := (le b a).


Variable compare : forall a b, {a<b}+{a=b}+{a>b}.
Variable eq_dec : forall a b:A, {a=b}+{~a=b}.
Hypothesis le_trans: forall a b c, a<=b -> b<=c -> a<= c.

Fixpoint bez m l : list A :=
  match l with
  | nil => nil
  | m'::l => if eq_dec m m' then l else m'::bez m l
  end.


Fixpoint maxim default l : A :=
  match l with
  | nil => default
  | m::l => if compare m default then maxim default l else maxim m l
  end.


Require Import Arith.
Require Import Recdef.
Require Import Sorting.
Require Import  TheoryList.

Definition lelist a l := forall b, In b l -> a <= b.

Program Fixpoint selsort_aux1 (l w:list A)(ss: sort le w)  
   (all: AllS (fun a => lelist a w) l) {measure length l} : 
	{l' : list A | sort le l' /\ Permutation (w++l) l'} :=
  match l with
  | nil => w
  | a::_ => let m:=maxim a l in 
                  selsort_aux1 (bez m l) (m::w) _ _ 
  end.

Lemma mniejsze_od_nil: forall l, 
  AllS (fun a => lelist a nil) l.


Definition selsort l := selsort_aux1 l nil (nil_sort le) 
  (mniejsze_od_nil l).


End Selsort.

Check selsort.


Definition natsort : list nat -> list nat.