source: src/common/Maps.ma @ 985

Last change on this file since 985 was 747, checked in by campbell, 10 years ago

Merge the two AST files together (although some definitions still need to be
harmonised).
File size: 42.2 KB
Line 
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
35include "utilities/Coqlib.ma".
36(* XXX: For ident type; should maybe follow original and use positives *)
37include "common/AST.ma".
38
39(*
40Set Implicit Arguments.
41*)
42(* * * The abstract signatures of trees *)
43
44record 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
145record 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).
169End MAP.
170
171(** * An implementation of trees over type [positive] *)
172*)
173
174(* XXX: need real tree impl *)
175let rec assoc_get (A:Type[0]) (i:ident) (l:list (ident × A)) on l ≝
176match 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
183axiom assoc_tree_eq: ∀A: Type[0]. ∀x,y: A. (x=y) + (x≠y) →
184      ∀a,b: list (ident × A). (a = b) + (a ≠ b).
185axiom assoc_remove: ∀A: Type[0]. ident → list (ident × A) → list (ident × A).
186axiom assoc_tree_map: ∀A,B: Type[0]. (ident → A → B) → list (ident × A) → list (ident × B).
187definition assoc_elements: ∀A: Type[0]. list (ident × A) → list (ident × A) ≝ λA,x.x.
188axiom assoc_tree_fold: ∀A,B: Type[0]. (B → ident → A → B) → list (ident × A) → B → B.
189
190definition PTree : TREE ident ≝
191mk_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(*
204Module 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
987End PTree.
988
989(** * An implementation of maps over type [positive] *)
990
991Module 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
1065End PMap.
1066
1067(** * An implementation of maps over any type that injects into type [positive] *)
1068
1069Module 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}.
1074End INDEXED_TYPE.
1075
1076Module 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
1127End IMap.
1128
1129Module 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.
1145End ZIndexed.
1146
1147Module ZMap := IMap(ZIndexed).
1148
1149Module 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.
1166End NIndexed.
1167
1168Module NMap := IMap(NIndexed).
1169
1170(** * An implementation of maps over any type with decidable equality *)
1171
1172Module Type EQUALITY_TYPE.
1173  Variable t: Type.
1174  Variable eq: forall (x y: t), {x = y} + {x <> y}.
1175End EQUALITY_TYPE.
1176
1177Module 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.
1224End EMap.
1225
1226(** * Additional properties over trees *)
1227
1228Module Tree_Properties(T: TREE).
1229
1230(** An induction principle over [fold]. *)
1231
1232Section TREE_FOLD_IND.
1233
1234Variables V A: Type.
1235Variable f: A -> T.elt -> V -> A.
1236Variable P: T.t V -> A -> Prop.
1237Variable init: A.
1238Variable m_final: T.t V.
1239
1240Hypothesis 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
1245Hypothesis H_base:
1246  P (T.empty _) init.
1247
1248Hypothesis 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
1252Definition f' (a: A) (p : T.elt * V) := f a (fst p) (snd p).
1253
1254Definition P' (l: list (T.elt * V)) (a: A) : Prop :=
1255  forall m, list_equiv l (T.elements m) -> P m a.
1256
1257Remark H_base':
1258  P' nil init.
1259Proof.
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.
1264Qed.
1265
1266Remark 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).
1272Proof.
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.
1291Qed.
1292
1293Lemma 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).
1299Proof.
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.
1310Qed.
1311
1312Theorem fold_rec:
1313  P m_final (T.fold f m_final init).
1314Proof.
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.
1323Qed.
1324
1325End TREE_FOLD_IND.
1326
1327End Tree_Properties.
1328
1329Module PTree_Properties := Tree_Properties(PTree).
1330
1331(** * Useful notations *)
1332
1333Notation "a ! b" := (PTree.get b a) (at level 1).
1334Notation "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 $ *)
Note: See TracBrowser for help on using the repository browser.