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, {ab}. 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. Function selsort_aux (w l:list A) {measure length l} : list A := match l with | nil => w | a::_ => let m:=maxim a l in selsort_aux (m::w) (bez m l) end. Proof. intros _ l a l' H. 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. Check selsort_aux_tcc. Print selsort_aux. Print selsort_aux_F. Print selsort_aux_terminate. Print selsort_aux_ind. Print selsort_aux_equation. Print R_selsort_aux. Definition selsort l := selsort_aux nil l. 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. Eval compute in natsort (2::6::1::5::nil). Recursive Extraction natsort.