pmap.v 15.7 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
From Coq Require Import PArith.
11
From stdpp Require Import mapset countable.
12
From stdpp Require Export fin_maps.
13
Set Default Proof Using "Type*".
Robbert Krebbers's avatar
Robbert Krebbers committed
14 15 16 17 18

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

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

30
Instance Pmap_raw_eq_dec `{EqDecision A} : EqDecision (Pmap_raw A).
Robbert Krebbers's avatar
Robbert Krebbers committed
31 32
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.
55 56 57
Instance Plookup_raw {A} : Lookup positive A (Pmap_raw A) :=
  fix go (i : positive) (t : Pmap_raw A) {struct t} : option A :=
  let _ : Lookup _ _ _ := @go in
Robbert Krebbers's avatar
Robbert Krebbers committed
58
  match t with
59
  | 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
     end
Robbert Krebbers's avatar
Robbert Krebbers committed
79
  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.
151
Lemma Plookup_singleton {A} i (x : A) : Psingleton_raw i x !! i = Some x.
152
Proof. by induction i. Qed.
153
Lemma Plookup_singleton_ne {A} i j (x : A) :
154
  i  j  Psingleton_raw i x !! j = None.
155
Proof. revert j. induction i; intros [?|?|]; simpl; auto with congruence. Qed.
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
Qed.
163
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.
172 173 174
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
175 176
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.
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 _). }
183
      destruct (IHr (j~1) acc) as [(i'&->&?)|?]; auto.
184
      left; exists (i' ~ 1). by rewrite Preverse_xI, (assoc_L _).
185
    - intros.
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 _). }
188
      destruct (IHr (j~1) acc) as [(i'&->&?)|?]; auto.
189
      left; exists (i' ~ 1). by rewrite Preverse_xI, (assoc_L _). }
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;
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/=.
198
    + right. apply help. specialize (IHr (j~1) i).
199
      rewrite Preverse_xI, (assoc_L _) in IHr. by apply IHr.
200
    + right. specialize (IHl (j~0) i).
201
      rewrite Preverse_xO, (assoc_L _) in IHl. by apply IHl.
202
    + left. by rewrite (left_id_L 1 (++))%positive.
203
  - destruct i as [i|i|]; simplify_eq/=.
204
    + apply help. specialize (IHr (j~1) i).
205
      rewrite Preverse_xI, (assoc_L _) in IHr. by apply IHr.
206
    + specialize (IHl (j~0) i).
207
      rewrite Preverse_xO, (assoc_L _) in IHl. by apply IHl.
208
Qed.
209 210 211
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).
212
Proof.
213
  revert j acc. induction t as [|[y|] l IHl r IHr]; simpl; intros j acc Hin ?.
214 215
  - done.
  - repeat constructor.
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.
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
Instance Pmap_eq_dec `{EqDecision A} : EqDecision (Pmap A) := λ m1 m2,
270 271 272 273 274
  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.
275 276
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,
277
  let (t,Ht) := m in PMap (partial_alter f i t) (Ppartial_alter_wf f i _ Ht).
278
Instance Pfmap : FMap Pmap := λ A B f m,
279
  let (t,Ht) := m in PMap (f <$> t) (Pfmap_wf f _ Ht).
280
Instance Pto_list {A} : FinMapToList positive A (Pmap A) := λ m,
281
  let (t,Ht) := m in Pto_list_raw 1 t [].
282
Instance Pomap : OMap Pmap := λ A B f m,
283
  let (t,Ht) := m in PMap (omap f t) (Pomap_wf f _ Ht).
284
Instance Pmerge : Merge Pmap := λ A B C f m1 m2,
285
  let (t1,Ht1) := m1 in let (t2,Ht2) := m2 in PMap _ (Pmerge_wf f _ _ Ht1 Ht2).
Robbert Krebbers's avatar
Robbert Krebbers committed
286

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

304 305 306 307 308 309 310 311
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.

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

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