Merge branch 'robbert/iSpecialize_forall' into 'master'

Better instance for `IntoWand` of `∀ _ : φ, P`

Closes #492

See merge request iris/iris!860

iris/proofmode/class_instances.v

@@ -497,11 +497,13 @@ Proof.
           -impl_wand_intuitionistically -pure_impl_forall
           bi.persistently_elim //.
 Qed.
-Global Instance into_wand_forall_prop_false p (φ : Prop) P :
-  Absorbing P → IntoWand p false (∀ _ : φ, P) ⌜ φ ⌝ P.
+Global Instance into_wand_forall_prop_false p (φ : Prop) Pφ P :
+  MakeAffinely ⌜ φ ⌝ Pφ →
+  IntoWand p false (∀ _ : φ, P) Pφ P.
 Proof.
-  intros ?.
-  rewrite /IntoWand (intuitionistically_if_elim p) /= pure_wand_forall //.
+  rewrite /MakeAffinely /IntoWand=> <-.
+  rewrite (intuitionistically_if_elim p) /=.
+  by rewrite -pure_impl_forall -persistent_impl_wand_affinely.
 Qed.
 
 Global Instance into_wand_forall {A} p q (Φ : A → PROP) P Q x :

tests/proofmode.ref

@@ -178,6 +178,50 @@ Tactic failure: iSpecialize: Q not persistent.
   ⌜φ⌝
 1 goal
   
+  PROP : bi
+  BiAffine0 : BiAffine PROP
+  φ : Prop
+  P, Q : PROP
+  H : φ
+  ============================
+  "H1" : P
+  --------------------------------------□
+  ⌜φ⌝
+"test_iSpecialize_impl_pure"
+     : string
+1 goal
+  
+  PROP : bi
+  φ : Prop
+  P, Q : PROP
+  H : φ
+  ============================
+  --------------------------------------∗
+  <affine> ⌜φ⌝
+1 goal
+  
+  PROP : bi
+  φ : Prop
+  P, Q : PROP
+  H : φ
+  ============================
+  "H1" : P
+  --------------------------------------□
+  <affine> ⌜φ⌝
+"test_iSpecialize_impl_pure_affine"
+     : string
+1 goal
+  
+  PROP : bi
+  BiAffine0 : BiAffine PROP
+  φ : Prop
+  P, Q : PROP
+  H : φ
+  ============================
+  --------------------------------------∗
+  ⌜φ⌝
+1 goal
+  
   PROP : bi
   BiAffine0 : BiAffine PROP
   φ : Prop

tests/proofmode.v

@@ -480,6 +480,38 @@ Restart.
   by iFrame.
 Abort.
 
+Check "test_iSpecialize_impl_pure".
+Lemma test_iSpecialize_forall_pure (φ : Prop) P Q :
+  φ → □ (∀ _ : φ, P) -∗ (∀ _ : φ, Q) -∗ P ∗ Q.
+Proof.
+  iIntros (?) "#H1 H2".
+  (* Adds an affine modality *)
+  iSpecialize ("H1" with "[]"). { Show. done. }
+  iSpecialize ("H2" with "[]"). { Show. done. }
+Restart.
+  iIntros (?) "#H1 H2".
+  (* Solving it directly as a pure goal also works. *)
+  iSpecialize ("H1" with "[% //]").
+  iSpecialize ("H2" with "[% //]").
+  by iFrame.
+Abort.
+
+Check "test_iSpecialize_impl_pure_affine".
+Lemma test_iSpecialize_forall_pure_affine `{!BiAffine PROP} (φ : Prop) P Q :
+  φ → □ (∀ _ : φ, P) -∗ (∀ _ : φ, Q) -∗ P ∗ Q.
+Proof.
+  iIntros (?) "#H1 H2".
+  (* Does not add an affine modality *)
+  iSpecialize ("H1" with "[]"). { Show. done. }
+  iSpecialize ("H2" with "[]"). { Show. done. }
+Restart.
+  iIntros (?) "#H1 H2".
+  (* Solving it directly as a pure goal also works. *)
+  iSpecialize ("H1" with "[% //]").
+  iSpecialize ("H2" with "[% //]").
+  by iFrame.
+Abort.
+
 Check "test_iAssert_intuitionistic".
 Lemma test_iAssert_intuitionistic `{!BiBUpd PROP} P :
   □ P -∗ □ |==> P.