pmap.v 15.7 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
2
3
4
5
6
7
8
9
(* Copyright (c) 2012-2015, Robbert Krebbers. *)
(* 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
From Coq Require Import PArith.
11
From iris.prelude Require Import mapset countable.
12
From iris.prelude Require Export fin_maps.
Robbert Krebbers's avatar
Robbert Krebbers committed
13
14
15
16
17
18
19
20
21
22
23
24

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

(** * 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. *)
Inductive Pmap_raw (A : Type) : Type :=
  | PLeaf: Pmap_raw A
25
  | PNode: option A  Pmap_raw A  Pmap_raw A  Pmap_raw A.
Robbert Krebbers's avatar
Robbert Krebbers committed
26
27
28
Arguments PLeaf {_}.
Arguments PNode {_} _ _ _.

29
Instance Pmap_raw_eq_dec `{EqDecision A} : EqDecision (Pmap_raw A).
Robbert Krebbers's avatar
Robbert Krebbers committed
30
31
Proof. solve_decision. Defined.

32
33
34
35
36
Fixpoint Pmap_wf {A} (t : Pmap_raw A) : bool :=
  match t with
  | PLeaf => true
  | PNode None PLeaf PLeaf => false
  | PNode _ l r => Pmap_wf l && Pmap_wf r
Robbert Krebbers's avatar
Robbert Krebbers committed
37
  end.
38
39
40
41
42
43
44
45
46
47
48
49
50
Arguments Pmap_wf _ !_ / : simpl nomatch.
Lemma Pmap_wf_l {A} o (l r : Pmap_raw A) : Pmap_wf (PNode o l r)  Pmap_wf l.
Proof. destruct o, l, r; simpl; rewrite ?andb_True; tauto. Qed.
Lemma Pmap_wf_r {A} o (l r : Pmap_raw A) : Pmap_wf (PNode o l r)  Pmap_wf r.
Proof. destruct o, l, r; simpl; rewrite ?andb_True; tauto. Qed.
Local Hint Immediate Pmap_wf_l Pmap_wf_r.
Definition PNode' {A} (o : option A) (l r : Pmap_raw A) :=
  match l, o, r with PLeaf, None, PLeaf => PLeaf | _, _, _ => PNode o l r end.
Arguments PNode' _ _ _ _ : simpl never.
Lemma PNode_wf {A} o (l r : Pmap_raw A) :
  Pmap_wf l  Pmap_wf r  Pmap_wf (PNode' o l r).
Proof. destruct o, l, r; simpl; auto. Qed.
Local Hint Resolve PNode_wf.
Robbert Krebbers's avatar
Robbert Krebbers committed
51

52
53
(** Operations *)
Instance Pempty_raw {A} : Empty (Pmap_raw A) := PLeaf.
Robbert Krebbers's avatar
Robbert Krebbers committed
54
55
Instance Plookup_raw {A} : Lookup positive A (Pmap_raw A) :=
  fix go (i : positive) (t : Pmap_raw A) {struct t} : option A :=
56
  let _ : Lookup _ _ _ := @go in
Robbert Krebbers's avatar
Robbert Krebbers committed
57
58
  match t with
  | PLeaf => None
59
60
61
62
63
64
65
66
67
68
69
70
71
72
  | PNode o l r => match i with 1 => o | i~0 => l !! i | i~1 => r !! i end
  end.
Local Arguments lookup _ _ _ _ _ !_ / : simpl nomatch.
Fixpoint Psingleton_raw {A} (i : positive) (x : A) : Pmap_raw A :=
  match i with
  | 1 => PNode (Some x) PLeaf PLeaf
  | i~0 => PNode None (Psingleton_raw i x) PLeaf
  | i~1 => PNode None PLeaf (Psingleton_raw i x)
  end.
Fixpoint Ppartial_alter_raw {A} (f : option A  option A)
    (i : positive) (t : Pmap_raw A) {struct t} : Pmap_raw A :=
  match t with
  | PLeaf => match f None with None => PLeaf | Some x => Psingleton_raw i x end
  | PNode o l r =>
Robbert Krebbers's avatar
Robbert Krebbers committed
73
     match i with
74
75
76
     | 1 => PNode' (f o) l r
     | i~0 => PNode' o (Ppartial_alter_raw f i l) r
     | i~1 => PNode' o l (Ppartial_alter_raw f i r)
Robbert Krebbers's avatar
Robbert Krebbers committed
77
78
     end
  end.
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
Fixpoint Pfmap_raw {A B} (f : A  B) (t : Pmap_raw A) : Pmap_raw B :=
  match t with
  | PLeaf => PLeaf
  | PNode o l r => PNode (f <$> o) (Pfmap_raw f l) (Pfmap_raw f r)
  end.
Fixpoint Pto_list_raw {A} (j : positive) (t : Pmap_raw A)
    (acc : list (positive * A)) : list (positive * A) :=
  match t with
  | PLeaf => acc
  | PNode o l r => default [] o (λ x, [(Preverse j, x)]) ++
     Pto_list_raw (j~0) l (Pto_list_raw (j~1) r acc)
  end%list.
Fixpoint Pomap_raw {A B} (f : A  option B) (t : Pmap_raw A) : Pmap_raw B :=
  match t with
  | PLeaf => PLeaf
  | PNode o l r => PNode' (o = f) (Pomap_raw f l) (Pomap_raw f r)
  end.
Fixpoint Pmerge_raw {A B C} (f : option A  option B  option C)
    (t1 : Pmap_raw A) (t2 : Pmap_raw B) : Pmap_raw C :=
  match t1, t2 with
  | PLeaf, t2 => Pomap_raw (f None  Some) t2
  | t1, PLeaf => Pomap_raw (flip f None  Some) t1
  | PNode o1 l1 r1, PNode o2 l2 r2 =>
      PNode' (f o1 o2) (Pmerge_raw f l1 l2) (Pmerge_raw f r1 r2)
  end.
Robbert Krebbers's avatar
Robbert Krebbers committed
104

105
106
107
(** Proofs *)
Lemma Pmap_wf_canon {A} (t : Pmap_raw A) :
  ( i, t !! i = None)  Pmap_wf t  t = PLeaf.
Robbert Krebbers's avatar
Robbert Krebbers committed
108
Proof.
109
110
111
112
  induction t as [|o l IHl r IHr]; intros Ht ?; auto.
  assert (o = None) as -> by (apply (Ht 1)).
  assert (l = PLeaf) as -> by (apply IHl; try apply (λ i, Ht (i~0)); eauto).
  by assert (r = PLeaf) as -> by (apply IHr; try apply (λ i, Ht (i~1)); eauto).
Robbert Krebbers's avatar
Robbert Krebbers committed
113
Qed.
114
115
Lemma Pmap_wf_eq {A} (t1 t2 : Pmap_raw A) :
  ( i, t1 !! i = t2 !! i)  Pmap_wf t1  Pmap_wf t2  t1 = t2.
Robbert Krebbers's avatar
Robbert Krebbers committed
116
Proof.
117
118
  revert t2.
  induction t1 as [|o1 l1 IHl r1 IHr]; intros [|o2 l2 r2] Ht ??; simpl; auto.
119
120
121
  - discriminate (Pmap_wf_canon (PNode o2 l2 r2)); eauto.
  - discriminate (Pmap_wf_canon (PNode o1 l1 r1)); eauto.
  - f_equal; [apply (Ht 1)| |].
122
123
    + apply IHl; try apply (λ x, Ht (x~0)); eauto.
    + apply IHr; try apply (λ x, Ht (x~1)); eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
124
Qed.
125
126
127
Lemma PNode_lookup {A} o (l r : Pmap_raw A) i :
  PNode' o l r !! i = PNode o l r !! i.
Proof. by destruct i, o, l, r. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
128
129

Lemma Psingleton_wf {A} i (x : A) : Pmap_wf (Psingleton_raw i x).
130
131
132
133
134
Proof. induction i as [[]|[]|]; simpl; rewrite ?andb_true_r; auto. Qed.
Lemma Ppartial_alter_wf {A} f i (t : Pmap_raw A) :
  Pmap_wf t  Pmap_wf (Ppartial_alter_raw f i t).
Proof.
  revert i; induction t as [|o l IHl r IHr]; intros i ?; simpl.
135
136
  - destruct (f None); auto using Psingleton_wf.
  - destruct i; simpl; eauto.
137
138
139
140
141
142
143
144
145
146
147
148
149
Qed.
Lemma Pfmap_wf {A B} (f : A  B) t : Pmap_wf t  Pmap_wf (Pfmap_raw f t).
Proof.
  induction t as [|[x|] [] ? [] ?]; simpl in *; rewrite ?andb_True; intuition.
Qed.
Lemma Pomap_wf {A B} (f : A  option B) t : Pmap_wf t  Pmap_wf (Pomap_raw f t).
Proof. induction t; simpl; eauto. Qed.
Lemma Pmerge_wf {A B C} (f : option A  option B  option C) t1 t2 :
  Pmap_wf t1  Pmap_wf t2  Pmap_wf (Pmerge_raw f t1 t2).
Proof. revert t2. induction t1; intros []; simpl; eauto using Pomap_wf. Qed.

Lemma Plookup_empty {A} i : ( : Pmap_raw A) !! i = None.
Proof. by destruct i. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
150
151
152
153
Lemma Plookup_singleton {A} i (x : A) : Psingleton_raw i x !! i = Some x.
Proof. by induction i. Qed.
Lemma Plookup_singleton_ne {A} i j (x : A) :
  i  j  Psingleton_raw i x !! j = None.
154
Proof. revert j. induction i; intros [?|?|]; simpl; auto with congruence. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
155
Lemma Plookup_alter {A} f i (t : Pmap_raw A) :
156
  Ppartial_alter_raw f i t !! i = f (t !! i).
Robbert Krebbers's avatar
Robbert Krebbers committed
157
Proof.
158
  revert i; induction t as [|o l IHl r IHr]; intros i; simpl.
159
160
  - by destruct (f None); rewrite ?Plookup_singleton.
  - destruct i; simpl; rewrite PNode_lookup; simpl; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
161
162
Qed.
Lemma Plookup_alter_ne {A} f i j (t : Pmap_raw A) :
163
  i  j  Ppartial_alter_raw f i t !! j = t !! j.
Robbert Krebbers's avatar
Robbert Krebbers committed
164
Proof.
165
  revert i j; induction t as [|o l IHl r IHr]; simpl.
166
167
  - by intros; destruct (f None); rewrite ?Plookup_singleton_ne.
  - by intros [?|?|] [?|?|] ?; simpl; rewrite ?PNode_lookup; simpl; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
168
Qed.
169
170
Lemma Plookup_fmap {A B} (f : A  B) t i : (Pfmap_raw f t) !! i = f <$> t !! i.
Proof. revert i. by induction t; intros [?|?|]; simpl. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
171
172
173
174
175
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.
Proof.
  split.
176
  { revert j acc. induction t as [|[y|] l IHl r IHr]; intros j acc; simpl.
177
    - by right.
178
    - rewrite elem_of_cons. intros [?|?]; simplify_eq.
Robbert Krebbers's avatar
Robbert Krebbers committed
179
180
      { left; exists 1. by rewrite (left_id_L 1 (++))%positive. }
      destruct (IHl (j~0) (Pto_list_raw j~1 r acc)) as [(i'&->&?)|?]; auto.
181
      { left; exists (i' ~ 0). by rewrite Preverse_xO, (assoc_L _). }
Robbert Krebbers's avatar
Robbert Krebbers committed
182
      destruct (IHr (j~1) acc) as [(i'&->&?)|?]; auto.
183
      left; exists (i' ~ 1). by rewrite Preverse_xI, (assoc_L _).
184
    - intros.
Robbert Krebbers's avatar
Robbert Krebbers committed
185
      destruct (IHl (j~0) (Pto_list_raw j~1 r acc)) as [(i'&->&?)|?]; auto.
186
      { left; exists (i' ~ 0). by rewrite Preverse_xO, (assoc_L _). }
Robbert Krebbers's avatar
Robbert Krebbers committed
187
      destruct (IHr (j~1) acc) as [(i'&->&?)|?]; auto.
188
      left; exists (i' ~ 1). by rewrite Preverse_xI, (assoc_L _). }
Robbert Krebbers's avatar
Robbert Krebbers committed
189
190
  revert t j i acc. assert ( t j i acc,
    (i, x)  acc  (i, x)  Pto_list_raw j t acc) as help.
191
  { intros t; induction t as [|[y|] l IHl r IHr]; intros j i acc;
Robbert Krebbers's avatar
Robbert Krebbers committed
192
193
      simpl; rewrite ?elem_of_cons; auto. }
  intros t j ? acc [(i&->&Hi)|?]; [|by auto]. revert j i acc Hi.
194
  induction t as [|[y|] l IHl r IHr]; intros j i acc ?; simpl.
195
  - done.
196
  - rewrite elem_of_cons. destruct i as [i|i|]; simplify_eq/=.
Robbert Krebbers's avatar
Robbert Krebbers committed
197
    + right. apply help. specialize (IHr (j~1) i).
198
      rewrite Preverse_xI, (assoc_L _) in IHr. by apply IHr.
Robbert Krebbers's avatar
Robbert Krebbers committed
199
    + right. specialize (IHl (j~0) i).
200
      rewrite Preverse_xO, (assoc_L _) in IHl. by apply IHl.
Robbert Krebbers's avatar
Robbert Krebbers committed
201
    + left. by rewrite (left_id_L 1 (++))%positive.
202
  - destruct i as [i|i|]; simplify_eq/=.
Robbert Krebbers's avatar
Robbert Krebbers committed
203
    + apply help. specialize (IHr (j~1) i).
204
      rewrite Preverse_xI, (assoc_L _) in IHr. by apply IHr.
Robbert Krebbers's avatar
Robbert Krebbers committed
205
    + specialize (IHl (j~0) i).
206
      rewrite Preverse_xO, (assoc_L _) in IHl. by apply IHl.
Robbert Krebbers's avatar
Robbert Krebbers committed
207
208
209
210
211
Qed.
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).
Proof.
212
  revert j acc. induction t as [|[y|] l IHl r IHr]; simpl; intros j acc Hin ?.
213
214
  - done.
  - repeat constructor.
Robbert Krebbers's avatar
Robbert Krebbers committed
215
216
217
218
219
220
221
222
    { 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). }
223
224
225
226
227
228
229
230
231
232
233
234
235
236
    apply IHl.
    { intros i x. rewrite Pelem_of_to_list. intros [(?&Hi&?)|Hi].
      + rewrite Preverse_xO, Preverse_xI, !(assoc_L _) in Hi.
        by apply (inj (++ _)) in Hi.
      + apply (Hin (i~0) x). by rewrite Preverse_xO, (assoc_L _) in Hi. }
    apply IHr; auto. intros i x Hi.
    apply (Hin (i~1) x). by rewrite Preverse_xI, (assoc_L _) in Hi.
  - apply IHl.
    { intros i x. rewrite Pelem_of_to_list. intros [(?&Hi&?)|Hi].
      + rewrite Preverse_xO, Preverse_xI, !(assoc_L _) in Hi.
        by apply (inj (++ _)) in Hi.
      + apply (Hin (i~0) x). by rewrite Preverse_xO, (assoc_L _) in Hi. }
    apply IHr; auto. intros i x Hi.
    apply (Hin (i~1) x). by rewrite Preverse_xI, (assoc_L _) in Hi.
Robbert Krebbers's avatar
Robbert Krebbers committed
237
Qed.
238
239
Lemma Pomap_lookup {A B} (f : A  option B) t i :
  Pomap_raw f t !! i = t !! i = f.
Robbert Krebbers's avatar
Robbert Krebbers committed
240
Proof.
241
242
243
244
245
246
247
248
249
250
251
  revert i. induction t as [|o l IHl r IHr]; intros [i|i|]; simpl;
    rewrite ?PNode_lookup; simpl; auto.
Qed.
Lemma Pmerge_lookup {A B C} (f : option A  option B  option C)
    (Hf : f None None = None) t1 t2 i :
  Pmerge_raw f t1 t2 !! i = f (t1 !! i) (t2 !! i).
Proof.
  revert t2 i; induction t1 as [|o1 l1 IHl1 r1 IHr1]; intros t2 i; simpl.
  { rewrite Pomap_lookup. by destruct (t2 !! i). }
  unfold compose, flip.
  destruct t2 as [|l2 o2 r2]; rewrite PNode_lookup.
252
  - by destruct i; rewrite ?Pomap_lookup; simpl; rewrite ?Pomap_lookup;
253
      match goal with |- ?o = _ = _ => destruct o end.
254
  - destruct i; rewrite ?Pomap_lookup; simpl; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
255
256
Qed.

257
258
259
260
261
262
263
(** Packed version and instance of the finite map type class *)
Inductive Pmap (A : Type) : Type :=
  PMap { pmap_car : Pmap_raw A; pmap_prf : Pmap_wf pmap_car }.
Arguments PMap {_} _ _.
Arguments pmap_car {_} _.
Arguments pmap_prf {_} _.
Lemma Pmap_eq {A} (m1 m2 : Pmap A) : m1 = m2  pmap_car m1 = pmap_car m2.
Robbert Krebbers's avatar
Robbert Krebbers committed
264
Proof.
265
  split; [by intros ->|intros]; destruct m1 as [t1 ?], m2 as [t2 ?].
266
  simplify_eq/=; f_equal; apply proof_irrel.
Robbert Krebbers's avatar
Robbert Krebbers committed
267
Qed.
268
Instance Pmap_eq_dec `{EqDecision A} : EqDecision (Pmap A) := λ m1 m2,
269
270
271
272
273
274
275
  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))
  end.
