From 05c58b27f299d64404bd4b78b7c349f7a40c5bd4 Mon Sep 17 00:00:00 2001
From: Michael Sammler <noreply@sammler.me>
Date: Mon, 8 Aug 2022 16:33:35 +0200
Subject: [PATCH] Add _1, _2 lemmas for not_elem_of_dom and lookup_union_None

---
 theories/fin_map_dom.v | 4 ++++
 theories/fin_maps.v    | 6 ++++++
 2 files changed, 10 insertions(+)

diff --git a/theories/fin_map_dom.v b/theories/fin_map_dom.v
index 4da774f9..b956dce9 100644
--- a/theories/fin_map_dom.v
+++ b/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.
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 6331dde7..1ade48be 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -2273,6 +2273,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.
-- 
GitLab