Generalize iAlways to also introduce ■ modalities.

This also applies to the introduction pattern `!#`. Both will now
introduce as many ■ or □ as possible. This behavior is consistent
with the dual, `#`, which also gets rid of as many ■ and □ modalities
as possible.

theories/proofmode/class_instances.v

@@ -146,11 +146,16 @@ Global Instance into_persistent_persistent P :
 Proof. intros. by rewrite /IntoPersistent. Qed.
 
 (* FromPersistent *)
-Global Instance from_persistent_persistently P : FromPersistent (□ P) P | 1.
+Global Instance from_persistent_here P : FromPersistent false false P P | 1.
 Proof. by rewrite /FromPersistent. Qed.
-Global Instance from_persistent_bare `{AffineBI PROP} P Q :
-  FromPersistent P Q → FromPersistent (■ P) Q.
-Proof. rewrite /FromPersistent=> ->. by rewrite affine_bare. Qed.
+Global Instance from_persistent_persistently a P Q :
+  FromPersistent a false P Q → FromPersistent false true (□ P) Q | 0.
+Proof.
+  rewrite /FromPersistent /= => <-. by destruct a; rewrite /= ?persistently_bare.
+Qed.
+Global Instance from_persistent_bare a p P Q :
+  FromPersistent a p P Q → FromPersistent true p (■ P) Q | 0.
+Proof. rewrite /FromPersistent /= => <-. destruct a; by rewrite /= ?bare_idemp. Qed.
 
 (* IntoWand *)
 Global Instance into_wand_wand p q P Q P' :
@@ -215,8 +220,6 @@ Global Instance into_wand_bare_persistently p q R P Q :
 Proof. by rewrite /IntoWand bare_persistently_elim. Qed.
 
 (* FromAnd *)
-Global Instance from_and_bare P : FromAnd (■ P) emp P | 100.
-Proof. by rewrite /FromAnd /bi_bare. Qed.
 Global Instance from_and_and P1 P2 : FromAnd (P1 ∧ P2) P1 P2 | 100.
 Proof. by rewrite /FromAnd. Qed.
 Global Instance from_and_sep_persistent_l P1 P1' P2 :

theories/proofmode/classes.v

@@ -55,11 +55,11 @@ Arguments IntoPersistent {_} _ _%I _%I : simpl never.
 Arguments into_persistent {_} _ _%I _%I {_}.
 Hint Mode IntoPersistent + + ! - : typeclass_instances.
 
-Class FromPersistent {PROP : bi} (P Q : PROP) :=
-  from_persistent : □ Q ⊢ P.
-Arguments FromPersistent {_} _%I _%I : simpl never.
-Arguments from_persistent {_} _%I _%I {_}.
-Hint Mode FromPersistent + ! - : typeclass_instances.
+Class FromPersistent {PROP : bi} (a p : bool) (P Q : PROP) :=
+  from_persistent : ■?a □?p Q ⊢ P.
+Arguments FromPersistent {_} _ _ _%I _%I : simpl never.
+Arguments from_persistent {_} _ _ _%I _%I {_}.
+Hint Mode FromPersistent + - - ! - : typeclass_instances.
 
 Class FromBare {PROP : bi} (P Q : PROP) :=
   from_bare : ■ Q ⊢ P.

theories/proofmode/coq_tactics.v

@@ -452,7 +452,7 @@ Lemma tac_emp_intro Δ :
   takes constant time). *)
   TCOr (AffineBI PROP) (AffineEnv (env_spatial Δ)) →
   Δ ⊢ emp.
-Proof. intros [?|?]; by rewrite (affine Δ). Qed.
+Proof. intros. by rewrite (affine Δ). Qed.
 
 Lemma tac_assumption Δ Δ' i p P Q :
   envs_lookup_delete i Δ = Some (p,P,Δ') →
@@ -520,13 +520,16 @@ Lemma tac_pure_revert Δ φ Q : (Δ ⊢ ⌜φ⌝ → Q) → (φ → Δ ⊢ Q).
 Proof. intros HΔ ?. by rewrite HΔ pure_True // left_id. Qed.
 
 (** * Persistently *)
-Lemma tac_persistently_intro Δ Q Q' :
-  FromPersistent Q' Q →
-  (envs_clear_spatial Δ ⊢ Q) → Δ ⊢ Q'.
+Lemma tac_persistently_intro Δ a p Q Q' :
+  FromPersistent a p Q' Q →
+  (if a then TCOr (AffineBI PROP) (AffineEnv (env_spatial Δ)) else TCTrue) →
+  ((if p then envs_clear_spatial Δ else Δ) ⊢ Q) → Δ ⊢ Q'.
 Proof.
-  intros ? HQ. rewrite -(from_persistent Q') -HQ envs_clear_spatial_sound.
-  rewrite {1}(env_spatial_is_nil_bare_persistently (envs_clear_spatial Δ)) //.
-  by rewrite -persistently_and_bare_sep_l and_elim_l.
+  intros ? Haffine HQ. rewrite -(from_persistent a p Q') -HQ. destruct p=> /=.
+  - rewrite envs_clear_spatial_sound.
+    rewrite {1}(env_spatial_is_nil_bare_persistently (envs_clear_spatial Δ)) //.
+    destruct a=> /=. by rewrite sep_elim_l. by rewrite bare_elim sep_elim_l.
+  - destruct a=> //=. apply and_intro; auto using tac_emp_intro.
 Qed.
 
 Lemma tac_persistent Δ Δ' i p P P' Q :

theories/proofmode/tactics.v

@@ -846,7 +846,9 @@ Local Tactic Notation "iExistDestruct" constr(H)
 Tactic Notation "iAlways":=
   iStartProof;
   eapply tac_persistently_intro;
-    [apply _ || fail "iAlways: the goal is not a persistently modality"
+    [apply _ (* || fail "iAlways: the goal is not a persistently modality" *)
+    |env_cbv; apply _ ||
+     fail "iAlways: spatial context contains non-affine hypotheses"
     |env_cbv].
 
 (** * Later *)
@@ -1764,7 +1766,7 @@ Hint Extern 1 (of_envs _ ⊢ _ ∧ _) => iSplit.
 Hint Extern 1 (of_envs _ ⊢ _ ∗ _) => iSplit.
 Hint Extern 1 (of_envs _ ⊢ ▷ _) => iNext.
 Hint Extern 1 (of_envs _ ⊢ □ _) => iAlways.
-Hint Extern 1 (of_envs _ ⊢ ■ _) => iSplit.
+Hint Extern 1 (of_envs _ ⊢ ■ _) => iAlways.
 Hint Extern 1 (of_envs _ ⊢ ∃ _, _) => iExists _.
 Hint Extern 1 (of_envs _ ⊢ ◇ _) => iModIntro.
 Hint Extern 1 (of_envs _ ⊢ _ ∨ _) => iLeft.

theories/tests/proofmode.v

@@ -219,7 +219,7 @@ Proof. iIntros (Q R) "$ _ $". Qed.
 
 Lemma test_foo P Q : ■ ▷ (Q ≡ P) -∗ ■ ▷ Q -∗ ■ ▷ P.
 Proof.
-  iIntros "#HPQ HQ". iSplit; first done. iNext. by iRewrite "HPQ" in "HQ".
+  iIntros "#HPQ HQ !#". iNext. by iRewrite "HPQ" in "HQ".
 Qed.
 
 Lemma test_iIntros_modalities `(!Absorbing P) :
@@ -230,4 +230,9 @@ Proof.
   iIntros ([]).
 Qed.
 
+Lemma test_iNext_affine P Q : ■ ▷ (Q ≡ P) -∗ ■ ▷ Q -∗ ■ ▷ P.
+Proof. iIntros "#HPQ HQ !#". iNext. by iRewrite "HPQ" in "HQ". Qed.
+
+Lemma test_iAlways P Q R : ⬕ P -∗ □ Q → R -∗ □ ■ ■ P ∗ ■ □ Q.
+Proof. iIntros "#HP #HQ HR". iSplitL. iAlways. done. iAlways. done. Qed.
 End tests.