gmap.v 12.9 KB
Newer Older
1
(* Copyright (c) 2012-2019, Coq-std++ developers. *)
2 3 4
(* This file is distributed under the terms of the BSD license. *)
(** This file implements finite maps and finite sets with keys of any countable
type. The implementation is based on [Pmap]s, radix-2 search trees. *)
5
From stdpp Require Export countable infinite fin_maps fin_map_dom.
6 7
From stdpp Require Import pmap mapset propset.
(* Set Default Proof Using "Type". *)
8 9 10 11 12 13 14 15 16 17

(** * The data structure *)
(** We pack a [Pmap] together with a proof that ensures that all keys correspond
to codes of actual elements of the countable type. *)
Definition gmap_wf `{Countable K} {A} : Pmap A  Prop :=
  map_Forall (λ p _, encode <$> decode p = Some p).
Record gmap K `{Countable K} A := GMap {
  gmap_car : Pmap A;
  gmap_prf : bool_decide (gmap_wf gmap_car)
}.
18 19
Arguments GMap {_ _ _ _} _ _ : assert.
Arguments gmap_car {_ _ _ _} _ : assert.
20 21 22
Lemma gmap_eq `{Countable K} {A} (m1 m2 : gmap K A) :
  m1 = m2  gmap_car m1 = gmap_car m2.
Proof.
23
  split; [by intros ->|intros]. destruct m1, m2; simplify_eq/=.
24 25
  f_equal; apply proof_irrel.
Qed.
26
Instance gmap_eq_eq `{Countable K, EqDecision A} : EqDecision (gmap K A).
27
Proof.
28
 refine (λ m1 m2, cast_if (decide (gmap_car m1 = gmap_car m2)));
29 30 31 32
  abstract (by rewrite gmap_eq).
Defined.

(** * Operations on the data structure *)
33
Instance gmap_lookup `{Countable K} {A} : Lookup K A (gmap K A) := λ i m,
34 35
  let (m,_) := m in m !! encode i.
Instance gmap_empty `{Countable K} {A} : Empty (gmap K A) := GMap  I.
36
Global Opaque gmap_empty.
37 38 39 40
Lemma gmap_partial_alter_wf `{Countable K} {A} (f : option A  option A) m i :
  gmap_wf m  gmap_wf (partial_alter f (encode i) m).
Proof.
  intros Hm p x. destruct (decide (encode i = p)) as [<-|?].
41 42
  - rewrite decode_encode; eauto.
  - rewrite lookup_partial_alter_ne by done. by apply Hm.
43
Qed.
44 45
Instance gmap_partial_alter `{Countable K} {A} :
    PartialAlter K A (gmap K A) := λ f i m,
46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73
  let (m,Hm) := m in GMap (partial_alter f (encode i) m)
    (bool_decide_pack _ (gmap_partial_alter_wf f m i
    (bool_decide_unpack _ Hm))).
Lemma gmap_fmap_wf `{Countable K} {A B} (f : A  B) m :
  gmap_wf m  gmap_wf (f <$> m).
Proof. intros ? p x. rewrite lookup_fmap, fmap_Some; intros (?&?&?); eauto. Qed.
Instance gmap_fmap `{Countable K} : FMap (gmap K) := λ A B f m,
  let (m,Hm) := m in GMap (f <$> m)
    (bool_decide_pack _ (gmap_fmap_wf f m (bool_decide_unpack _ Hm))).
Lemma gmap_omap_wf `{Countable K} {A B} (f : A  option B) m :
  gmap_wf m  gmap_wf (omap f m).
Proof. intros ? p x; rewrite lookup_omap, bind_Some; intros (?&?&?); eauto. Qed.
Instance gmap_omap `{Countable K} : OMap (gmap K) := λ A B f m,
  let (m,Hm) := m in GMap (omap f m)
    (bool_decide_pack _ (gmap_omap_wf f m (bool_decide_unpack _ Hm))).
Lemma gmap_merge_wf `{Countable K} {A B C}
    (f : option A  option B  option C) m1 m2 :
  let f' o1 o2 := match o1, o2 with None, None => None | _, _ => f o1 o2 end in
  gmap_wf m1  gmap_wf m2  gmap_wf (merge f' m1 m2).
Proof.
  intros f' Hm1 Hm2 p z; rewrite lookup_merge by done; intros.
  destruct (m1 !! _) eqn:?, (m2 !! _) eqn:?; naive_solver.
Qed.
Instance gmap_merge `{Countable K} : Merge (gmap K) := λ A B C f m1 m2,
  let (m1,Hm1) := m1 in let (m2,Hm2) := m2 in
  let f' o1 o2 := match o1, o2 with None, None => None | _, _ => f o1 o2 end in
  GMap (merge f' m1 m2) (bool_decide_pack _ (gmap_merge_wf f _ _
    (bool_decide_unpack _ Hm1) (bool_decide_unpack _ Hm2))).
