Add filter for gmap
A filter for (M : gmap K A) creates a submap of M whose (key,value) pairs satisfy the filter predicate (P : K * A → Prop).
Merge request reports
Activity
262 + rewrite 2!lookup_insert. naive_solver. 263 + do 2 (rewrite lookup_insert_ne; [|auto]). by apply Eq. 264 + rewrite Eq, Hm, lookup_insert. naive_solver. 265 + by rewrite lookup_insert_ne. 266 Qed. 267 268 Lemma gmap_filter_dom m: 269 dom (gset K) (filter P m) ⊆ dom (gset K) m. 270 Proof. 271 intros ?. rewrite 2!elem_of_dom. 272 destruct 1 as [?[Eq _]%gmap_filter_lookup_Some]. by eexists. 273 Qed. 274 275 Lemma gmap_filter_lookup_equiv `{Equiv A} `{Reflexive A (≡)} m1 m2: 276 (∀ k v, P (k,v) → m1 !! k = Some v ↔ m2 !! k = Some v) 277 → filter P m1 ≡ filter P m2. changed this line in version 2 of the diff
283 destruct (filter P m2 !! k) as [v2|] eqn: Hv2. 284 - apply gmap_filter_lookup_Some in Hv2 as [Hv2 _]. 285 rewrite Hv1, Hv2 in HP. destruct HP as [HP _]. 286 specialize (HP (eq_refl _)) as []. by apply option_Forall2_refl. 287 - apply gmap_filter_lookup_None in Hv2 as [Hv2|Hv2]; 288 [naive_solver|by apply HP, Hv2 in Hv1]. 289 - apply gmap_filter_lookup_Some in Hv2 as [Hv2 HP2]. 290 specialize (HP k v2 HP2). 291 apply gmap_filter_lookup_None in Hv1 as [Hv1|Hv1]. 292 + rewrite Hv1 in HP. naive_solver. 293 + by apply HP, Hv1 in Hv2. 294 - by apply option_Forall2_refl. 295 Qed. 296 297 Lemma gmap_filter_lookup_insert `{Equiv A} `{Reflexive A (≡)} m k v: 298 P (k,v) → <[k := v]> (filter P m) ≡ filter P (<[k := v]> m). changed this line in version 2 of the diff
304 + apply gmap_filter_lookup_Some in Hk. 305 rewrite lookup_insert in Hk. destruct Hk as [Hk _]. 306 inversion Hk. by apply option_Forall2_refl. 307 + apply gmap_filter_lookup_None in Hk. 308 rewrite lookup_insert in Hk. 309 destruct Hk as [->|HNP]. by apply option_Forall2_refl. 310 by specialize (HNP v (eq_refl _)). 311 - destruct (filter P (<[k:=v]> m) !! k') eqn: Hk; revert Hk; 312 [rewrite gmap_filter_lookup_Some|rewrite gmap_filter_lookup_None]; 313 (rewrite lookup_insert_ne ; [|by auto]); 314 [rewrite <-gmap_filter_lookup_Some|rewrite <-gmap_filter_lookup_None]; 315 intros Hk; rewrite Hk; by apply option_Forall2_refl. 316 Qed. 317 318 Lemma gmap_filter_empty `{Equiv A} : filter P (∅ : gmap K A) ≡ ∅. 319 Proof. intro l. rewrite lookup_empty. constructor. Qed. changed this line in version 2 of the diff
251 Qed. 252 253 Lemma gmap_filter_lookup_None: 254 ∀ m k, 255 filter P m !! k = None ↔ m !! k = None ∨ ∀ v, m !! k = Some v → ¬ P (k,v). 256 Proof. 257 apply (map_fold_ind (λ m1 m2, ∀ k, m1 !! k = None 258 ↔ (m2 !! k = None ∨ ∀ v, m2 !! k = Some v → ¬ P _))). 259 - naive_solver. 260 - intros k v m m' Hm Eq k'. 261 case_match; case (decide (k' = k)) as [->|?]. 262 + rewrite 2!lookup_insert. naive_solver. 263 + do 2 (rewrite lookup_insert_ne; [|auto]). by apply Eq. 264 + rewrite Eq, Hm, lookup_insert. naive_solver. 265 + by rewrite lookup_insert_ne. 266 Qed. changed this line in version 3 of the diff
I have simplified the proofs and generalized them to
fin_maps.Great, thanks!
Still I have a problem with
dom_map_filter: I can't derive from it the instance for gmap. Somehow the typeclasses do not match, but I haven't figure out which one.Do you have a small example demonstrating the problem, then I'll take a look.
I was trying to prove this lemma using the
dom_map_filter:Lemma dom_gmap_filter `{Countable K} {A} (P: K * A → Prop) `{∀ x, Decision (P x)} (m: gmap K A): dom (gset K) (filter P m) ⊆ dom (gset K) m. Proof. by apply dom_map_filter. Qed.applyfails (even with more annotation) because it cannot unify the FinMap instances in the goal (gmap_finmap) and in the lemma (a projection ofgmap_finmapthroughgset_dom_specandfinmap_dom_map).refine (dom_map_filter P m)works though.mentioned in commit 29f26e4e
Fixed in 29f26e4e and merged :) Thanks for the MR!
