From 7ed067a97b05844b62076d672bdc16b86dda5ce9 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 27 Sep 2017 16:58:09 +0200
Subject: [PATCH] Fix issue #99.

This causes a bit of backwards incompatibility: it may now succeed with
later stripping below unlocked/TC transparent definitions. This problem
actually occured for `wsat`.
---
 theories/base_logic/derived.v        |  6 +++++-
 theories/base_logic/lib/wsat.v       | 13 ++++++++-----
 theories/program_logic/adequacy.v    |  2 +-
 theories/proofmode/class_instances.v |  8 ++++++++
 theories/tests/proofmode.v           |  5 ++++-
 5 files changed, 26 insertions(+), 8 deletions(-)

diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index a703ad7d5..aceaa62ea 100644
--- a/theories/base_logic/derived.v
+++ b/theories/base_logic/derived.v
@@ -596,10 +596,12 @@ Proof.
   apply (anti_symm _); auto using later_forall_2.
   apply forall_intro=> x. by rewrite (forall_elim x).
 Qed.
+Lemma later_exist_2 {A} (Î¦ : A â†’ uPred M) : (âˆƒ a, â–· Î¦ a) âŠ¢ â–· (âˆƒ a, Î¦ a).
+Proof. apply exist_elim; eauto using exist_intro. Qed.
 Lemma later_exist `{Inhabited A} (Î¦ : A â†’ uPred M) :
   â–· (âˆƒ a, Î¦ a) âŠ£âŠ¢ (âˆƒ a, â–· Î¦ a).
 Proof.
-  apply: anti_symm; [|apply exist_elim; eauto using exist_intro].
+  apply: anti_symm; [|apply later_exist_2].
   rewrite later_exist_false. apply or_elim; last done.
   rewrite -(exist_intro inhabitant); auto.
 Qed.
@@ -647,6 +649,8 @@ Lemma laterN_True n : â–·^n True âŠ£âŠ¢ True.
 Proof. apply (anti_symm (âŠ¢)); auto using laterN_intro. Qed.
 Lemma laterN_forall {A} n (Î¦ : A â†’ uPred M) : (â–·^n âˆ€ a, Î¦ a) âŠ£âŠ¢ (âˆ€ a, â–·^n Î¦ a).
 Proof. induction n as [|n IH]; simpl; rewrite -?later_forall; auto. Qed.
+Lemma laterN_exist_2 {A} n (Î¦ : A â†’ uPred M) : (âˆƒ a, â–·^n Î¦ a) âŠ¢ â–·^n (âˆƒ a, Î¦ a).
+Proof. apply exist_elim; eauto using exist_intro, laterN_mono. Qed.
 Lemma laterN_exist `{Inhabited A} n (Î¦ : A â†’ uPred M) :
   (â–·^n âˆƒ a, Î¦ a) âŠ£âŠ¢ âˆƒ a, â–·^n Î¦ a.
 Proof. induction n as [|n IH]; simpl; rewrite -?later_exist; auto. Qed.
