(* based on an example in the Coq'Art book *) Require Import List. Require Import Arith. Import ListNotations. Fixpoint insert (n : nat) (l : list nat) := match l with [ ] => [n] | h :: t => if le_lt_dec n h then n :: l else h :: (insert n t) end. Example insert1 : insert 5 [2;3;6] = [2;3;5;6]. Proof. reflexivity. Qed. Fixpoint sort l := match l with [ ] => [ ] | h :: t => insert h (sort t) end. Example sort1 : sort [5;6;3;2] = [2;3;5;6]. Proof. reflexivity. Qed. (* The specification *) Inductive sorted : list nat -> Prop := sort_mt : sorted [ ] | sort_one : forall x, sorted [x] | sort_more : forall x y l, x <= y -> sorted (y :: l) -> sorted (x :: y :: l). Hint Constructors sorted: sortedbase. (* From List module (eq_dec is an implicit parameter) 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 Nat.eq_dec. Example count1 : count [3;2;4;5;2;2] 2 = 3. Proof. reflexivity. Qed. Definition permut (l1 l2 : list nat) := forall x:nat, count l1 x = count l2 x. (* We will show: Theorem sort_correctness : forall l, sorted (sort l) /\ permut l (sort l). Obvious helpful lemmas: Theorem insert_correct : forall l x, sorted l -> sorted (insert x l). Theorem insert_permut : forall l x, permut (x::l) (insert x l). *) (* Proof of correctness *) Lemma permut_refl : forall l, permut l l. Proof. unfold permut. auto. Qed. Lemma permut_swap : forall x y l l', permut l l' -> permut (x :: y :: l) (y :: x :: l'). Proof. intros x y l l' H z. simpl. case (Nat.eq_dec x z); case (Nat.eq_dec y z); simpl; auto. Qed. Lemma permut_trans: forall l l' l'', permut l l' -> permut l' l'' -> permut l l''. Proof. unfold permut. intros l l' l'' H1 H2 x. rewrite H1. apply H2. Qed. Lemma permut_cons: forall x l l', permut l l' -> permut (x :: l) (x :: l'). Proof. intros x l l' H z. simpl. case (Nat.eq_dec x z); auto. Qed. Hint Resolve permut_refl permut_swap permut_cons: sortedbase. Theorem insert_correct : forall l x, sorted l -> sorted (insert x l). Proof with (auto with sortedbase arith). intros l x H. elim H; simpl... intro z. case (le_lt_dec x z)... intros z1 z2. case (le_lt_dec x z2); simpl; intros; case (le_lt_dec x z1); simpl... Qed. Theorem insert_permut : forall l x, permut (x::l) (insert x l). Proof with (auto with sortedbase). induction l as [| a l' IH]; simpl... intro x. case (le_lt_dec x a)... intro. apply (permut_trans _ (a :: x :: l') _)... Qed. Theorem sort_sorts : forall l, sorted (sort l). Proof. induction l. - auto with sortedbase. - simpl. apply insert_correct; auto. Qed. Theorem sort_permutes : forall l, permut l (sort l). Proof. induction l; simpl. - unfold permut. auto. - apply (permut_trans _ (a :: (sort l)) _). auto with sortedbase. apply insert_permut. Qed. Theorem sort_correctness : forall l, sorted (sort l) /\ permut l (sort l). Proof. split. apply sort_sorts. apply sort_permutes. Qed.