From bc61b7a53d6075233589ac4a454ec67c479da263 Mon Sep 17 00:00:00 2001
From: HoangHai Dang
Date: Thu, 28 Sep 2017 11:20:31 +0200
Subject: [PATCH 1/3] add filter for gmap

theories/gmap.v  96 +++++++++++++++++++++++++++++++++++++++++++++++++
1 file changed, 96 insertions(+)
diff git a/theories/gmap.v b/theories/gmap.v
index 4572c905..ef704d64 100644
 a/theories/gmap.v
+++ b/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 [Hv2Hv2];
+ [naive_solverby 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 [Hv1Hv1].
+ + 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_insertrewrite 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_Somerewrite gmap_filter_lookup_None];
+ (rewrite lookup_insert_ne ; [by auto]);
+ [rewrite <gmap_filter_lookup_Somerewrite <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 adhoc and just for the case of [gset positive]. We need a
notion of countable nonfinite types to generalize this. *)

GitLab
From 8ed74c3a3f43a6ef430c4ef83ebf9255bfe8fd03 Mon Sep 17 00:00:00 2001
From: HoangHai Dang
Date: Thu, 28 Sep 2017 21:09:58 +0200
Subject: [PATCH 2/3] simplify proofs of gmap filter

theories/gmap.v  67 +++++++++++++++++
1 file changed, 23 insertions(+), 44 deletions()
diff git a/theories/gmap.v b/theories/gmap.v
index ef704d64..adb03cc2 100644
 a/theories/gmap.v
+++ b/theories/gmap.v
@@ 254,15 +254,8 @@ Section filter.
∀ 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.
+ intros m k. rewrite eq_None_not_Some. unfold is_Some.
+ setoid_rewrite gmap_filter_lookup_Some. naive_solver.
Qed.
Lemma gmap_filter_dom m:
@@ 272,51 +265,37 @@ Section filter.
destruct 1 as [?[Eq _]%gmap_filter_lookup_Some]. by eexists.
Qed.
 Lemma gmap_filter_lookup_equiv `{Equiv A} `{Reflexive A (≡)} m1 m2:
+ Lemma gmap_filter_lookup_equiv m1 m2:
(∀ k v, P (k,v) → m1 !! k = Some v ↔ m2 !! k = Some v)
 → filter P m1 ≡ filter P m2.
+ → 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 [Hv2Hv2];
 [naive_solverby 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 [Hv1Hv1].
 + rewrite Hv1 in HP. naive_solver.
 + by apply HP, Hv1 in Hv2.
  by apply option_Forall2_refl.
+ intros HP. apply map_eq. intros k.
+ destruct (filter P m2 !! k) as [v2] eqn:Hv2;
+ [apply gmap_filter_lookup_Some in Hv2 as [Hv2 HP2];
+ specialize (HP k v2 HP2)
+ apply gmap_filter_lookup_None; right; intros v EqS ISP;
+ apply gmap_filter_lookup_None in Hv2 as [Hv2Hv2]].
+  apply gmap_filter_lookup_Some. by rewrite HP.
+  specialize (HP _ _ ISP). rewrite HP, Hv2 in EqS. naive_solver.
+  apply (Hv2 v); [by apply HPdone].
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).
+ Lemma gmap_filter_lookup_insert m k v:
+ P (k,v) → <[k := v]> (filter P m) = filter P (<[k := v]> m).
Proof.
 intros HP k'.
