From 66520de3a1c59027d4b5959e0ca9116675540f37 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 13 Dec 2022 15:22:27 +0100
Subject: [PATCH] add some option union lemmas, and use it in lookup_union

---
 stdpp/fin_maps.v |  2 +-
 stdpp/option.v   | 19 +++++++++++++++++++
 2 files changed, 20 insertions(+), 1 deletion(-)

diff --git a/stdpp/fin_maps.v b/stdpp/fin_maps.v
index 8056df97..5adad1a9 100644
--- a/stdpp/fin_maps.v
+++ b/stdpp/fin_maps.v
@@ -2301,7 +2301,7 @@ Qed.
 Global Instance map_union_idemp {A} : IdemP (=@{M A}) (∪).
 Proof. intros ?. by apply union_with_idemp. Qed.
 Lemma lookup_union {A} (m1 m2 : M A) i :
-  (m1 ∪ m2) !! i = union_with (λ x _, Some x) (m1 !! i) (m2 !! i).
+  (m1 ∪ m2) !! i = (m1 !! i) ∪ (m2 !! i).
 Proof. apply lookup_union_with. Qed.
 Lemma lookup_union_r {A} (m1 m2 : M A) i :
   m1 !! i = None → (m1 ∪ m2) !! i = m2 !! i.
diff --git a/stdpp/option.v b/stdpp/option.v
index 0189d77e..4e4662d0 100644
--- a/stdpp/option.v
+++ b/stdpp/option.v
@@ -299,6 +299,17 @@ Global Instance option_union {A} : Union (option A) := union_with (λ x _, Some
 Lemma option_union_Some {A} (mx my : option A) z :
   mx ∪ my = Some z → mx = Some z ∨ my = Some z.
 Proof. destruct mx, my; naive_solver. Qed.
+Lemma option_union_Some_l {A} x (my : option A) :
+  (Some x) ∪ my = Some x.
+Proof. destruct my; done. Qed.
+Lemma option_union_Some_r {A} (mx : option A) y :
+  mx ∪ (Some y) = Some (default y mx).
+Proof. destruct mx; done. Qed.
+
+Global Instance option_union_left_id {A} : LeftId (=@{option A}) None union.
+Proof. by intros [?|]. Qed.
+Global Instance option_union_right_id {A} : RightId (=@{option A}) None union.
+Proof. by intros [?|]. Qed.
 
 Section union_intersection_difference.
   Context {A} (f : A → A → option A).
@@ -310,10 +321,18 @@ Section union_intersection_difference.
   Global Instance union_with_comm :
     Comm (=) f → Comm (=@{option A}) (union_with f).
   Proof. by intros ? [?|] [?|]; compute; rewrite 1?(comm f). Qed.
+  (* These are duplicates of the above LeftId/RightId instances, but easier to
+  find with SearchAbout. *)
+  Lemma union_with_None_l my : union_with f None my = my.
+  Proof. destruct my; done. Qed.
+  Lemma union_with_None_r mx : union_with f mx None = mx.
+  Proof. destruct mx; done. Qed.
+
   Global Instance intersection_with_left_ab : LeftAbsorb (=) None (intersection_with f).
   Proof. by intros [?|]. Qed.
   Global Instance intersection_with_right_ab : RightAbsorb (=) None (intersection_with f).
   Proof. by intros [?|]. Qed.
+
   Global Instance difference_with_comm :
     Comm (=) f → Comm (=@{option A}) (intersection_with f).
   Proof. by intros ? [?|] [?|]; compute; rewrite 1?(comm f). Qed.
-- 
GitLab