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')
53 ∀A:Set. ∀le: A → A → bool. ∀x:A.
55 ∀l:list A. P (insert A le x l).
56 intros (A le x P H l).
58 let rec insert_ind (l: list A) ≝
59 match l in list return λl.P (insert A le x l) with
62 match le x he return λb.P (match b with [ true ⇒ x::he::l' | false ⇒ he::(insert A le x l') ]) with
63 [ true ⇒ (H2 : P (x::he::l'))
64 | false ⇒ (? : P (he::(insert A le x l')))
72 let rec insertionsort (A:Set) (le: A → A → bool) (l: list A) on l ≝
76 let l'' ≝ insertionsort A le l' in
80 lemma ordered_injective:
81 ∀ A:Set. ∀ le:A → A → bool.
84 \to ordered A le (tail A l) = true.
87 [ simplify; reflexivity;
89 generalize in match H1;
92 [ simplify; reflexivity;
93 | cut ((le s s1 \land ordered A le (s1::l2)) = true);
94 [ generalize in match Hcut;
98 fold simplify (ordered ? le (s1::l2));
103 apply (not_eq_true_false);
115 \forall A:Set. \forall le:A\to A\to bool.
116 (\forall a,b:A. le a b = false \to le b a = true) \to
117 \forall l:list A. \forall x:A.
118 ordered A le l = true \to ordered A le (insert A le x l) = true.
119 intros (A le H l x K).
120 letin P ≝ (\lambda ll. ordered A le ll = true).
121 fold simplify (P (insert A le x l)).
123 let rec insert_ind (l: list A) \def
124 match l in list return λli. l = li → P (insert A le x li) with
125 [ nil ⇒ (? : l = [] → P [x])
129 λb. le x he = b → l = he::l' → P (match b with
131 | false ⇒ he::(insert A le x l') ])
133 [ true ⇒ (? : le x he = true → l = he::l' → P (x::he::l'))
135 (? : \forall lrec. P (insert A le x lrec) \to
136 le x he = false → l = he::l' → P (he::(insert A le x l')))
139 (refl_eq ? (le x he))
140 ] (refl_eq ? l) in insert_ind l);
144 apply andb_elim; simplify;
145 generalize in match K; clear K;
157 [ rewrite > H1; simplify;
158 generalize in match (ordered_injective A le l K);
159 rewrite > H2; simplify; intro; change with (ordered A le l' = true).
165 rewrite > H1; simplify.
166 elim l'; [ reflexivity | simplify;
173 \forall A:Set. \forall le:A\to A\to bool.
174 (\forall a,b:A. le a b = false \to le b a = true) \to
175 \forall l:list A. \forall x:A.
176 ordered A le l = true \to ordered A le (insert A le x l) = true.
177 intros 5 (A le H l x).
180 apply (bool_elim ? (le x s));
183 fold simplify (ordered ? le (s::l1));
187 | change with (le x s = false → ordered ? le (s::insert A le x l1) = true);
188 generalize in match H2;
190 generalize in match s;
194 rewrite > (H x a H2);
196 | simplify in \vdash (? ? (? ? ? %) ?);
197 change with (ordered A le (a::(insert A le x (s::l2))) = true);
199 apply (bool_elim ? (le x s));
202 fold simplify (ordered A le (s::l2));
204 rewrite > (H x a H3);
206 fold simplify (ordered A le (s::l2));
209 apply (ordered_injective A le (a::s::l2));
213 fold simplify (ordered A le (s::(insert A le x l2)));
216 fold simplify (ordered A le (s::l2)) in H2;
217 generalize in match H2;
218 apply (andb_elim (le a s));
220 [ change with (ordered A le (s::l2) = true \to ordered A le (s::insert A le x l2) = true);
224 | simplify; intros; assumption
229 | simplify; reflexivity;
233 theorem insertionsort_sorted:
235 ∀le:A → A → bool.∀eq:A → A → bool.
236 (∀a,b:A. le a b = false → le b a = true) \to
238 ordered A le (insertionsort A le l) = true.
239 intros 5 (A le eq le_tot l).
243 | apply (insert_sorted A le le_tot (insertionsort A le l1) s);