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

@@ -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.

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)).

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.
 

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.

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.