Make `iIntros (?)` introduce ∀s/pures under ▷ and □ modalities.

I have reimplemented the tactic for introduction of ∀s/pures using type
classes, which directly made it much more modular.

theories/base_logic/lib/core.v

@@ -24,7 +24,7 @@ Section core.
   Implicit Types P Q : uPred M.
 
   Lemma coreP_intro P : P -∗ coreP P.
-  Proof. iIntros "HP". by iIntros (Q HQ ->). Qed.
+  Proof. rewrite /coreP. iIntros "HP". by iIntros (Q HQ ->). Qed.
 
   Global Instance coreP_persistent P : PersistentP (coreP P).
   Proof. rewrite /coreP. apply _. Qed.

theories/proofmode/class_instances.v

@@ -721,6 +721,32 @@ Global Instance into_forall_always {A} P (Φ : A → uPred M) :
   IntoForall P Φ → IntoForall (□ P) (λ a, □ (Φ a))%I.
 Proof. rewrite /IntoForall=> HP. by rewrite HP always_forall. Qed.
 
+(* FromForall *)
+Global Instance from_forall_forall {A} (Φ : A → uPred M) :
+  FromForall (∀ x, Φ x) Φ.
+Proof. done. Qed.
+Global Instance from_forall_pure {A} (φ : A → Prop) :
+  @FromForall M A (⌜∀ a : A, φ a⌝) (λ a, ⌜ φ a ⌝)%I.
+Proof. by rewrite /FromForall pure_forall. Qed.
+Global Instance from_forall_impl_pure P Q φ :
+  IntoPureT P φ → FromForall (P → Q) (λ _ : φ, Q)%I.
+Proof.
+  intros (φ'&->&?). by rewrite /FromForall -pure_impl_forall (into_pure P).
+Qed.
+Global Instance from_forall_wand_pure P Q φ :
+  IntoPureT P φ → FromForall (P -∗ Q) (λ _ : φ, Q)%I.
+Proof.
+  intros (φ'&->&?). rewrite /FromForall -pure_impl_forall.
+  by rewrite always_impl_wand (into_pure P).
+Qed.
+
+Global Instance from_forall_always {A} P (Φ : A → uPred M) :
+  FromForall P Φ → FromForall (□ P) (λ a, □ (Φ a))%I.
+Proof. rewrite /FromForall=> <-. by rewrite always_forall. Qed.
+Global Instance from_forall_later {A} P (Φ : A → uPred M) :
+  FromForall P Φ → FromForall (▷ P) (λ a, ▷ (Φ a))%I.
+Proof. rewrite /FromForall=> <-. by rewrite later_forall. Qed.
+
 (* FromModal *)
 Global Instance from_modal_later P : FromModal (▷ P) P.
 Proof. apply later_intro. Qed.

theories/proofmode/classes.v

@@ -206,6 +206,11 @@ Class IntoForall {M A} (P : uPred M) (Φ : A → uPred M) :=
 Arguments into_forall {_ _} _ _ {_}.
 Hint Mode IntoForall + - ! - : typeclass_instances.
 
+Class FromForall {M A} (P : uPred M) (Φ : A → uPred M) :=
+  from_forall : (∀ x, Φ x) ⊢ P.
+Arguments from_forall {_ _} _ _ {_}.
+Hint Mode FromForall + - ! - : typeclass_instances.
+
 Class FromModal {M} (P Q : uPred M) := from_modal : Q ⊢ P.
 Arguments from_modal {_} _ _ {_}.
 Hint Mode FromModal + ! - : typeclass_instances.

theories/proofmode/coq_tactics.v

@@ -512,13 +512,7 @@ Proof.
   rewrite (_ : P = □?false P) // (into_persistentP false P).
   by rewrite right_id always_and_sep_l wand_elim_r.
 Qed.
-Lemma tac_pure_impl_intro Δ (φ ψ : Prop) :
-  (φ → Δ ⊢ ⌜ψ⌝) → Δ ⊢ ⌜φ → ψ⌝.
-Proof. intros. rewrite pure_impl. by apply impl_intro_l, pure_elim_l. Qed.
-Lemma tac_impl_intro_pure Δ P φ Q : IntoPure P φ → (φ → Δ ⊢ Q) → Δ ⊢ P → Q.
-Proof.
-  intros. by apply impl_intro_l; rewrite (into_pure P); apply pure_elim_l.
-Qed.
+
 Lemma tac_impl_intro_drop Δ P Q : (Δ ⊢ Q) → Δ ⊢ P → Q.
 Proof. intros. apply impl_intro_l. by rewrite and_elim_r. Qed.
 
@@ -863,12 +857,11 @@ Proof.
 Qed.
 
 (** * Forall *)
-Lemma tac_forall_intro {A} Δ (Φ : A → uPred M) : (∀ a, Δ ⊢ Φ a) → Δ ⊢ ∀ a, Φ a.
-Proof. apply forall_intro. Qed.
-
-Lemma tac_pure_forall_intro {A} Δ (φ : A → Prop) :
-  (∀ a, Δ ⊢ ⌜φ a⌝) → Δ ⊢ ⌜∀ a, φ a⌝.
-Proof. intros. rewrite pure_forall. by apply forall_intro. Qed.
+Lemma tac_forall_intro {A} Δ (Φ : A → uPred M) Q :
+  FromForall Q Φ →
+  (∀ a, Δ ⊢ Φ a) →
+  Δ ⊢ Q.
+Proof. rewrite /FromForall=> <-. apply forall_intro. Qed.
 
 Lemma tac_forall_specialize {A} Δ Δ' i p P (Φ : A → uPred M) Q :
   envs_lookup i Δ = Some (p, P) → IntoForall P Φ →

theories/proofmode/tactics.v

@@ -284,21 +284,15 @@ Tactic Notation "iFrame" "(" constr(t1) constr(t2) constr(t3) constr(t4)
 (** * Basic introduction tactics *)
 Local Tactic Notation "iIntro" "(" simple_intropattern(x) ")" :=
   try iStartProof;
-  try first
-    [(* (∀ _, _) *) apply tac_forall_intro
-    |(* (?P → _) *) eapply tac_impl_intro_pure;
-      [apply _ ||
-       let P := match goal with |- IntoPure ?P _ => P end in
-       fail "iIntro:" P "not pure"
-      |]
-    |(* (?P -∗ _) *) eapply tac_wand_intro_pure;
+  lazymatch goal with
+  | |- _ ⊢ _ =>
+    eapply tac_forall_intro;
       [apply _ ||
-       let P := match goal with |- IntoPure ?P _ => P end in
-       fail "iIntro:" P "not pure"
-      |]
-    |(* ⌜∀ _, _⌝ *) apply tac_pure_forall_intro
-    |(* ⌜_ → _⌝ *) apply tac_pure_impl_intro];
-  intros x.
+       let P := match goal with |- FromForall ?P _ => P end in
+       fail "iIntro: cannot turn" P "into a universal quantifier"
+      |lazy beta; intros x]
+  | |- _ => intros x
+  end.
 
 Local Tactic Notation "iIntro" constr(H) :=
   iStartProof;

theories/tests/proofmode.v

@@ -221,6 +221,14 @@ Qed.
 Lemma test_iIntros_let P :
   ∀ Q, let R := True%I in P -∗ R -∗ Q -∗ P ∗ Q.
 Proof. iIntros (Q R) "$ HR $". Qed.
+
+Lemma test_iIntros_modalities P :
+  (□ ▷ ∀ x : nat, ⌜ x = 0 ⌝ -∗ ⌜ x = 0 ⌝ → False -∗ P -∗ P)%I.
+Proof.
+  iIntros (x ??).
+  iIntros "* **". (* Test that fast intros do not work under modalities *)
+  iIntros ([]).
+Qed.
 End tests.
 
 Section more_tests.