Require Import List. Require Import Arith. Fixpoint insert (x : nat) (l : list nat) := match l with nil => x::nil | a::t => if leb x a then x::a::t else a::(insert x t) end. Fixpoint sort l := match l with nil => nil | a::t => insert a (sort t) end. (* The specification *) Inductive lelist : nat -> list nat -> Prop := lenil: forall x, lelist x nil | leS: forall x y l, x<=y -> lelist x l -> lelist x (y::l). Hint Resolve lenil : sortedbase. Hint Resolve leS : sortedbase. Inductive sorted : list nat -> Prop := sortnil : sorted nil | sortS : forall l x, lelist x l -> sorted l -> sorted (x::l). Hint Resolve sortnil : sortedbase. Hint Resolve sortS : sortedbase. (* Fixpoint count_occ (l : list A) (x : A) : nat := match l with | [] => 0 | y :: tl => let n := count_occ tl x in if eq_dec y x then S n else n end. *) Definition count := count_occ eq_nat_dec. Definition permut (l1 l2 : list nat) := forall x:nat, count l1 x = count l2 x. (* Proof of correctness *) Lemma le_lelist: forall l a x , le a x -> lelist x l -> lelist a l. induction l. auto with sortedbase. intros a0 x a0lex lelistH. inversion_clear lelistH. apply leS. apply le_trans with (m:=x);auto. apply (IHl a0 x);assumption. Qed. Lemma lelist_insert : forall l a x , le a x -> lelist a l -> lelist a (insert x l). induction l;simpl;intros. auto with sortedbase. inversion_clear H0. case_eq (leb x a);intro Hleb;auto with sortedbase. Qed. Lemma insert_correct : forall l x, sorted l -> sorted (insert x l). induction l; simpl;intros. auto with sortedbase. case_eq (leb x a);intro Hleb. assert (x<=a). apply leb_complete; assumption. apply sortS;try assumption. inversion_clear H. apply leS;try assumption. apply le_lelist with (x:=a);assumption. inversion_clear H. apply sortS;try auto. assert (a permut l2 l3 -> permut l1 l3. unfold permut. intros l1 l2 l3 Hpl1l2 Hpl2l3. intro x. transitivity (count l2 x);auto. Qed. Lemma permut_cons : forall a l1 l2, permut l1 l2 -> permut (a::l1) (a::l2). unfold permut;unfold count. intros. elim (eq_nat_dec a x);intro Hyp_eq. rewrite Hyp_eq. repeat(rewrite count_occ_cons_eq; try reflexivity). auto. repeat(rewrite count_occ_cons_neq;auto). Qed. Lemma sort_permut : forall l, permut l (sort l). induction l. simpl. unfold permut. simpl;auto. simpl. apply permut_trans with (l2:=a::(sort l)). apply permut_cons;assumption. apply insert_permut. Qed. Lemma sort_correctness : forall l, sorted(sort l) /\ permut l (sort l). split. induction l. auto with sortedbase. simpl. apply insert_correct; assumption. apply sort_permut. Qed.