74
Instance gmap_to_list `{Countable K} {A} : FinMapToList K A (gmap K A) := λ m,
75 76 77 78 79 80 81
  let (m,_) := m in omap (λ ix : positive * A,
    let (i,x) := ix in (,x) <$> decode i) (map_to_list m).

(** * Instantiation of the finite map interface *)
Instance gmap_finmap `{Countable K} : FinMap K (gmap K).
Proof.
  split.
82
  - unfold lookup; intros A [m1 Hm1] [m2 Hm2] Hm.
83 84 85 86
    apply gmap_eq, map_eq; intros i; simpl in *.
    apply bool_decide_unpack in Hm1; apply bool_decide_unpack in Hm2.
    apply option_eq; intros x; split; intros Hi.
    + pose proof (Hm1 i x Hi); simpl in *.
87
      by destruct (decode i); simplify_eq/=; rewrite <-Hm.
88
    + pose proof (Hm2 i x Hi); simpl in *.
89
      by destruct (decode i); simplify_eq/=; rewrite Hm.
90 91 92
  - done.
  - intros A f [m Hm] i; apply (lookup_partial_alter f m).
  - intros A f [m Hm] i j Hs; apply (lookup_partial_alter_ne f m).
93
    by contradict Hs; apply (inj encode).
94 95
  - intros A B f [m Hm] i; apply (lookup_fmap f m).
  - intros A [m Hm]; unfold map_to_list; simpl.
96 97
    apply bool_decide_unpack, map_Forall_to_list in Hm; revert Hm.
    induction (NoDup_map_to_list m) as [|[p x] l Hpx];
