Get rid of `FromLaterN` class.

ProofMode.md

@@ -114,15 +114,15 @@ Separating logic specific tactics
 Modalities
 ----------
 
-- `iModIntro` : introduction of a modality. The type class `FromModal` is used
-  to specify which modalities this tactic should introduce. Instances of that
-  type class include: later, except 0, basic update and fancy update,
+- `iModIntro mod` : introduction of a modality. The type class `FromModal` is
+  used to specify which modalities this tactic should introduce. Instances of
+  that type class include: later, except 0, basic update and fancy update,
   persistently, affinely, plainly, absorbingly, absolutely, and relatively.
+  The optional argument `mod` can be used to specify what modality to introduce
+  in case of ambiguity, e.g. `⎡|==> P⎤`.
 - `iAlways` : a deprecated alias of `iModIntro`.
-- `iNext n` : introduce `n` laters by stripping that number of laters from all
-  hypotheses. If the argument `n` is not given, it strips one later if the
-  leftmost conjunct is of the shape `▷ P`, or `n` laters if the leftmost
-  conjunct is of the shape `▷^n P`.
+- `iNext n` : an alias of `iModIntro (▷^n P)`.
+- `iNext` : an alias of `iModIntro (▷^1 P)`.
 - `iMod pm_trm as (x1 ... xn) "ipat"` : eliminate a modality `pm_trm` that is
   an instance of the `ElimModal` type class. Instances include: later, except 0,
   basic update and fancy update.

theories/base_logic/lib/boxes.v

@@ -127,7 +127,7 @@ Lemma slice_delete_empty E q f P Q γ :
   ↑N ⊆ E →
   f !! γ = Some false →
   slice N γ Q -∗ ▷?q box N f P ={E}=∗ ∃ P',
