Non step-indexed laws about exclusive and Some.

2227cd66 · Robbert Krebbers · d47d99dd · 2227cd66
Commit 2227cd66 authored Oct 03, 2016 by Robbert Krebbers
Hide whitespace changes
Inline Side-by-side

Showing with 5 additions and 0 deletions

algebra/cmra.v algebra/cmra.v +5 -0

No files found.
--- a/algebra/cmra.v
+++ b/algebra/cmra.v
@@ -1201,6 +1201,11 @@ Section option.
    ✓{n} (my ⋅ Some x) → my = None.
  Proof. rewrite comm. by apply exclusiveN_Some_l. Qed.

+  Lemma exclusive_Some_l x `{!Exclusive x} my : ✓ (Some x ⋅ my) → my = None.
+  Proof. destruct my. move=> /(exclusive_l x) []. done. Qed.
+  Lemma exclusive_Some_r x `{!Exclusive x} my : ✓ (my ⋅ Some x) → my = None.
+  Proof. rewrite comm. by apply exclusive_Some_l. Qed.
+
  Lemma Some_included x y : Some x ≼ Some y ↔ x ≡ y ∨ x ≼ y.
  Proof. rewrite option_included; naive_solver. Qed.
  Lemma Some_included' `{CMRATotal A} x y : Some x ≼ Some y ↔ x ≡ y ∨ x ≼ y.