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 include "datatypes/bool.ma".
16 include "datatypes/constructors.ma".
19 inductive sorted (A:Type) (P:A \to A \to Prop): list A \to Prop \def
20 | sort_nil : sorted A P []
21 | sort_cons : \forall x,l.sorted A P l \to (\forall y.in_list ? y l \to P x y)
22 \to sorted A P (x::l).
24 lemma sorted_cons_to_sorted : \forall A,P,x,l.sorted A P (x::l) \to sorted A P l.
25 intros;inversion H;intros
27 |destruct H4;assumption]
30 lemma sorted_to_minimum : \forall A,P,x,l.sorted A P (x::l) \to
31 \forall y.in_list ? y l \to P x y.
32 intros;inversion H;intros;
34 |destruct H5;apply H4;assumption]
38 let rec ordered (A:Type) (le: A → A → bool) (l: list A) on l ≝
45 le x y \land ordered A le l'
49 lemma sorted_to_eq_sorted_b_true :
51 (\forall x,y.ord x y \to ordb x y = true) \to
52 \forall l.sorted A ord l \to ordered A ordb l = true.
55 |simplify;rewrite > H1;generalize in match H2;cases l1;intros
59 |apply (sorted_to_minimum ? ? ? ? H3);apply in_list_head]
61 |apply (sorted_cons_to_sorted ? ? ? ? H3)]]
66 per far funzionare questa dimostrazione bisogna appoggiarsi a un
67 eqb (e utilizzare quindi in_list <-> mem), oppure modificare la definizione
68 di sorted in modo che non si appoggi più a in_list:
71 sorted x::y::l se ord x y e sorted y::l
73 lemma eq_sorted_b_true_to_sorted :
75 (\forall x,y.ordb x y = true \to ord x y) \to
76 \forall l.ordered A ordb l = true \to sorted A ord l.
80 [apply H1;simplify in H2;generalize in match H2;cases l1;intros
82 |simplify in H3;simplify;apply (andb_true_true_r ? ? H3)]
83 |intros;apply H;generalize in match H2;
84 generalize in match (in_list_to_mem_true ? ? ? ? H
88 let rec insert (A:Type) (le: A → A → bool) x (l: list A) on l ≝
94 | false ⇒ he::(insert A le x l')
99 ∀A:Type. ∀le: A → A → bool. ∀x.
100 ∀P:(list A → list A → Prop).
101 ∀H:(∀l: list A. l=[] → P [] [x]).
103 (∀l: list A. ∀he. ∀l'. P l' (insert ? le x l') →
104 le x he = false → l=he::l' → P (he::l') (he::(insert ? le x l'))).
106 (∀l: list A. ∀he. ∀l'. P l' (insert ? le x l') →
107 le x he = true → l=he::l' → P (he::l') (x::he::l')).
108 ∀l:list A. P l (insert ? le x l).
111 let rec insert_ind (l: list A) \def
115 l = li → P li (insert ? le x li)
121 λb. le x he = b → l = he::l' →
125 | false ⇒ he::(insert ? le x l') ])
127 [ true ⇒ H2 l he l' (insert_ind l')
128 | false ⇒ H1 l he l' (insert_ind l')
130 (refl_eq ? (le x he))
131 ] (refl_eq ? l) in insert_ind l).
135 let rec insertionsort (A:Type) (le: A → A → bool) (l: list A) on l ≝
139 let l'' ≝ insertionsort A le l' in
143 lemma ordered_injective:
144 ∀A:Type. ∀le:A → A → bool.
145 ∀l:list A. ordered A le l = true → ordered A le (tail A l) = true.
148 [ simplify; reflexivity;
150 generalize in match H1;
153 [ simplify; reflexivity;
154 | cut ((le a a1 \land ordered A le (a1::l2)) = true);
155 [ generalize in match Hcut;
159 fold simplify (ordered ? le (a1::l2));
164 apply (not_eq_true_false);
175 \forall A:Type. \forall le:A\to A\to bool.
176 (\forall a,b:A. le a b = false \to le b a = true) \to
177 \forall l:list A. \forall x:A.
178 ordered A le l = true \to ordered A le (insert A le x l) = true.
179 intros 5 (A le H l x).
180 apply (insert_ind ? ? ? (λl,il. ordered ? le l = true → ordered ? le il = true));
181 clear l; intros; simplify; intros;
183 [ generalize in match (H ? ? H2); clear H2; intro;
184 generalize in match H4; clear H4;
188 | elim (le x a); simplify;
192 rewrite > (andb_true_true ? ? H4);
196 | apply (ordered_injective ? ? ? H4)
205 theorem insertionsort_sorted:
207 ∀le:A → A → bool.∀eq:A → A → bool.
208 (∀a,b:A. le a b = false → le b a = true) \to
210 ordered A le (insertionsort A le l) = true.
211 intros 5 (A le eq le_tot l).
215 | apply (insert_sorted ? ? le_tot (insertionsort ? le l1) a);