Commit c809b3b5 by Hai Dang Committed by Robbert Krebbers

parent 2175e39f
 ... ... @@ -227,6 +227,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. *) ... ...
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!