Instance Pempty {A} : Empty (Pmap A) := PMap  I.
Instance Plookup {A} : Lookup positive A (Pmap A) := λ i m, pmap_car m !! i.
Instance Ppartial_alter {A} : PartialAlter positive A (Pmap A) := λ f i m,
276
  let (t,Ht) := m in PMap (partial_alter f i t) (Ppartial_alter_wf f i _ Ht).
277
Instance Pfmap : FMap Pmap := λ A B f m,
278
  let (t,Ht) := m in PMap (f <$> t) (Pfmap_wf f _ Ht).
279
Instance Pto_list {A} : FinMapToList positive A (Pmap A) := λ m,
280
  let (t,Ht) := m in Pto_list_raw 1 t [].
281
Instance Pomap : OMap Pmap := λ A B f m,
282
  let (t,Ht) := m in PMap (omap f t) (Pomap_wf f _ Ht).
283
Instance Pmerge : Merge Pmap := λ A B C f m1 m2,
284
  let (t1,Ht1) := m1 in let (t2,Ht2) := m2 in PMap _ (Pmerge_wf f _ _ Ht1 Ht2).
Robbert Krebbers's avatar
Robbert Krebbers committed
285

286
Instance Pmap_finmap : FinMap positive Pmap.
Robbert Krebbers's avatar
Robbert Krebbers committed
287
288
Proof.
  split.
