gmap.v 14.30 KiB
(* Copyright (c) 2012-2017, Coq-std++ developers. *)
(* 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. *)
From stdpp Require Export countable fin_maps fin_map_dom.
From stdpp Require Import pmap mapset set.
Set Default Proof Using "Type".
(** * 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)
}.
Arguments GMap {_ _ _ _} _ _.
Arguments gmap_car {_ _ _ _} _.
Lemma gmap_eq `{Countable K} {A} (m1 m2 : gmap K A) :
m1 = m2 ↔ gmap_car m1 = gmap_car m2.
Proof.
split; [by intros ->|intros]. destruct m1, m2; simplify_eq/=.
f_equal; apply proof_irrel.
Qed.
Instance gmap_eq_eq `{Countable K, EqDecision A} : EqDecision (gmap K A).
Proof.
refine (λ m1 m2, cast_if (decide (gmap_car m1 = gmap_car m2)));
abstract (by rewrite gmap_eq).
Defined.
(** * Operations on the data structure *)
Instance gmap_lookup `{Countable K} {A} : Lookup K A (gmap K A) := λ i m,
let (m,_) := m in m !! encode i.
Instance gmap_empty `{Countable K} {A} : Empty (gmap K A) := GMap ∅ I.
Global Opaque gmap_empty.
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 [<-|?].
- rewrite decode_encode; eauto.
- rewrite lookup_partial_alter_ne by done. by apply Hm.
Qed.
Instance gmap_partial_alter `{Countable K} {A} :
PartialAlter K A (gmap K A) := λ f i m,
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))).
Instance gmap_to_list `{Countable K} {A} : FinMapToList K A (gmap K A) := λ m,
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.
- unfold lookup; intros A [m1 Hm1] [m2 Hm2] Hm.
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 *.
by destruct (decode i); simplify_eq/=; rewrite <-Hm.
+ pose proof (Hm2 i x Hi); simpl in *.
by destruct (decode i); simplify_eq/=; rewrite Hm.
- 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).
by contradict Hs; apply (inj encode).
- intros A B f [m Hm] i; apply (lookup_fmap f m).
- intros A [m Hm]; unfold map_to_list; simpl.
apply bool_decide_unpack, map_Forall_to_list in Hm; revert Hm.
induction (NoDup_map_to_list m) as [|[p x] l Hpx];
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/=.
feed pose proof (proj1 (Forall_forall _ _) Hm' (p',x')); simpl in *; auto.
by destruct (decode p') as [i'|]; simplify_eq/=.
- intros A [m Hm] i x; unfold map_to_list, lookup; simpl.
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.
by destruct (decode p') as [i'|] eqn:?; simplify_eq/=.
+ intros; exists (encode i,x); simpl.
by rewrite elem_of_map_to_list, decode_encode.
- 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.
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.
Program Instance gmap_countable
`{Countable K, Countable A} : Countable (gmap K A) := {
encode m := encode (map_to_list m : list (K * A));
decode p := map_of_list <$> decode p
}.
Next Obligation.
intros K ?? A ?? m; simpl. rewrite decode_encode; simpl.
by rewrite map_of_to_list.
Qed.
(** * 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) :=
map_fold (λ ii x, let '(i1,i2) := ii in
partial_alter (Some ∘ <[i2:=x]> ∘ from_option id ∅) i1) ∅.
Section curry_uncurry.
Context `{Countable K1, Countable K2} {A : Type}.
Lemma lookup_gmap_curry (m : gmap K1 (gmap K2 A)) i j :
gmap_curry m !! (i,j) = m !! i ≫= (!! j). 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 :
gmap_uncurry m !! i ≫= (!! j) = m !! (i, j).
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.
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.
End curry_uncurry.
(** * Finite sets *)
Notation gset K := (mapset (gmap K)).
Instance gset_dom `{Countable K} {A} : Dom (gmap K A) (gset K) := mapset_dom.
Instance gset_dom_spec `{Countable K} :
FinMapDom K (gmap K) (gset K) := mapset_dom_spec.
Definition of_gset `{Countable A} (X : gset A) : set A := mkSet (λ x, x ∈ X).
Lemma elem_of_of_gset `{Countable A} (X : gset A) x : x ∈ of_gset X ↔ x ∈ X.
Proof. done. Qed.
Definition to_gmap `{Countable K} {A} (x : A) (X : gset K) : gmap K A :=
(λ _, x) <$> mapset_car X.
Lemma lookup_to_gmap `{Countable K} {A} (x : A) (X : gset K) i :
to_gmap x X !! i = guard (i ∈ X); Some x.
Proof.
destruct X as [X]; unfold to_gmap, elem_of, mapset_elem_of; simpl.
rewrite lookup_fmap.
case_option_guard; destruct (X !! i) as [[]|]; naive_solver.
Qed.
Lemma lookup_to_gmap_Some `{Countable K} {A} (x : A) (X : gset K) i y :
to_gmap x X !! i = Some y ↔ i ∈ X ∧ x = y.
Proof. rewrite lookup_to_gmap. simplify_option_eq; naive_solver. Qed.
Lemma lookup_to_gmap_None `{Countable K} {A} (x : A) (X : gset K) i :
to_gmap x X !! i = None ↔ i ∉ X.
Proof. rewrite lookup_to_gmap. simplify_option_eq; naive_solver. Qed.
Lemma to_gmap_empty `{Countable K} {A} (x : A) : to_gmap x ∅ = ∅.
Proof. apply fmap_empty. Qed.
Lemma to_gmap_union_singleton `{Countable K} {A} (x : A) i Y :
to_gmap x ({[ i ]} ∪ Y) = <[i:=x]>(to_gmap x Y).
Proof.
apply map_eq; intros j; apply option_eq; intros y.
rewrite lookup_insert_Some, !lookup_to_gmap_Some, elem_of_union,
elem_of_singleton; destruct (decide (i = j)); intuition.Qed.
Lemma fmap_to_gmap `{Countable K} {A B} (f : A → B) (X : gset K) (x : A) :
f <$> to_gmap x X = to_gmap (f x) X.
Proof.
apply map_eq; intros j. rewrite lookup_fmap, !lookup_to_gmap.
by simplify_option_eq.
Qed.
Lemma to_gmap_dom `{Countable K} {A B} (m : gmap K A) (y : B) :
to_gmap y (dom _ m) = const y <$> m.
Proof.
apply map_eq; intros j. rewrite lookup_fmap, lookup_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.
(** Filter *)
(* This filter creates a submap whose (key,value) pairs satisfy P *)
Instance gmap_filter `{Countable K} {A} : Filter (K * A) (gmap K A) :=
λ P _, map_fold (λ k v m, if decide (P (k,v)) then <[k := v]>m else m) ∅.
Section filter.
Context `{Countable K} {A} (P : K * A → Prop) `{!∀ x, Decision (P x)}.
Implicit Type (m: gmap K A) (k: K) (v: A).
Lemma gmap_filter_lookup_Some:
∀ m k v, filter P m !! k = Some v ↔ m !! k = Some v ∧ P (k,v).
Proof.
apply (map_fold_ind (λ m1 m2, ∀ k v, m1 !! k = Some v
↔ m2 !! k = Some v ∧ P _)).
- naive_solver.
- intros k v m m' Hm Eq k' v'.
case_match; case (decide (k' = k))as [->|?].
+ rewrite 2!lookup_insert. naive_solver.
+ do 2 (rewrite lookup_insert_ne; [|auto]). by apply Eq.
+ rewrite Eq, Hm, lookup_insert. split; [naive_solver|].
destruct 1 as [Eq' ]. inversion Eq'. by subst.
+ by rewrite lookup_insert_ne.
Qed.
Lemma gmap_filter_lookup_None:
∀ m k,
filter P m !! k = None ↔ m !! k = None ∨ ∀ v, m !! k = Some v → ¬ P (k,v).
Proof.
apply (map_fold_ind (λ m1 m2, ∀ k, m1 !! k = None
↔ (m2 !! k = None ∨ ∀ v, m2 !! k = Some v → ¬ P _))).
- naive_solver.
- intros k v m m' Hm Eq k'.
case_match; case (decide (k' = k)) as [->|?].
+ rewrite 2!lookup_insert. naive_solver.
+ do 2 (rewrite lookup_insert_ne; [|auto]). by apply Eq.
+ rewrite Eq, Hm, lookup_insert. naive_solver.
+ by rewrite lookup_insert_ne.
Qed.
Lemma gmap_filter_dom m:
dom (gset K) (filter P m) ⊆ dom (gset K) m.
Proof.
intros ?. rewrite 2!elem_of_dom.
destruct 1 as [?[Eq _]%gmap_filter_lookup_Some]. by eexists.
Qed.
Lemma gmap_filter_lookup_equiv `{Equiv A} `{Reflexive A (≡)} m1 m2:
(∀ k v, P (k,v) → m1 !! k = Some v ↔ m2 !! k = Some v)
→ filter P m1 ≡ filter P m2.
Proof.
intros HP k.
destruct (filter P m1 !! k) as [v1|] eqn:Hv1; [apply gmap_filter_lookup_Some in Hv1 as [Hv1 HP1];
specialize (HP k v1 HP1)|];
destruct (filter P m2 !! k) as [v2|] eqn: Hv2.
- apply gmap_filter_lookup_Some in Hv2 as [Hv2 _].
rewrite Hv1, Hv2 in HP. destruct HP as [HP _].
specialize (HP (eq_refl _)) as []. by apply option_Forall2_refl.
- apply gmap_filter_lookup_None in Hv2 as [Hv2|Hv2];
[naive_solver|by apply HP, Hv2 in Hv1].
- apply gmap_filter_lookup_Some in Hv2 as [Hv2 HP2].
specialize (HP k v2 HP2).
apply gmap_filter_lookup_None in Hv1 as [Hv1|Hv1].
+ rewrite Hv1 in HP. naive_solver.
+ by apply HP, Hv1 in Hv2.
- by apply option_Forall2_refl.
Qed.
Lemma gmap_filter_lookup_insert `{Equiv A} `{Reflexive A (≡)} m k v:
P (k,v) → <[k := v]> (filter P m) ≡ filter P (<[k := v]> m).
Proof.
intros HP k'.
case (decide (k' = k)) as [->|?];
[rewrite lookup_insert|rewrite lookup_insert_ne; [|auto]].
- destruct (filter P (<[k:=v]> m) !! k) eqn: Hk.
+ apply gmap_filter_lookup_Some in Hk.
rewrite lookup_insert in Hk. destruct Hk as [Hk _].
inversion Hk. by apply option_Forall2_refl.
+ apply gmap_filter_lookup_None in Hk.
rewrite lookup_insert in Hk.
destruct Hk as [->|HNP]. by apply option_Forall2_refl.
by specialize (HNP v (eq_refl _)).
- destruct (filter P (<[k:=v]> m) !! k') eqn: Hk; revert Hk;
[rewrite gmap_filter_lookup_Some|rewrite gmap_filter_lookup_None];
(rewrite lookup_insert_ne ; [|by auto]);
[rewrite <-gmap_filter_lookup_Some|rewrite <-gmap_filter_lookup_None];
intros Hk; rewrite Hk; by apply option_Forall2_refl.
Qed.
Lemma gmap_filter_empty `{Equiv A} : filter P (∅ : gmap K A) ≡ ∅.
Proof. intro l. rewrite lookup_empty. constructor. Qed.
End filter.
(** * Fresh elements *)
(* This is pretty ad-hoc and just for the case of [gset positive]. We need a
notion of countable non-finite types to generalize this. *)
Instance gset_positive_fresh : Fresh positive (gset positive) := λ X,
let 'Mapset (GMap m _) := X in fresh (dom _ m).
Instance gset_positive_fresh_spec : FreshSpec positive (gset positive).
Proof.
split.
- apply _.
- by intros X Y; rewrite <-elem_of_equiv_L; intros ->.
- intros [[m Hm]]; unfold fresh; simpl.
by intros ?; apply (is_fresh (dom Pset m)), elem_of_dom_2 with ().
Qed.