vastly simplify the counterexample

program_logic/counter_examples.v

@@ -90,36 +90,22 @@ Module inv. Section inv.
   Hypothesis inv_open :
     forall i P Q R, (P ★ Q ⊢ pvs0 (P ★ R)) → (inv i P ★ Q ⊢ pvs1 R).
 
-  (* We have tokens for a little "three-state STS": [fresh] -> [start n] ->
-     [finish n].  The [auth_*] tokens are in the invariant and assert an exact
-     state. [fresh] also asserts the exact state; it is owned by threads (i.e.,
-     there's a token needed to transition to [start].)  [started] and [finished]
-     are *lower bounds*. We don't need "auth_finish" because the state will
-     never change again, so [finished] is just as good. *)
-  Context (auth_fresh fresh : iProp).
-  Context (auth_start started finished : name → iProp).
-  Hypothesis fresh_start :
-    forall n, auth_fresh ★ fresh ⊢ pvs0 (auth_start n ★ started n).
-  Hypotheses start_finish :
-    forall n, auth_start n ⊢ pvs0 (finished n).
-
-  Hypothesis fresh_not_start : forall n, auth_start n ★ fresh ⊢ False.
-  Hypothesis fresh_not_finished : forall n, finished n ★ fresh ⊢ False.
-  Hypothesis started_not_fresh : forall n, auth_fresh ★ started n ⊢ False.
-  Hypothesis finished_not_start : forall n m, auth_start n ★ finished m ⊢ False.
-
-  Hypothesis started_start_agree : forall n m, auth_start n ★ started m ⊢ n = m.
-  Hypothesis started_finished_agree :
-    forall n m, finished n ★ started m ⊢ n = m.
-  Hypothesis finished_agree :
-    forall n m, finished n ★ finished m ⊢ n = m.
-
-  Hypothesis started_dup : forall n, started n ⊢ started n ★ started n.
-  Hypothesis finished_dup : forall n, finished n ⊢ finished n ★ finished n.
+  (* We have tokens for a little "two-state STS": [start] -> [finish].
+     state. [start] also asserts the exact state; it is only ever owned by the
+     invariant.  [finished] is duplicable. *)
+  Context (gname : Type).
+  Context (start finished : gname → iProp).
+
+  Hypothesis sts_alloc : True ⊢ pvs0 (∃ γ, start γ).
+  Hypotheses start_finish : forall γ, start γ ⊢ pvs0 (finished γ).
+
+  Hypothesis finished_not_start : forall γ, start γ ★ finished γ ⊢ False.
+
+  Hypothesis finished_dup : forall γ, finished γ ⊢ finished γ ★ finished γ.
 
   (* We have that we cannot view shift from the initial state to false
      (because the initial state is actually achievable). *)
-  Hypothesis soundness : ¬ (auth_fresh ★ fresh ⊢ pvs1 False).
+  Hypothesis soundness : ¬ (True ⊢ pvs1 False).
 
   (** Some general lemmas and proof mode compatibility. *)
   Lemma inv_open' i P R:
@@ -191,144 +177,73 @@ Module inv. Section inv.
     apply pvs1_mono. by rewrite -HP -(uPred.exist_intro a).
   Qed.
 
-  (* "Weak box" -- a weak form of □ for non-persistent assertions. *)
-  Definition wbox P : iProp :=
-    ∃ Q, Q ★ □(Q → P) ★ □(Q → Q ★ Q).
-
-  Lemma wbox_dup P :
-    wbox P ⊢ wbox P ★ wbox P.
-  Proof.
-    iIntros "H". iDestruct "H" as (Q) "(HQ & #HP & #Hdup)".
-    iDestruct ("Hdup" with "HQ") as "[HQ HQ']".
-    iSplitL "HQ"; iExists Q; iSplit; eauto.
-  Qed.
-
-  Lemma wbox_out P :
-    wbox P ⊢ P.
-  Proof.
-    iIntros "H". iDestruct "H" as (Q) "(HQ & #HP & _)".
-    iApply "HP". done.
-  Qed.
-
   (** Now to the actual counterexample. We start with a weird for of saved propositions. *)
-  Definition saved (i : name) (P : iProp) : iProp :=
-    ∃ F : name → iProp, P = F i ★ started i ★
-      inv i (auth_fresh ∨ ∃ j, auth_start j ∨ (finished j ★ wbox (F j))).
+  Definition saved (γ : gname) (P : iProp) : iProp :=
+    ∃ i, inv i (start γ ∨ (finished γ ★ □P)).
+  Global Instance : forall γ P, PersistentP (saved γ P) := _.
 
-  Lemma saved_dup i P :
-    saved i P ⊢ saved i P ★ saved i P.
+  Lemma saved_alloc (P : gname → iProp) :
+    True ⊢ pvs1 (∃ γ, saved γ (P γ)).
   Proof.
-    iIntros "H". iDestruct "H" as (F) "(#? & Hs & #?)".
-    iDestruct (started_dup with "Hs") as "[Hs Hs']". iSplitL "Hs".
-    - iExists F. eauto.
-    - iExists F. eauto.
-  Qed.
-
-  Lemma saved_alloc (P : name → iProp) :
-    auth_fresh ★ fresh ⊢ pvs1 (∃ i, saved i (P i)).
-  Proof.
-    iIntros "[Haf Hf]". iVs (inv_alloc (auth_fresh ∨ ∃ j, auth_start j ∨ (finished j ★ wbox (P j))) with "[Haf]") as (i) "#Hi".
+    iIntros "". iVs (sts_alloc) as (γ) "Hs".
+    iVs (inv_alloc (start γ ∨ (finished γ ★ □ (P γ))) with "[Hs]") as (i) "#Hi".
     { iLeft. done. }
-    iExists i. iApply inv_open'. iSplit; first done. iIntros "[Haf|Has]"; last first.
-    { iExFalso. iDestruct "Has" as (j) "[Has | [Haf _]]".
-      - iApply fresh_not_start. iSplitL "Has"; done.
-      - iApply fresh_not_finished. iSplitL "Haf"; done. }
-    iVs ((fresh_start i) with "[Hf Haf]") as "[Has Hs]"; first by iFrame.
-    iDestruct (started_dup with "Hs") as "[Hs Hs']".
-    iApply pvs0_intro. iSplitR "Hs'".
-    - iRight. iExists i. iLeft. done.
-    - iApply pvs1_intro. iExists P. iSplit; first done. by iFrame.
+    iApply pvs1_intro. iExists γ, i. done.
   Qed.
 
-  Lemma saved_cast i P Q :
-    saved i P ★ saved i Q ★ wbox P ⊢ pvs1 (wbox Q).
+  Lemma saved_cast γ P Q :
+    saved γ P ★ saved γ Q ★ □ P ⊢ pvs1 (□ Q).
   Proof.
-    iIntros "(HsP & HsQ & HP)". iDestruct "HsP" as (FP) "(% & HsP & #HiP)".
+    iIntros "(#HsP & #HsQ & #HP)". iDestruct "HsP" as (i) "HiP".
     iApply (inv_open' i). iSplit; first done.
-    iIntros "[HaP|HaP]".
-    { iExFalso. iApply started_not_fresh. iSplitL "HaP"; done. }
     (* Can I state a view-shift and immediately run it? *)
-    iAssert (pvs0 (finished i)) with "[HaP HsP]" as "Hf".
-    { iDestruct "HaP" as (j) "[Hs | [Hf _]]".
-      - iApply start_finish.
-        iDestruct (started_start_agree with "[#]") as "%"; first by iSplitL "Hs".
-        subst j. done.
-      - iApply pvs0_intro.
-        iDestruct (started_finished_agree with "[#]") as "%"; first by iSplitL "Hf".
-        subst j. done. }
-    iVs "Hf" as "Hf". iApply pvs0_intro.
-    iDestruct (finished_dup with "Hf") as "[Hf Hf']". iSplitL "Hf' HP".
-    { iRight. iExists i. iRight. subst. iSplitL "Hf'"; done. }
-    iDestruct "HsQ" as (FQ) "(% & HsQ & HiQ)".
-    iApply (inv_open' i). iSplit; first iExact "HiQ".
-    iIntros "[HaQ | HaQ]".
-    { iExFalso. iApply started_not_fresh. iSplitL "HaQ"; done. }
-    iDestruct "HaQ" as (j) "[HaS | [Hf' HQ]]".
-    { iExFalso. iApply finished_not_start. iSplitL "HaS"; done. }
-    iApply pvs0_intro.
-    iDestruct (finished_dup with "Hf'") as "[Hf' Hf'']".
-    iDestruct (wbox_dup with "HQ") as "[HQ HQ']".
-    iSplitL "Hf'' HQ'".
-    { iRight. iExists j. iRight. by iSplitR "HQ'". }
-    iPoseProof (finished_agree with "[#]") as "H".
-    { iFrame "Hf Hf'". done. }
-    iDestruct "H" as %<-. iApply pvs1_intro. subst Q. done.
+    iIntros "HaP". iAssert (pvs0 (finished γ)) with "[HaP]" as "Hf".
+    { iDestruct "HaP" as "[Hs | [Hf _]]".
+      - by iApply start_finish.
+      - by iApply pvs0_intro. }
+    iVs "Hf" as "Hf". iDestruct (finished_dup with "Hf") as "[Hf Hf']".
+    iApply pvs0_intro. iSplitL "Hf'"; first by eauto.
+    (* Step 2: Open the Q-invariant. *)
+    iClear "HiP". clear i. iDestruct "HsQ" as (i) "HiQ".
+    iApply (inv_open' i). iSplit; first done.
+    iIntros "[HaQ | [_ #HQ]]".
+    { iExFalso. iApply finished_not_start. iSplitL "HaQ"; done. }
+    iApply pvs0_intro. iSplitL "Hf".
+    { iRight. by iSplitL "Hf". }
+    by iApply pvs1_intro.
   Qed.
 
   (** And now we tie a bad knot. *)
-  Notation "¬ P" := (wbox (P -★ pvs1 False))%I : uPred_scope.
+  Notation "¬ P" := (□ (P -★ pvs1 False))%I : uPred_scope.
   Definition A i : iProp := ∃ P, ¬P ★ saved i P.
-  Lemma A_dup i :
-    A i ⊢ A i ★ A i.
-  Proof.
-    iIntros "HA". iDestruct "HA" as (P) "[HNP HsP]".
-    iDestruct (wbox_dup with "HNP") as "[HNP HNP']".
-    iDestruct (saved_dup with "HsP") as "[HsP HsP']".
-    iSplitL "HNP HsP"; iExists P.
-    - by iSplitL "HNP".
-    - by iSplitL "HNP'".
-  Qed.
-  Lemma A_wbox i :
-    A i ⊢ wbox (A i).
-  Proof.
-    iIntros "H". iExists (A i). iSplitL "H"; first done.
-    iSplit; first by iIntros "!# ?". iIntros "!# HA".
-    by iApply A_dup.
-  Qed.
+  Global Instance : forall i, PersistentP (A i) := _.
 
   Lemma A_alloc :
-    auth_fresh ★ fresh ⊢ pvs1 (∃ i, saved i (A i)).
+    True ⊢ pvs1 (∃ i, saved i (A i)).
   Proof. by apply saved_alloc. Qed.
 
   Lemma alloc_NA i :
     saved i (A i) ⊢ (¬A i).
   Proof.
-    iIntros "Hi". iExists (saved i (A i)). iSplitL "Hi"; first done.
-    iSplit; last by (iIntros "!# ?"; iApply saved_dup).
-    iIntros "!# Hi HAi".
-    iDestruct (A_dup with "HAi") as "[HAi HAi']".
-    iDestruct "HAi'" as (P) "[HNP Hi']".
-    iVs ((saved_cast i) with "[Hi Hi' HAi]") as "HP".
-    { iSplitL "Hi"; first done. iSplitL "Hi'"; first done. by iApply A_wbox. }
-    iPoseProof (wbox_out with "HNP") as "HNP".
-    iApply "HNP". iApply wbox_out. done.
+    iIntros "#Hi !# #HA". iPoseProof "HA" as "HA'".
+    iDestruct "HA'" as (P) "#[HNP Hi']".
+    iVs ((saved_cast i) with "[]") as "HP".
+    { iSplit; first iExact "Hi". iSplit; first iExact "Hi'". done. }
+    by iApply "HNP".
   Qed.
 
   Lemma alloc_A i :
     saved i (A i) ⊢ A i.
   Proof.
-    iIntros "Hi". iDestruct (saved_dup with "Hi") as "[Hi Hi']".
-    iPoseProof (alloc_NA with "Hi") as "HNA".
-    iExists (A i). iSplitL "HNA"; done.
+    iIntros "#Hi". iPoseProof (alloc_NA with "Hi") as "HNA".
+    iExists (A i). iSplit; done.
   Qed.
 
   Lemma contradiction : False.
   Proof.
-    apply soundness. iIntros "H".
-    iVs (A_alloc with "H") as "H". iDestruct "H" as (i) "H".
-    iDestruct (saved_dup with "H") as "[H H']".
+    apply soundness. iIntros "".
+    iVs A_alloc as (i) "#H".
     iPoseProof (alloc_NA with "H") as "HN".
-    iPoseProof (wbox_out with "HN") as "HN".
     iApply "HN".
     iApply alloc_A. done.
   Qed.