pmap.v 16.3 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
(* Copyright (c) 2012-2015, Robbert Krebbers. *)
2 3 4 5 6 7 8 9
(* This file is distributed under the terms of the BSD license. *)
(** This files implements an efficient implementation of finite maps whose keys
range over Coq's data type of positive binary naturals [positive]. The
implementation is based on Xavier Leroy's implementation of radix-2 search
trees (uncompressed Patricia trees) and guarantees logarithmic-time operations.
However, we extend Leroy's implementation by packing the trees into a Sigma
type such that canonicity of representation is ensured. This is necesarry for
Leibniz equality to become extensional. *)
10
Require Import PArith mapset.
11
Require Export fin_maps.
Robbert Krebbers's avatar
Robbert Krebbers committed
12 13 14 15 16

Local Open Scope positive_scope.
Local Hint Extern 0 (@eq positive _ _) => congruence.
Local Hint Extern 0 (¬@eq positive _ _) => congruence.

17 18 19 20 21
(** * The tree data structure *)
(** The data type [Pmap_raw] specifies radix-2 search trees. These trees do
not ensure canonical representations of maps. For example the empty map can
be represented as a binary tree of an arbitrary size that contains [None] at
all nodes. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
22
Inductive Pmap_raw A :=
23 24 25 26
  | PLeaf: Pmap_raw A
  | PNode: Pmap_raw A  option A  Pmap_raw A  Pmap_raw A.
Arguments PLeaf {_}.
Arguments PNode {_} _ _ _.
Robbert Krebbers's avatar
Robbert Krebbers committed
27

28 29
Instance Pmap_raw_eq_dec `{ x y : A, Decision (x = y)} (x y : Pmap_raw A) :
  Decision (x = y).
Robbert Krebbers's avatar
Robbert Krebbers committed
30 31
Proof. solve_decision. Defined.

32
(** The following decidable predicate describes non empty trees. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
33
Inductive Pmap_ne {A} : Pmap_raw A  Prop :=
34 35 36
  | Pmap_ne_val l x r : Pmap_ne (PNode l (Some x) r)
  | Pmap_ne_l l r : Pmap_ne l  Pmap_ne (PNode l None r)
  | Pmap_ne_r l r : Pmap_ne r  Pmap_ne (PNode l None r).
Robbert Krebbers's avatar
Robbert Krebbers committed
37 38
Local Hint Constructors Pmap_ne.

39
Instance Pmap_ne_dec {A} :  t : Pmap_raw A, Decision (Pmap_ne t).
Robbert Krebbers's avatar
Robbert Krebbers committed
40
Proof.
41 42 43 44 45 46 47 48
 refine (
  fix go t :=
  match t return Decision (Pmap_ne t) with
  | PLeaf => right _
  | PNode _ (Some x) _ => left _
  | PNode l Node r => cast_if_or (go l) (go r)
  end); clear go; abstract first [constructor (by auto)|by inversion 1].
Defined.
Robbert Krebbers's avatar
Robbert Krebbers committed
49

50 51
(** The following predicate describes well well formed trees. A tree is well
formed if it is empty or if all nodes at the bottom contain a value. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
52
Inductive Pmap_wf {A} : Pmap_raw A  Prop :=
53 54
  | Pmap_wf_leaf : Pmap_wf PLeaf
  | Pmap_wf_node l x r : Pmap_wf l  Pmap_wf r  Pmap_wf (PNode l (Some x) r)
55
  | Pmap_wf_empty l r :
56
     Pmap_wf l  Pmap_wf r  (Pmap_ne l  Pmap_ne r)  Pmap_wf (PNode l None r).
Robbert Krebbers's avatar
Robbert Krebbers committed
57 58
Local Hint Constructors Pmap_wf.

59
Instance Pmap_wf_dec {A} :  t : Pmap_raw A, Decision (Pmap_wf t).
Robbert Krebbers's avatar
Robbert Krebbers committed
60
Proof.
61 62 63 64 65 66 67 68 69
 refine (
  fix go t :=
  match t return Decision (Pmap_wf t) with
  | PLeaf => left _
  | PNode l (Some x) r => cast_if_and (go l) (go r)
  | PNode l Node r =>
     cast_if_and3 (decide (Pmap_ne l  Pmap_ne r)) (go l) (go r)
  end); clear go; abstract first [constructor (by auto)|by inversion 1].
Defined.
Robbert Krebbers's avatar
Robbert Krebbers committed
70

71 72
(** Now we restrict the data type of trees to those that are well formed and
thereby obtain a data type that ensures canonicity. *)
73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88
Inductive Pmap A := PMap {
  pmap_car : Pmap_raw A;
  pmap_bool_prf : bool_decide (Pmap_wf pmap_car)
}.
Arguments PMap {_} _ _.
Arguments pmap_car {_} _.
Arguments pmap_bool_prf {_} _.
Definition PMap' {A} (t : Pmap_raw A) (p : Pmap_wf t) : Pmap A :=
  PMap t (bool_decide_pack _ p).
Definition pmap_prf {A} (m : Pmap A) : Pmap_wf (pmap_car m) :=
  bool_decide_unpack _ (pmap_bool_prf m).
Lemma Pmap_eq {A} (m1 m2 : Pmap A) : m1 = m2  pmap_car m1 = pmap_car m2.
Proof.
  split; [by intros ->|intros]; destruct m1 as [t1 ?], m2 as [t2 ?].
  simplify_equality'; f_equal; apply proof_irrel.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
89

90
(** * Operations on the data structure *)
91 92 93 94 95
Global Instance Pmap_eq_dec `{ x y : A, Decision (x = y)}
    (m1 m2 : Pmap A) : Decision (m1 = m2) :=
  match Pmap_raw_eq_dec (pmap_car m1) (pmap_car m2) with
  | left H => left (proj2 (Pmap_eq m1 m2) H)
  | right H => right (H  proj1 (Pmap_eq m1 m2))
Robbert Krebbers's avatar
Robbert Krebbers committed
96
  end.
97
Instance Pempty_raw {A} : Empty (Pmap_raw A) := PLeaf.
98
Global Instance Pempty {A} : Empty (Pmap A) := PMap'  Pmap_wf_leaf.
Robbert Krebbers's avatar
Robbert Krebbers committed
99

Robbert Krebbers's avatar
Robbert Krebbers committed
100
Instance Plookup_raw {A} : Lookup positive A (Pmap_raw A) :=
101
  fix go (i : positive) (t : Pmap_raw A) {struct t} : option A :=
Robbert Krebbers's avatar
Robbert Krebbers committed
102
  match t with
103 104
  | PLeaf => None
  | PNode l o r =>
Robbert Krebbers's avatar
Robbert Krebbers committed
105
     match i with
106
     | 1 => o | i~0 => @lookup _ _ _ go i l | i~1 => @lookup _ _ _ go i r
Robbert Krebbers's avatar
Robbert Krebbers committed
107
     end
Robbert Krebbers's avatar
Robbert Krebbers committed
108
  end.
109
Instance Plookup {A} : Lookup positive A (Pmap A) := λ i m, pmap_car m !! i.
Robbert Krebbers's avatar
Robbert Krebbers committed
110

111
Lemma Plookup_empty {A} i : ( : Pmap_raw A) !! i = None.
112
Proof. by destruct i. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
113

114
Lemma Pmap_ne_lookup {A} (t : Pmap_raw A) : Pmap_ne t   i x, t !! i = Some x.
Robbert Krebbers's avatar
Robbert Krebbers committed
115 116
Proof.
  induction 1 as [? x ?| l r ? IHl | l r ? IHr].
117 118 119
  * intros. by exists 1 x.
  * destruct IHl as [i [x ?]]. by exists (i~0) x.
  * destruct IHr as [i [x ?]]. by exists (i~1) x.
Robbert Krebbers's avatar
Robbert Krebbers committed
120 121 122 123 124
Qed.

Lemma Pmap_wf_eq_get {A} (t1 t2 : Pmap_raw A) :
  Pmap_wf t1  Pmap_wf t2  ( i, t1 !! i = t2 !! i)  t1 = t2.
Proof.
125
  intros t1wf. revert t2.
126
  induction t1wf as [| ? x ? ? IHl ? IHr | l r ? IHl ? IHr Hne1].
127
  * destruct 1 as [| | ???? [?|?]]; intros Hget.
128
    + done.
129
    + discriminate (Hget 1).
130
    + destruct (Pmap_ne_lookup l) as [i [??]]; trivial.
131
      specialize (Hget (i~0)). simpl in *. congruence.
132
    + destruct (Pmap_ne_lookup r) as [i [??]]; trivial.
133 134 135 136
      specialize (Hget (i~1)). simpl in *. congruence.
  * destruct 1; intros Hget.
    + discriminate (Hget xH).
    + f_equal.
137 138 139
      - apply IHl; trivial. intros i. apply (Hget (i~0)).
      - apply (Hget 1).
      - apply IHr; trivial. intros i. apply (Hget (i~1)).
140 141 142
    + specialize (Hget 1). simpl in *. congruence.
  * destruct 1; intros Hget.
    + destruct Hne1.
143 144
      - destruct (Pmap_ne_lookup l) as [i [??]]; trivial.
        specialize (Hget (i~0)); simpl in *. congruence.
145
      - destruct (Pmap_ne_lookup r) as [i [??]]; trivial.
146 147
        specialize (Hget (i~1)); simpl in *. congruence.
    + specialize (Hget 1); simpl in *. congruence.
148
    + f_equal.
149 150
      - apply IHl; trivial. intros i. apply (Hget (i~0)).
      - apply IHr; trivial. intros i. apply (Hget (i~1)).
Robbert Krebbers's avatar
Robbert Krebbers committed
151 152 153 154
Qed.

Fixpoint Psingleton_raw {A} (i : positive) (x : A) : Pmap_raw A :=
  match i with
155 156 157
  | 1 => PNode PLeaf (Some x) PLeaf
  | i~0 => PNode (Psingleton_raw i x) None PLeaf
  | i~1 => PNode PLeaf None (Psingleton_raw i x)
Robbert Krebbers's avatar
Robbert Krebbers committed
158
  end.
159
Lemma Psingleton_ne {A} i (x : A) : Pmap_ne (Psingleton_raw i x).
Robbert Krebbers's avatar
Robbert Krebbers committed
160
Proof. induction i; simpl; intuition. Qed.
161 162
Local Hint Resolve Psingleton_ne.
Lemma Psingleton_wf {A} i (x : A) : Pmap_wf (Psingleton_raw i x).
Robbert Krebbers's avatar
Robbert Krebbers committed
163
Proof. induction i; simpl; intuition. Qed.
164 165
Local Hint Resolve Psingleton_wf.
Lemma Plookup_singleton {A} i (x : A) : Psingleton_raw i x !! i = Some x.
166
Proof. by induction i. Qed.
167
Lemma Plookup_singleton_ne {A} i j (x : A) :
168
  i  j  Psingleton_raw i x !! j = None.
Robbert Krebbers's avatar
Robbert Krebbers committed
169 170
Proof. revert j. induction i; intros [?|?|]; simpl; auto. congruence. Qed.

171 172 173
Definition PNode_canon {A} (l : Pmap_raw A) (o : option A) (r : Pmap_raw A) :=
  match l, o, r with PLeaf, None, PLeaf => PLeaf | _, _, _ => PNode l o r end.
Lemma PNode_canon_wf {A} (l : Pmap_raw A) (o : option A) (r : Pmap_raw A) :
174
  Pmap_wf l  Pmap_wf r  Pmap_wf (PNode_canon l o r).
Robbert Krebbers's avatar
Robbert Krebbers committed
175
Proof. intros H1 H2. destruct H1, o, H2; simpl; intuition. Qed.
176
Local Hint Resolve PNode_canon_wf.
177
Lemma PNode_canon_lookup_xH {A} (l : Pmap_raw A) o (r : Pmap_raw A) :
178
  PNode_canon l o r !! 1 = o.
179
Proof. by destruct l,o,r. Qed.
180
Lemma PNode_canon_lookup_xO {A} (l : Pmap_raw A) o (r : Pmap_raw A) i :
181
  PNode_canon l o r !! i~0 = l !! i.
182
Proof. by destruct l,o,r. Qed.
183
Lemma PNode_canon_lookup_xI {A} (l : Pmap_raw A) o (r : Pmap_raw A) i :
184
  PNode_canon l o r !! i~1 = r !! i.
185
Proof. by destruct l,o,r. Qed.
186 187 188
Ltac PNode_canon_rewrite := repeat first
  [ rewrite PNode_canon_lookup_xH | rewrite PNode_canon_lookup_xO
  | rewrite PNode_canon_lookup_xI].
Robbert Krebbers's avatar
Robbert Krebbers committed
189

Robbert Krebbers's avatar
Robbert Krebbers committed
190
Instance Ppartial_alter_raw {A} : PartialAlter positive A (Pmap_raw A) :=
191
  fix go f i t {struct t} : Pmap_raw A :=
Robbert Krebbers's avatar
Robbert Krebbers committed
192
  match t with
193
  | PLeaf => match f None with None => PLeaf | Some x => Psingleton_raw i x end
194
  | PNode l o r =>
Robbert Krebbers's avatar
Robbert Krebbers committed
195
     match i with
196 197 198
     | 1 => PNode_canon l (f o) r
     | i~0 => PNode_canon (@partial_alter _ _ _ go f i l) o r
     | i~1 => PNode_canon l o (@partial_alter _ _ _ go f i r)
Robbert Krebbers's avatar
Robbert Krebbers committed
199
     end
Robbert Krebbers's avatar
Robbert Krebbers committed
200
  end.
201
Lemma Ppartial_alter_wf {A} f i (t : Pmap_raw A) :
202
  Pmap_wf t  Pmap_wf (partial_alter f i t).
Robbert Krebbers's avatar
Robbert Krebbers committed
203 204
Proof.
  intros twf. revert i. induction twf.
205 206 207
  * unfold partial_alter. simpl. case (f None); intuition.
  * intros [?|?|]; simpl; intuition.
  * intros [?|?|]; simpl; intuition.
Robbert Krebbers's avatar
Robbert Krebbers committed
208
Qed.
209 210
Instance Ppartial_alter {A} : PartialAlter positive A (Pmap A) := λ f i m,
  PMap' (partial_alter f i (pmap_car m)) (Ppartial_alter_wf f i _ (pmap_prf m)).
211
Lemma Plookup_alter {A} f i (t : Pmap_raw A) :
212
  partial_alter f i t !! i = f (t !! i).
Robbert Krebbers's avatar
Robbert Krebbers committed
213 214
Proof.
  revert i. induction t.
215 216
  * intros i. change (match f None with Some x => Psingleton_raw i x
      | None => PLeaf end !! i = f None); destruct (f None).
217
    + intros. apply Plookup_singleton.
218
    + by destruct i.
219
  * intros [?|?|]; simpl; by PNode_canon_rewrite.
Robbert Krebbers's avatar
Robbert Krebbers committed
220
Qed.
221
Lemma Plookup_alter_ne {A} f i j (t : Pmap_raw A) :
222
  i  j  partial_alter f i t !! j = t !! j.
Robbert Krebbers's avatar
Robbert Krebbers committed
223 224
Proof.
  revert i j. induction t as [|l IHl ? r IHr].
225 226 227
  * intros. change (match f None with Some x => Psingleton_raw i x
      | None => PLeaf end !! j = None); destruct (f None); [|done].
    intros. by apply Plookup_singleton_ne.
228
  * intros [?|?|] [?|?|]; simpl; PNode_canon_rewrite; auto; congruence.
Robbert Krebbers's avatar
Robbert Krebbers committed
229 230
Qed.

231 232
Instance Pfmap_raw : FMap Pmap_raw := λ A B f,
  fix go t :=
Robbert Krebbers's avatar
Robbert Krebbers committed
233
  match t with
234
  | PLeaf => PLeaf | PNode l x r => PNode (go l) (f <$> x) (go r)
Robbert Krebbers's avatar
Robbert Krebbers committed
235
  end.
236
Lemma Pfmap_ne `(f : A  B) (t : Pmap_raw A) : Pmap_ne t  Pmap_ne (fmap f t).
237
Proof. induction 1; csimpl; auto. Qed.
238 239
Local Hint Resolve Pfmap_ne.
Lemma Pfmap_wf `(f : A  B) (t : Pmap_raw A) : Pmap_wf t  Pmap_wf (fmap f t).
240 241 242
Proof. induction 1; csimpl; intuition. Qed.
Global Instance Pfmap : FMap Pmap := λ A B f m,
  PMap' (f <$> pmap_car m) (Pfmap_wf f _ (pmap_prf m)).
243
Lemma Plookup_fmap {A B} (f : A  B) (t : Pmap_raw A) i :
244
  (f <$> t) !! i = f <$> t !! i.
245
Proof. revert i. induction t. done. by intros [?|?|]; simpl. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
246

247
Fixpoint Pto_list_raw {A} (j : positive) (t : Pmap_raw A)
248
    (acc : list (positive * A)) : list (positive * A) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
249
  match t with
250 251 252
  | PLeaf => acc
  | PNode l o r => default [] o (λ x, [(Preverse j, x)]) ++
     Pto_list_raw (j~0) l (Pto_list_raw (j~1) r acc)
253
  end%list.
254 255 256
Lemma Pelem_of_to_list {A} (t : Pmap_raw A) j i acc x :
  (i,x)  Pto_list_raw j t acc 
    ( i', i = i' ++ Preverse j  t !! i' = Some x)  (i,x)  acc.
Robbert Krebbers's avatar
Robbert Krebbers committed
257 258
Proof.
  split.
259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289
  { revert j acc. induction t as [|l IHl [y|] r IHr]; intros j acc; simpl.
    * by right.
    * rewrite elem_of_cons. intros [?|?]; simplify_equality.
      { left; exists 1. by rewrite (left_id_L 1 (++))%positive. }
      destruct (IHl (j~0) (Pto_list_raw j~1 r acc)) as [(i'&->&?)|?]; auto.
      { left; exists (i' ~ 0). by rewrite Preverse_xO, (associative_L _). }
      destruct (IHr (j~1) acc) as [(i'&->&?)|?]; auto.
      left; exists (i' ~ 1). by rewrite Preverse_xI, (associative_L _).
    * intros.
      destruct (IHl (j~0) (Pto_list_raw j~1 r acc)) as [(i'&->&?)|?]; auto.
      { left; exists (i' ~ 0). by rewrite Preverse_xO, (associative_L _). }
      destruct (IHr (j~1) acc) as [(i'&->&?)|?]; auto.
      left; exists (i' ~ 1). by rewrite Preverse_xI, (associative_L _). }
  revert t j i acc. assert ( t j i acc,
    (i, x)  acc  (i, x)  Pto_list_raw j t acc) as help.
  { intros t; induction t as [|l IHl [y|] r IHr]; intros j i acc;
      simpl; rewrite ?elem_of_cons; auto. }
  intros t j ? acc [(i&->&Hi)|?]; [|by auto]. revert j i acc Hi.
  induction t as [|l IHl [y|] r IHr]; intros j i acc ?; simpl.
  * done.
  * rewrite elem_of_cons. destruct i as [i|i|]; simplify_equality'.
    + right. apply help. specialize (IHr (j~1) i).
      rewrite Preverse_xI, (associative_L _) in IHr. by apply IHr.
    + right. specialize (IHl (j~0) i).
      rewrite Preverse_xO, (associative_L _) in IHl. by apply IHl.
    + left. by rewrite (left_id_L 1 (++))%positive.
  * destruct i as [i|i|]; simplify_equality'.
    + apply help. specialize (IHr (j~1) i).
      rewrite Preverse_xI, (associative_L _) in IHr. by apply IHr.
    + specialize (IHl (j~0) i).
      rewrite Preverse_xO, (associative_L _) in IHl. by apply IHl.
290
Qed.
291 292 293
Lemma Pto_list_nodup {A} j (t : Pmap_raw A) acc :
  ( i x, (i ++ Preverse j, x)  acc  t !! i = None) 
  NoDup acc  NoDup (Pto_list_raw j t acc).
294
Proof.
295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319
  revert j acc. induction t as [|l IHl [y|] r IHr]; simpl; intros j acc Hin ?.
  * done.
  * repeat constructor.
    { rewrite Pelem_of_to_list. intros [(i&Hi&?)|Hj].
      { apply (f_equal Plength) in Hi.
        rewrite Preverse_xO, !Papp_length in Hi; simpl in *; lia. }
      rewrite Pelem_of_to_list in Hj. destruct Hj as [(i&Hi&?)|Hj].
      { apply (f_equal Plength) in Hi.
        rewrite Preverse_xI, !Papp_length in Hi; simpl in *; lia. }
      specialize (Hin 1 y). rewrite (left_id_L 1 (++))%positive in Hin.
      discriminate (Hin Hj). }
   apply IHl.
   { intros i x. rewrite Pelem_of_to_list. intros [(?&Hi&?)|Hi].
     + rewrite Preverse_xO, Preverse_xI, !(associative_L _) in Hi.
       by apply (injective (++ _)) in Hi.
     + apply (Hin (i~0) x). by rewrite Preverse_xO, (associative_L _) in Hi. }
   apply IHr; auto. intros i x Hi.
   apply (Hin (i~1) x). by rewrite Preverse_xI, (associative_L _) in Hi.
 * apply IHl.
   { intros i x. rewrite Pelem_of_to_list. intros [(?&Hi&?)|Hi].
     + rewrite Preverse_xO, Preverse_xI, !(associative_L _) in Hi.
       by apply (injective (++ _)) in Hi.
     + apply (Hin (i~0) x). by rewrite Preverse_xO, (associative_L _) in Hi. }
   apply IHr; auto. intros i x Hi.
   apply (Hin (i~1) x). by rewrite Preverse_xI, (associative_L _) in Hi.
320
Qed.
321 322
Global Instance Pto_list {A} : FinMapToList positive A (Pmap A) := λ m,
  Pto_list_raw 1 (pmap_car m) [].
Robbert Krebbers's avatar
Robbert Krebbers committed
323

324 325
Instance Pomap_raw : OMap Pmap_raw := λ A B f,
  fix go t :=
Robbert Krebbers's avatar
Robbert Krebbers committed
326
  match t with
327
  | PLeaf => PLeaf | PNode l o r => PNode_canon (go l) (o = f) (go r)
Robbert Krebbers's avatar
Robbert Krebbers committed
328
  end.
329 330
Lemma Pomap_wf {A B} (f : A  option B) (t : Pmap_raw A) :
  Pmap_wf t  Pmap_wf (omap f t).
331
Proof. induction 1; csimpl; auto. Qed.
332 333 334
Local Hint Resolve Pomap_wf.
Lemma Pomap_lookup {A B} (f : A  option B) (t : Pmap_raw A) i :
  omap f t !! i = t !! i = f.
Robbert Krebbers's avatar
Robbert Krebbers committed
335
Proof.
336
  revert i. induction t as [| l IHl o r IHr ]; [done |].
337
  intros [?|?|]; csimpl; PNode_canon_rewrite; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
338
Qed.
339 340
Global Instance Pomap: OMap Pmap := λ A B f m,
  PMap' (omap f (pmap_car m)) (Pomap_wf f _ (pmap_prf m)).
Robbert Krebbers's avatar
Robbert Krebbers committed
341

342
Instance Pmerge_raw : Merge Pmap_raw :=
343
  fix Pmerge_raw A B C f t1 t2 : Pmap_raw C :=
Robbert Krebbers's avatar
Robbert Krebbers committed
344
  match t1, t2 with
345 346
  | PLeaf, t2 => omap (f None  Some) t2
  | t1, PLeaf => omap (flip f None  Some) t1
347 348
  | PNode l1 o1 r1, PNode l2 o2 r2 =>
     PNode_canon (@merge _ Pmerge_raw A B C f l1 l2)
349
      (f o1 o2) (@merge _ Pmerge_raw A B C f r1 r2)
Robbert Krebbers's avatar
Robbert Krebbers committed
350
  end.
351
Local Arguments omap _ _ _ _ _ _ : simpl never.
352
Lemma Pmerge_wf {A B C} (f : option A  option B  option C) t1 t2 :
353
  Pmap_wf t1  Pmap_wf t2  Pmap_wf (merge f t1 t2).
Robbert Krebbers's avatar
Robbert Krebbers committed
354
Proof. intros t1wf. revert t2. induction t1wf; destruct 1; simpl; auto. Qed.
355 356
Global Instance Pmerge: Merge Pmap := λ A B C f m1 m2,
  PMap' _ (Pmerge_wf f _ _ (pmap_prf m1) (pmap_prf m2)).
357
Lemma Pmerge_spec {A B C} (f : option A  option B  option C)
358
    (Hf : f None None = None) (t1 : Pmap_raw A) t2 i :
Robbert Krebbers's avatar
Robbert Krebbers committed
359 360
  merge f t1 t2 !! i = f (t1 !! i) (t2 !! i).
Proof.
361 362 363 364 365 366
  revert t2 i. induction t1 as [|l1 IHl1 o1 r1 IHr1]; intros t2 i.
  { unfold merge; simpl. rewrite Pomap_lookup. by destruct (t2 !! i). }
  destruct t2 as [|l2 o2 r2].
  * unfold merge, Pmerge_raw. rewrite Pomap_lookup.
    by destruct (PNode _ _ _ !! i).
  * destruct i; simpl; by PNode_canon_rewrite.
Robbert Krebbers's avatar
Robbert Krebbers committed
367 368
Qed.

369
(** * Instantiation of the finite map interface *)
Robbert Krebbers's avatar
Robbert Krebbers committed
370 371 372
Global Instance: FinMap positive Pmap.
Proof.
  split.
373
  * intros ? [t1 ?] [t2 ?] ?. apply Pmap_eq; simpl.
374
    apply Pmap_wf_eq_get; trivial; by apply (bool_decide_unpack _).
375
  * by intros ? [].
376 377 378
  * intros ?? [??] ?. by apply Plookup_alter.
  * intros ?? [??] ??. by apply Plookup_alter_ne.
  * intros ??? [??]. by apply Plookup_fmap.
379 380
  * intros ? [??]. apply Pto_list_nodup; [|constructor].
    intros ??. by rewrite elem_of_nil.
381 382 383
  * intros ? [??] i x; unfold map_to_list, Pto_list.
    rewrite Pelem_of_to_list, elem_of_nil.
    split. by intros [(?&->&?)|]. by left; exists i.
384
  * intros ?? ? [??] ?. by apply Pomap_lookup.
385
  * intros ??? ?? [??] [??] ?. by apply Pmerge_spec.
Robbert Krebbers's avatar
Robbert Krebbers committed
386
Qed.
387

388 389
(** * Finite sets *)
(** We construct sets of [positives]s satisfying extensional equality. *)
390
Notation Pset := (mapset (Pmap unit)).
391 392
Instance Pmap_dom {A} : Dom (Pmap A) Pset := mapset_dom.
Instance: FinMapDom positive Pmap Pset := mapset_dom_spec.