Make `union_Some` a ``, add `union_None` and `union_is_Some`.

This makes it more consistent with other Some lemmas, that are also bidirectional.

See also the discussion !466 (comment 91517)

The change to union_Some is not backwards compatible, so we need to either provide a new lemma (with a new name, but what?) for the → direction, or we need to update existing code. It's not clear to me how much union_Some is used in reverse dependencies.

stdpp/option.v

@@ -297,7 +297,7 @@ Global Instance option_difference_with {A} : DifferenceWith A (option A) := λ f
 Global Instance option_union {A} : Union (option A) := union_with (λ x _, Some x).
 
 Lemma union_Some {A} (mx my : option A) z :
-  mx ∪ my = Some z → mx = Some z ∨ my = Some z.
+  mx ∪ my = Some z ↔ mx = Some z ∨ (mx = None ∧ my = Some z).
 Proof. destruct mx, my; naive_solver. Qed.
 Lemma union_Some_l {A} x (my : option A) :
   Some x ∪ my = Some x.
@@ -305,6 +305,12 @@ Proof. destruct my; done. Qed.
 Lemma union_Some_r {A} (mx : option A) y :
   mx ∪ Some y = Some (default y mx).
 Proof. destruct mx; done. Qed.
+Lemma union_None {A} (mx my : option A) :
+  mx ∪ my = None ↔ mx = None ∧ my = None.
+Proof. destruct mx, my; naive_solver. Qed.
+Lemma union_is_Some {A} (mx my : option A) :
+  is_Some (mx ∪ my) ↔ is_Some mx ∨ is_Some my.
+Proof. destruct mx, my; naive_solver. Qed.
 
 Global Instance option_union_left_id {A} : LeftId (=@{option A}) None union.
 Proof. by intros [?|]. Qed.