From bc61b7a53d6075233589ac4a454ec67c479da263 Mon Sep 17 00:00:00 2001 From: Hoang-Hai 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 [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. *) -- GitLab From 8ed74c3a3f43a6ef430c4ef83ebf9255bfe8fd03 Mon Sep 17 00:00:00 2001 From: Hoang-Hai 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 [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. + 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 [Hv2|Hv2]]. + - apply gmap_filter_lookup_Some. by rewrite HP. + - specialize (HP _ _ ISP). rewrite HP, Hv2 in EqS. naive_solver. + - apply (Hv2 v); [by apply HP|done]. 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_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 _)). + - 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|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. + [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: Hoang-Hai 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 [Hv2|Hv2]]. + - apply map_filter_lookup_Some. by rewrite HP. + - specialize (HP _ _ ISP). rewrite HP, Hv2 in EqS. naive_solver. + - apply (Hv2 v); [by apply HP|done]. + 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_insert|rewrite 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 [Hv2|Hv2]]. - - apply gmap_filter_lookup_Some. by rewrite HP. - - specialize (HP _ _ ISP). rewrite HP, Hv2 in EqS. naive_solver. - - apply (Hv2 v); [by apply HP|done]. - 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_insert|rewrite 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 ad-hoc and just for the case of [gset positive]. We need a notion of countable non-finite types to generalize this. *) -- GitLab