(* insertsort.v *) (* Przykład zaczerpnięty z Coq'Art *) Require Import List. Require Import ZArith. Open Scope Z_scope. (**** Implementacja ****) Fixpoint insert (z:Z) (l : list Z) {struct l} : list Z := match l with | nil => z :: nil | a::l' => match Z_le_gt_dec z a with | left _ => z :: a :: l' | right _ => a :: (insert z l') end end. Fixpoint sort (l : list Z) {struct l} : (list Z) := match l with | nil => nil | a::l' => insert a (sort l') end. (**** Testy ****) Eval compute in (sort (5::2::7::9::0::nil)). (**** Specyfikacja ****) Inductive sorted : list Z -> Prop := | sorted0 : sorted nil | sorted1: forall z:Z, sorted (z :: nil) | sorted2: forall (z1 z2 : Z) (l : list Z), z1 <= z2 -> sorted (z2 :: l) -> sorted (z1 :: z2 :: l). (* Jaka jest liczba wystąpień elementu w liście? *) Fixpoint nb_occ (z:Z) (l : list Z) {struct l} : nat := match l with | nil => 0%nat | (z' :: l') => match Z_eq_dec z z' with | left _ => S (nb_occ z l') | right _ => nb_occ z l' end end. (* Kiedy jedna lista jest permutacją drugiej? *) Definition equiv (l l' : list Z) := forall z : Z, nb_occ z l = nb_occ z l'. Program Definition sort' : forall l : list Z, {l' : list Z | equiv l l' /\ sorted l'} := sort. Obligations. (**** Dowód ****) Hint Resolve sorted0 sorted1 sorted2 : sort. (* Wstawienie elementu do posortowanej listy daje posortowaną listę. *) Lemma insert_sorted : forall (l : list Z) (x : Z), sorted l -> sorted (insert x l). Proof. intros l x H; elim H; simpl; auto with sort. intro z; case (Z_le_gt_dec x z); simpl; auto with sort zarith. intros z1 z2; case (Z_le_gt_dec x z2); simpl; intros; case (Z_le_gt_dec x z1); simpl; auto with sort zarith. Qed. Lemma sort_sorted : forall (l : list Z), sorted (sort l). Proof. induction l. auto with sort. simpl. apply insert_sorted. assumption. Qed. (* Relacja equiv jest relacją równoważności. *) (* Zwrotność. *) Lemma equiv_refl : forall l : list Z, equiv l l. Proof. unfold equiv. trivial. Qed. (* Symetria. *) Lemma equiv_sym : forall l l' : list Z, equiv l l' -> equiv l' l. Proof. unfold equiv. auto. Qed. (* Przechodniość. *) Lemma equiv_trans : forall l l' l'' : list Z, equiv l l' -> equiv l' l'' -> equiv l l''. Proof. intros. unfold equiv in *. intro. eapply trans_eq; eauto. Qed. (* Lista o tej samej głowie co inna lista i ogonie będącym *) (* permutacją ogona tej innej listy, jest jej permutacją. *) Lemma equiv_cons : forall (z : Z) (l l' : list Z), equiv l l' -> equiv (z :: l) (z :: l'). Proof. intros z l l' H. intro z'. simpl. case (Z_eq_dec z' z); auto. Qed. (* Permutacja dwóch pierwszych elementów i reszty daje *) (* permutację całości. *) Lemma equiv_perm : forall (a b : Z) (l l' : list Z), equiv l l' -> equiv (a :: b :: l) (b :: a :: l'). Proof. intros a b l l' H z; simpl. case (Z_eq_dec z a); case (Z_eq_dec z b); simpl; case (H z); auto. Qed. Hint Resolve equiv_cons equiv_refl equiv_perm : sort. (* Lista powstała przez wstawienie do innej listy elementu na właściwe *) (* miejsce jest permutacją listy powstałej z tej innej listy przez *) (* dołączenie wstawianego elementu na początek listy. *) Lemma insert_equiv : forall (l : list Z) (x : Z), equiv (x :: l) (insert x l). Proof. induction l as [| a l0 H]; simpl; auto with sort. intros x; case (Z_le_gt_dec x a); simpl; auto with sort. intro; eapply equiv_trans with (a :: x :: l0); eauto with sort. Qed. Lemma sort_equiv : forall (l : list Z), (equiv l (sort l)). Proof. induction l. auto with sort. simpl. apply equiv_trans with (a :: (sort l)). auto with sort. apply insert_equiv. Qed. (* Finał: *) Next Obligation. Proof. split. apply sort_equiv. apply sort_sorted. Qed. Check sort'. Extraction insert. Extraction sort. (**** Koniec ****)