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);
95 \forall A:Set. \forall le:A\to A\to bool.
96 (\forall a,b:A. le a b = false \to le b a = true) \to
97 \forall l:list A. \forall x:A.
98 ordered A le l = true \to ordered A le (insert A le x l) = true.
99 intros 5 (A le H l x).
101 let rec insert_ind (l: list A) \def
105 l = li → ordered ? le li = true →
106 ordered ? le (insert A le x li) = true
112 λb. le x he = b → l = he::l' →
113 ordered ? le (he::l') = true → ordered ? le
116 | false ⇒ he::(insert A le x l') ]) = true
119 | false ⇒ let res ≝ insert_ind l' in ?
121 (refl_eq ? (le x he))
122 ] (refl_eq ? l) in insert_ind l);
125 [ rewrite > insert_ind;
126 [ generalize in match (H ? ? H1); clear H1; intro;
127 generalize in match H3; clear H3;
131 | elim (le x s); simplify;
135 rewrite > (andb_true_true ? ? H3);
140 | apply (ordered_injective ? ? ? H3)
149 theorem insertionsort_sorted:
151 ∀le:A → A → bool.∀eq:A → A → bool.
152 (∀a,b:A. le a b = false → le b a = true) \to
154 ordered A le (insertionsort A le l) = true.
155 intros 5 (A le eq le_tot l).
159 | apply (insert_sorted A le le_tot (insertionsort A le l1) s);