From 0a05a8c0b22b31f94e31e510c467800ea2dfc1f2 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 11 Jun 2019 14:50:31 +0200
Subject: [PATCH] show that owning a prophecy is exclusive

---
 theories/base_logic/lib/proph_map.v | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/theories/base_logic/lib/proph_map.v b/theories/base_logic/lib/proph_map.v
index c1a990384..f4ead7f01 100644
--- a/theories/base_logic/lib/proph_map.v
+++ b/theories/base_logic/lib/proph_map.v
@@ -128,6 +128,18 @@ Section proph_map.
   Global Instance proph_timeless p vs : Timeless (proph p vs).
   Proof. rewrite proph_eq /proph_def. apply _. Qed.
 
+  Lemma proph_exclusive p vs1 vs2 :
+    proph p vs1 -∗ proph p vs2 -∗ False.
+  Proof.
+    rewrite proph_eq /proph_def. iIntros "Hp1 Hp2".
+    iCombine "Hp1 Hp2" as "Hp".
+    iDestruct (own_valid with "Hp") as %Hp.
+    (* FIXME: [apply auth_frag_valid in Hp] and
+       [rewrite ->auth_frag_valid in Hp] both should work but do not. *)
+    move:Hp. rewrite auth_frag_valid singleton_valid=>Hp.
+    done.
+  Qed.
+
   Lemma proph_map_new_proph p ps pvs :
     p ∉ ps →
     proph_map_ctx pvs ps ==∗
-- 
GitLab