From 6b6381fe41fc569057da2e3223d5f4b8b5048ae1 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 5 Aug 2016 00:14:59 +0200
Subject: [PATCH] Use rvs in counter_example and integrate with adequacy to
 obtain False.

---
 program_logic/counter_examples.v | 21 ++++++++++++---------
 1 file changed, 12 insertions(+), 9 deletions(-)

diff --git a/program_logic/counter_examples.v b/program_logic/counter_examples.v
index 34795155f..4c6dc9c69 100644
--- a/program_logic/counter_examples.v
+++ b/program_logic/counter_examples.v
@@ -2,8 +2,7 @@ From iris.algebra Require Import upred.
 From iris.proofmode Require Import tactics.
 
 (** This proves that we need the â–· in a "Saved Proposition" construction with
-    name-dependend allocation. *)
-(** We fork in [uPred M] for any M, but the proof would work in any BI. *)
+name-dependend allocation. *)
 Section savedprop.
   Context (M : ucmraT).
   Notation iProp := (uPred M).
@@ -11,11 +10,10 @@ Section savedprop.
   Implicit Types P : iProp.
 
   (* Saved Propositions and view shifts. *)
-  Context (sprop : Type) (saved : sprop → iProp → iProp) (pvs : iProp → iProp).
-  Hypothesis pvs_mono : ∀ P Q, (P ⊢ Q) → pvs P ⊢ pvs Q.
+  Context (sprop : Type) (saved : sprop → iProp → iProp).
   Hypothesis sprop_persistent : ∀ i P, PersistentP (saved i P).
   Hypothesis sprop_alloc_dep :
-    ∀ (P : sprop → iProp), True ⊢ pvs (∃ i, saved i (P i)).
+    ∀ (P : sprop → iProp), True =r=> (∃ i, saved i (P i)).
   Hypothesis sprop_agree : ∀ i P Q, saved i P ∧ saved i Q ⊢ P ↔ Q.
 
   (* Self-contradicting assertions are inconsistent *)
@@ -44,14 +42,19 @@ Section savedprop.
   Proof. iIntros "#HQ !". by iApply (saved_is_A i (¬A i)). Qed.
 
   (* We can obtain such a [Q i]. *)
-  Lemma make_Q : True ⊢ pvs (∃ i, Q i).
+  Lemma make_Q : True =r=> ∃ i, Q i.
   Proof. apply sprop_alloc_dep. Qed.
 
   (* Put together all the pieces to derive a contradiction. *)
-  (* TODO: Have a lemma in upred.v that says that we cannot view shift to False. *)
-  Lemma contradiction : True ⊢ pvs False.
+  Lemma rvs_false : (True : uPred M) =r=> False.
   Proof.
-    rewrite make_Q. apply pvs_mono. iDestruct 1 as (i) "HQ".
+    rewrite make_Q. apply uPred.rvs_mono. iDestruct 1 as (i) "HQ".
     iApply (no_self_contradiction (A i)). by iApply Q_self_contradiction.
   Qed.
+
+  Lemma contradiction : False.
+  Proof.
+    apply (@uPred.adequacy M False 1); simpl.
+    rewrite -uPred.later_intro. apply rvs_false.
+  Qed.
 End savedprop.
-- 
GitLab