pmap.v 13.8 KB
Newer Older
1
(* Copyright (c) 2012-2019, Coq-std++ developers. *)
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

Local Open Scope positive_scope.
16 17
Local Hint Extern 0 (_ =@{positive} _) => congruence : core.
Local Hint Extern 0 (_ @{positive} _) => congruence : core.
Robbert Krebbers's avatar
Robbert Krebbers committed
18

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. *)
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 {_} : assert.
Arguments PNode {_} _ _ _ : assert.
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
Arguments Pmap_wf _ !_ / : simpl nomatch, assert.
40 41 42 43
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.
44
Local Hint Immediate Pmap_wf_l Pmap_wf_r : core.
45 46
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.
47
Arguments PNode' : simpl never.
48 49 50
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.
51
Local Hint Resolve PNode_wf : core.
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
  | PNode o l r => match i with 1 => o | i~0 => l !! i | i~1 => r !! i end
  end.
62
Local Arguments lookup _ _ _ _ _ !_ / : simpl nomatch, assert.
63 64 65 66 67 68 69 70 71 72 73
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 =>
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)
78
     end
Robbert Krebbers's avatar
Robbert Krebbers committed
79
  end.
80 81 82 83 84 85 86 87 88
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
89
  | PNode o l r => from_option (λ x, [(Preverse j, x)]) [] o ++
90 91 92 93 94 95 96 97 98 99 100 101 102 103 104
     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.
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
(** 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 }.
261 262 263
Arguments PMap {_} _ _ : assert.
Arguments pmap_car {_} _ : assert.
Arguments pmap_prf {_} _ : assert.
264
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
Program Instance Pmap_countable `{Countable A} : Countable (Pmap A) := {
  encode m := encode (map_to_list m : list (positive * A));
306
  decode p := list_to_map <$> decode p
307 308
}.
Next Obligation.
309
  intros A ?? m; simpl. rewrite decode_encode; simpl. by rewrite list_to_map_to_list.
310 311
Qed.

312 313
(** * Finite sets *)
(** We construct sets of [positives]s satisfying extensional equality. *)
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.