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.
54 ∀P:(list A → list A → Prop).
55 ∀H:(∀l: list A. l=[] → P [] [x]).
57 (∀l: list A. ∀he. ∀l'. P l' (insert ? le x l') →
58 le x he = false → l=he::l' → P (he::l') (he::(insert ? le x l'))).
60 (∀l: list A. ∀he. ∀l'. P l' (insert ? le x l') →
61 le x he = true → l=he::l' → P (he::l') (x::he::l')).
62 ∀l:list A. P l (insert ? le x l).
65 let rec insert_ind (l: list A) \def
69 l = li → P li (insert ? le x li)
75 λb. le x he = b → l = he::l' →
79 | false ⇒ he::(insert ? le x l') ])
81 [ true ⇒ H2 l he l' (insert_ind l')
82 | false ⇒ H1 l he l' (insert_ind l')
85 ] (refl_eq ? l) in insert_ind l).
89 let rec insertionsort (A:Set) (le: A → A → bool) (l: list A) on l ≝
93 let l'' ≝ insertionsort A le l' in
97 lemma ordered_injective:
98 ∀ A:Set. ∀ le:A → A → bool.
100 ordered A le l = true
101 \to ordered A le (tail A l) = true.
104 [ simplify; reflexivity;
106 generalize in match H1;
109 [ simplify; reflexivity;
110 | cut ((le s s1 \land ordered A le (s1::l2)) = true);
111 [ generalize in match Hcut;
115 fold simplify (ordered ? le (s1::l2));
120 apply (not_eq_true_false);
131 \forall A:Set. \forall le:A\to A\to bool.
132 (\forall a,b:A. le a b = false \to le b a = true) \to
133 \forall l:list A. \forall x:A.
134 ordered A le l = true \to ordered A le (insert A le x l) = true.
135 intros 5 (A le H l x).
136 apply (insert_ind ? ? ? (λl,il. ordered ? le l = true → ordered ? le il = true));
137 intros; simplify; intros;
139 [ generalize in match (H ? ? H2); clear H2; intro;
140 generalize in match H4; clear H4;
144 | elim (le x s); simplify;
148 rewrite > (andb_true_true ? ? H4);
152 | apply (ordered_injective ? ? ? H4)
161 theorem insertionsort_sorted:
163 ∀le:A → A → bool.∀eq:A → A → bool.
164 (∀a,b:A. le a b = false → le b a = true) \to
166 ordered A le (insertionsort A le l) = true.
167 intros 5 (A le eq le_tot l).
171 | apply (insert_sorted A le le_tot (insertionsort A le l1) s);