Require Import List.

Section Selsort.

Variable A:Set.
Variable lt : A -> A -> Prop.

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

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

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.

Lemma bez_length : forall m l, length (bez m l) <= length l.
Proof.
  induction l.
  simpl.
  auto.
  simpl.
  destruct (eq_dec m a).
  auto.
  simpl.
  auto with arith.
Qed.

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.

Lemma maxim_length : forall l a, maxim a l <> a -> (length (bez (maxim a l) l) < length l)%nat.
Proof.
  induction l as [_ | a0 l].
  simpl.
  intuition.

  simpl.
  intro a.
  destruct (compare a0 a).
  destruct (eq_dec (maxim a l) a0).
  auto with arith.
  intros; auto with arith.
  simpl; auto with arith.
  destruct (eq_dec (maxim a0 l) a0).
  auto with arith.
  simpl.
  auto with arith.
Qed.

Require Import Arith.
Require Import Recdef.
Require Import Program.
Require Import Sorting.

Program Fixpoint selsort_aux (l w:list A) {measure length l} : 
	{l' : list A | sort lt l' /\ Permutation (w++l) l'} :=
  match l with
  | nil => w
  | a::_ => let m:=maxim a l in selsort_aux (bez m l) (m::w) 
  end.
Next Obligation.
Proof.
  split.
  admit.
  rewrite app_nil_end.
  apply Permutation_refl.
Defined.
Next Obligation.
Proof.  
  rename w into l.
  rename wildcard' into l'.
  assert (length (bez (maxim a l') l') <= length l').
  apply bez_length.
  simpl.
  remember (compare a a).
  destruct s.
  destruct (eq_dec (maxim a l') a).
  auto with arith.
  simpl.
  apply maxim_length in n.
  auto with arith.
  destruct (eq_dec (maxim a l') a).
  auto with arith.
  simpl.
  apply maxim_length in n.
  auto with arith.
Defined.
Next Obligation.
Proof.
admit.
Defined.



Print selsort_aux.


Definition selsort l := selsort_aux l nil.

End Selsort.

Check selsort.


Definition natsort : list nat -> list nat.
intro l.
eapply selsort.
apply lt_eq_lt_dec.
apply eq_nat_dec.
exact l.
Defined.