add filter for gmap

theories/gmap.v

@@ -225,6 +225,102 @@ Proof.
   - 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. *)