289
290
291
292
293
294
  - by intros ? [t1 ?] [t2 ?] ?; apply Pmap_eq, Pmap_wf_eq.
  - by intros ? [].
  - intros ?? [??] ?. by apply Plookup_alter.
  - intros ?? [??] ??. by apply Plookup_alter_ne.
  - intros ??? [??]. by apply Plookup_fmap.
  - intros ? [??]. apply Pto_list_nodup; [|constructor].
Robbert Krebbers's avatar
Robbert Krebbers committed
295
    intros ??. by rewrite elem_of_nil.
296
  - intros ? [??] i x; unfold map_to_list, Pto_list.
Robbert Krebbers's avatar
Robbert Krebbers committed
297
298
    rewrite Pelem_of_to_list, elem_of_nil.
    split. by intros [(?&->&?)|]. by left; exists i.
299
300
  - intros ?? ? [??] ?. by apply Pomap_lookup.
  - intros ??? ?? [??] [??] ?. by apply Pmerge_lookup.
Robbert Krebbers's avatar
Robbert Krebbers committed
301
302
Qed.

303
304
305
306
307
308
309
310
Program Instance Pmap_countable `{Countable A} : Countable (Pmap A) := {
  encode m := encode (map_to_list m : list (positive * A));
  decode p := map_of_list <$> decode p
}.
Next Obligation.
  intros A ?? m; simpl. rewrite decode_encode; simpl. by rewrite map_of_to_list.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
311
312
313
314
(** * Finite sets *)
(** We construct sets of [positives]s satisfying extensional equality. *)
Notation Pset := (mapset Pmap).
Instance Pmap_dom {A} : Dom (Pmap A) Pset := mapset_dom.
315
Instance Pmap_dom_spec : FinMapDom positive Pmap Pset := mapset_dom_spec.
Robbert Krebbers's avatar
Robbert Krebbers committed
316
317
318
319

(** * Fresh numbers *)
Fixpoint Pdepth {A} (m : Pmap_raw A) : nat :=
  match m with
320
  | PLeaf | PNode None _ _ => O | PNode _ l _ => S (Pdepth l)
Robbert Krebbers's avatar
Robbert Krebbers committed
321
322
323
  end.
Fixpoint Pfresh_at_depth {A} (m : Pmap_raw A) (d : nat) : option positive :=
  match d, m with
324
325
  | O, (PLeaf | PNode None _ _) => Some 1
  | S d, PNode _ l r =>
Robbert Krebbers's avatar
Robbert Krebbers committed
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
     match Pfresh_at_depth l d with
     | Some i => Some (i~0) | None => (~1) <$> Pfresh_at_depth r d
     end
  | _, _ => None
  end.
Fixpoint Pfresh_go {A} (m : Pmap_raw A) (d : nat) : option positive :=
  match d with
  | O => None
  | S d =>
     match Pfresh_go m d with
     | Some i => Some i | None => Pfresh_at_depth m d
     end
  end.
Definition Pfresh {A} (m : Pmap A) : positive :=
  let d := Pdepth (pmap_car m) in
  match Pfresh_go (pmap_car m) d with
  | Some i => i | None => Pos.shiftl_nat 1 d
  end.

Lemma Pfresh_at_depth_fresh {A} (m : Pmap_raw A) d i :
  Pfresh_at_depth m d = Some i  m !! i = None.
Proof.
  revert i m; induction d as [|d IH].
349
  { intros i [|[] l r] ?; naive_solver. }
350
  intros i [|o l r] ?; simplify_eq/=.
Robbert Krebbers's avatar
Robbert Krebbers committed
351
  destruct (Pfresh_at_depth l d) as [i'|] eqn:?,
352
    (Pfresh_at_depth r d) as [i''|] eqn:?; simplify_eq/=; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
353
354
355
356
Qed.
Lemma Pfresh_go_fresh {A} (m : Pmap_raw A) d i :
  Pfresh_go m d = Some i  m !! i = None.
Proof.
357
  induction d as [|d IH]; intros; simplify_eq/=.
Robbert Krebbers's avatar
Robbert Krebbers committed
358
359
360
361
  destruct (Pfresh_go m d); eauto using Pfresh_at_depth_fresh.
Qed.
Lemma Pfresh_depth {A} (m : Pmap_raw A) :
  m !! Pos.shiftl_nat 1 (Pdepth m) = None.
362
Proof. induction m as [|[x|] l IHl r IHr]; auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
363
364
365
366
367
368
369
370
371
372
373
Lemma Pfresh_fresh {A} (m : Pmap A) : m !! Pfresh m = None.
Proof.
  destruct m as [m ?]; unfold lookup, Plookup, Pfresh; simpl.
  destruct (Pfresh_go m _) eqn:?; eauto using Pfresh_go_fresh, Pfresh_depth.
Qed.

Instance Pset_fresh : Fresh positive Pset := λ X,
  let (m) := X in Pfresh m.
Instance Pset_fresh_spec : FreshSpec positive Pset.
Proof.
  split.
374
375
376
  - apply _.
  - intros X Y; rewrite <-elem_of_equiv_L. by intros ->.
  - unfold elem_of, mapset_elem_of, fresh; intros [m]; simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
377
378
    by rewrite Pfresh_fresh.
Qed.