gmap.v 13.1 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

(** * 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. *)
12 13
Definition gmap_wf K `{Countable K} {A} : Pmap A  Prop :=
  map_Forall (λ p _, encode (A:=K) <$> decode p = Some p).
14 15
Record gmap K `{Countable K} A := GMap {
  gmap_car : Pmap A;
16
  gmap_prf : bool_decide (gmap_wf K gmap_car)
17
}.
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
Lemma gmap_partial_alter_wf `{Countable K} {A} (f : option A  option A) m i :
38
  gmap_wf K m  gmap_wf K (partial_alter f (encode (A:=K) i) m).
39 40
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
  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 :
50
  gmap_wf K m  gmap_wf K (f <$> m).
51 52 53 54 55
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 :
56
  gmap_wf K m  gmap_wf K (omap f m).
57 58 59 60 61 62 63
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
64
  gmap_wf K m1  gmap_wf K m2  gmap_wf K (merge f' m1 m2).
65 66 67 68 69 70 71 72 73
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
  let (m,_) := m in omap (λ ix : positive * A,
76
    let (i,x) := ix in (., x) <$> decode i) (map_to_list m).
77 78 79 80 81

(** * 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) :=
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
  Proof.
144
    apply (map_fold_ind (λ mr m, mr !! (i,j) = m !! i = (.!! j))).
145 146
    { by rewrite !lookup_empty. }
    clear m; intros i' m2 m m12 Hi' IH.
147
    apply (map_fold_ind (λ m2r m2, m2r !! (i,j) = <[i':=m2]> m !! i = (.!! j))).
148 149 150 151 152 153 154 155 156 157 158
    { 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
  Proof.
161
    apply (map_fold_ind (λ mr m, mr !! i = (.!! j) = m !! (i, j))).
162 163 164 165 166 167 168 169 170
    { 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.
189

190 191
  Lemma gmap_uncurry_non_empty (m : gmap (K1 * K2) A) i x :
    gmap_uncurry m !! i = Some x  x  .
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.
196 197
  Qed.

198 199
  Lemma gmap_uncurry_curry_non_empty (m : gmap K1 (gmap K2 A)) :
    ( i x, m !! i = Some x  x  ) 
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.
204
      + f_equal. apply map_eq. intros j.
205
        trans ((gmap_uncurry (gmap_curry m) !! i : option (gmap _ _)) = (.!! j)).
206 207 208 209 210 211
        { 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.
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.
239

240 241
  Definition gset_to_gmap {A} (x : A) (X : gset K) : gmap K A :=
    (λ _, x) <$> mapset_car X.
242

243 244 245 246 247 248 249 250 251 252 253 254 255 256
  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.
257

258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281
  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.
282 283 284 285 286 287 288
  Lemma dom_gset_to_gmap {A} (X : gset K) (x : A) :
    dom _ (gset_to_gmap x X) = X.
  Proof.
    induction X as [| y X not_in IH] using set_ind_L.
    - rewrite gset_to_gmap_empty, dom_empty_L; done.
    - rewrite gset_to_gmap_union_singleton, dom_insert_L, IH; done.
  Qed.
289 290 291
End gset.

Typeclasses Opaque gset.