source: Deliverables/D3.1/C-semantics/Maps.ma @ 405

Last change on this file since 405 was 11, checked in by campbell, 9 years ago

Fill in some axioms to aid executablity.
Implement global variable lookups and funtion returns.
Update compcert patch to use binary representation.

File size: 42.1 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 "Coqlib.ma".
36(* XXX: For ident type; should maybe follow original and use positives *)
37include "AST.ma".
38
39(*
40Set Implicit Arguments.
41*)
42(* * * The abstract signatures of trees *)
43
44nrecord TREE (elt:Type) : Type[1] ≝ {
45  elt_eq: ∀a,b: elt. (a = b) + (a ≠ b);
46  tree_t: Type → Type;
47  tree_eq: ∀A: Type. ∀x,y: A. (x=y) + (x≠y) →
48      ∀a,b: tree_t A. (a = b) + (a ≠ b);
49  empty: ∀A: Type. tree_t A;
50  get: ∀A: Type. elt → tree_t A → option A;
51  set: ∀A: Type. elt → A → tree_t A → tree_t A;
52  remove: ∀A: Type. 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. (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. tree_t A → list (elt × A);
121(*
122  Hypothesis elements_correct:
123    forall (A: Type) (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. (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
145nrecord MAP : Type[1] ≝ {
146  elt: Type;
147  elt_eq: ∀a,b: elt. (a = b) + (a ≠ b);
148  t: Type → Type;
149  init: ∀A: Type. A → t A;
150  get: ∀A: Type. elt → t A → A;
151  set: ∀A: Type. 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 *)
175nlet rec assoc_get (A:Type) (i:ident) (l:list (ident × A)) on l ≝
176match l with
177[ nil ⇒ None ?
178| cons h t ⇒
179  match h with [ mk_pair hi ha ⇒
180    match ident_eq i hi with [ inl _ ⇒ Some ? ha | inr _ ⇒ assoc_get A i t ] ]
181].
182
183naxiom assoc_tree_eq: ∀A: Type. ∀x,y: A. (x=y) + (x≠y) →
184      ∀a,b: list (ident × A). (a = b) + (a ≠ b).
185naxiom assoc_remove: ∀A: Type. ident → list (ident × A) → list (ident × A).
186naxiom assoc_tree_map: ∀A,B: Type. (ident → A → B) → list (ident × A) → list (ident × B).
187ndefinition assoc_elements: ∀A: Type. list (ident × A) → list (ident × A) ≝ λA,x.x.
188naxiom assoc_tree_fold: ∀A,B: Type. (B → ident → A → B) → list (ident × A) → B → B.
189
190ndefinition 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.