From 1c8276cb35d06680cfd8b390b018ff6b4d1206e9 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 16 Jan 2016 01:29:43 +0100
Subject: [PATCH] More option properties.

---
 modures/option.v | 16 ++++++++++++++--
 prelude/option.v |  2 ++
 2 files changed, 16 insertions(+), 2 deletions(-)

diff --git a/modures/option.v b/modures/option.v
index e227ffc47..256331bfa 100644
--- a/modures/option.v
+++ b/modures/option.v
@@ -45,6 +45,10 @@ Qed.
 Canonical Structure optionC := CofeT option_cofe_mixin.
 Global Instance Some_ne : Proper (dist n ==> dist n) (@Some A).
 Proof. by constructor. Qed.
+Global Instance is_Some_ne n : Proper (dist (S n) ==> iff) (@is_Some A).
+Proof. inversion_clear 1; split; eauto. Qed.
+Global Instance Some_dist_inj : Injective (dist n) (dist n) (@Some A).
+Proof. by inversion_clear 1. Qed.
 Global Instance None_timeless : Timeless (@None A).
 Proof. inversion_clear 1; constructor. Qed.
 Global Instance Some_timeless x : Timeless x → Timeless (Some x).
@@ -56,8 +60,7 @@ Arguments optionC : clear implicits.
 Instance option_fmap_ne {A B : cofeT} (f : A → B) n:
   Proper (dist n ==> dist n) f → Proper (dist n==>dist n) (fmap (M:=option) f).
 Proof. by intros Hf; destruct 1; constructor; apply Hf. Qed.
-Instance is_Some_ne `{A : cofeT} : Proper (dist (S n) ==> iff) (@is_Some A).
-Proof. intros n; inversion_clear 1; split; eauto. Qed.
+
 
 (* CMRA *)
 Section cmra.
@@ -95,6 +98,11 @@ Proof.
       try (by exists my; destruct my; constructor).
     by exists (Some z); constructor.
 Qed.
+Lemma None_includedN n (mx : option A) : None ≼{n} mx.
+Proof. rewrite option_includedN; auto. Qed.
+Lemma Some_Some_includedN n (x y : A) : x ≼{n} y → Some x ≼{n} Some y.
+Proof. rewrite option_includedN; eauto 10. Qed.
+
 Definition option_cmra_mixin  : CMRAMixin (option A).
 Proof.
   split.
@@ -138,6 +146,10 @@ Qed.
 Canonical Structure optionRA :=
   CMRAT option_cofe_mixin option_cmra_mixin option_cmra_extend_mixin.
 
+Lemma op_is_Some x y : is_Some (x ⋅ y) ↔ is_Some x ∨ is_Some y.
+Proof.
+  destruct x, y; rewrite /op /option_op /= -!not_eq_None_Some; naive_solver.
+Qed.
 Lemma option_op_positive_dist_l n x y : x ⋅ y ={n}= None → x ={n}= None.
 Proof. by destruct x, y; inversion_clear 1. Qed.
 Lemma option_op_positive_dist_r n x y : x ⋅ y ={n}= None → y ={n}= None.
diff --git a/prelude/option.v b/prelude/option.v
index 237194c24..865311fdc 100644
--- a/prelude/option.v
+++ b/prelude/option.v
@@ -107,6 +107,8 @@ Section setoids.
   Lemma equiv_Some (mx my : option A) x :
     mx ≡ my → mx = Some x → ∃ y, my = Some y ∧ x ≡ y.
   Proof. destruct 1; naive_solver. Qed.
+  Global Instance is_Some_proper : Proper ((≡) ==> iff) (@is_Some A).
+  Proof. inversion_clear 1; split; eauto. Qed.
 End setoids.
 
 (** Equality on [option] is decidable. *)
-- 
GitLab