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 11 12
From Coq Require Import PArith.
From prelude Require Import mapset.
From 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 120 121 122 123 124
  revert t2.
  induction t1 as [|o1 l1 IHl r1 IHr]; intros [|o2 l2 r2] Ht ??; simpl; auto.
  * discriminate (Pmap_wf_canon (PNode o2 l2 r2)); eauto.
  * discriminate (Pmap_wf_canon (PNode o1 l1 r1)); eauto.
  * f_equal; [apply (Ht 1)| |].
    + 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 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150
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.
  * destruct (f None); auto using Psingleton_wf.
  * destruct i; simpl; eauto.
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 160 161
  revert i; induction t as [|o l IHl r IHr]; intros i; simpl.
  * 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 167 168
  revert i j; induction t as [|o l IHl r IHr]; simpl.
  * 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.
Robbert Krebbers's avatar
Robbert Krebbers committed
178 179 180 181
    * 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.
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 _).
Robbert Krebbers's avatar
Robbert Krebbers committed
185 186
    * intros.
      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.
Robbert Krebbers's avatar
Robbert Krebbers committed
196 197 198
  * done.
  * rewrite elem_of_cons. destruct i as [i|i|]; simplify_equality'.
    + 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 203 204
    + left. by rewrite (left_id_L 1 (++))%positive.
  * destruct i as [i|i|]; simplify_equality'.
    + 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 ?.
Robbert Krebbers's avatar
Robbert Krebbers committed
214 215 216 217 218 219 220 221 222 223 224 225
  * 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].
226 227 228
     + 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. }
Robbert Krebbers's avatar
Robbert Krebbers committed
229
   apply IHr; auto. intros i x Hi.
230
   apply (Hin (i~1) x). by rewrite Preverse_xI, (assoc_L _) in Hi.
Robbert Krebbers's avatar
Robbert Krebbers committed
231 232
 * apply IHl.
   { intros i x. rewrite Pelem_of_to_list. intros [(?&Hi&?)|Hi].
233 234 235
     + 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. }
Robbert Krebbers's avatar
Robbert Krebbers committed
236
   apply IHr; auto. intros i x Hi.
237
   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 253 254 255
  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.
  * by destruct i; rewrite ?Pomap_lookup; simpl; rewrite ?Pomap_lookup;
      match goal with |- ?o = _ = _ => destruct o end.
  * 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 267
  split; [by intros ->|intros]; destruct m1 as [t1 ?], m2 as [t2 ?].
  simplify_equality'; 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
  * by intros ? [t1 ?] [t2 ?] ?; apply Pmap_eq, Pmap_wf_eq.
Robbert Krebbers's avatar
Robbert Krebbers committed
292 293 294 295 296 297 298 299 300 301
  * by intros ? [].
  * intros ?? [??] ?. by apply Plookup_alter.
  * intros ?? [??] ??. by apply Plookup_alter_ne.
  * intros ??? [??]. by apply Plookup_fmap.
  * intros ? [??]. apply Pto_list_nodup; [|constructor].
    intros ??. by rewrite elem_of_nil.
  * intros ? [??] i x; unfold map_to_list, Pto_list.
    rewrite Pelem_of_to_list, elem_of_nil.
    split. by intros [(?&->&?)|]. by left; exists i.
  * intros ?? ? [??] ?. by apply Pomap_lookup.
302
  * 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 344
  { intros i [|[] l r] ?; naive_solver. }
  intros i [|o l r] ?; simplify_equality'.
Robbert Krebbers's avatar
Robbert Krebbers committed
345 346 347 348 349 350 351 352 353 354 355
  destruct (Pfresh_at_depth l d) as [i'|] eqn:?,
    (Pfresh_at_depth r d) as [i''|] eqn:?; simplify_equality'; auto.
Qed.
Lemma Pfresh_go_fresh {A} (m : Pmap_raw A) d i :
  Pfresh_go m d = Some i  m !! i = None.
Proof.
  induction d as [|d IH]; intros; simplify_equality'.
  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 368 369 370 371 372
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.
  * apply _.
  * intros X Y; rewrite <-elem_of_equiv_L. by intros ->.
  * unfold elem_of, mapset_elem_of, fresh; intros [m]; simpl.
    by rewrite Pfresh_fresh.
Qed.