Add some _1, _2 lemmas

theories/fin_map_dom.v

@@ -42,6 +42,10 @@ Lemma elem_of_dom_2 {A} (m : M A) i x : m !! i = Some x → i ∈ dom m.
 Proof. rewrite elem_of_dom; eauto. Qed.
 Lemma not_elem_of_dom {A} (m : M A) i : i ∉ dom m ↔ m !! i = None.
 Proof. by rewrite elem_of_dom, eq_None_not_Some. Qed.
+Lemma not_elem_of_dom_1 {A} (m : M A) i : i ∉ dom m → m !! i = None.
+Proof. apply not_elem_of_dom. Qed.
+Lemma not_elem_of_dom_2 {A} (m : M A) i : m !! i = None → i ∉ dom m.
+Proof. apply not_elem_of_dom. Qed.
 Lemma subseteq_dom {A} (m1 m2 : M A) : m1 ⊆ m2 → dom m1 ⊆ dom m2.
 Proof.
   rewrite map_subseteq_spec.

theories/fin_maps.v

@@ -1385,6 +1385,14 @@ Section map_filter.
     - intros Hm i. destruct (m !! i) as [x|] eqn:?; [|by auto].
       right; intros ? [= <-]. by apply Hm.
   Qed.
+  Lemma map_filter_empty_iff_1 m :
+    filter P m = ∅ →
+    map_Forall (λ i x, ¬P (i,x)) m.
+  Proof. apply map_filter_empty_iff. Qed.
+  Lemma map_filter_empty_iff_2 m :
+    map_Forall (λ i x, ¬P (i,x)) m →
+    filter P m = ∅.
+  Proof. apply map_filter_empty_iff. Qed.
 
   Lemma map_filter_delete m i : filter P (delete i m) = delete i (filter P m).
   Proof.
@@ -2273,6 +2281,12 @@ Proof. rewrite lookup_union. destruct (m1 !! i), (m2 !! i); naive_solver. Qed.
 Lemma lookup_union_None {A} (m1 m2 : M A) i :
   (m1 ∪ m2) !! i = None ↔ m1 !! i = None ∧ m2 !! i = None.
 Proof. rewrite lookup_union.  destruct (m1 !! i), (m2 !! i); naive_solver. Qed.
+Lemma lookup_union_None_1 {A} (m1 m2 : M A) i :
+  (m1 ∪ m2) !! i = None → m1 !! i = None ∧ m2 !! i = None.
+Proof. apply lookup_union_None. Qed.
+Lemma lookup_union_None_2 {A} (m1 m2 : M A) i :
+  m1 !! i = None → m2 !! i = None → (m1 ∪ m2) !! i = None.
+Proof. intros. by apply lookup_union_None. Qed.
 Lemma lookup_union_Some {A} (m1 m2 : M A) i x :
   m1 ##ₘ m2 → (m1 ∪ m2) !! i = Some x ↔ m1 !! i = Some x ∨ m2 !! i = Some x.
 Proof.