diff --git a/theories/base_logic/lib/wsat.v b/theories/base_logic/lib/wsat.v
index ce126984a..3d658b58f 100644
--- a/theories/base_logic/lib/wsat.v
+++ b/theories/base_logic/lib/wsat.v
@@ -36,7 +36,7 @@ Typeclasses Opaque ownD.
 Instance: Params (@ownD) 3.
 
 Definition wsat `{invG Î£} : iProp Î£ :=
-  (âˆƒ I : gmap positive (iProp Î£),
+  locked (âˆƒ I : gmap positive (iProp Î£),
     own invariant_name (â— (invariant_unfold <$> I : gmap _ _)) âˆ—
     [âˆ— map] i â†¦ Q âˆˆ I, â–· Q âˆ— ownD {[i]} âˆ¨ ownE {[i]})%I.
 
@@ -103,7 +103,8 @@ Qed.
 
 Lemma ownI_open i P : wsat âˆ— ownI i P âˆ— ownE {[i]} âŠ¢ wsat âˆ— â–· P âˆ— ownD {[i]}.
 Proof.
-  rewrite /ownI. iIntros "(Hw & Hi & HiE)". iDestruct "Hw" as (I) "[? HI]".
+  rewrite /ownI /wsat -!lock.
+  iIntros "(Hw & Hi & HiE)". iDestruct "Hw" as (I) "[? HI]".
   iDestruct (invariant_lookup I i P with "[$]") as (Q) "[% #HPQ]".
   iDestruct (big_opM_delete _ _ i with "HI") as "[[[HQ $]|HiE'] HI]"; eauto.
   - iSplitR "HQ"; last by iNext; iRewrite -"HPQ".
@@ -113,7 +114,8 @@ Proof.
 Qed.
 Lemma ownI_close i P : wsat âˆ— ownI i P âˆ— â–· P âˆ— ownD {[i]} âŠ¢ wsat âˆ— ownE {[i]}.
 Proof.
-  rewrite /ownI. iIntros "(Hw & Hi & HP & HiD)". iDestruct "Hw" as (I) "[? HI]".
+  rewrite /ownI /wsat -!lock.
+  iIntros "(Hw & Hi & HP & HiD)". iDestruct "Hw" as (I) "[? HI]".
   iDestruct (invariant_lookup with "[$]") as (Q) "[% #HPQ]".
   iDestruct (big_opM_delete _ _ i with "HI") as "[[[HQ ?]|$] HI]"; eauto.
   - iDestruct (ownD_singleton_twice with "[$]") as %[].
@@ -125,7 +127,8 @@ Lemma ownI_alloc Ï† P :
   (âˆ€ E : gset positive, âˆƒ i, i âˆ‰ E âˆ§ Ï† i) â†’
   wsat âˆ— â–· P ==âˆ— âˆƒ i, âŒœÏ† iâŒ âˆ— wsat âˆ— ownI i P.
 Proof.
-  iIntros (Hfresh) "[Hw HP]". iDestruct "Hw" as (I) "[? HI]".
+  iIntros (Hfresh) "[Hw HP]". rewrite /wsat -!lock.
+  iDestruct "Hw" as (I) "[? HI]".
   iMod (own_unit (gset_disjUR positive) disabled_name) as "HE".
   iMod (own_updateP with "[$]") as "HE".
   { apply (gset_disj_alloc_empty_updateP_strong' (Î» i, I !! i = None âˆ§ Ï† i)).
@@ -147,7 +150,7 @@ Lemma ownI_alloc_open Ï† P :
   (âˆ€ E : gset positive, âˆƒ i, i âˆ‰ E âˆ§ Ï† i) â†’
   wsat ==âˆ— âˆƒ i, âŒœÏ† iâŒ âˆ— (ownE {[i]} -âˆ— wsat) âˆ— ownI i P âˆ— ownD {[i]}.
 Proof.
-  iIntros (Hfresh) "Hw". iDestruct "Hw" as (I) "[? HI]".
+  iIntros (Hfresh) "Hw". rewrite /wsat -!lock. iDestruct "Hw" as (I) "[? HI]".
   iMod (own_unit (gset_disjUR positive) disabled_name) as "HD".
   iMod (own_updateP with "[$]") as "HD".
   { apply (gset_disj_alloc_empty_updateP_strong' (Î» i, I !! i = None âˆ§ Ï† i)).
diff --git a/theories/program_logic/adequacy.v b/theories/program_logic/adequacy.v
index 9678b0e9a..81488f46b 100644
--- a/theories/program_logic/adequacy.v
+++ b/theories/program_logic/adequacy.v
@@ -29,7 +29,7 @@ Proof.
   iMod (own_alloc (CoPset âŠ¤)) as (Î³E) "HE"; first done.
   iMod (own_alloc (GSet âˆ…)) as (Î³D) "HD"; first done.
   iModIntro; iExists (WsatG _ _ _ _ Î³I Î³E Î³D).
-  rewrite /wsat /ownE; iFrame.
+  rewrite /wsat /ownE -lock; iFrame.
   iExists âˆ…. rewrite fmap_empty big_opM_empty. by iFrame.
 Qed.
 
diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index 2d1b5a7f9..a55899d06 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -169,6 +169,14 @@ Proof.
   rewrite /IntoLaterN' /IntoLaterN=> ->. by rewrite laterN_and -(laterN_intro _ P).
 Qed.
 
+Global Instance into_later_forall {A} n (Î¦ Î¨ : A â†’ uPred M) :
+  (âˆ€ x, IntoLaterN' n (Î¦ x) (Î¨ x)) â†’ IntoLaterN' n (âˆ€ x, Î¦ x) (âˆ€ x, Î¨ x).
+Proof. rewrite /IntoLaterN' /IntoLaterN laterN_forall=> ?. by apply forall_mono. Qed.
+Global Instance into_later_exist {A} n (Î¦ Î¨ : A â†’ uPred M) :
+  (âˆ€ x, IntoLaterN' n (Î¦ x) (Î¨ x)) â†’
+  IntoLaterN' n (âˆƒ x, Î¦ x) (âˆƒ x, Î¨ x).
+Proof. rewrite /IntoLaterN' /IntoLaterN -laterN_exist_2=> ?. by apply exist_mono. Qed.
+
 Global Instance into_laterN_or_l n P1 P2 Q1 Q2 :
   IntoLaterN' n P1 Q1 â†’ IntoLaterN n P2 Q2 â†’
   IntoLaterN' n (P1 âˆ¨ P2) (Q1 âˆ¨ Q2) | 10.
diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index 4a3895317..356a64bd2 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -165,6 +165,10 @@ Proof.
   iIntros "H". iNext. iExact "H". (* Check that the laters are all gone. *)
 Qed.
 
+Lemma test_iNext_quantifier (Î¦ : M â†’ M â†’ uPred M) :
+  (âˆ€ y, âˆƒ x, â–· Î¦ x y) -âˆ— â–· (âˆ€ y, âˆƒ x, Î¦ x y).
+Proof. iIntros "H". iNext. done. Qed.
+
 Lemma test_iFrame_persistent (P Q : uPred M) :
   â–¡ P -âˆ— Q -âˆ— â–¡ (P âˆ— P) âˆ— (P âˆ§ Q âˆ¨ Q).
 Proof. iIntros "#HP". iFrame "HP". iIntros "$". Qed.
@@ -193,7 +197,6 @@ Lemma test_True_intros : (True : uPred M) -âˆ— True.
 Proof.
   iIntros "?". done.
 Qed.
-
 End tests.
 
 Section more_tests.
-- 
GitLab