pmap.v 15.4 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 12
From iris.prelude Require Import mapset.
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 29 30 31 32
Arguments PLeaf {_}.
Arguments PNode {_} _ _ _.

Instance Pmap_raw_eq_dec `{ x y : A, Decision (x = y)} (x y : Pmap_raw A) :
  Decision (x = y).
Proof. solve_decision. Defined.

33 34 35 36 37
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
38
  end.
39 40 41 42 43 44 45 46 47 48 49 50 51
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
52

53 54
(** Operations *)
Instance Pempty_raw {A} : Empty (Pmap_raw A) := PLeaf.
Robbert Krebbers's avatar
Robbert Krebbers committed
55 56
Instance Plookup_raw {A} : Lookup positive A (Pmap_raw A) :=
  fix go (i : positive) (t : Pmap_raw A) {struct t} : option A :=
57
  let _ : Lookup _ _ _ := @go in
Robbert Krebbers's avatar
Robbert Krebbers committed
58 59
  match t with
  | PLeaf => None
60 61 62 63 64 65 66 67 68 69 70 71 72 73
  | 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
74
     match i with
75 76 77
     | 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
78 79
     end
  end.
80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104
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
105

106 107 108
(** 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
109
Proof.
110 111 112 113
  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
114
Qed.
115 116
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
117
Proof.
118 119
  revert t2.
  induction t1 as [|o1 l1 IHl r1 IHr]; intros [|o2 l2 r2] Ht ??; simpl; auto.
120 121 122
  - discriminate (Pmap_wf_canon (PNode o2 l2 r2)); eauto.
  - discriminate (Pmap_wf_canon (PNode o1 l1 r1)); eauto.
  - f_equal; [apply (Ht 1)| |].
123 124
    + 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
125
Qed.
126 127 128
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
129 130

Lemma Psingleton_wf {A} i (x : A) : Pmap_wf (Psingleton_raw i x).
131 132 133 134 135
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.
136 137
  - destruct (f None); auto using Psingleton_wf.
  - destruct i; simpl; eauto.
138 139 140 141 142 143 144 145 146 147 148 149 150
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
151 152 153 154
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.
155
Proof. revert j. induction i; intros [?|?|]; simpl; auto with congruence. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
156
Lemma Plookup_alter {A} f i (t : Pmap_raw A) :
157
  Ppartial_alter_raw f i t !! i = f (t !! i).
Robbert Krebbers's avatar
Robbert Krebbers committed
158
Proof.
159
  revert i; induction t as [|o l IHl r IHr]; intros i; simpl.
160 161
  - by destruct (f None); rewrite ?Plookup_singleton.
  - destruct i; simpl; rewrite PNode_lookup; simpl; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
162 163
Qed.
Lemma Plookup_alter_ne {A} f i j (t : Pmap_raw A) :
164
  i  j  Ppartial_alter_raw f i t !! j = t !! j.
Robbert Krebbers's avatar
Robbert Krebbers committed
165
Proof.
166
  revert i j; induction t as [|o l IHl r IHr]; simpl.
167 168
  - by intros; destruct (f None); rewrite ?Plookup_singleton_ne.
  - by intros [?|?|] [?|?|] ?; simpl; rewrite ?PNode_lookup; simpl; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
169
Qed.
170 171
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
172 173 174 175 176
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.
177
  { revert j acc. induction t as [|[y|] l IHl r IHr]; intros j acc; simpl.
178
    - by right.
179
    - rewrite elem_of_cons. intros [?|?]; simplify_eq.
Robbert Krebbers's avatar
Robbert Krebbers committed
180 181
      { left; exists 1. by rewrite (left_id_L 1 (++))%positive. }
      destruct (IHl (j~0) (Pto_list_raw j~1 r acc)) as [(i'&->&?)|?]; auto.
182
      { left; exists (i' ~ 0). by rewrite Preverse_xO, (assoc_L _). }
Robbert Krebbers's avatar
Robbert Krebbers committed
183
      destruct (IHr (j~1) acc) as [(i'&->&?)|?]; auto.
184
      left; exists (i' ~ 1). by rewrite Preverse_xI, (assoc_L _).
185
    - intros.
Robbert Krebbers's avatar
Robbert Krebbers committed
186
      destruct (IHl (j~0) (Pto_list_raw j~1 r acc)) as [(i'&->&?)|?]; auto.
187
      { left; exists (i' ~ 0). by rewrite Preverse_xO, (assoc_L _). }
Robbert Krebbers's avatar
Robbert Krebbers committed
188
      destruct (IHr (j~1) acc) as [(i'&->&?)|?]; auto.
189
      left; exists (i' ~ 1). by rewrite Preverse_xI, (assoc_L _). }
Robbert Krebbers's avatar
Robbert Krebbers committed
190 191
  revert t j i acc. assert ( t j i acc,
    (i, x)  acc  (i, x)  Pto_list_raw j t acc) as help.
192
  { intros t; induction t as [|[y|] l IHl r IHr]; intros j i acc;
Robbert Krebbers's avatar
Robbert Krebbers committed
193 194
      simpl; rewrite ?elem_of_cons; auto. }
  intros t j ? acc [(i&->&Hi)|?]; [|by auto]. revert j i acc Hi.
195
  induction t as [|[y|] l IHl r IHr]; intros j i acc ?; simpl.
196
  - done.
197
  - rewrite elem_of_cons. destruct i as [i|i|]; simplify_eq/=.
Robbert Krebbers's avatar
Robbert Krebbers committed
198
    + right. apply help. specialize (IHr (j~1) i).
199
      rewrite Preverse_xI, (assoc_L _) in IHr. by apply IHr.
Robbert Krebbers's avatar
Robbert Krebbers committed
200
    + right. specialize (IHl (j~0) i).
201
      rewrite Preverse_xO, (assoc_L _) in IHl. by apply IHl.
Robbert Krebbers's avatar
Robbert Krebbers committed
202
    + left. by rewrite (left_id_L 1 (++))%positive.
203
  - destruct i as [i|i|]; simplify_eq/=.
Robbert Krebbers's avatar
Robbert Krebbers committed
204
    + apply help. specialize (IHr (j~1) i).
205
      rewrite Preverse_xI, (assoc_L _) in IHr. by apply IHr.
Robbert Krebbers's avatar
Robbert Krebbers committed
206
    + specialize (IHl (j~0) i).
207
      rewrite Preverse_xO, (assoc_L _) in IHl. by apply IHl.
Robbert Krebbers's avatar
Robbert Krebbers committed
208 209 210 211 212
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.
213
  revert j acc. induction t as [|[y|] l IHl r IHr]; simpl; intros j acc Hin ?.
214 215
  - done.
  - repeat constructor.
Robbert Krebbers's avatar
Robbert Krebbers committed
216 217 218 219 220 221 222 223
    { 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). }
224 225 226 227 228 229 230 231 232 233 234 235 236 237
    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
238
Qed.
239 240
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
241
Proof.
242 243 244 245 246 247 248 249 250 251 252
  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.
253
  - by destruct i; rewrite ?Pomap_lookup; simpl; rewrite ?Pomap_lookup;
254
      match goal with |- ?o = _ = _ => destruct o end.
255
  - destruct i; rewrite ?Pomap_lookup; simpl; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
256 257
Qed.

258 259 260 261 262 263 264
(** 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
265
Proof.
266
  split; [by intros ->|intros]; destruct m1 as [t1 ?], m2 as [t2 ?].
267
  simplify_eq/=; f_equal; apply proof_irrel.
Robbert Krebbers's avatar
Robbert Krebbers committed
268
Qed.
269 270 271 272 273 274 275 276 277
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))
  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,
278
  let (t,Ht) := m in PMap (partial_alter f i t) (Ppartial_alter_wf f i _ Ht).
279
Instance Pfmap : FMap Pmap := λ A B f m,
280
  let (t,Ht) := m in PMap (f <$> t) (Pfmap_wf f _ Ht).
281
Instance Pto_list {A} : FinMapToList positive A (Pmap A) := λ m,
282
  let (t,Ht) := m in Pto_list_raw 1 t [].
283
Instance Pomap : OMap Pmap := λ A B f m,
284
  let (t,Ht) := m in PMap (omap f t) (Pomap_wf f _ Ht).
285
Instance Pmerge : Merge Pmap := λ A B C f m1 m2,
286
  let (t1,Ht1) := m1 in let (t2,Ht2) := m2 in PMap _ (Pmerge_wf f _ _ Ht1 Ht2).
Robbert Krebbers's avatar
Robbert Krebbers committed
287

288
Instance Pmap_finmap : FinMap positive Pmap.
Robbert Krebbers's avatar
Robbert Krebbers committed
289 290
Proof.
  split.
291 292 293 294 295 296
  - 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
297
    intros ??. by rewrite elem_of_nil.
298
  - intros ? [??] i x; unfold map_to_list, Pto_list.
Robbert Krebbers's avatar
Robbert Krebbers committed
299 300
    rewrite Pelem_of_to_list, elem_of_nil.
    split. by intros [(?&->&?)|]. by left; exists i.
301 302
  - intros ?? ? [??] ?. by apply Pomap_lookup.
  - intros ??? ?? [??] [??] ?. by apply Pmerge_lookup.
Robbert Krebbers's avatar
Robbert Krebbers committed
303 304 305 306 307 308 309 310 311 312 313
Qed.

(** * 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.
Instance: FinMapDom positive Pmap Pset := mapset_dom_spec.

(** * Fresh numbers *)
Fixpoint Pdepth {A} (m : Pmap_raw A) : nat :=
  match m with
314
  | PLeaf | PNode None _ _ => O | PNode _ l _ => S (Pdepth l)
Robbert Krebbers's avatar
Robbert Krebbers committed
315 316 317
  end.
Fixpoint Pfresh_at_depth {A} (m : Pmap_raw A) (d : nat) : option positive :=
  match d, m with
318 319
  | O, (PLeaf | PNode None _ _) => Some 1
  | S d, PNode _ l r =>
Robbert Krebbers's avatar
Robbert Krebbers committed
320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342
     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].
343
  { intros i [|[] l r] ?; naive_solver. }
344
  intros i [|o l r] ?; simplify_eq/=.
Robbert Krebbers's avatar
Robbert Krebbers committed
345
  destruct (Pfresh_at_depth l d) as [i'|] eqn:?,
346
    (Pfresh_at_depth r d) as [i''|] eqn:?; simplify_eq/=; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
347 348 349 350
Qed.
Lemma Pfresh_go_fresh {A} (m : Pmap_raw A) d i :
  Pfresh_go m d = Some i  m !! i = None.
Proof.
351
  induction d as [|d IH]; intros; simplify_eq/=.
Robbert Krebbers's avatar
Robbert Krebbers committed
352 353 354 355
  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.
356
Proof. induction m as [|[x|] l IHl r IHr]; auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
357 358 359 360 361 362 363 364 365 366 367
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.
368 369 370
  - 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
371 372
    by rewrite Pfresh_fresh.
Qed.