+ intros HP. apply map_eq. intros k'.
case (decide (k' = k)) as [>?];
[rewrite lookup_insertrewrite 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 _)).
+  symmetry. apply gmap_filter_lookup_Some. by rewrite lookup_insert.
 destruct (filter P (<[k:=v]> m) !! k') eqn: Hk; revert Hk;
 [rewrite gmap_filter_lookup_Somerewrite gmap_filter_lookup_None];
 (rewrite lookup_insert_ne ; [by auto]);
 [rewrite <gmap_filter_lookup_Somerewrite <gmap_filter_lookup_None];
 intros Hk; rewrite Hk; by apply option_Forall2_refl.
+ [rewrite gmap_filter_lookup_Some, lookup_insert_ne; [by auto];
+ by rewrite <gmap_filter_lookup_Some
+ rewrite gmap_filter_lookup_None, lookup_insert_ne; [auto];
+ by rewrite <gmap_filter_lookup_None].
Qed.
 Lemma gmap_filter_empty `{Equiv A} : filter P (∅ : gmap K A) ≡ ∅.
 Proof. intro l. rewrite lookup_empty. constructor. Qed.
+ Lemma gmap_filter_empty `{Equiv A} : filter P (∅ : gmap K A) = ∅.
+ Proof. apply map_fold_empty. Qed.
End filter.

GitLab
From 1b1a0296a3d6c57ecb8e52ff09e2f96465c7cfcf Mon Sep 17 00:00:00 2001
From: HoangHai Dang
Date: Thu, 28 Sep 2017 21:55:06 +0200
Subject: [PATCH 3/3] generalize filter from gmap to fin_map

theories/fin_map_dom.v  7 ++++
theories/fin_maps.v  64 +++++++++++++++++++++++++++++++++++
theories/gmap.v  75 
3 files changed, 71 insertions(+), 75 deletions()
diff git a/theories/fin_map_dom.v b/theories/fin_map_dom.v
index 5be84036..19d72b45 100644
 a/theories/fin_map_dom.v
+++ b/theories/fin_map_dom.v
@@ 19,6 +19,13 @@ Class FinMapDom K M D `{FMap M,
Section fin_map_dom.
Context `{FinMapDom K M D}.
+Lemma dom_map_filter {A} (P : K * A → Prop) `{!∀ x, Decision (P x)} (m : M A):
+ dom D (filter P m) ⊆ dom D m.
+Proof.
+ intros ?. rewrite 2!elem_of_dom.
+ destruct 1 as [?[Eq _]%map_filter_lookup_Some]. by eexists.
+Qed.
+
Lemma elem_of_dom_2 {A} (m : M A) i x : m !! i = Some x → i ∈ dom D m.
Proof. rewrite elem_of_dom; eauto. Qed.
Lemma not_elem_of_dom {A} (m : M A) i : i ∉ dom D m ↔ m !! i = None.
diff git a/theories/fin_maps.v b/theories/fin_maps.v
index 19a81607..79858b77 100644
 a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ 128,6 +128,9 @@ is unspecified. *)
Definition map_fold `{FinMapToList K A M} {B}
(f : K → A → B → B) (b : B) : M → B := foldr (curry f) b ∘ map_to_list.
+Instance map_filter `{FinMap K M} {A} : Filter (K * A) (M A) :=
+ λ P _, map_fold (λ k v m, if decide (P (k,v)) then <[k := v]>m else m) ∅.
+
(** * Theorems *)
Section theorems.
Context `{FinMap K M}.
@@ 984,6 +987,67 @@ Proof.
assert (m !! j = Some y) by (apply Hm; by right). naive_solver.
Qed.
+(** ** The filter operation *)
+Section map_Filter.
+ Context {A} (P : K * A → Prop) `{!∀ x, Decision (P x)}.
+
+ Lemma map_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 _)).
+  setoid_rewrite lookup_empty. 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 map_filter_lookup_None:
+ ∀ m k,
+ filter P m !! k = None ↔ m !! k = None ∨ ∀ v, m !! k = Some v → ¬ P (k,v).
+ Proof.
+ intros m k. rewrite eq_None_not_Some. unfold is_Some.
+ setoid_rewrite map_filter_lookup_Some. naive_solver.
+ Qed.
+
+ Lemma map_filter_lookup_equiv m1 m2:
+ (∀ k v, P (k,v) → m1 !! k = Some v ↔ m2 !! k = Some v)
+ → filter P m1 = filter P m2.
+ Proof.
+ intros HP. apply map_eq. intros k.
+ destruct (filter P m2 !! k) as [v2] eqn:Hv2;
+ [apply map_filter_lookup_Some in Hv2 as [Hv2 HP2];
+ specialize (HP k v2 HP2)
+ apply map_filter_lookup_None; right; intros v EqS ISP;
+ apply map_filter_lookup_None in Hv2 as [Hv2Hv2]].
+  apply map_filter_lookup_Some. by rewrite HP.
+  specialize (HP _ _ ISP). rewrite HP, Hv2 in EqS. naive_solver.
+  apply (Hv2 v); [by apply HPdone].
+ Qed.
+
+ Lemma map_filter_lookup_insert m k v:
+ P (k,v) → <[k := v]> (filter P m) = filter P (<[k := v]> m).
+ Proof.
+ intros HP. apply map_eq. intros k'.
+ case (decide (k' = k)) as [>?];
+ [rewrite lookup_insertrewrite lookup_insert_ne; [auto]].
+  symmetry. apply map_filter_lookup_Some. by rewrite lookup_insert.
+  destruct (filter P (<[k:=v]> m) !! k') eqn: Hk; revert Hk;
+ [rewrite map_filter_lookup_Some, lookup_insert_ne; [by auto];
+ by rewrite <map_filter_lookup_Some
+ rewrite map_filter_lookup_None, lookup_insert_ne; [auto];
+ by rewrite <map_filter_lookup_None].
+ Qed.
+
+ Lemma map_filter_empty : filter P ∅ = ∅.
+ Proof. apply map_fold_empty. Qed.
+
+End map_Filter.
+
(** ** Properties of the [map_Forall] predicate *)
Section map_Forall.
Context {A} (P : K → A → Prop).
diff git a/theories/gmap.v b/theories/gmap.v
index adb03cc2..4572c905 100644
 a/theories/gmap.v
+++ b/theories/gmap.v
@@ 225,81 +225,6 @@ 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.
 intros m k. rewrite eq_None_not_Some. unfold is_Some.
 setoid_rewrite gmap_filter_lookup_Some. naive_solver.
 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 m1 m2:
 (∀ k v, P (k,v) → m1 !! k = Some v ↔ m2 !! k = Some v)
 → filter P m1 = filter P m2.
 Proof.
 intros HP. apply map_eq. intros k.
 destruct (filter P m2 !! k) as [v2] eqn:Hv2;
 [apply gmap_filter_lookup_Some in Hv2 as [Hv2 HP2];
 specialize (HP k v2 HP2)
 apply gmap_filter_lookup_None; right; intros v EqS ISP;
 apply gmap_filter_lookup_None in Hv2 as [Hv2Hv2]].
  apply gmap_filter_lookup_Some. by rewrite HP.
  specialize (HP _ _ ISP). rewrite HP, Hv2 in EqS. naive_solver.
  apply (Hv2 v); [by apply HPdone].
 Qed.

 Lemma gmap_filter_lookup_insert m k v:
 P (k,v) → <[k := v]> (filter P m) = filter P (<[k := v]> m).
 Proof.
 intros HP. apply map_eq. intros k'.
 case (decide (k' = k)) as [>?];
 [rewrite lookup_insertrewrite lookup_insert_ne; [auto]].
  symmetry. apply gmap_filter_lookup_Some. by rewrite lookup_insert.
  destruct (filter P (<[k:=v]> m) !! k') eqn: Hk; revert Hk;
 [rewrite gmap_filter_lookup_Some, lookup_insert_ne; [by auto];
 by rewrite <gmap_filter_lookup_Some
 rewrite gmap_filter_lookup_None, lookup_insert_ne; [auto];
 by rewrite <gmap_filter_lookup_None].
 Qed.

 Lemma gmap_filter_empty `{Equiv A} : filter P (∅ : gmap K A) = ∅.
 Proof. apply map_fold_empty. Qed.

End filter.


(** * Fresh elements *)
(* This is pretty adhoc and just for the case of [gset positive]. We need a
notion of countable nonfinite types to generalize this. *)

GitLab