-    ▷?q ▷ (P ≡ (Q ∗ P')) ∗ ▷?q box N (delete γ f) P'.
+    ▷?q (▷ (P ≡ (Q ∗ P')) ∗ box N (delete γ f) P').
 Proof.
   iIntros (??) "[#HγQ Hinv] H". iDestruct "H" as (Φ) "[#HeqP Hf]".
   iExists ([∗ map] γ'↦_ ∈ delete γ f, Φ γ')%I.

theories/base_logic/lib/cancelable_invariants.v

@@ -57,7 +57,7 @@ Section proofs.
     ▷ □ (P ↔ P') -∗ cinv N γ P -∗ cinv N γ P'.
   Proof.
     iIntros "#HP' Hinv". iDestruct "Hinv" as (P'') "[#HP'' Hinv]".
-    iExists _. iFrame "Hinv". iNext. iAlways. iSplit.
+    iExists _. iFrame "Hinv". iAlways. iNext. iSplit.
     - iIntros "?". iApply "HP''". iApply "HP'". done.
     - iIntros "?". iApply "HP'". iApply "HP''". done.
   Qed.

theories/heap_lang/lifting.v

@@ -107,7 +107,7 @@ Implicit Types σ : state.
 
 (** Base axioms for core primitives of the language: Stateless reductions *)
 Lemma wp_fork s E e Φ :
-  ▷ Φ (LitV LitUnit) ∗ ▷ WP e @ s; ⊤ {{ _, True }} ⊢ WP Fork e @ s; E {{ Φ }}.
+  ▷ (Φ (LitV LitUnit) ∗ WP e @ s; ⊤ {{ _, True }}) ⊢ WP Fork e @ s; E {{ Φ }}.
 Proof.
   iIntros "[HΦ He]".
   iApply wp_lift_pure_det_head_step; [auto|intros; inv_head_step; eauto|].

theories/proofmode/class_instances.v

@@ -1394,12 +1394,12 @@ Global Instance is_except_0_fupd `{FUpdFacts PROP} E1 E2 P :
 Proof. by rewrite /IsExcept0 except_0_fupd. Qed.
 
 (* FromModal *)
-Global Instance from_modal_later n P Q :
-  NoBackTrack (FromLaterN n P Q) →
-  TCIf (TCEq n 0) False TCTrue →
-  FromModal (modality_laterN n) (▷^n P) P Q | 99.
-  (* below [from_modal_embed] to prefer introducing a later *)
-Proof. rewrite /FromLaterN /FromModal. by intros [?] [_ []|?]. Qed.
+Global Instance from_modal_later P :
+  FromModal (modality_laterN 1) (▷^1 P) (▷ P) P.
+Proof. by rewrite /FromModal. Qed.
+Global Instance from_modal_laterN n P :
+  FromModal (modality_laterN n) (▷^n P) (▷^n P) P.
+Proof. by rewrite /FromModal. Qed.
 Global Instance from_modal_except_0 P : FromModal modality_id (◇ P) (◇ P) P.
 Proof. by rewrite /FromModal /= -except_0_intro. Qed.
 
@@ -1681,55 +1681,4 @@ Proof.
   rewrite /IntoLaterN /MaybeIntoLaterN=> ?.
   rewrite big_opMS_commute. by apply big_sepMS_mono.
 Qed.
-
-(* FromLater *)
-Global Instance from_laterN_later P : FromLaterN 1 (▷ P) P | 0.
-Proof. by rewrite /FromLaterN. Qed.
-Global Instance from_laterN_laterN n P : FromLaterN n (▷^n P) P | 0.
-Proof. by rewrite /FromLaterN. Qed.
-
-(* The instances below are used when stripping a specific number of laters, or
-to balance laters in different branches of ∧, ∨ and ∗. *)
-Global Instance from_laterN_0 P : FromLaterN 0 P P | 100. (* fallthrough *)
-Proof. by rewrite /FromLaterN. Qed.
-Global Instance from_laterN_later_S n P Q :
-  FromLaterN n P Q → FromLaterN (S n) (▷ P) Q.
-Proof. by rewrite /FromLaterN=><-. Qed.
-Global Instance from_laterN_later_plus n m P Q :
-  FromLaterN m P Q → FromLaterN (n + m) (▷^n P) Q.
-Proof. rewrite /FromLaterN=><-. by rewrite laterN_plus. Qed.
-
-Global Instance from_later_and n P1 P2 Q1 Q2 :
-  FromLaterN n P1 Q1 → FromLaterN n P2 Q2 → FromLaterN n (P1 ∧ P2) (Q1 ∧ Q2).
-Proof. intros ??; red. by rewrite laterN_and; apply and_mono. Qed.
-Global Instance from_later_or n P1 P2 Q1 Q2 :
-  FromLaterN n P1 Q1 → FromLaterN n P2 Q2 → FromLaterN n (P1 ∨ P2) (Q1 ∨ Q2).
-Proof. intros ??; red. by rewrite laterN_or; apply or_mono. Qed.
-Global Instance from_later_sep n P1 P2 Q1 Q2 :
-  FromLaterN n P1 Q1 → FromLaterN n P2 Q2 → FromLaterN n (P1 ∗ P2) (Q1 ∗ Q2).
-Proof. intros ??; red. by rewrite laterN_sep; apply sep_mono. Qed.
-
-Global Instance from_later_affinely n P Q `{BiAffine PROP} :
-  FromLaterN n P Q → FromLaterN n (bi_affinely P) (bi_affinely Q).
-Proof. rewrite /FromLaterN=><-. by rewrite affinely_elim affine_affinely. Qed.
-Global Instance from_later_plainly n P Q :
-  FromLaterN n P Q → FromLaterN n (bi_plainly P) (bi_plainly Q).
-Proof. by rewrite /FromLaterN laterN_plainly=> ->. Qed.
-Global Instance from_later_persistently n P Q :
-  FromLaterN n P Q → FromLaterN n (bi_persistently P) (bi_persistently Q).
-Proof. by rewrite /FromLaterN laterN_persistently=> ->. Qed.
-Global Instance from_later_absorbingly n P Q :
-  FromLaterN n P Q → FromLaterN n (bi_absorbingly P) (bi_absorbingly Q).
-Proof. by rewrite /FromLaterN laterN_absorbingly=> ->. Qed.
-Global Instance from_later_embed`{SbiEmbedding PROP PROP'} n P Q :
-  FromLaterN n P Q → FromLaterN n ⎡P⎤ ⎡Q⎤.
-Proof. rewrite /FromLaterN=> <-. by rewrite sbi_embed_laterN. Qed.
-
-Global Instance from_later_forall {A} n (Φ Ψ : A → PROP) :
-  (∀ x, FromLaterN n (Φ x) (Ψ x)) → FromLaterN n (∀ x, Φ x) (∀ x, Ψ x).
-Proof. rewrite /FromLaterN laterN_forall=> ?. by apply forall_mono. Qed.
-Global Instance from_later_exist {A} n (Φ Ψ : A → PROP) :
-  Inhabited A → (∀ x, FromLaterN n (Φ x) (Ψ x)) →
-  FromLaterN n (∃ x, Φ x) (∃ x, Ψ x).
-Proof. intros ?. rewrite /FromLaterN laterN_exist=> ?. by apply exist_mono. Qed.
 End sbi_instances.

theories/proofmode/classes.v

@@ -446,11 +446,6 @@ Instance maybe_into_laterN_default_0 {PROP : sbi} only_head (P : PROP) :
   MaybeIntoLaterN only_head 0 P P | 0.
 Proof. apply _. Qed.
 
-Class FromLaterN {PROP : sbi} (n : nat) (P Q : PROP) := from_laterN : ▷^n Q ⊢ P.
-Arguments FromLaterN {_} _%nat_scope _%I _%I.
-Arguments from_laterN {_} _%nat_scope _%I _%I {_}.
-Hint Mode FromLaterN + - ! - : typeclass_instances.
-
 (** The class [IntoEmbed P Q] is used to transform hypotheses while introducing
 embeddings using [iModIntro].
 
@@ -531,8 +526,6 @@ Instance into_pure_tc_opaque {PROP : bi} (P : PROP) φ :
   IntoPure P φ → IntoPure (tc_opaque P) φ := id.
 Instance from_pure_tc_opaque {PROP : bi} (a : bool) (P : PROP) φ :
   FromPure a P φ → FromPure a (tc_opaque P) φ := id.
-Instance from_laterN_tc_opaque {PROP : sbi} n (P Q : PROP) :
-  FromLaterN n P Q → FromLaterN n (tc_opaque P) Q := id.
 Instance from_wand_tc_opaque {PROP : bi} (P Q1 Q2 : PROP) :
   FromWand P Q1 Q2 → FromWand (tc_opaque P) Q1 Q2 := id.
 Instance into_wand_tc_opaque {PROP : bi} p q (R P Q : PROP) :

theories/proofmode/monpred.v

@@ -430,12 +430,13 @@ Global Instance maybe_into_later_monPred_at i n P Q 𝓠 :
   IntoLaterN false n (P i) 𝓠.
 Proof.
   rewrite /IntoLaterN /MaybeIntoLaterN /MakeMonPredAt=> -> <-. elim n=>//= ? <-.
-   by rewrite monPred_at_later.
+  by rewrite monPred_at_later.
 Qed.
-Global Instance from_later_monPred_at i n P Q 𝓠 :
-  FromLaterN n P Q → MakeMonPredAt i Q 𝓠 → FromLaterN n (P i) 𝓠.
+Global Instance from_later_monPred_at i `(sel : A) n P Q 𝓠 :
+  FromModal (modality_laterN n) sel P Q → MakeMonPredAt i Q 𝓠 →
+  FromModal (modality_laterN n) sel (P i) 𝓠.
 Proof.
-  rewrite /FromLaterN /MakeMonPredAt=> <- <-. elim n=>//= ? ->.
+  rewrite /FromModal /MakeMonPredAt=> <- <-. elim n=>//= ? ->.
   by rewrite monPred_at_later.
 Qed.
 

theories/tests/proofmode.v

@@ -171,9 +171,8 @@ Proof.
   iIntros "?". iNext. iAssumption.
 Qed.
 
-Lemma test_iNext_sep1 P Q
-    (R1 := (P ∗ Q)%I) (R2 := (▷ P ∗ ▷ Q)%I) :
-  (▷ P ∗ ▷ Q) ∗ R1 ∗ R2 -∗ ▷ (P ∗ Q) ∗ ▷ R1 ∗ R2.
+Lemma test_iNext_sep1 P Q (R1 := (P ∗ Q)%I) :
+  (▷ P ∗ ▷ Q) ∗ R1 -∗ ▷ ((P ∗ Q) ∗ R1).
 Proof.
   iIntros "H". iNext.
   rewrite {1 2}(lock R1). (* check whether R1 has not been unfolded *) done.