← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to theories/FSets/FMapPositive.v

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

Lines of Context:
theories/FSets/FMapPositive.v
 
1
(***********************************************************************)
 
2
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
 
3
(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
 
4
(*   \VV/  *************************************************************)
 
5
(*    //   *      This file is distributed under the terms of the      *)
 
6
(*         *       GNU Lesser General Public License Version 2.1       *)
 
7
(***********************************************************************)
 
8
 
 
9
(* Finite sets library.  
 
10
 * Authors: Pierre Letouzey and Jean-Christophe Filliâtre 
 
11
 * Institution: LRI, CNRS UMR 8623 - Université Paris Sud
 
12
 *              91405 Orsay, France *)
 
13
 
 
14
(* $Id: FMapPositive.v 11699 2008-12-18 11:49:08Z letouzey $ *)
 
15
 
 
16
Require Import Bool.
 
17
Require Import ZArith.
 
18
Require Import OrderedType.
 
19
Require Import OrderedTypeEx.
 
20
Require Import FMapInterface.
 
21
 
 
22
Set Implicit Arguments.
 
23
 
 
24
Open Local Scope positive_scope.
 
25
 
 
26
(** * An implementation of [FMapInterface.S] for positive keys. *)
 
27
 
 
28
(** This file is an adaptation to the [FMap] framework of a work by 
 
29
  Xavier Leroy and Sandrine Blazy (used for building certified compilers).
 
30
  Keys are of type [positive], and maps are binary trees: the sequence 
 
31
  of binary digits of a positive number corresponds to a path in such a tree.
 
32
  This is quite similar to the [IntMap] library, except that no path compression 
 
33
  is implemented, and that the current file is simple enough to be 
 
34
  self-contained. *)
 
35
 
 
36
(** Even if [positive] can be seen as an ordered type with respect to the 
 
37
  usual order (see [OrderedTypeEx]), we use here a lexicographic order 
 
38
  over bits, which is more natural here (lower bits are considered first). *)
 
39
 
 
40
Module PositiveOrderedTypeBits <: UsualOrderedType.
 
41
  Definition t:=positive.
 
42
  Definition eq:=@eq positive.
 
43
  Definition eq_refl := @refl_equal t.
 
44
  Definition eq_sym := @sym_eq t.
 
45
  Definition eq_trans := @trans_eq t.
 
46
 
 
47
  Fixpoint bits_lt (p q:positive) { struct p } : Prop := 
 
48
   match p, q with 
 
49
   | xH, xI _ => True
 
50
   | xH, _ => False
 
51
   | xO p, xO q => bits_lt p q
 
52
   | xO _, _ => True
 
53
   | xI p, xI q => bits_lt p q
 
54
   | xI _, _ => False
 
55
   end.
 
56
 
 
57
  Definition lt:=bits_lt.
 
58
 
 
59
  Lemma bits_lt_trans : forall x y z : positive, bits_lt x y -> bits_lt y z -> bits_lt x z.
 
60
  Proof.
 
61
  induction x.
 
62
  induction y; destruct z; simpl; eauto; intuition.
 
63
  induction y; destruct z; simpl; eauto; intuition.
 
64
  induction y; destruct z; simpl; eauto; intuition.
 
65
  Qed.
 
66
 
 
67
  Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z.
 
68
  Proof. 
 
69
  exact bits_lt_trans.
 
70
  Qed.
 
71
 
 
72
  Lemma bits_lt_antirefl : forall x : positive, ~ bits_lt x x.
 
73
  Proof.
 
74
  induction x; simpl; auto.
 
75
  Qed.
 
76
 
 
77
  Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y.
 
78
  Proof.
 
79
  intros; intro.
 
80
  rewrite <- H0 in H; clear H0 y.
 
81
  unfold lt in H.
 
82
  exact (bits_lt_antirefl x H).
 
83
  Qed.
 
84
 
 
85
  Definition compare : forall x y : t, Compare lt eq x y.
 
86
  Proof.
 
87
  induction x; destruct y.
 
88
  (* I I *)
 
89
  destruct (IHx y).
 
90
  apply LT; auto.
 
91
  apply EQ; rewrite e; red; auto.
 
92
  apply GT; auto.
 
93
  (* I O *)
 
94
  apply GT; simpl; auto.
 
95
  (* I H *)
 
96
  apply GT; simpl; auto.
 
97
  (* O I *)
 
98
  apply LT; simpl; auto.
 
99
  (* O O *)
 
100
  destruct (IHx y).
 
101
  apply LT; auto.
 
102
  apply EQ; rewrite e; red; auto.
 
103
  apply GT; auto.
 
104
  (* O H *) 
 
105
  apply LT; simpl; auto.
 
106
  (* H I *)
 
107
  apply LT; simpl; auto.
 
108
  (* H O *)
 
109
  apply GT; simpl; auto.
 
110
  (* H H *)
 
111
  apply EQ; red; auto.
 
112
  Qed.
 
113
 
 
114
  Lemma eq_dec (x y: positive): {x = y} + {x <> y}.
 
115
  Proof.
 
116
  intros. case_eq ((x ?= y) Eq); intros.
 
117
  left. apply Pcompare_Eq_eq; auto.
 
118
  right. red. intro. subst y. rewrite (Pcompare_refl x) in H. discriminate.
 
119
  right. red. intro. subst y. rewrite (Pcompare_refl x) in H. discriminate.
 
120
  Qed.
 
121
 
 
122
End PositiveOrderedTypeBits.
 
123
 
 
124
(** Other positive stuff *)
 
125
 
 
126
Fixpoint append (i j : positive) {struct i} : positive :=
 
127
    match i with
 
128
      | xH => j
 
129
      | xI ii => xI (append ii j)
 
130
      | xO ii => xO (append ii j)
 
131
    end.
 
132
 
 
133
Lemma append_assoc_0 : 
 
134
  forall (i j : positive), append i (xO j) = append (append i (xO xH)) j.
 
135
Proof.
 
136
 induction i; intros; destruct j; simpl;
 
137
 try rewrite (IHi (xI j));
 
138
 try rewrite (IHi (xO j));
 
139
 try rewrite <- (IHi xH);
 
140
 auto.
 
141
Qed.
 
142
 
 
143
Lemma append_assoc_1 : 
 
144
  forall (i j : positive), append i (xI j) = append (append i (xI xH)) j.
 
145
Proof.
 
146
 induction i; intros; destruct j; simpl;
 
147
 try rewrite (IHi (xI j));
 
148
 try rewrite (IHi (xO j));
 
149
 try rewrite <- (IHi xH);
 
150
 auto.
 
151
Qed.
 
152
 
 
153
Lemma append_neutral_r : forall (i : positive), append i xH = i.
 
154
Proof.
 
155
 induction i; simpl; congruence.
 
156
Qed.
 
157
 
 
158
Lemma append_neutral_l : forall (i : positive), append xH i = i.
 
159
Proof.
 
160
 simpl; auto.
 
161
Qed.
 
162
 
 
163
 
 
164
(** The module of maps over positive keys *)
 
165
 
 
166
Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
 
167
 
 
168
  Module E:=PositiveOrderedTypeBits.
 
169
  Module ME:=KeyOrderedType E.
 
170
 
 
171
  Definition key := positive.
 
172
 
 
173
  Inductive tree (A : Type) :=
 
174
    | Leaf : tree A
 
175
    | Node : tree A -> option A -> tree A -> tree A.
 
176
 
 
177
  Definition t := tree.
 
178
 
 
179
  Section A.
 
180
  Variable A:Type.
 
181
 
 
182
  Implicit Arguments Leaf [A].
 
183
 
 
184
  Definition empty : t A := Leaf.
 
185
 
 
186
  Fixpoint is_empty (m : t A) {struct m} : bool := 
 
187
   match m with 
 
188
    | Leaf => true
 
189
    | Node l None r => (is_empty l) && (is_empty r)
 
190
    | _ => false
 
191
   end.
 
192
 
 
193
  Fixpoint find (i : positive) (m : t A) {struct i} : option A :=
 
194
    match m with
 
195
    | Leaf => None
 
196
    | Node l o r =>
 
197
        match i with
 
198
        | xH => o
 
199
        | xO ii => find ii l
 
200
        | xI ii => find ii r
 
201
        end
 
202
    end.
 
203
 
 
204
  Fixpoint mem (i : positive) (m : t A) {struct i} : bool :=
 
205
    match m with
 
206
    | Leaf => false
 
207
    | Node l o r =>
 
208
        match i with
 
209
        | xH => match o with None => false | _ => true end
 
210
        | xO ii => mem ii l
 
211
        | xI ii => mem ii r
 
212
        end
 
213
    end.
 
214
 
 
215
  Fixpoint add (i : positive) (v : A) (m : t A) {struct i} : t A :=
 
216
    match m with
 
217
    | Leaf =>
 
218
        match i with
 
219
        | xH => Node Leaf (Some v) Leaf
 
220
        | xO ii => Node (add ii v Leaf) None Leaf
 
221
        | xI ii => Node Leaf None (add ii v Leaf)
 
222
        end
 
223
    | Node l o r =>
 
224
        match i with
 
225
        | xH => Node l (Some v) r
 
226
        | xO ii => Node (add ii v l) o r
 
227
        | xI ii => Node l o (add ii v r)
 
228
        end
 
229
    end.
 
230
 
 
231
  Fixpoint remove (i : positive) (m : t A) {struct i} : t A :=
 
232
    match i with
 
233
    | xH =>
 
234
        match m with
 
235
        | Leaf => Leaf
 
236
        | Node Leaf o Leaf => Leaf
 
237
        | Node l o r => Node l None r
 
238
        end
 
239
    | xO ii =>
 
240
        match m with
 
241
        | Leaf => Leaf
 
242
        | Node l None Leaf =>
 
243
            match remove ii l with
 
244
            | Leaf => Leaf
 
245
            | mm => Node mm None Leaf
 
246
            end
 
247
        | Node l o r => Node (remove ii l) o r
 
248
        end
 
249
    | xI ii =>
 
250
        match m with
 
251
        | Leaf => Leaf
 
252
        | Node Leaf None r =>
 
253
            match remove ii r with
 
254
            | Leaf => Leaf
 
255
            | mm => Node Leaf None mm
 
256
            end
 
257
        | Node l o r => Node l o (remove ii r)
 
258
        end
 
259
    end.
 
260
 
 
261
  (** [elements] *)
 
262
 
 
263
    Fixpoint xelements (m : t A) (i : positive) {struct m}
 
264
             : list (positive * A) :=
 
265
      match m with
 
266
      | Leaf => nil
 
267
      | Node l None r =>
 
268
          (xelements l (append i (xO xH))) ++ (xelements r (append i (xI xH)))
 
269
      | Node l (Some x) r =>
 
270
          (xelements l (append i (xO xH)))
 
271
          ++ ((i, x) :: xelements r (append i (xI xH)))
 
272
      end.
 
273
 
 
274
  (* Note: function [xelements] above is inefficient.  We should apply
 
275
     deforestation to it, but that makes the proofs even harder. *)
 
276
 
 
277
  Definition elements (m : t A) := xelements m xH.
 
278
 
 
279
  (** [cardinal] *)
 
280
 
 
281
  Fixpoint cardinal (m : t A) : nat :=
 
282
    match m with 
 
283
      | Leaf => 0%nat 
 
284
      | Node l None r => (cardinal l + cardinal r)%nat
 
285
      | Node l (Some _) r => S (cardinal l + cardinal r)
 
286
    end.
 
287
 
 
288
  Section CompcertSpec.
 
289
 
 
290
  Theorem gempty:
 
291
    forall (i: positive), find i empty = None.
 
292
  Proof.
 
293
    destruct i; simpl; auto.
 
294
  Qed.
 
295
 
 
296
  Theorem gss:
 
297
    forall (i: positive) (x: A) (m: t A), find i (add i x m) = Some x.
 
298
  Proof.
 
299
    induction i; destruct m; simpl; auto.
 
300
  Qed.
 
301
 
 
302
  Lemma gleaf : forall (i : positive), find i (Leaf : t A) = None.
 
303
  Proof. exact gempty. Qed.
 
304
 
 
305
  Theorem gso:
 
306
    forall (i j: positive) (x: A) (m: t A),
 
307
    i <> j -> find i (add j x m) = find i m.
 
308
  Proof.
 
309
    induction i; intros; destruct j; destruct m; simpl;
 
310
       try rewrite <- (gleaf i); auto; try apply IHi; congruence.
 
311
  Qed.
 
312
 
 
313
  Lemma rleaf : forall (i : positive), remove i (Leaf : t A) = Leaf.
 
314
  Proof. destruct i; simpl; auto. Qed.
 
315
 
 
316
  Theorem grs:
 
317
    forall (i: positive) (m: t A), find i (remove i m) = None.
 
318
  Proof.
 
319
    induction i; destruct m.
 
320
     simpl; auto.
 
321
     destruct m1; destruct o; destruct m2 as [ | ll oo rr]; simpl; auto.
 
322
      rewrite (rleaf i); auto.
 
323
      cut (find i (remove i (Node ll oo rr)) = None).
 
324
        destruct (remove i (Node ll oo rr)); auto; apply IHi.
 
325
        apply IHi.
 
326
     simpl; auto.
 
327
     destruct m1 as [ | ll oo rr]; destruct o; destruct m2; simpl; auto.
 
328
      rewrite (rleaf i); auto.
 
329
      cut (find i (remove i (Node ll oo rr)) = None).
 
330
        destruct (remove i (Node ll oo rr)); auto; apply IHi.
 
331
        apply IHi.
 
332
     simpl; auto.
 
333
     destruct m1; destruct m2; simpl; auto.
 
334
  Qed.
 
335
 
 
336
  Theorem gro:
 
337
    forall (i j: positive) (m: t A),
 
338
    i <> j -> find i (remove j m) = find i m.
 
339
  Proof.
 
340
    induction i; intros; destruct j; destruct m;
 
341
        try rewrite (rleaf (xI j));
 
342
        try rewrite (rleaf (xO j));
 
343
        try rewrite (rleaf 1); auto;
 
344
        destruct m1; destruct o; destruct m2;
 
345
        simpl;
 
346
        try apply IHi; try congruence;
 
347
        try rewrite (rleaf j); auto;
 
348
        try rewrite (gleaf i); auto.
 
349
     cut (find i (remove j (Node m2_1 o m2_2)) = find i (Node m2_1 o m2_2));
 
350
        [ destruct (remove j (Node m2_1 o m2_2)); try rewrite (gleaf i); auto
 
351
        | apply IHi; congruence ].
 
352
     destruct (remove j (Node m1_1 o0 m1_2)); simpl; try rewrite (gleaf i);
 
353
        auto.
 
354
     destruct (remove j (Node m2_1 o m2_2)); simpl; try rewrite (gleaf i);
 
355
        auto.
 
356
     cut (find i (remove j (Node m1_1 o0 m1_2)) = find i (Node m1_1 o0 m1_2));
 
357
        [ destruct (remove j (Node m1_1 o0 m1_2)); try rewrite (gleaf i); auto
 
358
        | apply IHi; congruence ].
 
359
     destruct (remove j (Node m2_1 o m2_2)); simpl; try rewrite (gleaf i);
 
360
        auto.
 
361
     destruct (remove j (Node m1_1 o0 m1_2)); simpl; try rewrite (gleaf i);
 
362
        auto.
 
363
  Qed.
 
364
 
 
365
  Lemma xelements_correct:
 
366
      forall (m: t A) (i j : positive) (v: A),
 
367
      find i m = Some v -> List.In (append j i, v) (xelements m j).
 
368
    Proof.
 
369
      induction m; intros.
 
370
       rewrite (gleaf i) in H; congruence.
 
371
       destruct o; destruct i; simpl; simpl in H.
 
372
        rewrite append_assoc_1; apply in_or_app; right; apply in_cons;
 
373
          apply IHm2; auto.
 
374
        rewrite append_assoc_0; apply in_or_app; left; apply IHm1; auto.
 
375
        rewrite append_neutral_r; apply in_or_app; injection H;
 
376
          intro EQ; rewrite EQ; right; apply in_eq.
 
377
        rewrite append_assoc_1; apply in_or_app; right; apply IHm2; auto.
 
378
        rewrite append_assoc_0; apply in_or_app; left; apply IHm1; auto.
 
379
        congruence.
 
380
    Qed.
 
381
 
 
382
  Theorem elements_correct:
 
383
    forall (m: t A) (i: positive) (v: A),
 
384
    find i m = Some v -> List.In (i, v) (elements m).
 
385
  Proof.
 
386
    intros m i v H.
 
387
    exact (xelements_correct m i xH H).
 
388
  Qed.
 
389
 
 
390
  Fixpoint xfind (i j : positive) (m : t A) {struct j} : option A :=
 
391
      match i, j with
 
392
      | _, xH => find i m
 
393
      | xO ii, xO jj => xfind ii jj m
 
394
      | xI ii, xI jj => xfind ii jj m
 
395
      | _, _ => None
 
396
      end.
 
397
 
 
398
   Lemma xfind_left :
 
399
      forall (j i : positive) (m1 m2 : t A) (o : option A) (v : A),
 
400
      xfind i (append j (xO xH)) m1 = Some v -> xfind i j (Node m1 o m2) = Some v.
 
401
    Proof.
 
402
      induction j; intros; destruct i; simpl; simpl in H; auto; try congruence.
 
403
      destruct i; congruence.
 
404
    Qed.
 
405
 
 
406
    Lemma xelements_ii :
 
407
      forall (m: t A) (i j : positive) (v: A),
 
408
      List.In (xI i, v) (xelements m (xI j)) -> List.In (i, v) (xelements m j).
 
409
    Proof.
 
410
      induction m.
 
411
       simpl; auto.
 
412
       intros; destruct o; simpl; simpl in H; destruct (in_app_or _ _ _ H);
 
413
         apply in_or_app.
 
414
        left; apply IHm1; auto.
 
415
        right; destruct (in_inv H0).
 
416
         injection H1; intros Eq1 Eq2; rewrite Eq1; rewrite Eq2; apply in_eq.
 
417
         apply in_cons; apply IHm2; auto.
 
418
        left; apply IHm1; auto.
 
419
        right; apply IHm2; auto.
 
420
    Qed.
 
421
 
 
422
    Lemma xelements_io :
 
423
      forall (m: t A) (i j : positive) (v: A),
 
424
      ~List.In (xI i, v) (xelements m (xO j)).
 
425
    Proof.
 
426
      induction m.
 
427
       simpl; auto.
 
428
       intros; destruct o; simpl; intro H; destruct (in_app_or _ _ _ H).
 
429
        apply (IHm1 _ _ _ H0).
 
430
        destruct (in_inv H0).
 
431
         congruence.
 
432
         apply (IHm2 _ _ _ H1).
 
433
        apply (IHm1 _ _ _ H0).
 
434
        apply (IHm2 _ _ _ H0).
 
435
    Qed.
 
436
 
 
437
    Lemma xelements_oo :
 
438
      forall (m: t A) (i j : positive) (v: A),
 
439
      List.In (xO i, v) (xelements m (xO j)) -> List.In (i, v) (xelements m j).
 
440
    Proof.
 
441
      induction m.
 
442
       simpl; auto.
 
443
       intros; destruct o; simpl; simpl in H; destruct (in_app_or _ _ _ H);
 
444
         apply in_or_app.
 
445
        left; apply IHm1; auto.
 
446
        right; destruct (in_inv H0).
 
447
         injection H1; intros Eq1 Eq2; rewrite Eq1; rewrite Eq2; apply in_eq.
 
448
         apply in_cons; apply IHm2; auto.
 
449
        left; apply IHm1; auto.
 
450
        right; apply IHm2; auto.
 
451
    Qed.
 
452
 
 
453
    Lemma xelements_oi :
 
454
      forall (m: t A) (i j : positive) (v: A),
 
455
      ~List.In (xO i, v) (xelements m (xI j)).
 
456
    Proof.
 
457
      induction m.
 
458
       simpl; auto.
 
459
       intros; destruct o; simpl; intro H; destruct (in_app_or _ _ _ H).
 
460
        apply (IHm1 _ _ _ H0).
 
461
        destruct (in_inv H0).
 
462
         congruence.
 
463
         apply (IHm2 _ _ _ H1).
 
464
        apply (IHm1 _ _ _ H0).
 
465
        apply (IHm2 _ _ _ H0).
 
466
    Qed.
 
467
 
 
468
    Lemma xelements_ih :
 
469
      forall (m1 m2: t A) (o: option A) (i : positive) (v: A),
 
470
      List.In (xI i, v) (xelements (Node m1 o m2) xH) -> List.In (i, v) (xelements m2 xH).
 
471
    Proof.
 
472
      destruct o; simpl; intros; destruct (in_app_or _ _ _ H).
 
473
        absurd (List.In (xI i, v) (xelements m1 2)); auto; apply xelements_io; auto.
 
474
        destruct (in_inv H0).
 
475
         congruence.
 
476
         apply xelements_ii; auto.
 
477
        absurd (List.In (xI i, v) (xelements m1 2)); auto; apply xelements_io; auto.
 
478
        apply xelements_ii; auto.
 
479
    Qed.
 
480
 
 
481
    Lemma xelements_oh :
 
482
      forall (m1 m2: t A) (o: option A) (i : positive) (v: A),
 
483
      List.In (xO i, v) (xelements (Node m1 o m2) xH) -> List.In (i, v) (xelements m1 xH).
 
484
    Proof.
 
485
      destruct o; simpl; intros; destruct (in_app_or _ _ _ H).
 
486
        apply xelements_oo; auto.
 
487
        destruct (in_inv H0).
 
488
         congruence.
 
489
         absurd (List.In (xO i, v) (xelements m2 3)); auto; apply xelements_oi; auto.
 
490
        apply xelements_oo; auto.
 
491
        absurd (List.In (xO i, v) (xelements m2 3)); auto; apply xelements_oi; auto.
 
492
    Qed.
 
493
 
 
494
    Lemma xelements_hi :
 
495
      forall (m: t A) (i : positive) (v: A),
 
496
      ~List.In (xH, v) (xelements m (xI i)).
 
497
    Proof.
 
498
      induction m; intros.
 
499
       simpl; auto.
 
500
       destruct o; simpl; intro H; destruct (in_app_or _ _ _ H).
 
501
        generalize H0; apply IHm1; auto.
 
502
        destruct (in_inv H0).
 
503
         congruence.
 
504
         generalize H1; apply IHm2; auto.
 
505
        generalize H0; apply IHm1; auto.
 
506
        generalize H0; apply IHm2; auto.
 
507
    Qed.
 
508
 
 
509
    Lemma xelements_ho :
 
510
      forall (m: t A) (i : positive) (v: A),
 
511
      ~List.In (xH, v) (xelements m (xO i)).
 
512
    Proof.
 
513
      induction m; intros.
 
514
       simpl; auto.
 
515
       destruct o; simpl; intro H; destruct (in_app_or _ _ _ H).
 
516
        generalize H0; apply IHm1; auto.
 
517
        destruct (in_inv H0).
 
518
         congruence.
 
519
         generalize H1; apply IHm2; auto.
 
520
        generalize H0; apply IHm1; auto.
 
521
        generalize H0; apply IHm2; auto.
 
522
    Qed.
 
523
 
 
524
    Lemma find_xfind_h :
 
525
      forall (m: t A) (i: positive), find i m = xfind i xH m.
 
526
    Proof.
 
527
      destruct i; simpl; auto.
 
528
    Qed.
 
529
 
 
530
    Lemma xelements_complete:
 
531
      forall (i j : positive) (m: t A) (v: A),
 
532
      List.In (i, v) (xelements m j) -> xfind i j m = Some v.
 
533
    Proof.
 
534
      induction i; simpl; intros; destruct j; simpl.
 
535
       apply IHi; apply xelements_ii; auto.
 
536
       absurd (List.In (xI i, v) (xelements m (xO j))); auto; apply xelements_io.
 
537
       destruct m.
 
538
        simpl in H; tauto.
 
539
        rewrite find_xfind_h. apply IHi. apply (xelements_ih _ _ _ _ _ H).
 
540
       absurd (List.In (xO i, v) (xelements m (xI j))); auto; apply xelements_oi.
 
541
       apply IHi; apply xelements_oo; auto.
 
542
       destruct m.
 
543
        simpl in H; tauto.
 
544
        rewrite find_xfind_h. apply IHi. apply (xelements_oh _ _ _ _ _ H).
 
545
       absurd (List.In (xH, v) (xelements m (xI j))); auto; apply xelements_hi.
 
546
       absurd (List.In (xH, v) (xelements m (xO j))); auto; apply xelements_ho.
 
547
       destruct m.
 
548
        simpl in H; tauto.
 
549
        destruct o; simpl in H; destruct (in_app_or _ _ _ H).
 
550
         absurd (List.In (xH, v) (xelements m1 (xO xH))); auto; apply xelements_ho.
 
551
         destruct (in_inv H0).
 
552
          congruence.
 
553
          absurd (List.In (xH, v) (xelements m2 (xI xH))); auto; apply xelements_hi.
 
554
         absurd (List.In (xH, v) (xelements m1 (xO xH))); auto; apply xelements_ho.
 
555
         absurd (List.In (xH, v) (xelements m2 (xI xH))); auto; apply xelements_hi.
 
556
    Qed.
 
557
 
 
558
  Theorem elements_complete:
 
559
    forall (m: t A) (i: positive) (v: A),
 
560
    List.In (i, v) (elements m) -> find i m = Some v.
 
561
  Proof.
 
562
    intros m i v H.
 
563
    unfold elements in H.
 
564
    rewrite find_xfind_h.
 
565
    exact (xelements_complete i xH m v H).
 
566
  Qed.
 
567
 
 
568
  Lemma cardinal_1 : 
 
569
   forall (m: t A), cardinal m = length (elements m).
 
570
  Proof.
 
571
   unfold elements.
 
572
   intros m; set (p:=1); clearbody p; revert m p.
 
573
   induction m; simpl; auto; intros.
 
574
   rewrite (IHm1 (append p 2)), (IHm2 (append p 3)); auto.
 
575
   destruct o; rewrite app_length; simpl; omega.
 
576
  Qed.
 
577
 
 
578
  End CompcertSpec.
 
579
 
 
580
  Definition MapsTo (i:positive)(v:A)(m:t A) := find i m = Some v.
 
581
 
 
582
  Definition In (i:positive)(m:t A) := exists e:A, MapsTo i e m.
 
583
 
 
584
  Definition Empty m := forall (a : positive)(e:A) , ~ MapsTo a e m.
 
585
 
 
586
  Definition eq_key (p p':positive*A) := E.eq (fst p) (fst p').
 
587
      
 
588
  Definition eq_key_elt (p p':positive*A) := 
 
589
          E.eq (fst p) (fst p') /\ (snd p) = (snd p').
 
590
 
 
591
  Definition lt_key (p p':positive*A) := E.lt (fst p) (fst p').
 
592
 
 
593
  Lemma mem_find : 
 
594
    forall m x, mem x m = match find x m with None => false | _ => true end.
 
595
  Proof.
 
596
  induction m; destruct x; simpl; auto.
 
597
  Qed.
 
598
 
 
599
  Lemma Empty_alt : forall m, Empty m <-> forall a, find a m = None.
 
600
  Proof.
 
601
  unfold Empty, MapsTo.
 
602
  intuition.
 
603
  generalize (H a).
 
604
  destruct (find a m); intuition.
 
605
  elim (H0 a0); auto.
 
606
  rewrite H in H0; discriminate.
 
607
  Qed.
 
608
 
 
609
  Lemma Empty_Node : forall l o r, Empty (Node l o r) <-> o=None /\ Empty l /\ Empty r.
 
610
  Proof.
 
611
  intros l o r.
 
612
  split.
 
613
  rewrite Empty_alt.
 
614
  split.
 
615
  destruct o; auto.
 
616
  generalize (H 1); simpl; auto.
 
617
  split; rewrite Empty_alt; intros.
 
618
  generalize (H (xO a)); auto.
 
619
  generalize (H (xI a)); auto.
 
620
  intros (H,(H0,H1)).
 
621
  subst.
 
622
  rewrite Empty_alt; intros.
 
623
  destruct a; auto.
 
624
  simpl; generalize H1; rewrite Empty_alt; auto.
 
625
  simpl; generalize H0; rewrite Empty_alt; auto.
 
626
  Qed.
 
627
 
 
628
  Section FMapSpec. 
 
629
 
 
630
  Lemma mem_1 : forall m x, In x m -> mem x m = true.
 
631
  Proof.
 
632
  unfold In, MapsTo; intros m x; rewrite mem_find.
 
633
  destruct 1 as (e0,H0); rewrite H0; auto.
 
634
  Qed.
 
635
 
 
636
  Lemma mem_2 : forall m x, mem x m = true -> In x m. 
 
637
  Proof.
 
638
  unfold In, MapsTo; intros m x; rewrite mem_find.
 
639
  destruct (find x m).
 
640
  exists a; auto.
 
641
  intros; discriminate.
 
642
  Qed.
 
643
 
 
644
  Variable  m m' m'' : t A.
 
645
  Variable x y z : key.
 
646
  Variable e e' : A.
 
647
 
 
648
  Lemma MapsTo_1 : E.eq x y -> MapsTo x e m -> MapsTo y e m.
 
649
  Proof. intros; rewrite <- H; auto. Qed.
 
650
 
 
651
  Lemma find_1 : MapsTo x e m -> find x m = Some e.
 
652
  Proof. unfold MapsTo; auto. Qed.
 
653
 
 
654
  Lemma find_2 : find x m = Some e -> MapsTo x e m.
 
655
  Proof. red; auto. Qed.
 
656
 
 
657
  Lemma empty_1 : Empty empty.
 
658
  Proof.
 
659
  rewrite Empty_alt; apply gempty.
 
660
  Qed.
 
661
 
 
662
  Lemma is_empty_1 : Empty m -> is_empty m = true. 
 
663
  Proof.
 
664
  induction m; simpl; auto.
 
665
  rewrite Empty_Node.
 
666
  intros (H,(H0,H1)).
 
667
  subst; simpl.
 
668
  rewrite IHt0_1; simpl; auto.
 
669
  Qed.
 
670
 
 
671
  Lemma is_empty_2 : is_empty m = true -> Empty m.
 
672
  Proof.
 
673
  induction m; simpl; auto.
 
674
  rewrite Empty_alt.
 
675
  intros _; exact gempty.
 
676
  rewrite Empty_Node.
 
677
  destruct o.
 
678
  intros; discriminate.
 
679
  intro H; destruct (andb_prop _ _ H); intuition.
 
680
  Qed.
 
681
 
 
682
  Lemma add_1 : E.eq x y -> MapsTo y e (add x e m).
 
683
  Proof.
 
684
  unfold MapsTo.
 
685
  intro H; rewrite H; clear H.
 
686
  apply gss.
 
687
  Qed.
 
688
 
 
689
  Lemma add_2 : ~ E.eq x y -> MapsTo y e m -> MapsTo y e (add x e' m).
 
690
  Proof.
 
691
  unfold MapsTo.
 
692
  intros; rewrite gso; auto.
 
693
  Qed.
 
694
 
 
695
  Lemma add_3 : ~ E.eq x y -> MapsTo y e (add x e' m) -> MapsTo y e m.
 
696
  Proof.
 
697
  unfold MapsTo.
 
698
  intro H; rewrite gso; auto.
 
699
  Qed.
 
700
 
 
701
  Lemma remove_1 : E.eq x y -> ~ In y (remove x m).
 
702
  Proof. 
 
703
  intros; intro.
 
704
  generalize (mem_1 H0).
 
705
  rewrite mem_find.
 
706
  rewrite H.
 
707
  rewrite grs.
 
708
  intros; discriminate.
 
709
  Qed.
 
710
 
 
711
  Lemma remove_2 : ~ E.eq x y -> MapsTo y e m -> MapsTo y e (remove x m).
 
712
  Proof.
 
713
  unfold MapsTo.
 
714
  intro H; rewrite gro; auto.
 
715
  Qed.
 
716
 
 
717
  Lemma remove_3 : MapsTo y e (remove x m) -> MapsTo y e m.
 
718
  Proof. 
 
719
  unfold MapsTo.
 
720
  destruct (E.eq_dec x y).
 
721
  subst.
 
722
  rewrite grs; intros; discriminate.
 
723
  rewrite gro; auto.
 
724
  Qed.
 
725
  
 
726
  Lemma elements_1 : 
 
727
     MapsTo x e m -> InA eq_key_elt (x,e) (elements m).
 
728
  Proof.
 
729
  unfold MapsTo.
 
730
  rewrite InA_alt.
 
731
  intro H.
 
732
  exists (x,e).
 
733
  split.
 
734
  red; simpl; unfold E.eq; auto.
 
735
  apply elements_correct; auto.
 
736
  Qed.
 
737
 
 
738
  Lemma elements_2 : 
 
739
     InA eq_key_elt (x,e) (elements m) -> MapsTo x e m.
 
740
  Proof.
 
741
  unfold MapsTo.
 
742
  rewrite InA_alt.
 
743
  intros ((e0,a),(H,H0)).
 
744
  red in H; simpl in H; unfold E.eq in H; destruct H; subst.
 
745
  apply elements_complete; auto.
 
746
  Qed.
 
747
 
 
748
  Lemma xelements_bits_lt_1 : forall p p0 q m v, 
 
749
     List.In (p0,v) (xelements m (append p (xO q))) -> E.bits_lt p0 p.
 
750
  Proof.
 
751
  intros.
 
752
  generalize (xelements_complete _ _ _ _ H); clear H; intros.
 
753
  revert p0 q m v H.
 
754
  induction p; destruct p0; simpl; intros; eauto; try discriminate.
 
755
  Qed.
 
756
 
 
757
  Lemma xelements_bits_lt_2 : forall p p0 q m v, 
 
758
     List.In (p0,v) (xelements m (append p (xI q))) -> E.bits_lt p p0.
 
759
  Proof.
 
760
  intros.
 
761
  generalize (xelements_complete _ _ _ _ H); clear H; intros.
 
762
  revert p0 q m v H.
 
763
  induction p; destruct p0; simpl; intros; eauto; try discriminate.
 
764
  Qed.
 
765
 
 
766
  Lemma xelements_sort : forall p, sort lt_key (xelements m p).
 
767
  Proof.
 
768
  induction m.
 
769
  simpl; auto.
 
770
  destruct o; simpl; intros.
 
771
  (* Some *)
 
772
  apply (SortA_app (eqA:=eq_key_elt)); auto.
 
773
  compute; intuition.
 
774
  constructor; auto.
 
775
  apply In_InfA; intros.
 
776
  destruct y0.
 
777
  red; red; simpl.
 
778
  eapply xelements_bits_lt_2; eauto.
 
779
  intros x0 y0.
 
780
  do 2 rewrite InA_alt.
 
781
  intros (y1,(Hy1,H)) (y2,(Hy2,H0)).
 
782
  destruct y1; destruct x0; compute in Hy1; destruct Hy1; subst.
 
783
  destruct y2; destruct y0; compute in Hy2; destruct Hy2; subst.
 
784
  red; red; simpl.
 
785
  destruct H0.
 
786
  injection H0; clear H0; intros _ H0; subst.
 
787
  eapply xelements_bits_lt_1; eauto.
 
788
  apply E.bits_lt_trans with p.
 
789
  eapply xelements_bits_lt_1; eauto.
 
790
  eapply xelements_bits_lt_2; eauto.
 
791
  (* None *)
 
792
  apply (SortA_app (eqA:=eq_key_elt)); auto.
 
793
  compute; intuition.
 
794
  intros x0 y0.
 
795
  do 2 rewrite InA_alt.
 
796
  intros (y1,(Hy1,H)) (y2,(Hy2,H0)).
 
797
  destruct y1; destruct x0; compute in Hy1; destruct Hy1; subst.
 
798
  destruct y2; destruct y0; compute in Hy2; destruct Hy2; subst.
 
799
  red; red; simpl.
 
800
  apply E.bits_lt_trans with p.
 
801
  eapply xelements_bits_lt_1; eauto.
 
802
  eapply xelements_bits_lt_2; eauto.
 
803
  Qed.
 
804
 
 
805
  Lemma elements_3 : sort lt_key (elements m). 
 
806
  Proof.
 
807
  unfold elements.
 
808
  apply xelements_sort; auto.
 
809
  Qed.
 
810
 
 
811
  Lemma elements_3w : NoDupA eq_key (elements m).
 
812
  Proof.
 
813
  change eq_key with (@ME.eqk A).
 
814
  apply ME.Sort_NoDupA; apply elements_3; auto.
 
815
  Qed.
 
816
 
 
817
  End FMapSpec.
 
818
 
 
819
  (** [map] and [mapi] *)
 
820
 
 
821
  Variable B : Type.
 
822
 
 
823
  Section Mapi.
 
824
 
 
825
    Variable f : positive -> A -> B.
 
826
 
 
827
    Fixpoint xmapi (m : t A) (i : positive) {struct m} : t B :=
 
828
       match m with
 
829
        | Leaf => @Leaf B
 
830
        | Node l o r => Node (xmapi l (append i (xO xH)))
 
831
                             (option_map (f i) o)
 
832
                             (xmapi r (append i (xI xH)))
 
833
       end.
 
834
 
 
835
    Definition mapi m := xmapi m xH.
 
836
 
 
837
  End Mapi.
 
838
 
 
839
  Definition map (f : A -> B) m := mapi (fun _ => f) m.
 
840
 
 
841
  End A.
 
842
 
 
843
  Lemma xgmapi:
 
844
      forall (A B: Type) (f: positive -> A -> B) (i j : positive) (m: t A),
 
845
      find i (xmapi f m j) = option_map (f (append j i)) (find i m).
 
846
  Proof.
 
847
  induction i; intros; destruct m; simpl; auto.
 
848
  rewrite (append_assoc_1 j i); apply IHi.
 
849
  rewrite (append_assoc_0 j i); apply IHi.
 
850
  rewrite (append_neutral_r j); auto.
 
851
  Qed.
 
852
 
 
853
  Theorem gmapi:
 
854
    forall (A B: Type) (f: positive -> A -> B) (i: positive) (m: t A),
 
855
    find i (mapi f m) = option_map (f i) (find i m).
 
856
  Proof.
 
857
  intros.
 
858
  unfold mapi.
 
859
  replace (f i) with (f (append xH i)).
 
860
  apply xgmapi.
 
861
  rewrite append_neutral_l; auto.
 
862
  Qed.
 
863
 
 
864
  Lemma mapi_1 : 
 
865
    forall (elt elt':Type)(m: t elt)(x:key)(e:elt)(f:key->elt->elt'), 
 
866
    MapsTo x e m -> 
 
867
    exists y, E.eq y x /\ MapsTo x (f y e) (mapi f m).
 
868
  Proof.
 
869
  intros.
 
870
  exists x.
 
871
  split; [red; auto|].
 
872
  apply find_2.
 
873
  generalize (find_1 H); clear H; intros.
 
874
  rewrite gmapi.
 
875
  rewrite H.
 
876
  simpl; auto.
 
877
  Qed.
 
878
 
 
879
  Lemma mapi_2 : 
 
880
    forall (elt elt':Type)(m: t elt)(x:key)(f:key->elt->elt'), 
 
881
    In x (mapi f m) -> In x m.
 
882
  Proof.
 
883
  intros.
 
884
  apply mem_2.
 
885
  rewrite mem_find.
 
886
  destruct H as (v,H).
 
887
  generalize (find_1 H); clear H; intros.
 
888
  rewrite gmapi in H.
 
889
  destruct (find x m); auto.
 
890
  simpl in *; discriminate.
 
891
  Qed.
 
892
 
 
893
  Lemma map_1 : forall (elt elt':Type)(m: t elt)(x:key)(e:elt)(f:elt->elt'), 
 
894
    MapsTo x e m -> MapsTo x (f e) (map f m).
 
895
  Proof.
 
896
  intros; unfold map.
 
897
  destruct (mapi_1 (fun _ => f) H); intuition.
 
898
  Qed.
 
899
  
 
900
  Lemma map_2 : forall (elt elt':Type)(m: t elt)(x:key)(f:elt->elt'), 
 
901
    In x (map f m) -> In x m.
 
902
  Proof.
 
903
  intros; unfold map in *; eapply mapi_2; eauto.
 
904
  Qed.
 
905
 
 
906
  Section map2.
 
907
  Variable A B C : Type.
 
908
  Variable f : option A -> option B -> option C.
 
909
  
 
910
  Implicit Arguments Leaf [A].
 
911
 
 
912
  Fixpoint xmap2_l (m : t A) {struct m} : t C :=
 
913
      match m with
 
914
      | Leaf => Leaf
 
915
      | Node l o r => Node (xmap2_l l) (f o None) (xmap2_l r)
 
916
      end.
 
917
 
 
918
  Lemma xgmap2_l : forall (i : positive) (m : t A),
 
919
          f None None = None -> find i (xmap2_l m) = f (find i m) None.
 
920
    Proof.
 
921
      induction i; intros; destruct m; simpl; auto.
 
922
    Qed.
 
923
 
 
924
  Fixpoint xmap2_r (m : t B) {struct m} : t C :=
 
925
      match m with
 
926
      | Leaf => Leaf
 
927
      | Node l o r => Node (xmap2_r l) (f None o) (xmap2_r r)
 
928
      end.
 
929
 
 
930
  Lemma xgmap2_r : forall (i : positive) (m : t B),
 
931
          f None None = None -> find i (xmap2_r m) = f None (find i m).
 
932
    Proof.
 
933
      induction i; intros; destruct m; simpl; auto.
 
934
    Qed.
 
935
 
 
936
  Fixpoint _map2 (m1 : t A)(m2 : t B) {struct m1} : t C :=
 
937
    match m1 with
 
938
    | Leaf => xmap2_r m2
 
939
    | Node l1 o1 r1 =>
 
940
        match m2 with
 
941
        | Leaf => xmap2_l m1
 
942
        | Node l2 o2 r2 => Node (_map2 l1 l2) (f o1 o2) (_map2 r1 r2)
 
943
        end
 
944
    end.
 
945
 
 
946
    Lemma gmap2: forall (i: positive)(m1:t A)(m2: t B),
 
947
      f None None = None ->
 
948
      find i (_map2 m1 m2) = f (find i m1) (find i m2).
 
949
    Proof.
 
950
      induction i; intros; destruct m1; destruct m2; simpl; auto;
 
951
      try apply xgmap2_r; try apply xgmap2_l; auto.
 
952
    Qed.
 
953
 
 
954
  End map2.
 
955
 
 
956
  Definition map2 (elt elt' elt'':Type)(f:option elt->option elt'->option elt'') := 
 
957
   _map2 (fun o1 o2 => match o1,o2 with None,None => None | _, _ => f o1 o2 end).
 
958
 
 
959
  Lemma map2_1 : forall (elt elt' elt'':Type)(m: t elt)(m': t elt')
 
960
    (x:key)(f:option elt->option elt'->option elt''), 
 
961
    In x m \/ In x m' -> 
 
962
    find x (map2 f m m') = f (find x m) (find x m'). 
 
963
  Proof. 
 
964
  intros.
 
965
  unfold map2.
 
966
  rewrite gmap2; auto.
 
967
  generalize (@mem_1 _ m x) (@mem_1 _ m' x).
 
968
  do 2 rewrite mem_find.
 
969
  destruct (find x m); simpl; auto.
 
970
  destruct (find x m'); simpl; auto.
 
971
  intros.
 
972
  destruct H; intuition; try discriminate.
 
973
  Qed.
 
974
 
 
975
  Lemma  map2_2 : forall (elt elt' elt'':Type)(m: t elt)(m': t elt')
 
976
    (x:key)(f:option elt->option elt'->option elt''), 
 
977
    In x (map2 f m m') -> In x m \/ In x m'.
 
978
  Proof.
 
979
  intros.
 
980
  generalize (mem_1 H); clear H; intros.
 
981
  rewrite mem_find in H.
 
982
  unfold map2 in H.
 
983
  rewrite gmap2 in H; auto.
 
984
  generalize (@mem_2 _ m x) (@mem_2 _ m' x).
 
985
  do 2 rewrite mem_find.
 
986
  destruct (find x m); simpl in *; auto.
 
987
  destruct (find x m'); simpl in *; auto.
 
988
  Qed.
 
989
 
 
990
 
 
991
  Section Fold.
 
992
 
 
993
    Variables A B : Type.
 
994
    Variable f : positive -> A -> B -> B.
 
995
 
 
996
    Fixpoint xfoldi (m : t A) (v : B) (i : positive) :=
 
997
      match m with
 
998
        | Leaf => v
 
999
        | Node l (Some x) r =>
 
1000
          xfoldi r (f i x (xfoldi l v (append i 2))) (append i 3)
 
1001
        | Node l None r =>
 
1002
          xfoldi r (xfoldi l v (append i 2)) (append i 3)
 
1003
      end.
 
1004
 
 
1005
    Lemma xfoldi_1 :
 
1006
      forall m v i,
 
1007
      xfoldi m v i = fold_left (fun a p => f (fst p) (snd p) a) (xelements m i) v.
 
1008
    Proof.
 
1009
      set (F := fun a p => f (fst p) (snd p) a).
 
1010
      induction m; intros; simpl; auto.
 
1011
      destruct o.
 
1012
      rewrite fold_left_app; simpl.
 
1013
      rewrite <- IHm1.
 
1014
      rewrite <- IHm2.
 
1015
      unfold F; simpl; reflexivity.
 
1016
      rewrite fold_left_app; simpl.
 
1017
      rewrite <- IHm1.
 
1018
      rewrite <- IHm2.
 
1019
      reflexivity.
 
1020
    Qed.
 
1021
 
 
1022
    Definition fold m i := xfoldi m i 1.
 
1023
 
 
1024
  End Fold.
 
1025
 
 
1026
  Lemma fold_1 :
 
1027
    forall (A:Type)(m:t A)(B:Type)(i : B) (f : key -> A -> B -> B),
 
1028
    fold f m i = fold_left (fun a p => f (fst p) (snd p) a) (elements m) i.
 
1029
  Proof.
 
1030
    intros; unfold fold, elements.
 
1031
    rewrite xfoldi_1; reflexivity.
 
1032
  Qed.
 
1033
 
 
1034
  Fixpoint equal (A:Type)(cmp : A -> A -> bool)(m1 m2 : t A) {struct m1} : bool := 
 
1035
    match m1, m2 with 
 
1036
      | Leaf, _ => is_empty m2
 
1037
      | _, Leaf => is_empty m1
 
1038
      | Node l1 o1 r1, Node l2 o2 r2 => 
 
1039
           (match o1, o2 with 
 
1040
             | None, None => true
 
1041
             | Some v1, Some v2 => cmp v1 v2
 
1042
             | _, _ => false
 
1043
            end)
 
1044
           && equal cmp l1 l2 && equal cmp r1 r2
 
1045
     end.
 
1046
 
 
1047
  Definition Equal (A:Type)(m m':t A) := 
 
1048
    forall y, find y m = find y m'.
 
1049
  Definition Equiv (A:Type)(eq_elt:A->A->Prop) m m' := 
 
1050
    (forall k, In k m <-> In k m') /\ 
 
1051
    (forall k e e', MapsTo k e m -> MapsTo k e' m' -> eq_elt e e').  
 
1052
  Definition Equivb (A:Type)(cmp: A->A->bool) := Equiv (Cmp cmp).
 
1053
 
 
1054
  Lemma equal_1 : forall (A:Type)(m m':t A)(cmp:A->A->bool), 
 
1055
    Equivb cmp m m' -> equal cmp m m' = true. 
 
1056
  Proof. 
 
1057
  induction m.
 
1058
  (* m = Leaf *)
 
1059
  destruct 1. 
 
1060
  simpl.
 
1061
  apply is_empty_1.
 
1062
  red; red; intros.
 
1063
  assert (In a (Leaf A)).
 
1064
  rewrite H.
 
1065
  exists e; auto.
 
1066
  destruct H2; red in H2.
 
1067
  destruct a; simpl in *; discriminate.
 
1068
  (* m = Node *)
 
1069
  destruct m'.
 
1070
  (* m' = Leaf *)
 
1071
  destruct 1. 
 
1072
  simpl.
 
1073
  destruct o.
 
1074
  assert (In xH (Leaf A)).
 
1075
  rewrite <- H.
 
1076
  exists a; red; auto.
 
1077
  destruct H1; red in H1; simpl in H1; discriminate.
 
1078
  apply andb_true_intro; split; apply is_empty_1; red; red; intros.
 
1079
  assert (In (xO a) (Leaf A)).
 
1080
  rewrite <- H.
 
1081
  exists e; auto.
 
1082
  destruct H2; red in H2; simpl in H2; discriminate.
 
1083
  assert (In (xI a) (Leaf A)).
 
1084
  rewrite <- H.
 
1085
  exists e; auto.
 
1086
  destruct H2; red in H2; simpl in H2; discriminate.
 
1087
  (* m' = Node *)
 
1088
  destruct 1.
 
1089
  assert (Equivb cmp m1 m'1).
 
1090
    split.
 
1091
    intros k; generalize (H (xO k)); unfold In, MapsTo; simpl; auto.
 
1092
    intros k e e'; generalize (H0 (xO k) e e'); unfold In, MapsTo; simpl; auto.
 
1093
  assert (Equivb cmp m2 m'2).
 
1094
    split.
 
1095
    intros k; generalize (H (xI k)); unfold In, MapsTo; simpl; auto.
 
1096
    intros k e e'; generalize (H0 (xI k) e e'); unfold In, MapsTo; simpl; auto.
 
1097
  simpl.
 
1098
  destruct o; destruct o0; simpl.
 
1099
  repeat (apply andb_true_intro; split); auto.
 
1100
  apply (H0 xH); red; auto.
 
1101
  generalize (H xH); unfold In, MapsTo; simpl; intuition.
 
1102
  destruct H4; try discriminate; eauto.
 
1103
  generalize (H xH); unfold In, MapsTo; simpl; intuition.
 
1104
  destruct H5; try discriminate; eauto.
 
1105
  apply andb_true_intro; split; auto.
 
1106
  Qed.
 
1107
 
 
1108
  Lemma equal_2 : forall (A:Type)(m m':t A)(cmp:A->A->bool), 
 
1109
    equal cmp m m' = true -> Equivb cmp m m'. 
 
1110
  Proof. 
 
1111
  induction m.
 
1112
  (* m = Leaf *)
 
1113
  simpl.
 
1114
  split; intros.
 
1115
  split.
 
1116
  destruct 1; red in H0; destruct k; discriminate.
 
1117
  destruct 1; elim (is_empty_2 H H0).
 
1118
  red in H0; destruct k; discriminate.
 
1119
  (* m = Node *)
 
1120
  destruct m'.
 
1121
  (* m' = Leaf *)
 
1122
  simpl.
 
1123
  destruct o; intros; try discriminate.
 
1124
  destruct (andb_prop _ _ H); clear H.
 
1125
  split; intros.
 
1126
  split; unfold In, MapsTo; destruct 1.
 
1127
  destruct k; simpl in *; try discriminate.
 
1128
  destruct (is_empty_2 H1 (find_2 _ _ H)).
 
1129
  destruct (is_empty_2 H0 (find_2 _ _ H)).
 
1130
  destruct k; simpl in *; discriminate.
 
1131
  unfold In, MapsTo; destruct k; simpl in *; discriminate.
 
1132
  (* m' = Node *)
 
1133
  destruct o; destruct o0; simpl; intros; try discriminate.
 
1134
  destruct (andb_prop _ _ H); clear H.
 
1135
  destruct (andb_prop _ _ H0); clear H0.
 
1136
  destruct (IHm1 _ _ H2); clear H2 IHm1.
 
1137
  destruct (IHm2 _ _ H1); clear H1 IHm2.
 
1138
  split; intros.
 
1139
  destruct k; unfold In, MapsTo in *; simpl; auto.
 
1140
  split; eauto.
 
1141
  destruct k; unfold In, MapsTo in *; simpl in *.
 
1142
  eapply H4; eauto.
 
1143
  eapply H3; eauto.
 
1144
  congruence.
 
1145
  destruct (andb_prop _ _ H); clear H.
 
1146
  destruct (IHm1 _ _ H0); clear H0 IHm1.
 
1147
  destruct (IHm2 _ _ H1); clear H1 IHm2.
 
1148
  split; intros.
 
1149
  destruct k; unfold In, MapsTo in *; simpl; auto.
 
1150
  split; eauto.
 
1151
  destruct k; unfold In, MapsTo in *; simpl in *.
 
1152
  eapply H3; eauto.
 
1153
  eapply H2; eauto.
 
1154
  try discriminate.
 
1155
  Qed.
 
1156
 
 
1157
End PositiveMap.
 
1158
 
 
1159
(** Here come some additionnal facts about this implementation.
 
1160
  Most are facts that cannot be derivable from the general interface. *)
 
1161
 
 
1162
 
 
1163
Module PositiveMapAdditionalFacts.
 
1164
  Import PositiveMap.
 
1165
 
 
1166
  (* Derivable from the Map interface *)
 
1167
  Theorem gsspec:
 
1168
    forall (A:Type)(i j: positive) (x: A) (m: t A),
 
1169
    find i (add j x m) = if E.eq_dec i j then Some x else find i m.
 
1170
  Proof.
 
1171
    intros.
 
1172
    destruct (E.eq_dec i j); [ rewrite e; apply gss | apply gso; auto ].
 
1173
  Qed.
 
1174
 
 
1175
   (* Not derivable from the Map interface *)
 
1176
  Theorem gsident:
 
1177
    forall (A:Type)(i: positive) (m: t A) (v: A),
 
1178
    find i m = Some v -> add i v m = m.
 
1179
  Proof.
 
1180
    induction i; intros; destruct m; simpl; simpl in H; try congruence.
 
1181
     rewrite (IHi m2 v H); congruence.
 
1182
     rewrite (IHi m1 v H); congruence.
 
1183
  Qed.
 
1184
  
 
1185
  Lemma xmap2_lr :
 
1186
      forall (A B : Type)(f g: option A -> option A -> option B)(m : t A),
 
1187
      (forall (i j : option A), f i j = g j i) ->
 
1188
      xmap2_l f m = xmap2_r g m.
 
1189
    Proof.
 
1190
      induction m; intros; simpl; auto.
 
1191
      rewrite IHm1; auto.
 
1192
      rewrite IHm2; auto.
 
1193
      rewrite H; auto.
 
1194
    Qed.
 
1195
 
 
1196
  Theorem map2_commut:
 
1197
    forall (A B: Type) (f g: option A -> option A -> option B),
 
1198
    (forall (i j: option A), f i j = g j i) ->
 
1199
    forall (m1 m2: t A),
 
1200
    _map2 f m1 m2 = _map2 g m2 m1.
 
1201
  Proof.
 
1202
    intros A B f g Eq1.
 
1203
    assert (Eq2: forall (i j: option A), g i j = f j i).
 
1204
      intros; auto.
 
1205
    induction m1; intros; destruct m2; simpl;
 
1206
      try rewrite Eq1;
 
1207
      repeat rewrite (xmap2_lr f g);
 
1208
      repeat rewrite (xmap2_lr g f);
 
1209
      auto.
 
1210
     rewrite IHm1_1.
 
1211
     rewrite IHm1_2.
 
1212
     auto. 
 
1213
  Qed.
 
1214
 
 
1215
End PositiveMapAdditionalFacts.
 
1216