1 | (* *********************************************************************) |
---|
2 | (* *) |
---|
3 | (* The Compcert verified compiler *) |
---|
4 | (* *) |
---|
5 | (* Xavier Leroy, INRIA Paris-Rocquencourt *) |
---|
6 | (* *) |
---|
7 | (* Copyright Institut National de Recherche en Informatique et en *) |
---|
8 | (* Automatique. All rights reserved. This file is distributed *) |
---|
9 | (* under the terms of the GNU General Public License as published by *) |
---|
10 | (* the Free Software Foundation, either version 2 of the License, or *) |
---|
11 | (* (at your option) any later version. This file is also distributed *) |
---|
12 | (* under the terms of the INRIA Non-Commercial License Agreement. *) |
---|
13 | (* *) |
---|
14 | (* *********************************************************************) |
---|
15 | |
---|
16 | (* * Applicative finite maps are the main data structure used in this |
---|
17 | project. A finite map associates data to keys. The two main operations |
---|
18 | are [set k d m], which returns a map identical to [m] except that [d] |
---|
19 | is associated to [k], and [get k m] which returns the data associated |
---|
20 | to key [k] in map [m]. In this library, we distinguish two kinds of maps: |
---|
21 | - Trees: the [get] operation returns an option type, either [None] |
---|
22 | if no data is associated to the key, or [Some d] otherwise. |
---|
23 | - Maps: the [get] operation always returns a data. If no data was explicitly |
---|
24 | associated with the key, a default data provided at map initialization time |
---|
25 | is returned. |
---|
26 | |
---|
27 | In this library, we provide efficient implementations of trees and |
---|
28 | maps whose keys range over the type [positive] of binary positive |
---|
29 | integers or any type that can be injected into [positive]. The |
---|
30 | implementation is based on radix-2 search trees (uncompressed |
---|
31 | Patricia trees) and guarantees logarithmic-time operations. An |
---|
32 | inefficient implementation of maps as functions is also provided. |
---|
33 | *) |
---|
34 | |
---|
35 | include "Coqlib.ma". |
---|
36 | (* XXX: For ident type; should maybe follow original and use positives *) |
---|
37 | include "AST.ma". |
---|
38 | |
---|
39 | (* |
---|
40 | Set Implicit Arguments. |
---|
41 | *) |
---|
42 | (* * * The abstract signatures of trees *) |
---|
43 | |
---|
44 | record TREE (elt:Type[0]) : Type[1] ≝ { |
---|
45 | elt_eq: ∀a,b: elt. (a = b) + (a ≠ b); |
---|
46 | tree_t: Type[0] → Type[0]; |
---|
47 | tree_eq: ∀A: Type[0]. ∀x,y: A. (x=y) + (x≠y) → |
---|
48 | ∀a,b: tree_t A. (a = b) + (a ≠ b); |
---|
49 | empty: ∀A: Type[0]. tree_t A; |
---|
50 | get: ∀A: Type[0]. elt → tree_t A → option A; |
---|
51 | set: ∀A: Type[0]. elt → A → tree_t A → tree_t A; |
---|
52 | remove: ∀A: Type[0]. elt → tree_t A → tree_t A; |
---|
53 | (* |
---|
54 | (** The ``good variables'' properties for trees, expressing |
---|
55 | commutations between [get], [set] and [remove]. *) |
---|
56 | Hypothesis gempty: |
---|
57 | forall (A: Type) (i: elt), get i (empty A) = None. |
---|
58 | Hypothesis gss: |
---|
59 | forall (A: Type) (i: elt) (x: A) (m: t A), get i (set i x m) = Some x. |
---|
60 | Hypothesis gso: |
---|
61 | forall (A: Type) (i j: elt) (x: A) (m: t A), |
---|
62 | i <> j -> get i (set j x m) = get i m. |
---|
63 | Hypothesis gsspec: |
---|
64 | forall (A: Type) (i j: elt) (x: A) (m: t A), |
---|
65 | get i (set j x m) = if elt_eq i j then Some x else get i m. |
---|
66 | Hypothesis gsident: |
---|
67 | forall (A: Type) (i: elt) (m: t A) (v: A), |
---|
68 | get i m = Some v -> set i v m = m. |
---|
69 | (* We could implement the following, but it's not needed for the moment. |
---|
70 | Hypothesis grident: |
---|
71 | forall (A: Type) (i: elt) (m: t A) (v: A), |
---|
72 | get i m = None -> remove i m = m. |
---|
73 | *) |
---|
74 | Hypothesis grs: |
---|
75 | forall (A: Type) (i: elt) (m: t A), get i (remove i m) = None. |
---|
76 | Hypothesis gro: |
---|
77 | forall (A: Type) (i j: elt) (m: t A), |
---|
78 | i <> j -> get i (remove j m) = get i m. |
---|
79 | Hypothesis grspec: |
---|
80 | forall (A: Type) (i j: elt) (m: t A), |
---|
81 | get i (remove j m) = if elt_eq i j then None else get i m. |
---|
82 | |
---|
83 | (** Extensional equality between trees. *) |
---|
84 | Variable beq: forall (A: Type), (A -> A -> bool) -> t A -> t A -> bool. |
---|
85 | Hypothesis beq_correct: |
---|
86 | forall (A: Type) (P: A -> A -> Prop) (cmp: A -> A -> bool), |
---|
87 | (forall (x y: A), cmp x y = true -> P x y) -> |
---|
88 | forall (t1 t2: t A), beq cmp t1 t2 = true -> |
---|
89 | forall (x: elt), |
---|
90 | match get x t1, get x t2 with |
---|
91 | | None, None => True |
---|
92 | | Some y1, Some y2 => P y1 y2 |
---|
93 | | _, _ => False |
---|
94 | end. |
---|
95 | |
---|
96 | (** Applying a function to all data of a tree. *) |
---|
97 | *) |
---|
98 | tree_map: ∀A,B: Type[0]. (elt → A → B) → tree_t A → tree_t B; |
---|
99 | (* |
---|
100 | Hypothesis gmap: |
---|
101 | forall (A B: Type) (f: elt -> A -> B) (i: elt) (m: t A), |
---|
102 | get i (map f m) = option_map (f i) (get i m). |
---|
103 | |
---|
104 | (** Applying a function pairwise to all data of two trees. *) |
---|
105 | Variable combine: |
---|
106 | forall (A: Type), (option A -> option A -> option A) -> t A -> t A -> t A. |
---|
107 | Hypothesis gcombine: |
---|
108 | forall (A: Type) (f: option A -> option A -> option A), |
---|
109 | f None None = None -> |
---|
110 | forall (m1 m2: t A) (i: elt), |
---|
111 | get i (combine f m1 m2) = f (get i m1) (get i m2). |
---|
112 | Hypothesis combine_commut: |
---|
113 | forall (A: Type) (f g: option A -> option A -> option A), |
---|
114 | (forall (i j: option A), f i j = g j i) -> |
---|
115 | forall (m1 m2: t A), |
---|
116 | combine f m1 m2 = combine g m2 m1. |
---|
117 | |
---|
118 | (** Enumerating the bindings of a tree. *) |
---|
119 | *) |
---|
120 | elements: ∀A: Type[0]. tree_t A → list (elt × A); |
---|
121 | (* |
---|
122 | Hypothesis elements_correct: |
---|
123 | forall (A: Type[0]) (m: t A) (i: elt) (v: A), |
---|
124 | get i m = Some v -> In (i, v) (elements m). |
---|
125 | Hypothesis elements_complete: |
---|
126 | forall (A: Type) (m: t A) (i: elt) (v: A), |
---|
127 | In (i, v) (elements m) -> get i m = Some v. |
---|
128 | Hypothesis elements_keys_norepet: |
---|
129 | forall (A: Type) (m: t A), |
---|
130 | list_norepet (List.map (@fst elt A) (elements m)). |
---|
131 | |
---|
132 | (** Folding a function over all bindings of a tree. *) |
---|
133 | *) |
---|
134 | tree_fold: ∀A,B: Type[0]. (B → elt → A → B) → tree_t A → B → B |
---|
135 | (* |
---|
136 | Hypothesis fold_spec: |
---|
137 | forall (A B: Type) (f: B -> elt -> A -> B) (v: B) (m: t A), |
---|
138 | fold f m v = |
---|
139 | List.fold_left (fun a p => f a (fst p) (snd p)) (elements m) v. |
---|
140 | *) |
---|
141 | }. |
---|
142 | (* |
---|
143 | (** * The abstract signatures of maps *) |
---|
144 | |
---|
145 | record MAP : Type[1] ≝ { |
---|
146 | elt: Type[0]; |
---|
147 | elt_eq: ∀a,b: elt. (a = b) + (a ≠ b); |
---|
148 | t: Type[0] → Type[0]; |
---|
149 | init: ∀A: Type[0]. A → t A; |
---|
150 | get: ∀A: Type[0]. elt → t A → A; |
---|
151 | set: ∀A: Type[0]. elt → A → t A → t A |
---|
152 | }. |
---|
153 | Hypothesis gi: |
---|
154 | forall (A: Type) (i: elt) (x: A), get i (init x) = x. |
---|
155 | Hypothesis gss: |
---|
156 | forall (A: Type) (i: elt) (x: A) (m: t A), get i (set i x m) = x. |
---|
157 | Hypothesis gso: |
---|
158 | forall (A: Type) (i j: elt) (x: A) (m: t A), |
---|
159 | i <> j -> get i (set j x m) = get i m. |
---|
160 | Hypothesis gsspec: |
---|
161 | forall (A: Type) (i j: elt) (x: A) (m: t A), |
---|
162 | get i (set j x m) = if elt_eq i j then x else get i m. |
---|
163 | Hypothesis gsident: |
---|
164 | forall (A: Type) (i j: elt) (m: t A), get j (set i (get i m) m) = get j m. |
---|
165 | Variable map: forall (A B: Type), (A -> B) -> t A -> t B. |
---|
166 | Hypothesis gmap: |
---|
167 | forall (A B: Type) (f: A -> B) (i: elt) (m: t A), |
---|
168 | get i (map f m) = f(get i m). |
---|
169 | End MAP. |
---|
170 | |
---|
171 | (** * An implementation of trees over type [positive] *) |
---|
172 | *) |
---|
173 | |
---|
174 | (* XXX: need real tree impl *) |
---|
175 | let rec assoc_get (A:Type[0]) (i:ident) (l:list (ident × A)) on l ≝ |
---|
176 | match l with |
---|
177 | [ nil ⇒ None ? |
---|
178 | | cons h t ⇒ |
---|
179 | match h with [ pair hi ha ⇒ |
---|
180 | match ident_eq i hi with [ inl _ ⇒ Some ? ha | inr _ ⇒ assoc_get A i t ] ] |
---|
181 | ]. |
---|
182 | |
---|
183 | axiom assoc_tree_eq: ∀A: Type[0]. ∀x,y: A. (x=y) + (x≠y) → |
---|
184 | ∀a,b: list (ident × A). (a = b) + (a ≠ b). |
---|
185 | axiom assoc_remove: ∀A: Type[0]. ident → list (ident × A) → list (ident × A). |
---|
186 | axiom assoc_tree_map: ∀A,B: Type[0]. (ident → A → B) → list (ident × A) → list (ident × B). |
---|
187 | definition assoc_elements: ∀A: Type[0]. list (ident × A) → list (ident × A) ≝ λA,x.x. |
---|
188 | axiom assoc_tree_fold: ∀A,B: Type[0]. (B → ident → A → B) → list (ident × A) → B → B. |
---|
189 | |
---|
190 | definition PTree : TREE ident ≝ |
---|
191 | mk_TREE ? |
---|
192 | ident_eq |
---|
193 | (λA. list (ident × A)) |
---|
194 | assoc_tree_eq |
---|
195 | (λA. nil ?) |
---|
196 | assoc_get |
---|
197 | (λA,i,a,l.〈i,a〉::l) |
---|
198 | assoc_remove |
---|
199 | assoc_tree_map |
---|
200 | assoc_elements |
---|
201 | assoc_tree_fold. |
---|
202 | |
---|
203 | (* |
---|
204 | Module PTree <: TREE. |
---|
205 | Definition elt := positive. |
---|
206 | Definition elt_eq := peq. |
---|
207 | |
---|
208 | Inductive tree (A : Type) : Type := |
---|
209 | | Leaf : tree A |
---|
210 | | Node : tree A -> option A -> tree A -> tree A |
---|
211 | . |
---|
212 | Implicit Arguments Leaf [A]. |
---|
213 | Implicit Arguments Node [A]. |
---|
214 | |
---|
215 | Definition t := tree. |
---|
216 | |
---|
217 | Theorem eq : forall (A : Type), |
---|
218 | (forall (x y: A), {x=y} + {x<>y}) -> |
---|
219 | forall (a b : t A), {a = b} + {a <> b}. |
---|
220 | Proof. |
---|
221 | intros A eqA. |
---|
222 | decide equality. |
---|
223 | generalize o o0; decide equality. |
---|
224 | Qed. |
---|
225 | |
---|
226 | Definition empty (A : Type) := (Leaf : t A). |
---|
227 | |
---|
228 | Fixpoint get (A : Type) (i : positive) (m : t A) {struct i} : option A := |
---|
229 | match m with |
---|
230 | | Leaf => None |
---|
231 | | Node l o r => |
---|
232 | match i with |
---|
233 | | xH => o |
---|
234 | | xO ii => get ii l |
---|
235 | | xI ii => get ii r |
---|
236 | end |
---|
237 | end. |
---|
238 | |
---|
239 | Fixpoint set (A : Type) (i : positive) (v : A) (m : t A) {struct i} : t A := |
---|
240 | match m with |
---|
241 | | Leaf => |
---|
242 | match i with |
---|
243 | | xH => Node Leaf (Some v) Leaf |
---|
244 | | xO ii => Node (set ii v Leaf) None Leaf |
---|
245 | | xI ii => Node Leaf None (set ii v Leaf) |
---|
246 | end |
---|
247 | | Node l o r => |
---|
248 | match i with |
---|
249 | | xH => Node l (Some v) r |
---|
250 | | xO ii => Node (set ii v l) o r |
---|
251 | | xI ii => Node l o (set ii v r) |
---|
252 | end |
---|
253 | end. |
---|
254 | |
---|
255 | Fixpoint remove (A : Type) (i : positive) (m : t A) {struct i} : t A := |
---|
256 | match i with |
---|
257 | | xH => |
---|
258 | match m with |
---|
259 | | Leaf => Leaf |
---|
260 | | Node Leaf o Leaf => Leaf |
---|
261 | | Node l o r => Node l None r |
---|
262 | end |
---|
263 | | xO ii => |
---|
264 | match m with |
---|
265 | | Leaf => Leaf |
---|
266 | | Node l None Leaf => |
---|
267 | match remove ii l with |
---|
268 | | Leaf => Leaf |
---|
269 | | mm => Node mm None Leaf |
---|
270 | end |
---|
271 | | Node l o r => Node (remove ii l) o r |
---|
272 | end |
---|
273 | | xI ii => |
---|
274 | match m with |
---|
275 | | Leaf => Leaf |
---|
276 | | Node Leaf None r => |
---|
277 | match remove ii r with |
---|
278 | | Leaf => Leaf |
---|
279 | | mm => Node Leaf None mm |
---|
280 | end |
---|
281 | | Node l o r => Node l o (remove ii r) |
---|
282 | end |
---|
283 | end. |
---|
284 | |
---|
285 | Theorem gempty: |
---|
286 | forall (A: Type) (i: positive), get i (empty A) = None. |
---|
287 | Proof. |
---|
288 | induction i; simpl; auto. |
---|
289 | Qed. |
---|
290 | |
---|
291 | Theorem gss: |
---|
292 | forall (A: Type) (i: positive) (x: A) (m: t A), get i (set i x m) = Some x. |
---|
293 | Proof. |
---|
294 | induction i; destruct m; simpl; auto. |
---|
295 | Qed. |
---|
296 | |
---|
297 | Lemma gleaf : forall (A : Type) (i : positive), get i (Leaf : t A) = None. |
---|
298 | Proof. exact gempty. Qed. |
---|
299 | |
---|
300 | Theorem gso: |
---|
301 | forall (A: Type) (i j: positive) (x: A) (m: t A), |
---|
302 | i <> j -> get i (set j x m) = get i m. |
---|
303 | Proof. |
---|
304 | induction i; intros; destruct j; destruct m; simpl; |
---|
305 | try rewrite <- (gleaf A i); auto; try apply IHi; congruence. |
---|
306 | Qed. |
---|
307 | |
---|
308 | Theorem gsspec: |
---|
309 | forall (A: Type) (i j: positive) (x: A) (m: t A), |
---|
310 | get i (set j x m) = if peq i j then Some x else get i m. |
---|
311 | Proof. |
---|
312 | intros. |
---|
313 | destruct (peq i j); [ rewrite e; apply gss | apply gso; auto ]. |
---|
314 | Qed. |
---|
315 | |
---|
316 | Theorem gsident: |
---|
317 | forall (A: Type) (i: positive) (m: t A) (v: A), |
---|
318 | get i m = Some v -> set i v m = m. |
---|
319 | Proof. |
---|
320 | induction i; intros; destruct m; simpl; simpl in H; try congruence. |
---|
321 | rewrite (IHi m2 v H); congruence. |
---|
322 | rewrite (IHi m1 v H); congruence. |
---|
323 | Qed. |
---|
324 | |
---|
325 | Lemma rleaf : forall (A : Type) (i : positive), remove i (Leaf : t A) = Leaf. |
---|
326 | Proof. destruct i; simpl; auto. Qed. |
---|
327 | |
---|
328 | Theorem grs: |
---|
329 | forall (A: Type) (i: positive) (m: t A), get i (remove i m) = None. |
---|
330 | Proof. |
---|
331 | induction i; destruct m. |
---|
332 | simpl; auto. |
---|
333 | destruct m1; destruct o; destruct m2 as [ | ll oo rr]; simpl; auto. |
---|
334 | rewrite (rleaf A i); auto. |
---|
335 | cut (get i (remove i (Node ll oo rr)) = None). |
---|
336 | destruct (remove i (Node ll oo rr)); auto; apply IHi. |
---|
337 | apply IHi. |
---|
338 | simpl; auto. |
---|
339 | destruct m1 as [ | ll oo rr]; destruct o; destruct m2; simpl; auto. |
---|
340 | rewrite (rleaf A i); auto. |
---|
341 | cut (get i (remove i (Node ll oo rr)) = None). |
---|
342 | destruct (remove i (Node ll oo rr)); auto; apply IHi. |
---|
343 | apply IHi. |
---|
344 | simpl; auto. |
---|
345 | destruct m1; destruct m2; simpl; auto. |
---|
346 | Qed. |
---|
347 | |
---|
348 | Theorem gro: |
---|
349 | forall (A: Type) (i j: positive) (m: t A), |
---|
350 | i <> j -> get i (remove j m) = get i m. |
---|
351 | Proof. |
---|
352 | induction i; intros; destruct j; destruct m; |
---|
353 | try rewrite (rleaf A (xI j)); |
---|
354 | try rewrite (rleaf A (xO j)); |
---|
355 | try rewrite (rleaf A 1); auto; |
---|
356 | destruct m1; destruct o; destruct m2; |
---|
357 | simpl; |
---|
358 | try apply IHi; try congruence; |
---|
359 | try rewrite (rleaf A j); auto; |
---|
360 | try rewrite (gleaf A i); auto. |
---|
361 | cut (get i (remove j (Node m2_1 o m2_2)) = get i (Node m2_1 o m2_2)); |
---|
362 | [ destruct (remove j (Node m2_1 o m2_2)); try rewrite (gleaf A i); auto |
---|
363 | | apply IHi; congruence ]. |
---|
364 | destruct (remove j (Node m1_1 o0 m1_2)); simpl; try rewrite (gleaf A i); |
---|
365 | auto. |
---|
366 | destruct (remove j (Node m2_1 o m2_2)); simpl; try rewrite (gleaf A i); |
---|
367 | auto. |
---|
368 | cut (get i (remove j (Node m1_1 o0 m1_2)) = get i (Node m1_1 o0 m1_2)); |
---|
369 | [ destruct (remove j (Node m1_1 o0 m1_2)); try rewrite (gleaf A i); auto |
---|
370 | | apply IHi; congruence ]. |
---|
371 | destruct (remove j (Node m2_1 o m2_2)); simpl; try rewrite (gleaf A i); |
---|
372 | auto. |
---|
373 | destruct (remove j (Node m1_1 o0 m1_2)); simpl; try rewrite (gleaf A i); |
---|
374 | auto. |
---|
375 | Qed. |
---|
376 | |
---|
377 | Theorem grspec: |
---|
378 | forall (A: Type) (i j: elt) (m: t A), |
---|
379 | get i (remove j m) = if elt_eq i j then None else get i m. |
---|
380 | Proof. |
---|
381 | intros. destruct (elt_eq i j). subst j. apply grs. apply gro; auto. |
---|
382 | Qed. |
---|
383 | |
---|
384 | Section EXTENSIONAL_EQUALITY. |
---|
385 | |
---|
386 | Variable A: Type. |
---|
387 | Variable eqA: A -> A -> Prop. |
---|
388 | Variable beqA: A -> A -> bool. |
---|
389 | Hypothesis beqA_correct: forall x y, beqA x y = true -> eqA x y. |
---|
390 | |
---|
391 | Definition exteq (m1 m2: t A) : Prop := |
---|
392 | forall (x: elt), |
---|
393 | match get x m1, get x m2 with |
---|
394 | | None, None => True |
---|
395 | | Some y1, Some y2 => eqA y1 y2 |
---|
396 | | _, _ => False |
---|
397 | end. |
---|
398 | |
---|
399 | Fixpoint bempty (m: t A) : bool := |
---|
400 | match m with |
---|
401 | | Leaf => true |
---|
402 | | Node l None r => bempty l && bempty r |
---|
403 | | Node l (Some _) r => false |
---|
404 | end. |
---|
405 | |
---|
406 | Lemma bempty_correct: |
---|
407 | forall m, bempty m = true -> forall x, get x m = None. |
---|
408 | Proof. |
---|
409 | induction m; simpl; intros. |
---|
410 | change (@Leaf A) with (empty A). apply gempty. |
---|
411 | destruct o. congruence. destruct (andb_prop _ _ H). |
---|
412 | destruct x; simpl; auto. |
---|
413 | Qed. |
---|
414 | |
---|
415 | Fixpoint beq (m1 m2: t A) {struct m1} : bool := |
---|
416 | match m1, m2 with |
---|
417 | | Leaf, _ => bempty m2 |
---|
418 | | _, Leaf => bempty m1 |
---|
419 | | Node l1 o1 r1, Node l2 o2 r2 => |
---|
420 | match o1, o2 with |
---|
421 | | None, None => true |
---|
422 | | Some y1, Some y2 => beqA y1 y2 |
---|
423 | | _, _ => false |
---|
424 | end |
---|
425 | && beq l1 l2 && beq r1 r2 |
---|
426 | end. |
---|
427 | |
---|
428 | Lemma beq_correct: |
---|
429 | forall m1 m2, beq m1 m2 = true -> exteq m1 m2. |
---|
430 | Proof. |
---|
431 | induction m1; destruct m2; simpl. |
---|
432 | intros; red; intros. change (@Leaf A) with (empty A). |
---|
433 | repeat rewrite gempty. auto. |
---|
434 | destruct o; intro. congruence. |
---|
435 | red; intros. change (@Leaf A) with (empty A). rewrite gempty. |
---|
436 | rewrite bempty_correct. auto. assumption. |
---|
437 | destruct o; intro. congruence. |
---|
438 | red; intros. change (@Leaf A) with (empty A). rewrite gempty. |
---|
439 | rewrite bempty_correct. auto. assumption. |
---|
440 | destruct o; destruct o0; simpl; intro; try congruence. |
---|
441 | destruct (andb_prop _ _ H). destruct (andb_prop _ _ H0). |
---|
442 | red; intros. destruct x; simpl. |
---|
443 | apply IHm1_2; auto. apply IHm1_1; auto. |
---|
444 | apply beqA_correct; auto. |
---|
445 | destruct (andb_prop _ _ H). |
---|
446 | red; intros. destruct x; simpl. |
---|
447 | apply IHm1_2; auto. apply IHm1_1; auto. |
---|
448 | auto. |
---|
449 | Qed. |
---|
450 | |
---|
451 | End EXTENSIONAL_EQUALITY. |
---|
452 | |
---|
453 | Fixpoint append (i j : positive) {struct i} : positive := |
---|
454 | match i with |
---|
455 | | xH => j |
---|
456 | | xI ii => xI (append ii j) |
---|
457 | | xO ii => xO (append ii j) |
---|
458 | end. |
---|
459 | |
---|
460 | Lemma append_assoc_0 : forall (i j : positive), |
---|
461 | append i (xO j) = append (append i (xO xH)) j. |
---|
462 | Proof. |
---|
463 | induction i; intros; destruct j; simpl; |
---|
464 | try rewrite (IHi (xI j)); |
---|
465 | try rewrite (IHi (xO j)); |
---|
466 | try rewrite <- (IHi xH); |
---|
467 | auto. |
---|
468 | Qed. |
---|
469 | |
---|
470 | Lemma append_assoc_1 : forall (i j : positive), |
---|
471 | append i (xI j) = append (append i (xI xH)) j. |
---|
472 | Proof. |
---|
473 | induction i; intros; destruct j; simpl; |
---|
474 | try rewrite (IHi (xI j)); |
---|
475 | try rewrite (IHi (xO j)); |
---|
476 | try rewrite <- (IHi xH); |
---|
477 | auto. |
---|
478 | Qed. |
---|
479 | |
---|
480 | Lemma append_neutral_r : forall (i : positive), append i xH = i. |
---|
481 | Proof. |
---|
482 | induction i; simpl; congruence. |
---|
483 | Qed. |
---|
484 | |
---|
485 | Lemma append_neutral_l : forall (i : positive), append xH i = i. |
---|
486 | Proof. |
---|
487 | simpl; auto. |
---|
488 | Qed. |
---|
489 | |
---|
490 | Fixpoint xmap (A B : Type) (f : positive -> A -> B) (m : t A) (i : positive) |
---|
491 | {struct m} : t B := |
---|
492 | match m with |
---|
493 | | Leaf => Leaf |
---|
494 | | Node l o r => Node (xmap f l (append i (xO xH))) |
---|
495 | (option_map (f i) o) |
---|
496 | (xmap f r (append i (xI xH))) |
---|
497 | end. |
---|
498 | |
---|
499 | Definition map (A B : Type) (f : positive -> A -> B) m := xmap f m xH. |
---|
500 | |
---|
501 | Lemma xgmap: |
---|
502 | forall (A B: Type) (f: positive -> A -> B) (i j : positive) (m: t A), |
---|
503 | get i (xmap f m j) = option_map (f (append j i)) (get i m). |
---|
504 | Proof. |
---|
505 | induction i; intros; destruct m; simpl; auto. |
---|
506 | rewrite (append_assoc_1 j i); apply IHi. |
---|
507 | rewrite (append_assoc_0 j i); apply IHi. |
---|
508 | rewrite (append_neutral_r j); auto. |
---|
509 | Qed. |
---|
510 | |
---|
511 | Theorem gmap: |
---|
512 | forall (A B: Type) (f: positive -> A -> B) (i: positive) (m: t A), |
---|
513 | get i (map f m) = option_map (f i) (get i m). |
---|
514 | Proof. |
---|
515 | intros. |
---|
516 | unfold map. |
---|
517 | replace (f i) with (f (append xH i)). |
---|
518 | apply xgmap. |
---|
519 | rewrite append_neutral_l; auto. |
---|
520 | Qed. |
---|
521 | |
---|
522 | Definition Node' (A: Type) (l: t A) (x: option A) (r: t A): t A := |
---|
523 | match l, x, r with |
---|
524 | | Leaf, None, Leaf => Leaf |
---|
525 | | _, _, _ => Node l x r |
---|
526 | end. |
---|
527 | |
---|
528 | Lemma gnode': |
---|
529 | forall (A: Type) (l r: t A) (x: option A) (i: positive), |
---|
530 | get i (Node' l x r) = get i (Node l x r). |
---|
531 | Proof. |
---|
532 | intros. unfold Node'. |
---|
533 | destruct l; destruct x; destruct r; auto. |
---|
534 | destruct i; simpl; auto; rewrite gleaf; auto. |
---|
535 | Qed. |
---|
536 | |
---|
537 | Section COMBINE. |
---|
538 | |
---|
539 | Variable A: Type. |
---|
540 | Variable f: option A -> option A -> option A. |
---|
541 | Hypothesis f_none_none: f None None = None. |
---|
542 | |
---|
543 | Fixpoint xcombine_l (m : t A) {struct m} : t A := |
---|
544 | match m with |
---|
545 | | Leaf => Leaf |
---|
546 | | Node l o r => Node' (xcombine_l l) (f o None) (xcombine_l r) |
---|
547 | end. |
---|
548 | |
---|
549 | Lemma xgcombine_l : |
---|
550 | forall (m: t A) (i : positive), |
---|
551 | get i (xcombine_l m) = f (get i m) None. |
---|
552 | Proof. |
---|
553 | induction m; intros; simpl. |
---|
554 | repeat rewrite gleaf. auto. |
---|
555 | rewrite gnode'. destruct i; simpl; auto. |
---|
556 | Qed. |
---|
557 | |
---|
558 | Fixpoint xcombine_r (m : t A) {struct m} : t A := |
---|
559 | match m with |
---|
560 | | Leaf => Leaf |
---|
561 | | Node l o r => Node' (xcombine_r l) (f None o) (xcombine_r r) |
---|
562 | end. |
---|
563 | |
---|
564 | Lemma xgcombine_r : |
---|
565 | forall (m: t A) (i : positive), |
---|
566 | get i (xcombine_r m) = f None (get i m). |
---|
567 | Proof. |
---|
568 | induction m; intros; simpl. |
---|
569 | repeat rewrite gleaf. auto. |
---|
570 | rewrite gnode'. destruct i; simpl; auto. |
---|
571 | Qed. |
---|
572 | |
---|
573 | Fixpoint combine (m1 m2 : t A) {struct m1} : t A := |
---|
574 | match m1 with |
---|
575 | | Leaf => xcombine_r m2 |
---|
576 | | Node l1 o1 r1 => |
---|
577 | match m2 with |
---|
578 | | Leaf => xcombine_l m1 |
---|
579 | | Node l2 o2 r2 => Node' (combine l1 l2) (f o1 o2) (combine r1 r2) |
---|
580 | end |
---|
581 | end. |
---|
582 | |
---|
583 | Theorem gcombine: |
---|
584 | forall (m1 m2: t A) (i: positive), |
---|
585 | get i (combine m1 m2) = f (get i m1) (get i m2). |
---|
586 | Proof. |
---|
587 | induction m1; intros; simpl. |
---|
588 | rewrite gleaf. apply xgcombine_r. |
---|
589 | destruct m2; simpl. |
---|
590 | rewrite gleaf. rewrite <- xgcombine_l. auto. |
---|
591 | repeat rewrite gnode'. destruct i; simpl; auto. |
---|
592 | Qed. |
---|
593 | |
---|
594 | End COMBINE. |
---|
595 | |
---|
596 | Lemma xcombine_lr : |
---|
597 | forall (A : Type) (f g : option A -> option A -> option A) (m : t A), |
---|
598 | (forall (i j : option A), f i j = g j i) -> |
---|
599 | xcombine_l f m = xcombine_r g m. |
---|
600 | Proof. |
---|
601 | induction m; intros; simpl; auto. |
---|
602 | rewrite IHm1; auto. |
---|
603 | rewrite IHm2; auto. |
---|
604 | rewrite H; auto. |
---|
605 | Qed. |
---|
606 | |
---|
607 | Theorem combine_commut: |
---|
608 | forall (A: Type) (f g: option A -> option A -> option A), |
---|
609 | (forall (i j: option A), f i j = g j i) -> |
---|
610 | forall (m1 m2: t A), |
---|
611 | combine f m1 m2 = combine g m2 m1. |
---|
612 | Proof. |
---|
613 | intros A f g EQ1. |
---|
614 | assert (EQ2: forall (i j: option A), g i j = f j i). |
---|
615 | intros; auto. |
---|
616 | induction m1; intros; destruct m2; simpl; |
---|
617 | try rewrite EQ1; |
---|
618 | repeat rewrite (xcombine_lr f g); |
---|
619 | repeat rewrite (xcombine_lr g f); |
---|
620 | auto. |
---|
621 | rewrite IHm1_1. |
---|
622 | rewrite IHm1_2. |
---|
623 | auto. |
---|
624 | Qed. |
---|
625 | |
---|
626 | Fixpoint xelements (A : Type) (m : t A) (i : positive) {struct m} |
---|
627 | : list (positive * A) := |
---|
628 | match m with |
---|
629 | | Leaf => nil |
---|
630 | | Node l None r => |
---|
631 | (xelements l (append i (xO xH))) ++ (xelements r (append i (xI xH))) |
---|
632 | | Node l (Some x) r => |
---|
633 | (xelements l (append i (xO xH))) |
---|
634 | ++ ((i, x) :: xelements r (append i (xI xH))) |
---|
635 | end. |
---|
636 | |
---|
637 | (* Note: function [xelements] above is inefficient. We should apply |
---|
638 | deforestation to it, but that makes the proofs even harder. *) |
---|
639 | |
---|
640 | Definition elements A (m : t A) := xelements m xH. |
---|
641 | |
---|
642 | Lemma xelements_correct: |
---|
643 | forall (A: Type) (m: t A) (i j : positive) (v: A), |
---|
644 | get i m = Some v -> In (append j i, v) (xelements m j). |
---|
645 | Proof. |
---|
646 | induction m; intros. |
---|
647 | rewrite (gleaf A i) in H; congruence. |
---|
648 | destruct o; destruct i; simpl; simpl in H. |
---|
649 | rewrite append_assoc_1; apply in_or_app; right; apply in_cons; |
---|
650 | apply IHm2; auto. |
---|
651 | rewrite append_assoc_0; apply in_or_app; left; apply IHm1; auto. |
---|
652 | rewrite append_neutral_r; apply in_or_app; injection H; |
---|
653 | intro EQ; rewrite EQ; right; apply in_eq. |
---|
654 | rewrite append_assoc_1; apply in_or_app; right; apply IHm2; auto. |
---|
655 | rewrite append_assoc_0; apply in_or_app; left; apply IHm1; auto. |
---|
656 | congruence. |
---|
657 | Qed. |
---|
658 | |
---|
659 | Theorem elements_correct: |
---|
660 | forall (A: Type) (m: t A) (i: positive) (v: A), |
---|
661 | get i m = Some v -> In (i, v) (elements m). |
---|
662 | Proof. |
---|
663 | intros A m i v H. |
---|
664 | exact (xelements_correct m i xH H). |
---|
665 | Qed. |
---|
666 | |
---|
667 | Fixpoint xget (A : Type) (i j : positive) (m : t A) {struct j} : option A := |
---|
668 | match i, j with |
---|
669 | | _, xH => get i m |
---|
670 | | xO ii, xO jj => xget ii jj m |
---|
671 | | xI ii, xI jj => xget ii jj m |
---|
672 | | _, _ => None |
---|
673 | end. |
---|
674 | |
---|
675 | Lemma xget_left : |
---|
676 | forall (A : Type) (j i : positive) (m1 m2 : t A) (o : option A) (v : A), |
---|
677 | xget i (append j (xO xH)) m1 = Some v -> xget i j (Node m1 o m2) = Some v. |
---|
678 | Proof. |
---|
679 | induction j; intros; destruct i; simpl; simpl in H; auto; try congruence. |
---|
680 | destruct i; congruence. |
---|
681 | Qed. |
---|
682 | |
---|
683 | Lemma xelements_ii : |
---|
684 | forall (A: Type) (m: t A) (i j : positive) (v: A), |
---|
685 | In (xI i, v) (xelements m (xI j)) -> In (i, v) (xelements m j). |
---|
686 | Proof. |
---|
687 | induction m. |
---|
688 | simpl; auto. |
---|
689 | intros; destruct o; simpl; simpl in H; destruct (in_app_or _ _ _ H); |
---|
690 | apply in_or_app. |
---|
691 | left; apply IHm1; auto. |
---|
692 | right; destruct (in_inv H0). |
---|
693 | injection H1; intros EQ1 EQ2; rewrite EQ1; rewrite EQ2; apply in_eq. |
---|
694 | apply in_cons; apply IHm2; auto. |
---|
695 | left; apply IHm1; auto. |
---|
696 | right; apply IHm2; auto. |
---|
697 | Qed. |
---|
698 | |
---|
699 | Lemma xelements_io : |
---|
700 | forall (A: Type) (m: t A) (i j : positive) (v: A), |
---|
701 | ~In (xI i, v) (xelements m (xO j)). |
---|
702 | Proof. |
---|
703 | induction m. |
---|
704 | simpl; auto. |
---|
705 | intros; destruct o; simpl; intro H; destruct (in_app_or _ _ _ H). |
---|
706 | apply (IHm1 _ _ _ H0). |
---|
707 | destruct (in_inv H0). |
---|
708 | congruence. |
---|
709 | apply (IHm2 _ _ _ H1). |
---|
710 | apply (IHm1 _ _ _ H0). |
---|
711 | apply (IHm2 _ _ _ H0). |
---|
712 | Qed. |
---|
713 | |
---|
714 | Lemma xelements_oo : |
---|
715 | forall (A: Type) (m: t A) (i j : positive) (v: A), |
---|
716 | In (xO i, v) (xelements m (xO j)) -> In (i, v) (xelements m j). |
---|
717 | Proof. |
---|
718 | induction m. |
---|
719 | simpl; auto. |
---|
720 | intros; destruct o; simpl; simpl in H; destruct (in_app_or _ _ _ H); |
---|
721 | apply in_or_app. |
---|
722 | left; apply IHm1; auto. |
---|
723 | right; destruct (in_inv H0). |
---|
724 | injection H1; intros EQ1 EQ2; rewrite EQ1; rewrite EQ2; apply in_eq. |
---|
725 | apply in_cons; apply IHm2; auto. |
---|
726 | left; apply IHm1; auto. |
---|
727 | right; apply IHm2; auto. |
---|
728 | Qed. |
---|
729 | |
---|
730 | Lemma xelements_oi : |
---|
731 | forall (A: Type) (m: t A) (i j : positive) (v: A), |
---|
732 | ~In (xO i, v) (xelements m (xI j)). |
---|
733 | Proof. |
---|
734 | induction m. |
---|
735 | simpl; auto. |
---|
736 | intros; destruct o; simpl; intro H; destruct (in_app_or _ _ _ H). |
---|
737 | apply (IHm1 _ _ _ H0). |
---|
738 | destruct (in_inv H0). |
---|
739 | congruence. |
---|
740 | apply (IHm2 _ _ _ H1). |
---|
741 | apply (IHm1 _ _ _ H0). |
---|
742 | apply (IHm2 _ _ _ H0). |
---|
743 | Qed. |
---|
744 | |
---|
745 | Lemma xelements_ih : |
---|
746 | forall (A: Type) (m1 m2: t A) (o: option A) (i : positive) (v: A), |
---|
747 | In (xI i, v) (xelements (Node m1 o m2) xH) -> In (i, v) (xelements m2 xH). |
---|
748 | Proof. |
---|
749 | destruct o; simpl; intros; destruct (in_app_or _ _ _ H). |
---|
750 | absurd (In (xI i, v) (xelements m1 2)); auto; apply xelements_io; auto. |
---|
751 | destruct (in_inv H0). |
---|
752 | congruence. |
---|
753 | apply xelements_ii; auto. |
---|
754 | absurd (In (xI i, v) (xelements m1 2)); auto; apply xelements_io; auto. |
---|
755 | apply xelements_ii; auto. |
---|
756 | Qed. |
---|
757 | |
---|
758 | Lemma xelements_oh : |
---|
759 | forall (A: Type) (m1 m2: t A) (o: option A) (i : positive) (v: A), |
---|
760 | In (xO i, v) (xelements (Node m1 o m2) xH) -> In (i, v) (xelements m1 xH). |
---|
761 | Proof. |
---|
762 | destruct o; simpl; intros; destruct (in_app_or _ _ _ H). |
---|
763 | apply xelements_oo; auto. |
---|
764 | destruct (in_inv H0). |
---|
765 | congruence. |
---|
766 | absurd (In (xO i, v) (xelements m2 3)); auto; apply xelements_oi; auto. |
---|
767 | apply xelements_oo; auto. |
---|
768 | absurd (In (xO i, v) (xelements m2 3)); auto; apply xelements_oi; auto. |
---|
769 | Qed. |
---|
770 | |
---|
771 | Lemma xelements_hi : |
---|
772 | forall (A: Type) (m: t A) (i : positive) (v: A), |
---|
773 | ~In (xH, v) (xelements m (xI i)). |
---|
774 | Proof. |
---|
775 | induction m; intros. |
---|
776 | simpl; auto. |
---|
777 | destruct o; simpl; intro H; destruct (in_app_or _ _ _ H). |
---|
778 | generalize H0; apply IHm1; auto. |
---|
779 | destruct (in_inv H0). |
---|
780 | congruence. |
---|
781 | generalize H1; apply IHm2; auto. |
---|
782 | generalize H0; apply IHm1; auto. |
---|
783 | generalize H0; apply IHm2; auto. |
---|
784 | Qed. |
---|
785 | |
---|
786 | Lemma xelements_ho : |
---|
787 | forall (A: Type) (m: t A) (i : positive) (v: A), |
---|
788 | ~In (xH, v) (xelements m (xO i)). |
---|
789 | Proof. |
---|
790 | induction m; intros. |
---|
791 | simpl; auto. |
---|
792 | destruct o; simpl; intro H; destruct (in_app_or _ _ _ H). |
---|
793 | generalize H0; apply IHm1; auto. |
---|
794 | destruct (in_inv H0). |
---|
795 | congruence. |
---|
796 | generalize H1; apply IHm2; auto. |
---|
797 | generalize H0; apply IHm1; auto. |
---|
798 | generalize H0; apply IHm2; auto. |
---|
799 | Qed. |
---|
800 | |
---|
801 | Lemma get_xget_h : |
---|
802 | forall (A: Type) (m: t A) (i: positive), get i m = xget i xH m. |
---|
803 | Proof. |
---|
804 | destruct i; simpl; auto. |
---|
805 | Qed. |
---|
806 | |
---|
807 | Lemma xelements_complete: |
---|
808 | forall (A: Type) (i j : positive) (m: t A) (v: A), |
---|
809 | In (i, v) (xelements m j) -> xget i j m = Some v. |
---|
810 | Proof. |
---|
811 | induction i; simpl; intros; destruct j; simpl. |
---|
812 | apply IHi; apply xelements_ii; auto. |
---|
813 | absurd (In (xI i, v) (xelements m (xO j))); auto; apply xelements_io. |
---|
814 | destruct m. |
---|
815 | simpl in H; tauto. |
---|
816 | rewrite get_xget_h. apply IHi. apply (xelements_ih _ _ _ _ _ H). |
---|
817 | absurd (In (xO i, v) (xelements m (xI j))); auto; apply xelements_oi. |
---|
818 | apply IHi; apply xelements_oo; auto. |
---|
819 | destruct m. |
---|
820 | simpl in H; tauto. |
---|
821 | rewrite get_xget_h. apply IHi. apply (xelements_oh _ _ _ _ _ H). |
---|
822 | absurd (In (xH, v) (xelements m (xI j))); auto; apply xelements_hi. |
---|
823 | absurd (In (xH, v) (xelements m (xO j))); auto; apply xelements_ho. |
---|
824 | destruct m. |
---|
825 | simpl in H; tauto. |
---|
826 | destruct o; simpl in H; destruct (in_app_or _ _ _ H). |
---|
827 | absurd (In (xH, v) (xelements m1 (xO xH))); auto; apply xelements_ho. |
---|
828 | destruct (in_inv H0). |
---|
829 | congruence. |
---|
830 | absurd (In (xH, v) (xelements m2 (xI xH))); auto; apply xelements_hi. |
---|
831 | absurd (In (xH, v) (xelements m1 (xO xH))); auto; apply xelements_ho. |
---|
832 | absurd (In (xH, v) (xelements m2 (xI xH))); auto; apply xelements_hi. |
---|
833 | Qed. |
---|
834 | |
---|
835 | Theorem elements_complete: |
---|
836 | forall (A: Type) (m: t A) (i: positive) (v: A), |
---|
837 | In (i, v) (elements m) -> get i m = Some v. |
---|
838 | Proof. |
---|
839 | intros A m i v H. |
---|
840 | unfold elements in H. |
---|
841 | rewrite get_xget_h. |
---|
842 | exact (xelements_complete i xH m v H). |
---|
843 | Qed. |
---|
844 | |
---|
845 | Lemma in_xelements: |
---|
846 | forall (A: Type) (m: t A) (i k: positive) (v: A), |
---|
847 | In (k, v) (xelements m i) -> |
---|
848 | exists j, k = append i j. |
---|
849 | Proof. |
---|
850 | induction m; simpl; intros. |
---|
851 | tauto. |
---|
852 | assert (k = i \/ In (k, v) (xelements m1 (append i 2)) |
---|
853 | \/ In (k, v) (xelements m2 (append i 3))). |
---|
854 | destruct o. |
---|
855 | elim (in_app_or _ _ _ H); simpl; intuition. |
---|
856 | replace k with i. tauto. congruence. |
---|
857 | elim (in_app_or _ _ _ H); simpl; intuition. |
---|
858 | elim H0; intro. |
---|
859 | exists xH. rewrite append_neutral_r. auto. |
---|
860 | elim H1; intro. |
---|
861 | elim (IHm1 _ _ _ H2). intros k1 EQ. rewrite EQ. |
---|
862 | rewrite <- append_assoc_0. exists (xO k1); auto. |
---|
863 | elim (IHm2 _ _ _ H2). intros k1 EQ. rewrite EQ. |
---|
864 | rewrite <- append_assoc_1. exists (xI k1); auto. |
---|
865 | Qed. |
---|
866 | |
---|
867 | Definition xkeys (A: Type) (m: t A) (i: positive) := |
---|
868 | List.map (@fst positive A) (xelements m i). |
---|
869 | |
---|
870 | Lemma in_xkeys: |
---|
871 | forall (A: Type) (m: t A) (i k: positive), |
---|
872 | In k (xkeys m i) -> |
---|
873 | exists j, k = append i j. |
---|
874 | Proof. |
---|
875 | unfold xkeys; intros. |
---|
876 | elim (list_in_map_inv _ _ _ H). intros [k1 v1] [EQ IN]. |
---|
877 | simpl in EQ; subst k1. apply in_xelements with A m v1. auto. |
---|
878 | Qed. |
---|
879 | |
---|
880 | Remark list_append_cons_norepet: |
---|
881 | forall (A: Type) (l1 l2: list A) (x: A), |
---|
882 | list_norepet l1 -> list_norepet l2 -> list_disjoint l1 l2 -> |
---|
883 | ~In x l1 -> ~In x l2 -> |
---|
884 | list_norepet (l1 ++ x :: l2). |
---|
885 | Proof. |
---|
886 | intros. apply list_norepet_append_commut. simpl; constructor. |
---|
887 | red; intros. elim (in_app_or _ _ _ H4); intro; tauto. |
---|
888 | apply list_norepet_append; auto. |
---|
889 | apply list_disjoint_sym; auto. |
---|
890 | Qed. |
---|
891 | |
---|
892 | Lemma append_injective: |
---|
893 | forall i j1 j2, append i j1 = append i j2 -> j1 = j2. |
---|
894 | Proof. |
---|
895 | induction i; simpl; intros. |
---|
896 | apply IHi. congruence. |
---|
897 | apply IHi. congruence. |
---|
898 | auto. |
---|
899 | Qed. |
---|
900 | |
---|
901 | Lemma xelements_keys_norepet: |
---|
902 | forall (A: Type) (m: t A) (i: positive), |
---|
903 | list_norepet (xkeys m i). |
---|
904 | Proof. |
---|
905 | induction m; unfold xkeys; simpl; fold xkeys; intros. |
---|
906 | constructor. |
---|
907 | assert (list_disjoint (xkeys m1 (append i 2)) (xkeys m2 (append i 3))). |
---|
908 | red; intros; red; intro. subst y. |
---|
909 | elim (in_xkeys _ _ _ H); intros j1 EQ1. |
---|
910 | elim (in_xkeys _ _ _ H0); intros j2 EQ2. |
---|
911 | rewrite EQ1 in EQ2. |
---|
912 | rewrite <- append_assoc_0 in EQ2. |
---|
913 | rewrite <- append_assoc_1 in EQ2. |
---|
914 | generalize (append_injective _ _ _ EQ2). congruence. |
---|
915 | assert (forall (m: t A) j, |
---|
916 | j = 2%positive \/ j = 3%positive -> |
---|
917 | ~In i (xkeys m (append i j))). |
---|
918 | intros; red; intros. |
---|
919 | elim (in_xkeys _ _ _ H1); intros k EQ. |
---|
920 | assert (EQ1: append i xH = append (append i j) k). |
---|
921 | rewrite append_neutral_r. auto. |
---|
922 | elim H0; intro; subst j; |
---|
923 | try (rewrite <- append_assoc_0 in EQ1); |
---|
924 | try (rewrite <- append_assoc_1 in EQ1); |
---|
925 | generalize (append_injective _ _ _ EQ1); congruence. |
---|
926 | destruct o; rewrite list_append_map; simpl; |
---|
927 | change (List.map (@fst positive A) (xelements m1 (append i 2))) |
---|
928 | with (xkeys m1 (append i 2)); |
---|
929 | change (List.map (@fst positive A) (xelements m2 (append i 3))) |
---|
930 | with (xkeys m2 (append i 3)). |
---|
931 | apply list_append_cons_norepet; auto. |
---|
932 | apply list_norepet_append; auto. |
---|
933 | Qed. |
---|
934 | |
---|
935 | Theorem elements_keys_norepet: |
---|
936 | forall (A: Type) (m: t A), |
---|
937 | list_norepet (List.map (@fst elt A) (elements m)). |
---|
938 | Proof. |
---|
939 | intros. change (list_norepet (xkeys m 1)). apply xelements_keys_norepet. |
---|
940 | Qed. |
---|
941 | |
---|
942 | (* |
---|
943 | Definition fold (A B : Type) (f: B -> positive -> A -> B) (tr: t A) (v: B) := |
---|
944 | List.fold_left (fun a p => f a (fst p) (snd p)) (elements tr) v. |
---|
945 | *) |
---|
946 | |
---|
947 | Fixpoint xfold (A B: Type) (f: B -> positive -> A -> B) |
---|
948 | (i: positive) (m: t A) (v: B) {struct m} : B := |
---|
949 | match m with |
---|
950 | | Leaf => v |
---|
951 | | Node l None r => |
---|
952 | let v1 := xfold f (append i (xO xH)) l v in |
---|
953 | xfold f (append i (xI xH)) r v1 |
---|
954 | | Node l (Some x) r => |
---|
955 | let v1 := xfold f (append i (xO xH)) l v in |
---|
956 | let v2 := f v1 i x in |
---|
957 | xfold f (append i (xI xH)) r v2 |
---|
958 | end. |
---|
959 | |
---|
960 | Definition fold (A B : Type) (f: B -> positive -> A -> B) (m: t A) (v: B) := |
---|
961 | xfold f xH m v. |
---|
962 | |
---|
963 | Lemma xfold_xelements: |
---|
964 | forall (A B: Type) (f: B -> positive -> A -> B) m i v, |
---|
965 | xfold f i m v = |
---|
966 | List.fold_left (fun a p => f a (fst p) (snd p)) |
---|
967 | (xelements m i) |
---|
968 | v. |
---|
969 | Proof. |
---|
970 | induction m; intros. |
---|
971 | simpl. auto. |
---|
972 | simpl. destruct o. |
---|
973 | rewrite fold_left_app. simpl. |
---|
974 | rewrite IHm1. apply IHm2. |
---|
975 | rewrite fold_left_app. simpl. |
---|
976 | rewrite IHm1. apply IHm2. |
---|
977 | Qed. |
---|
978 | |
---|
979 | Theorem fold_spec: |
---|
980 | forall (A B: Type) (f: B -> positive -> A -> B) (v: B) (m: t A), |
---|
981 | fold f m v = |
---|
982 | List.fold_left (fun a p => f a (fst p) (snd p)) (elements m) v. |
---|
983 | Proof. |
---|
984 | intros. unfold fold, elements. apply xfold_xelements. |
---|
985 | Qed. |
---|
986 | |
---|
987 | End PTree. |
---|
988 | |
---|
989 | (** * An implementation of maps over type [positive] *) |
---|
990 | |
---|
991 | Module PMap <: MAP. |
---|
992 | Definition elt := positive. |
---|
993 | Definition elt_eq := peq. |
---|
994 | |
---|
995 | Definition t (A : Type) : Type := (A * PTree.t A)%type. |
---|
996 | |
---|
997 | Definition eq: forall (A: Type), (forall (x y: A), {x=y} + {x<>y}) -> |
---|
998 | forall (a b: t A), {a = b} + {a <> b}. |
---|
999 | Proof. |
---|
1000 | intros. |
---|
1001 | generalize (PTree.eq X). intros. |
---|
1002 | decide equality. |
---|
1003 | Qed. |
---|
1004 | |
---|
1005 | Definition init (A : Type) (x : A) := |
---|
1006 | (x, PTree.empty A). |
---|
1007 | |
---|
1008 | Definition get (A : Type) (i : positive) (m : t A) := |
---|
1009 | match PTree.get i (snd m) with |
---|
1010 | | Some x => x |
---|
1011 | | None => fst m |
---|
1012 | end. |
---|
1013 | |
---|
1014 | Definition set (A : Type) (i : positive) (x : A) (m : t A) := |
---|
1015 | (fst m, PTree.set i x (snd m)). |
---|
1016 | |
---|
1017 | Theorem gi: |
---|
1018 | forall (A: Type) (i: positive) (x: A), get i (init x) = x. |
---|
1019 | Proof. |
---|
1020 | intros. unfold init. unfold get. simpl. rewrite PTree.gempty. auto. |
---|
1021 | Qed. |
---|
1022 | |
---|
1023 | Theorem gss: |
---|
1024 | forall (A: Type) (i: positive) (x: A) (m: t A), get i (set i x m) = x. |
---|
1025 | Proof. |
---|
1026 | intros. unfold get. unfold set. simpl. rewrite PTree.gss. auto. |
---|
1027 | Qed. |
---|
1028 | |
---|
1029 | Theorem gso: |
---|
1030 | forall (A: Type) (i j: positive) (x: A) (m: t A), |
---|
1031 | i <> j -> get i (set j x m) = get i m. |
---|
1032 | Proof. |
---|
1033 | intros. unfold get. unfold set. simpl. rewrite PTree.gso; auto. |
---|
1034 | Qed. |
---|
1035 | |
---|
1036 | Theorem gsspec: |
---|
1037 | forall (A: Type) (i j: positive) (x: A) (m: t A), |
---|
1038 | get i (set j x m) = if peq i j then x else get i m. |
---|
1039 | Proof. |
---|
1040 | intros. destruct (peq i j). |
---|
1041 | rewrite e. apply gss. auto. |
---|
1042 | apply gso. auto. |
---|
1043 | Qed. |
---|
1044 | |
---|
1045 | Theorem gsident: |
---|
1046 | forall (A: Type) (i j: positive) (m: t A), |
---|
1047 | get j (set i (get i m) m) = get j m. |
---|
1048 | Proof. |
---|
1049 | intros. destruct (peq i j). |
---|
1050 | rewrite e. rewrite gss. auto. |
---|
1051 | rewrite gso; auto. |
---|
1052 | Qed. |
---|
1053 | |
---|
1054 | Definition map (A B : Type) (f : A -> B) (m : t A) : t B := |
---|
1055 | (f (fst m), PTree.map (fun _ => f) (snd m)). |
---|
1056 | |
---|
1057 | Theorem gmap: |
---|
1058 | forall (A B: Type) (f: A -> B) (i: positive) (m: t A), |
---|
1059 | get i (map f m) = f(get i m). |
---|
1060 | Proof. |
---|
1061 | intros. unfold map. unfold get. simpl. rewrite PTree.gmap. |
---|
1062 | unfold option_map. destruct (PTree.get i (snd m)); auto. |
---|
1063 | Qed. |
---|
1064 | |
---|
1065 | End PMap. |
---|
1066 | |
---|
1067 | (** * An implementation of maps over any type that injects into type [positive] *) |
---|
1068 | |
---|
1069 | Module Type INDEXED_TYPE. |
---|
1070 | Variable t: Type. |
---|
1071 | Variable index: t -> positive. |
---|
1072 | Hypothesis index_inj: forall (x y: t), index x = index y -> x = y. |
---|
1073 | Variable eq: forall (x y: t), {x = y} + {x <> y}. |
---|
1074 | End INDEXED_TYPE. |
---|
1075 | |
---|
1076 | Module IMap(X: INDEXED_TYPE). |
---|
1077 | |
---|
1078 | Definition elt := X.t. |
---|
1079 | Definition elt_eq := X.eq. |
---|
1080 | Definition t : Type -> Type := PMap.t. |
---|
1081 | Definition eq: forall (A: Type), (forall (x y: A), {x=y} + {x<>y}) -> |
---|
1082 | forall (a b: t A), {a = b} + {a <> b} := PMap.eq. |
---|
1083 | Definition init (A: Type) (x: A) := PMap.init x. |
---|
1084 | Definition get (A: Type) (i: X.t) (m: t A) := PMap.get (X.index i) m. |
---|
1085 | Definition set (A: Type) (i: X.t) (v: A) (m: t A) := PMap.set (X.index i) v m. |
---|
1086 | Definition map (A B: Type) (f: A -> B) (m: t A) : t B := PMap.map f m. |
---|
1087 | |
---|
1088 | Lemma gi: |
---|
1089 | forall (A: Type) (x: A) (i: X.t), get i (init x) = x. |
---|
1090 | Proof. |
---|
1091 | intros. unfold get, init. apply PMap.gi. |
---|
1092 | Qed. |
---|
1093 | |
---|
1094 | Lemma gss: |
---|
1095 | forall (A: Type) (i: X.t) (x: A) (m: t A), get i (set i x m) = x. |
---|
1096 | Proof. |
---|
1097 | intros. unfold get, set. apply PMap.gss. |
---|
1098 | Qed. |
---|
1099 | |
---|
1100 | Lemma gso: |
---|
1101 | forall (A: Type) (i j: X.t) (x: A) (m: t A), |
---|
1102 | i <> j -> get i (set j x m) = get i m. |
---|
1103 | Proof. |
---|
1104 | intros. unfold get, set. apply PMap.gso. |
---|
1105 | red. intro. apply H. apply X.index_inj; auto. |
---|
1106 | Qed. |
---|
1107 | |
---|
1108 | Lemma gsspec: |
---|
1109 | forall (A: Type) (i j: X.t) (x: A) (m: t A), |
---|
1110 | get i (set j x m) = if X.eq i j then x else get i m. |
---|
1111 | Proof. |
---|
1112 | intros. unfold get, set. |
---|
1113 | rewrite PMap.gsspec. |
---|
1114 | case (X.eq i j); intro. |
---|
1115 | subst j. rewrite peq_true. reflexivity. |
---|
1116 | rewrite peq_false. reflexivity. |
---|
1117 | red; intro. elim n. apply X.index_inj; auto. |
---|
1118 | Qed. |
---|
1119 | |
---|
1120 | Lemma gmap: |
---|
1121 | forall (A B: Type) (f: A -> B) (i: X.t) (m: t A), |
---|
1122 | get i (map f m) = f(get i m). |
---|
1123 | Proof. |
---|
1124 | intros. unfold map, get. apply PMap.gmap. |
---|
1125 | Qed. |
---|
1126 | |
---|
1127 | End IMap. |
---|
1128 | |
---|
1129 | Module ZIndexed. |
---|
1130 | Definition t := Z. |
---|
1131 | Definition index (z: Z): positive := |
---|
1132 | match z with |
---|
1133 | | Z0 => xH |
---|
1134 | | Zpos p => xO p |
---|
1135 | | Zneg p => xI p |
---|
1136 | end. |
---|
1137 | Lemma index_inj: forall (x y: Z), index x = index y -> x = y. |
---|
1138 | Proof. |
---|
1139 | unfold index; destruct x; destruct y; intros; |
---|
1140 | try discriminate; try reflexivity. |
---|
1141 | congruence. |
---|
1142 | congruence. |
---|
1143 | Qed. |
---|
1144 | Definition eq := zeq. |
---|
1145 | End ZIndexed. |
---|
1146 | |
---|
1147 | Module ZMap := IMap(ZIndexed). |
---|
1148 | |
---|
1149 | Module NIndexed. |
---|
1150 | Definition t := N. |
---|
1151 | Definition index (n: N): positive := |
---|
1152 | match n with |
---|
1153 | | N0 => xH |
---|
1154 | | Npos p => xO p |
---|
1155 | end. |
---|
1156 | Lemma index_inj: forall (x y: N), index x = index y -> x = y. |
---|
1157 | Proof. |
---|
1158 | unfold index; destruct x; destruct y; intros; |
---|
1159 | try discriminate; try reflexivity. |
---|
1160 | congruence. |
---|
1161 | Qed. |
---|
1162 | Lemma eq: forall (x y: N), {x = y} + {x <> y}. |
---|
1163 | Proof. |
---|
1164 | decide equality. apply peq. |
---|
1165 | Qed. |
---|
1166 | End NIndexed. |
---|
1167 | |
---|
1168 | Module NMap := IMap(NIndexed). |
---|
1169 | |
---|
1170 | (** * An implementation of maps over any type with decidable equality *) |
---|
1171 | |
---|
1172 | Module Type EQUALITY_TYPE. |
---|
1173 | Variable t: Type. |
---|
1174 | Variable eq: forall (x y: t), {x = y} + {x <> y}. |
---|
1175 | End EQUALITY_TYPE. |
---|
1176 | |
---|
1177 | Module EMap(X: EQUALITY_TYPE) <: MAP. |
---|
1178 | |
---|
1179 | Definition elt := X.t. |
---|
1180 | Definition elt_eq := X.eq. |
---|
1181 | Definition t (A: Type) := X.t -> A. |
---|
1182 | Definition init (A: Type) (v: A) := fun (_: X.t) => v. |
---|
1183 | Definition get (A: Type) (x: X.t) (m: t A) := m x. |
---|
1184 | Definition set (A: Type) (x: X.t) (v: A) (m: t A) := |
---|
1185 | fun (y: X.t) => if X.eq y x then v else m y. |
---|
1186 | Lemma gi: |
---|
1187 | forall (A: Type) (i: elt) (x: A), init x i = x. |
---|
1188 | Proof. |
---|
1189 | intros. reflexivity. |
---|
1190 | Qed. |
---|
1191 | Lemma gss: |
---|
1192 | forall (A: Type) (i: elt) (x: A) (m: t A), (set i x m) i = x. |
---|
1193 | Proof. |
---|
1194 | intros. unfold set. case (X.eq i i); intro. |
---|
1195 | reflexivity. tauto. |
---|
1196 | Qed. |
---|
1197 | Lemma gso: |
---|
1198 | forall (A: Type) (i j: elt) (x: A) (m: t A), |
---|
1199 | i <> j -> (set j x m) i = m i. |
---|
1200 | Proof. |
---|
1201 | intros. unfold set. case (X.eq i j); intro. |
---|
1202 | congruence. reflexivity. |
---|
1203 | Qed. |
---|
1204 | Lemma gsspec: |
---|
1205 | forall (A: Type) (i j: elt) (x: A) (m: t A), |
---|
1206 | get i (set j x m) = if elt_eq i j then x else get i m. |
---|
1207 | Proof. |
---|
1208 | intros. unfold get, set, elt_eq. reflexivity. |
---|
1209 | Qed. |
---|
1210 | Lemma gsident: |
---|
1211 | forall (A: Type) (i j: elt) (m: t A), get j (set i (get i m) m) = get j m. |
---|
1212 | Proof. |
---|
1213 | intros. unfold get, set. case (X.eq j i); intro. |
---|
1214 | congruence. reflexivity. |
---|
1215 | Qed. |
---|
1216 | Definition map (A B: Type) (f: A -> B) (m: t A) := |
---|
1217 | fun (x: X.t) => f(m x). |
---|
1218 | Lemma gmap: |
---|
1219 | forall (A B: Type) (f: A -> B) (i: elt) (m: t A), |
---|
1220 | get i (map f m) = f(get i m). |
---|
1221 | Proof. |
---|
1222 | intros. unfold get, map. reflexivity. |
---|
1223 | Qed. |
---|
1224 | End EMap. |
---|
1225 | |
---|
1226 | (** * Additional properties over trees *) |
---|
1227 | |
---|
1228 | Module Tree_Properties(T: TREE). |
---|
1229 | |
---|
1230 | (** An induction principle over [fold]. *) |
---|
1231 | |
---|
1232 | Section TREE_FOLD_IND. |
---|
1233 | |
---|
1234 | Variables V A: Type. |
---|
1235 | Variable f: A -> T.elt -> V -> A. |
---|
1236 | Variable P: T.t V -> A -> Prop. |
---|
1237 | Variable init: A. |
---|
1238 | Variable m_final: T.t V. |
---|
1239 | |
---|
1240 | Hypothesis P_compat: |
---|
1241 | forall m m' a, |
---|
1242 | (forall x, T.get x m = T.get x m') -> |
---|
1243 | P m a -> P m' a. |
---|
1244 | |
---|
1245 | Hypothesis H_base: |
---|
1246 | P (T.empty _) init. |
---|
1247 | |
---|
1248 | Hypothesis H_rec: |
---|
1249 | forall m a k v, |
---|
1250 | T.get k m = None -> T.get k m_final = Some v -> P m a -> P (T.set k v m) (f a k v). |
---|
1251 | |
---|
1252 | Definition f' (a: A) (p : T.elt * V) := f a (fst p) (snd p). |
---|
1253 | |
---|
1254 | Definition P' (l: list (T.elt * V)) (a: A) : Prop := |
---|
1255 | forall m, list_equiv l (T.elements m) -> P m a. |
---|
1256 | |
---|
1257 | Remark H_base': |
---|
1258 | P' nil init. |
---|
1259 | Proof. |
---|
1260 | red; intros. apply P_compat with (T.empty _); auto. |
---|
1261 | intros. rewrite T.gempty. symmetry. case_eq (T.get x m); intros; auto. |
---|
1262 | assert (In (x, v) nil). rewrite (H (x, v)). apply T.elements_correct. auto. |
---|
1263 | contradiction. |
---|
1264 | Qed. |
---|
1265 | |
---|
1266 | Remark H_rec': |
---|
1267 | forall k v l a, |
---|
1268 | ~In k (List.map (@fst T.elt V) l) -> |
---|
1269 | In (k, v) (T.elements m_final) -> |
---|
1270 | P' l a -> |
---|
1271 | P' (l ++ (k, v) :: nil) (f a k v). |
---|
1272 | Proof. |
---|
1273 | unfold P'; intros. |
---|
1274 | set (m0 := T.remove k m). |
---|
1275 | apply P_compat with (T.set k v m0). |
---|
1276 | intros. unfold m0. rewrite T.gsspec. destruct (T.elt_eq x k). |
---|
1277 | symmetry. apply T.elements_complete. rewrite <- (H2 (x, v)). |
---|
1278 | apply in_or_app. simpl. intuition congruence. |
---|
1279 | apply T.gro. auto. |
---|
1280 | apply H_rec. unfold m0. apply T.grs. apply T.elements_complete. auto. |
---|
1281 | apply H1. red. intros [k' v']. |
---|
1282 | split; intros. |
---|
1283 | apply T.elements_correct. unfold m0. rewrite T.gro. apply T.elements_complete. |
---|
1284 | rewrite <- (H2 (k', v')). apply in_or_app. auto. |
---|
1285 | red; intro; subst k'. elim H. change k with (fst (k, v')). apply in_map. auto. |
---|
1286 | assert (T.get k' m0 = Some v'). apply T.elements_complete. auto. |
---|
1287 | unfold m0 in H4. rewrite T.grspec in H4. destruct (T.elt_eq k' k). congruence. |
---|
1288 | assert (In (k', v') (T.elements m)). apply T.elements_correct; auto. |
---|
1289 | rewrite <- (H2 (k', v')) in H5. destruct (in_app_or _ _ _ H5). auto. |
---|
1290 | simpl in H6. intuition congruence. |
---|
1291 | Qed. |
---|
1292 | |
---|
1293 | Lemma fold_rec_aux: |
---|
1294 | forall l1 l2 a, |
---|
1295 | list_equiv (l2 ++ l1) (T.elements m_final) -> |
---|
1296 | list_disjoint (List.map (@fst T.elt V) l1) (List.map (@fst T.elt V) l2) -> |
---|
1297 | list_norepet (List.map (@fst T.elt V) l1) -> |
---|
1298 | P' l2 a -> P' (l2 ++ l1) (List.fold_left f' l1 a). |
---|
1299 | Proof. |
---|
1300 | induction l1; intros; simpl. |
---|
1301 | rewrite <- List.app_nil_end. auto. |
---|
1302 | destruct a as [k v]; simpl in *. inv H1. |
---|
1303 | change ((k, v) :: l1) with (((k, v) :: nil) ++ l1). rewrite <- List.app_ass. apply IHl1. |
---|
1304 | rewrite app_ass. auto. |
---|
1305 | red; intros. rewrite map_app in H3. destruct (in_app_or _ _ _ H3). apply H0; auto with coqlib. |
---|
1306 | simpl in H4. intuition congruence. |
---|
1307 | auto. |
---|
1308 | unfold f'. simpl. apply H_rec'; auto. eapply list_disjoint_notin; eauto with coqlib. |
---|
1309 | rewrite <- (H (k, v)). apply in_or_app. simpl. auto. |
---|
1310 | Qed. |
---|
1311 | |
---|
1312 | Theorem fold_rec: |
---|
1313 | P m_final (T.fold f m_final init). |
---|
1314 | Proof. |
---|
1315 | intros. rewrite T.fold_spec. fold f'. |
---|
1316 | assert (P' (nil ++ T.elements m_final) (List.fold_left f' (T.elements m_final) init)). |
---|
1317 | apply fold_rec_aux. |
---|
1318 | simpl. red; intros; tauto. |
---|
1319 | simpl. red; intros. elim H0. |
---|
1320 | apply T.elements_keys_norepet. |
---|
1321 | apply H_base'. |
---|
1322 | simpl in H. red in H. apply H. red; intros. tauto. |
---|
1323 | Qed. |
---|
1324 | |
---|
1325 | End TREE_FOLD_IND. |
---|
1326 | |
---|
1327 | End Tree_Properties. |
---|
1328 | |
---|
1329 | Module PTree_Properties := Tree_Properties(PTree). |
---|
1330 | |
---|
1331 | (** * Useful notations *) |
---|
1332 | |
---|
1333 | Notation "a ! b" := (PTree.get b a) (at level 1). |
---|
1334 | Notation "a !! b" := (PMap.get b a) (at level 1). |
---|
1335 | *) |
---|
1336 | |
---|
1337 | |
---|
1338 | |
---|
1339 | (* $Id: Maps.v,v 1.12.4.4 2006/01/07 11:46:55 xleroy Exp $ *) |
---|