1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 set "baseuri" "cic:/matita/list/sort/".
17 include "datatypes/bool.ma".
18 include "datatypes/constructors.ma".
19 include "list/list.ma".
21 let rec mem (A:Set) (eq: A → A → bool) x (l: list A) on l ≝
27 | false ⇒ mem A eq x l'
31 let rec ordered (A:Set) (le: A → A → bool) (l: list A) on l ≝
38 le x y \land ordered A le l'
42 let rec insert (A:Set) (le: A → A → bool) x (l: list A) on l ≝
48 | false ⇒ he::(insert A le x l')
52 let rec insertionsort (A:Set) (le: A → A → bool) (l: list A) on l ≝
56 let l'' ≝ insertionsort A le l' in
60 lemma ordered_injective:
61 ∀ A:Set. ∀ le:A → A → bool.
64 \to ordered A le (tail A l) = true.
67 [ simplify; reflexivity;
69 generalize in match H1;
72 [ simplify; reflexivity;
73 | cut ((le s s1 \land ordered A le (s1::l2)) = true);
74 [ generalize in match Hcut;
78 fold simplify (ordered ? le (s1::l2));
83 apply (not_eq_true_false);
94 \forall A:Set. \forall le:A\to A\to bool.
95 (\forall a,b:A. le a b = false \to le b a = true) \to
96 \forall l:list A. \forall x:A.
97 ordered A le l = true \to ordered A le (insert A le x l) = true.
98 intros 5 (A le H l x).
101 apply (bool_elim ? (le x s));
104 fold simplify (ordered ? le (s::l1));
108 | generalize in match H2;
110 generalize in match s;
114 rewrite > (H x a H2);
116 | simplify in \vdash (? ? (? ? ? %) ?);
117 apply (bool_elim ? (le x s));
120 fold simplify (ordered A le (s::l2));
122 rewrite > (H x a H3);
124 fold simplify (ordered A le (s::l2));
127 apply (ordered_injective A le (a::s::l2));
131 fold simplify (ordered A le (s::(insert A le x l2)));
134 fold simplify (ordered A le (s::l2)) in H2;
135 generalize in match H2;
136 apply (andb_elim (le a s));
138 [ change with (ordered A le (s::l2) = true \to ordered A le (s::insert A le x l2) = true);
142 | simplify; intros; assumption
147 | simplify; reflexivity;
151 theorem insertionsort_sorted:
153 ∀le:A → A → bool.∀eq:A → A → bool.
154 (∀a,b:A. le a b = false → le b a = true) \to
156 ordered A le (insertionsort A le l) = true.
157 intros 5 (A le eq le_tot l).
161 | apply (insert_sorted A le le_tot (insertionsort A le l1) s);
167 theorem insertionsort_correct:
169 ∀le:A → A → bool.∀eq:A → A → bool.
170 (∀a,b:A. le a b = false → le b a = true) \to
172 l' = insertionsort A le l
173 \to ordered A le l' = true
174 ∧ ((\forall x:A. mem A eq x l = true \to mem A eq x l' = true)
175 ∧ (\forall x:A. mem A eq x l = true \to mem A eq x l' = true)).
179 apply (insertionsort_sorted A le eq H);
181 [ TO BE CONTINUED ...