Use rvs in counter_example and integrate with adequacy to obtain False.

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.