98 99 100
      inversion 1 as [|??? Hm']; simplify_eq/=; [by constructor|].
    destruct (decode p) as [i|] eqn:?; simplify_eq/=; constructor; eauto.
    rewrite elem_of_list_omap; intros ([p' x']&?&?); simplify_eq/=.
101
    feed pose proof (proj1 (Forall_forall _ _) Hm' (p',x')); simpl in *; auto.
102
    by destruct (decode p') as [i'|]; simplify_eq/=.
103
  - intros A [m Hm] i x; unfold map_to_list, lookup; simpl.
104 105 106
    apply bool_decide_unpack in Hm; rewrite elem_of_list_omap; split.
    + intros ([p' x']&Hp'&?); apply elem_of_map_to_list in Hp'.
      feed pose proof (Hm p' x'); simpl in *; auto.
107
      by destruct (decode p') as [i'|] eqn:?; simplify_eq/=.
108 109
    + intros; exists (encode i,x); simpl.
      by rewrite elem_of_map_to_list, decode_encode.
110 111
  - intros A B f [m Hm] i; apply (lookup_omap f m).
  - intros A B C f ? [m1 Hm1] [m2 Hm2] i; unfold merge, lookup; simpl.
112 113 114 115
    set (f' o1 o2 := match o1, o2 with None,None => None | _, _ => f o1 o2 end).
    by rewrite lookup_merge by done; destruct (m1 !! _), (m2 !! _).
Qed.

116 117 118
Program Instance gmap_countable
    `{Countable K, Countable A} : Countable (gmap K A) := {
  encode m := encode (map_to_list m : list (K * A));
119
  decode p := list_to_map <$> decode p
120 121 122
}.
Next Obligation.
  intros K ?? A ?? m; simpl. rewrite decode_encode; simpl.
123
  by rewrite list_to_map_to_list.
124 125
Qed.

126 127 128 129 130 131 132
(** * Curry and uncurry *)
Definition gmap_curry `{Countable K1, Countable K2} {A} :
    gmap K1 (gmap K2 A)  gmap (K1 * K2) A :=
  map_fold (λ i1 m' macc,
    map_fold (λ i2 x, <[(i1,i2):=x]>) macc m') .
Definition gmap_uncurry `{Countable K1, Countable K2} {A} :
    gmap (K1 * K2) A  gmap K1 (gmap K2 A) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
133
  map_fold (λ ii x, let '(i1,i2) := ii in
134
    partial_alter (Some  <[i2:=x]>  default ) i1) .
135 136 137 138

Section curry_uncurry.
  Context `{Countable K1, Countable K2} {A : Type}.

139 140
  (* FIXME: the type annotations `option (gmap K2 A)` are silly. Maybe these are
  a consequence of Coq bug #5735 *)
141
  Lemma lookup_gmap_curry (m : gmap K1 (gmap K2 A)) i j :
142
    gmap_curry m !! (i,j) = (m !! i : option (gmap K2 A)) = (!! j).
143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158
  Proof.
    apply (map_fold_ind (λ mr m, mr !! (i,j) = m !! i = (!! j))).
    { by rewrite !lookup_empty. }
    clear m; intros i' m2 m m12 Hi' IH.
    apply (map_fold_ind (λ m2r m2, m2r !! (i,j) = <[i':=m2]> m !! i = (!! j))).
    { rewrite IH. destruct (decide (i' = i)) as [->|].
      - rewrite lookup_insert, Hi'; simpl; by rewrite lookup_empty.
      - by rewrite lookup_insert_ne by done. }
    intros j' y m2' m12' Hj' IH'. destruct (decide (i = i')) as [->|].
    - rewrite lookup_insert; simpl. destruct (decide (j = j')) as [->|].
      + by rewrite !lookup_insert.
      + by rewrite !lookup_insert_ne, IH', lookup_insert by congruence.
    - by rewrite !lookup_insert_ne, IH', lookup_insert_ne by congruence.
  Qed.

  Lemma lookup_gmap_uncurry (m : gmap (K1 * K2) A) i j :
159
    (gmap_uncurry m !! i : option (gmap K2 A)) = (!! j) = m !! (i, j).
160 161 162 163 164 165 166 167 168 169 170
  Proof.
    apply (map_fold_ind (λ mr m, mr !! i = (!! j) = m !! (i, j))).
    { by rewrite !lookup_empty. }
    clear m; intros [i' j'] x m12 mr Hij' IH.
    destruct (decide (i = i')) as [->|].
    - rewrite lookup_partial_alter. destruct (decide (j = j')) as [->|].
      + destruct (mr !! i'); simpl; by rewrite !lookup_insert.
      + destruct (mr !! i'); simpl; by rewrite !lookup_insert_ne by congruence.
    - by rewrite lookup_partial_alter_ne, lookup_insert_ne by congruence.
  Qed.

171 172 173 174 175 176 177 178 179 180 181 182 183
  Lemma lookup_gmap_uncurry_None (m : gmap (K1 * K2) A) i :
    gmap_uncurry m !! i = None  ( j, m !! (i, j) = None).
  Proof.
    apply (map_fold_ind (λ mr m, mr !! i = None  ( j, m !! (i, j) = None)));
      [done|].
    clear m; intros [i' j'] x m12 mr Hij' IH.
    destruct (decide (i = i')) as [->|].
    - split; [by rewrite lookup_partial_alter|].
      intros Hi. specialize (Hi j'). by rewrite lookup_insert in Hi.
    - rewrite lookup_partial_alter_ne, IH; [|done]. apply forall_proper.
      intros j. rewrite lookup_insert_ne; [done|congruence].
  Qed.

184 185 186 187 188
  Lemma gmap_curry_uncurry (m : gmap (K1 * K2) A) :
    gmap_curry (gmap_uncurry m) = m.
  Proof.
   apply map_eq; intros [i j]. by rewrite lookup_gmap_curry, lookup_gmap_uncurry.
  Qed.
Hai Dang's avatar
Hai Dang committed
189

190 191
  Lemma gmap_uncurry_non_empty (m : gmap (K1 * K2) A) i x :
    gmap_uncurry m !! i = Some x  x  .
Hai Dang's avatar
Hai Dang committed
192
  Proof.
193 194 195
    intros Hm ->. eapply eq_None_not_Some; [|by eexists].
    eapply lookup_gmap_uncurry_None; intros j.
    by rewrite <-lookup_gmap_uncurry, Hm.
Hai Dang's avatar
Hai Dang committed
196 197
  Qed.

198 199
  Lemma gmap_uncurry_curry_non_empty (m : gmap K1 (gmap K2 A)) :
    ( i x, m !! i = Some x  x  ) 
Hai Dang's avatar
Hai Dang committed
200 201
    gmap_uncurry (gmap_curry m) = m.
  Proof.
202 203
    intros Hne. apply map_eq; intros i. destruct (m !! i) as [m2|] eqn:Hm.
    - destruct (gmap_uncurry (gmap_curry m) !! i) as [m2'|] eqn:Hcurry.
Hai Dang's avatar
Hai Dang committed
204
      + f_equal. apply map_eq. intros j.
205 206 207 208 209 210 211
        trans ((gmap_uncurry (gmap_curry m) !! i : option (gmap _ _)) = (!! j)).
        { by rewrite Hcurry. }
        by rewrite lookup_gmap_uncurry, lookup_gmap_curry, Hm.
      + rewrite lookup_gmap_uncurry_None in Hcurry.
        exfalso; apply (Hne i m2), map_eq; [done|intros j].
        by rewrite lookup_empty, <-(Hcurry j), lookup_gmap_curry, Hm.
   - apply lookup_gmap_uncurry_None; intros j. by rewrite lookup_gmap_curry, Hm.
Hai Dang's avatar
Hai Dang committed
212
  Qed.
213 214
End curry_uncurry.

215
(** * Finite sets *)
216
Definition gset K `{Countable K} := mapset (gmap K).
217

218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238
Section gset.
  Context `{Countable K}.
  Global Instance gset_elem_of: ElemOf K (gset K) := _.
  Global Instance gset_empty : Empty (gset K) := _.
  Global Instance gset_singleton : Singleton K (gset K) := _.
  Global Instance gset_union: Union (gset K) := _.
  Global Instance gset_intersection: Intersection (gset K) := _.
  Global Instance gset_difference: Difference (gset K) := _.
  Global Instance gset_elements: Elements K (gset K) := _.
  Global Instance gset_leibniz : LeibnizEquiv (gset K) := _.
  Global Instance gset_semi_set : SemiSet K (gset K) | 1 := _.
  Global Instance gset_set : Set_ K (gset K) | 1 := _.
  Global Instance gset_fin_set : FinSet K (gset K) := _.
  Global Instance gset_eq_dec : EqDecision (gset K) := _.
  Global Instance gset_countable : Countable (gset K) := _.
  Global Instance gset_equiv_dec : RelDecision (@{gset K}) | 1 := _.
  Global Instance gset_elem_of_dec : RelDecision (@{gset K}) | 1 := _.
  Global Instance gset_disjoint_dec : RelDecision (##@{gset K}) := _.
  Global Instance gset_subseteq_dec : RelDecision (@{gset K}) := _.
  Global Instance gset_dom {A} : Dom (gmap K A) (gset K) := mapset_dom.
  Global Instance gset_dom_spec : FinMapDom K (gmap K) (gset K) := mapset_dom_spec.
Robbert Krebbers's avatar
Robbert Krebbers committed
239

240 241 242 243
  Definition gset_to_propset (X : gset K) : propset K :=
    {[ x | x  X ]}.
  Lemma elem_of_gset_to_propset (X : gset K) x : x  gset_to_propset X  x  X.
  Proof. done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
244

245 246
  Definition gset_to_gmap {A} (x : A) (X : gset K) : gmap K A :=
    (λ _, x) <$> mapset_car X.
Robbert Krebbers's avatar
Robbert Krebbers committed
247

248 249 250 251 252 253 254 255 256 257 258 259 260 261
  Lemma lookup_gset_to_gmap {A} (x : A) (X : gset K) i :
    gset_to_gmap x X !! i = guard (i  X); Some x.
  Proof.
    destruct X as [X].
    unfold gset_to_gmap, gset_elem_of, elem_of, mapset_elem_of; simpl.
    rewrite lookup_fmap.
    case_option_guard; destruct (X !! i) as [[]|]; naive_solver.
  Qed.
  Lemma lookup_gset_to_gmap_Some {A} (x : A) (X : gset K) i y :
    gset_to_gmap x X !! i = Some y  i  X  x = y.
  Proof. rewrite lookup_gset_to_gmap. simplify_option_eq; naive_solver. Qed.
  Lemma lookup_gset_to_gmap_None {A} (x : A) (X : gset K) i :
    gset_to_gmap x X !! i = None  i  X.
  Proof. rewrite lookup_gset_to_gmap. simplify_option_eq; naive_solver. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
262

263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289
  Lemma gset_to_gmap_empty {A} (x : A) : gset_to_gmap x  = .
  Proof. apply fmap_empty. Qed.
  Lemma gset_to_gmap_union_singleton {A} (x : A) i Y :
    gset_to_gmap x ({[ i ]}  Y) = <[i:=x]>(gset_to_gmap x Y).
  Proof.
    apply map_eq; intros j; apply option_eq; intros y.
    rewrite lookup_insert_Some, !lookup_gset_to_gmap_Some, elem_of_union,
      elem_of_singleton; destruct (decide (i = j)); intuition.
  Qed.

  Lemma fmap_gset_to_gmap {A B} (f : A  B) (X : gset K) (x : A) :
    f <$> gset_to_gmap x X = gset_to_gmap (f x) X.
  Proof.
    apply map_eq; intros j. rewrite lookup_fmap, !lookup_gset_to_gmap.
    by simplify_option_eq.
  Qed.
  Lemma gset_to_gmap_dom {A B} (m : gmap K A) (y : B) :
    gset_to_gmap y (dom _ m) = const y <$> m.
  Proof.
    apply map_eq; intros j. rewrite lookup_fmap, lookup_gset_to_gmap.
    destruct (m !! j) as [x|] eqn:?.
    - by rewrite option_guard_True by (rewrite elem_of_dom; eauto).
    - by rewrite option_guard_False by (rewrite not_elem_of_dom; eauto).
  Qed.
End gset.

Typeclasses Opaque gset.