Merge branch 'robbert/option_union' into 'master'

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

See merge request !472

CHANGELOG.md

@@ -30,7 +30,6 @@ longer supported by this release.
   `submseteq_Permutation_length_eq`; use `submseteq_length_Permutation` instead.
 - Remove `map_to_list_length` (which seemed to be an unneeded auxiliary lemma);
   use `map_subset_size` instead.
-- Rename `option_union_Some` → `union_Some`.
 - Rename `prefix_lookup` → `prefix_lookup_Some`.
 - Extend `set_solver` with support for `set_Forall` and `set_Exists`.
 - Change `lookup_union` lemma statement to use `∪` on maps instead of `union_with`.
@@ -50,6 +49,8 @@ longer supported by this release.
   uses of `≡`.
 - Set `intuition_solver ::= auto` (the default is `auto with *`) instead of
   redeclaring `intuition`.
+- Rename `option_union_Some` → `union_Some`, and strengthen it to become a
+  biimplication.
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).

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.