From 96184edb93791e05850e670d22570cdd26780dea Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 17 Jun 2016 01:40:14 +0200
Subject: [PATCH] Better statement of posivitity of option.

---
 algebra/cmra.v | 11 ++++-------
 algebra/gmap.v |  8 ++++----
 2 files changed, 8 insertions(+), 11 deletions(-)

diff --git a/algebra/cmra.v b/algebra/cmra.v
index 1b5323bb2..87f4f717b 100644
--- a/algebra/cmra.v
+++ b/algebra/cmra.v
@@ -1033,14 +1033,11 @@ Section option.
   (** Misc *)
   Global Instance Some_cmra_monotone : CMRAMonotone Some.
   Proof. split; [apply _|done|intros x y [z ->]; by exists (Some z)]. Qed.
+
+  Lemma op_None mx my : mx ⋅ my = None ↔ mx = None ∧ my = None.
+  Proof. destruct mx, my; naive_solver. Qed.
   Lemma op_is_Some mx my : is_Some (mx ⋅ my) ↔ is_Some mx ∨ is_Some my.
-  Proof.
-    destruct mx, my; rewrite /op /option_op /= -!not_eq_None_Some; naive_solver.
-  Qed.
-  Lemma option_op_positive_dist_l n mx my : mx ⋅ my ≡{n}≡ None → mx ≡{n}≡ None.
-  Proof. by destruct mx, my; inversion_clear 1. Qed.
-  Lemma option_op_positive_dist_r n mx my : mx ⋅ my ≡{n}≡ None → my ≡{n}≡ None.
-  Proof. by destruct mx, my; inversion_clear 1. Qed.
+  Proof. rewrite -!not_eq_None_Some op_None. destruct mx, my; naive_solver. Qed.
 
   Global Instance Some_persistent (x : A) : Persistent x → Persistent (Some x).
   Proof. by constructor. Qed.
diff --git a/algebra/gmap.v b/algebra/gmap.v
index 5b5c3bad8..c9858eba7 100644
--- a/algebra/gmap.v
+++ b/algebra/gmap.v
@@ -147,11 +147,11 @@ Proof.
     + destruct (m !! i) as [x|] eqn:Hx; rewrite !Hx /=; [|constructor].
       rewrite -Hx; apply (proj2_sig (f i)).
     + destruct (m !! i) as [x|] eqn:Hx; rewrite /=; [apply (proj2_sig (f i))|].
-      pose proof (Hm12' i) as Hm12''; rewrite Hx in Hm12''.
-      by symmetry; apply option_op_positive_dist_l with (m2 !! i).
+      move: (Hm12' i). rewrite Hx -!timeless_iff.
+      rewrite !(symmetry_iff _ None) !equiv_None op_None; tauto.
     + destruct (m !! i) as [x|] eqn:Hx; simpl; [apply (proj2_sig (f i))|].
-      pose proof (Hm12' i) as Hm12''; rewrite Hx in Hm12''.
-      by symmetry; apply option_op_positive_dist_r with (m1 !! i).
+      move: (Hm12' i). rewrite Hx -!timeless_iff.
+      rewrite !(symmetry_iff _ None) !equiv_None op_None; tauto.
 Qed.
 Canonical Structure gmapR :=
   CMRAT (gmap K A) gmap_cofe_mixin gmap_cmra_mixin.
-- 
GitLab