diff --git a/theories/fin_maps.v b/theories/fin_maps.v index 6c7270a3ed045d669e8f43273c957bdc544a653d..2465f3b52a535c5847ffe8a86efbfdbebcb5d0ba 100644 --- a/theories/fin_maps.v +++ b/theories/fin_maps.v @@ -1081,13 +1081,18 @@ Section map_filter. naive_solver. Qed. - Lemma map_filter_insert_not m i x : - (∀ y, ¬ P (i, y)) → filter P (<[i:=x]> m) = filter P m. + Lemma map_filter_insert_not' m i x : + ¬ P (i, x) → (∀ y, m !! i = Some y → ¬ P (i, y)) → + filter P (<[i:=x]> m) = filter P m. Proof. - intros HP. apply map_filter_lookup_eq. intros j y Hy. - by rewrite lookup_insert_ne by naive_solver. + intros Hx HP. apply map_filter_lookup_eq. intros j y Hy. + rewrite lookup_insert_Some. naive_solver. Qed. + Lemma map_filter_insert_not m i x : + (∀ y, ¬ P (i, y)) → filter P (<[i:=x]> m) = filter P m. + Proof. intros HP. by apply map_filter_insert_not'. Qed. + Lemma map_filter_delete m i : filter P (delete i m) = delete i (filter P m). Proof. apply map_eq. intros j. apply option_eq; intros y. @@ -1106,6 +1111,16 @@ Section map_filter. Lemma map_filter_empty : filter P (∅ : M A) = ∅. Proof. apply map_fold_empty. Qed. + + Lemma map_filter_alt m : filter P m = list_to_map (filter P (map_to_list m)). + Proof. + apply list_to_map_flip. induction m as [|k x m ? IH] using map_ind. + { by rewrite map_to_list_empty, map_filter_empty, map_to_list_empty. } + rewrite map_to_list_insert, filter_cons by done. destruct (decide (P _)). + - rewrite map_filter_insert by done. + by rewrite map_to_list_insert, IH by (rewrite map_filter_lookup_None; auto). + - by rewrite map_filter_insert_not' by naive_solver. + Qed. End map_filter. (** ** Properties of the [map_Forall] predicate *) diff --git a/theories/gmap.v b/theories/gmap.v index c98df62b9e2536e103f66408290b6c57646fbbeb..2edcb42d67b878e4a8177be589d69a9915c064ae 100644 --- a/theories/gmap.v +++ b/theories/gmap.v @@ -279,6 +279,13 @@ Section gset. - by rewrite option_guard_True by (rewrite elem_of_dom; eauto). - by rewrite option_guard_False by (rewrite not_elem_of_dom; eauto). Qed. + Lemma dom_gset_to_gmap {A} (X : gset K) (x : A) : + dom _ (gset_to_gmap x X) = X. + Proof. + induction X as [| y X not_in IH] using set_ind_L. + - rewrite gset_to_gmap_empty, dom_empty_L; done. + - rewrite gset_to_gmap_union_singleton, dom_insert_L, IH; done. + Qed. End gset. Typeclasses Opaque gset. diff --git a/theories/list.v b/theories/list.v index 994917a015971bf5e132d317202d0044d19092e5..6b9f7b18e9c5040dd2621d53c9b72cf17096414f 100644 --- a/theories/list.v +++ b/theories/list.v @@ -668,6 +668,42 @@ Proof. revert i j. induction k; intros i j ?; simpl; rewrite 1?list_insert_commute by lia; auto with f_equal. Qed. +Lemma list_inserts_app_l l1 l2 l3 i : + list_inserts i (l1 ++ l2) l3 = list_inserts (length l1 + i) l2 (list_inserts i l1 l3). +Proof. + revert l1 i; induction l1 as [|x l1 IH]; [done|]. + intro i. simpl. rewrite IH, Nat.add_succ_r. apply list_insert_inserts_lt. lia. +Qed. +Lemma list_inserts_app_r l1 l2 l3 i : + list_inserts (length l2 + i) l1 (l2 ++ l3) = l2 ++ list_inserts i l1 l3. +Proof. + revert l1 i; induction l1 as [|x l1 IH]; [done|]. + intros i. simpl. by rewrite plus_n_Sm, IH, insert_app_r. +Qed. +Lemma list_inserts_nil l1 i : list_inserts i l1 [] = []. +Proof. + revert i; induction l1 as [|x l1 IH]; [done|]. + intro i. simpl. by rewrite IH. +Qed. +Lemma list_inserts_cons l1 l2 i x : + list_inserts (S i) l1 (x :: l2) = x :: list_inserts i l1 l2. +Proof. + revert i; induction l1 as [|y l1 IH]; [done|]. + intro i. simpl. by rewrite IH. +Qed. +Lemma list_inserts_0_r l1 l2 l3 : + length l1 = length l2 → list_inserts 0 l1 (l2 ++ l3) = l1 ++ l3. +Proof. + revert l2. induction l1 as [|x l1 IH]; intros [|y l2] ?; simplify_eq/=; [done|]. + rewrite list_inserts_cons. simpl. by rewrite IH. +Qed. +Lemma list_inserts_0_l l1 l2 l3 : + length l1 = length l3 → list_inserts 0 (l1 ++ l2) l3 = l1. +Proof. + revert l3. induction l1 as [|x l1 IH]; intros [|z l3] ?; simplify_eq/=. + { by rewrite list_inserts_nil. } + rewrite list_inserts_cons. simpl. by rewrite IH. +Qed. (** ** Properties of the [elem_of] predicate *) Lemma not_elem_of_nil x : x ∉ [].