From 1a14cdd344cc00aecc0e7ef5ef2153b74e4c4e90 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 6 May 2019 16:34:44 +0200
Subject: [PATCH] Generalize `iPureIntro` to support non-empty spatial contexts
 with just affine hypotheses.

---
 tests/proofmode.v                        |  11 +++
 theories/base_logic/proofmode.v          |   6 +-
 theories/proofmode/class_instances_bi.v  | 115 ++++++++++++-----------
 theories/proofmode/class_instances_sbi.v |   6 +-
 theories/proofmode/classes.v             |  24 ++---
 theories/proofmode/coq_tactics.v         |  27 +++---
 theories/proofmode/frame_instances.v     |  16 +++-
 theories/proofmode/ltac_tactics.v        |   7 +-
 theories/proofmode/monpred.v             |   4 +-
 9 files changed, 120 insertions(+), 96 deletions(-)

diff --git a/tests/proofmode.v b/tests/proofmode.v
index 528eec38e..0cc675ed2 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -133,10 +133,21 @@ Lemma test_iSpecialize_Coq_entailment P Q R :
   P â†’ (P -âˆ— Q) â†’ Q.
 Proof. iIntros (HP HPQ). iDestruct (HPQ $! HP) as "?". done. Qed.
 
+Lemma test_iPure_intro_emp R `{!Affine R} :
+  R -âˆ— emp.
+Proof. iIntros "HR". by iPureIntro. Qed.
+
 Lemma test_iEmp_intro P Q R `{!Affine P, !Persistent Q, !Affine R} :
   P -âˆ— Q â†’ R -âˆ— emp.
 Proof. iIntros "HP #HQ HR". iEmpIntro. Qed.
 
+Lemma test_iPure_intro (Ï† : nat â†’ Prop) P Q R `{!Affine P, !Persistent Q, !Affine R} :
+  Ï† 0 â†’ P -âˆ— Q â†’ R -âˆ— âˆƒ x : nat, <affine> âŒœ Ï† x âŒ âˆ§ âŒœ Ï† x âŒ.
+Proof. iIntros (?) "HP #HQ HR". iPureIntro; eauto. Qed.
+Lemma test_iPure_intro_2 (Ï† : nat â†’ Prop) P Q R `{!Persistent Q} :
+  Ï† 0 â†’ P -âˆ— Q â†’ R -âˆ— âˆƒ x : nat, <affine> âŒœ Ï† x âŒ âˆ— âŒœ Ï† x âŒ.
+Proof. iIntros (?) "HP #HQ HR". iPureIntro; eauto. Qed.
+
 Lemma test_fresh P Q:
   (P âˆ— Q) -âˆ— (P âˆ— Q).
 Proof.
diff --git a/theories/base_logic/proofmode.v b/theories/base_logic/proofmode.v
index 9475d6c5a..944b92e84 100644
--- a/theories/base_logic/proofmode.v
+++ b/theories/base_logic/proofmode.v
@@ -12,10 +12,10 @@ Global Instance into_pure_cmra_valid `{!CmraDiscrete A} (a : A) :
   @IntoPure (uPredI M) (âœ“ a) (âœ“ a).
 Proof. by rewrite /IntoPure discrete_valid. Qed.
 
-Global Instance from_pure_cmra_valid {A : cmraT} af (a : A) :
-  @FromPure (uPredI M) af (âœ“ a) (âœ“ a).
+Global Instance from_pure_cmra_valid {A : cmraT} (a : A) :
+  @FromPure (uPredI M) false (âœ“ a) (âœ“ a).
 Proof.
-  rewrite /FromPure. eapply bi.pure_elim; [by apply bi.affinely_if_elim|]=> ?.
+  rewrite /FromPure /=. eapply bi.pure_elim=> // ?.
   rewrite -uPred.cmra_valid_intro //.
 Qed.
 
diff --git a/theories/proofmode/class_instances_bi.v b/theories/proofmode/class_instances_bi.v
index c3f3bd219..7b9c78bd3 100644
--- a/theories/proofmode/class_instances_bi.v
+++ b/theories/proofmode/class_instances_bi.v
@@ -153,13 +153,12 @@ Proof. rewrite /IntoPure=>Hx. rewrite -pure_forall_2. by setoid_rewrite Hx. Qed.
 Global Instance into_pure_pure_sep (Ï†1 Ï†2 : Prop) P1 P2 :
   IntoPure P1 Ï†1 â†’ IntoPure P2 Ï†2 â†’ IntoPure (P1 âˆ— P2) (Ï†1 âˆ§ Ï†2).
 Proof. rewrite /IntoPure=> -> ->. by rewrite sep_and pure_and. Qed.
-Global Instance into_pure_pure_wand (Ï†1 Ï†2 : Prop) P1 P2 :
-  FromPure true P1 Ï†1 â†’ IntoPure P2 Ï†2 â†’ IntoPure (P1 -âˆ— P2) (Ï†1 â†’ Ï†2).
+Global Instance into_pure_pure_wand a (Ï†1 Ï†2 : Prop) P1 P2 :
+  FromPure a P1 Ï†1 â†’ IntoPure P2 Ï†2 â†’ IntoPure (P1 -âˆ— P2) (Ï†1 â†’ Ï†2).
 Proof.
-  rewrite /FromPure /IntoPure=> <- -> /=.
-  rewrite pure_impl -impl_wand_2. apply bi.wand_intro_l.
-  rewrite -{1}(persistent_absorbingly_affinely âŒœÏ†1âŒ%I) absorbingly_sep_l
-          bi.wand_elim_r absorbing //.
+  rewrite /FromPure /IntoPure=> <- -> /=. rewrite pure_impl.
+  apply impl_intro_l, pure_elim_l=> ?. rewrite (pure_True Ï†1) //.
+  by rewrite -affinely_affinely_if affinely_True_emp affinely_emp left_id.
 Qed.
 
 Global Instance into_pure_affinely P Ï† : IntoPure P Ï† â†’ IntoPure (<affine> P) Ï†.
@@ -177,14 +176,24 @@ Global Instance into_pure_embed `{BiEmbed PROP PROP'} P Ï† :
 Proof. rewrite /IntoPure=> ->. by rewrite embed_pure. Qed.
 
 (** FromPure *)
-Global Instance from_pure_pure a Ï† : @FromPure PROP a âŒœÏ†âŒ Ï†.
-Proof. rewrite /FromPure. apply affinely_if_elim. Qed.
-Global Instance from_pure_pure_and a (Ï†1 Ï†2 : Prop) P1 P2 :
-  FromPure a P1 Ï†1 â†’ FromPure a P2 Ï†2 â†’ FromPure a (P1 âˆ§ P2) (Ï†1 âˆ§ Ï†2).
-Proof. rewrite /FromPure pure_and=> <- <- /=. by rewrite affinely_if_and. Qed.
-Global Instance from_pure_pure_or a (Ï†1 Ï†2 : Prop) P1 P2 :
-  FromPure a P1 Ï†1 â†’ FromPure a P2 Ï†2 â†’ FromPure a (P1 âˆ¨ P2) (Ï†1 âˆ¨ Ï†2).
-Proof. by rewrite /FromPure pure_or affinely_if_or=><- <-. Qed.
+Global Instance from_pure_emp : @FromPure PROP true emp True.
+Proof. rewrite /FromPure /=. apply (affine _). Qed.
+Global Instance from_pure_pure Ï† : @FromPure PROP false âŒœÏ†âŒ Ï†.
+Proof. by rewrite /FromPure /=. Qed.
+Global Instance from_pure_pure_and a1 a2 (Ï†1 Ï†2 : Prop) P1 P2 :
+  FromPure a1 P1 Ï†1 â†’ FromPure a2 P2 Ï†2 â†’
+  FromPure (if a1 then true else a2) (P1 âˆ§ P2) (Ï†1 âˆ§ Ï†2).
+Proof.
+  rewrite /FromPure pure_and=> <- <- /=. rewrite affinely_if_and.
+  f_equiv; apply affinely_if_flag_mono; destruct a1; naive_solver.
+Qed.
+Global Instance from_pure_pure_or a1 a2 (Ï†1 Ï†2 : Prop) P1 P2 :
+  FromPure a1 P1 Ï†1 â†’ FromPure a2 P2 Ï†2 â†’
+  FromPure (if a1 then true else a2) (P1 âˆ¨ P2) (Ï†1 âˆ¨ Ï†2).
+Proof.
+  rewrite /FromPure pure_or=> <- <- /=. rewrite affinely_if_or.
+  f_equiv; apply affinely_if_flag_mono; destruct a1; naive_solver.
+Qed.
 Global Instance from_pure_pure_impl a (Ï†1 Ï†2 : Prop) P1 P2 :
   IntoPure P1 Ï†1 â†’ FromPure a P2 Ï†2 â†’ FromPure a (P1 â†’ P2) (Ï†1 â†’ Ï†2).
 Proof.
@@ -205,27 +214,25 @@ Proof.
   destruct a=>//=. apply affinely_forall.
 Qed.
 
-Global Instance from_pure_pure_sep_true (Ï†1 Ï†2 : Prop) P1 P2 :
-  FromPure true P1 Ï†1 â†’ FromPure true P2 Ï†2 â†’ FromPure true (P1 âˆ— P2) (Ï†1 âˆ§ Ï†2).
-Proof.
-  rewrite /FromPure=> <- <- /=.
-  by rewrite -persistent_and_affinely_sep_l affinely_and_r pure_and.
-Qed.
-Global Instance from_pure_pure_sep_false_l (Ï†1 Ï†2 : Prop) P1 P2 :
-  FromPure false P1 Ï†1 â†’ FromPure true P2 Ï†2 â†’ FromPure false (P1 âˆ— P2) (Ï†1 âˆ§ Ï†2).
-Proof.
-  rewrite /FromPure=> <- <- /=. by rewrite -persistent_and_affinely_sep_r pure_and.
-Qed.
-Global Instance from_pure_pure_sep_false_r (Ï†1 Ï†2 : Prop) P1 P2 :
-  FromPure true P1 Ï†1 â†’ FromPure false P2 Ï†2 â†’ FromPure false (P1 âˆ— P2) (Ï†1 âˆ§ Ï†2).
+Global Instance from_pure_pure_sep_true a1 a2 (Ï†1 Ï†2 : Prop) P1 P2 :
+  FromPure a1 P1 Ï†1 â†’ FromPure a2 P2 Ï†2 â†’
+  FromPure (if a1 then a2 else false) (P1 âˆ— P2) (Ï†1 âˆ§ Ï†2).
 Proof.
-  rewrite /FromPure=> <- <- /=. by rewrite -persistent_and_affinely_sep_l pure_and.
+  rewrite /FromPure=> <- <-. destruct a1; simpl.
+  - by rewrite pure_and -persistent_and_affinely_sep_l affinely_if_and_r.
+  - by rewrite pure_and -affinely_affinely_if -persistent_and_affinely_sep_r_1.
 Qed.
-Global Instance from_pure_pure_wand (Ï†1 Ï†2 : Prop) a P1 P2 :
-  IntoPure P1 Ï†1 â†’ FromPure false P2 Ï†2 â†’ FromPure a (P1 -âˆ— P2) (Ï†1 â†’ Ï†2).
+Global Instance from_pure_pure_wand a (Ï†1 Ï†2 : Prop) P1 P2 :
+  IntoPure P1 Ï†1 â†’ FromPure a P2 Ï†2 â†’
+  TCOr (TCEq a false) (Affine P1) â†’
+  FromPure a (P1 -âˆ— P2) (Ï†1 â†’ Ï†2).
 Proof.
-  rewrite /FromPure /IntoPure=> -> <- /=.
-  by rewrite bi.affinely_if_elim pure_wand_forall pure_impl pure_impl_forall.
+  rewrite /FromPure /IntoPure=> HP1 <- Ha /=. apply wand_intro_l.
+  destruct a; simpl.
+  - destruct Ha as [Ha|?]; first inversion Ha.
+    rewrite -persistent_and_affinely_sep_r -(affine_affinely P1) HP1.
+    by rewrite affinely_and_l pure_impl impl_elim_r.
+  - by rewrite HP1 sep_and pure_impl impl_elim_r.
 Qed.
 
 Global Instance from_pure_persistently P a Ï† :
@@ -234,24 +241,21 @@ Proof.
   rewrite /FromPure=> <- /=.
   by rewrite persistently_affinely_elim affinely_if_elim persistently_pure.
 Qed.
-Global Instance from_pure_affinely_true P Ï† :
-  FromPure true P Ï† â†’ FromPure true (<affine> P) Ï†.
-Proof. rewrite /FromPure=><- /=. by rewrite affinely_idemp. Qed.
-Global Instance from_pure_affinely_false P Ï† `{!Affine P} :
-  FromPure false P Ï† â†’ FromPure false (<affine> P) Ï†.
-Proof. rewrite /FromPure /= affine_affinely //. Qed.
-Global Instance from_pure_intuitionistically_true P Ï† :
-  FromPure true P Ï† â†’ FromPure true (â–¡ P) Ï†.
+Global Instance from_pure_affinely_true a P Ï† :
+  FromPure a P Ï† â†’ FromPure true (<affine> P) Ï†.
+Proof. rewrite /FromPure=><- /=. by rewrite -affinely_affinely_if affinely_idemp. Qed.
+Global Instance from_pure_intuitionistically_true a P Ï† :
+  FromPure a P Ï† â†’ FromPure true (â–¡ P) Ï†.
 Proof.
-  rewrite /FromPure=><- /=. rewrite intuitionistically_affinely_elim.
-  rewrite {1}(persistent âŒœÏ†âŒ%I) //.
+  rewrite /FromPure=><- /=.
+  rewrite -intuitionistically_affinely_elim -affinely_affinely_if affinely_idemp.
+  by rewrite intuitionistic_intuitionistically.
 Qed.
-
-Global Instance from_pure_absorbingly P Ï† p :
-  FromPure true P Ï† â†’ FromPure p (<absorb> P) Ï†.
+Global Instance from_pure_absorbingly a P Ï† :
+  FromPure a P Ï† â†’ FromPure false (<absorb> P) Ï†.
 Proof.
-  rewrite /FromPure=> <- /=.
-  rewrite persistent_absorbingly_affinely affinely_if_elim //.
+  rewrite /FromPure=> <- /=. rewrite -affinely_affinely_if.
+  by rewrite -persistent_absorbingly_affinely_2.
 Qed.
 Global Instance from_pure_embed `{BiEmbed PROP PROP'} a P Ï† :
   FromPure a P Ï† â†’ FromPure a âŽ¡PâŽ¤ Ï†.
@@ -946,17 +950,20 @@ Global Instance into_forall_embed `{BiEmbed PROP PROP'} {A} P (Î¦ : A â†’ PROP)
   IntoForall P Î¦ â†’ IntoForall âŽ¡PâŽ¤ (Î» a, âŽ¡Î¦ aâŽ¤%I).
 Proof. by rewrite /IntoForall -embed_forall => <-. Qed.
 
-Global Instance into_forall_impl_pure Ï† P Q :
-  FromPureT false P Ï† â†’ IntoForall (P â†’ Q) (Î» _ : Ï†, Q).
+Global Instance into_forall_impl_pure a Ï† P Q :
+  FromPureT a P Ï† â†’
+  TCOr (TCEq a false) (BiAffine PROP) â†’
+  IntoForall (P â†’ Q) (Î» _ : Ï†, Q).
 Proof.
-  rewrite /FromPureT /FromPure /IntoForall=> -[Ï†' [-> <-]].
-  by rewrite pure_impl_forall.
+  rewrite /FromPureT /FromPure /IntoForall=> -[Ï†' [-> <-]] [->|?] /=.
+  - by rewrite pure_impl_forall.
+  - by rewrite -affinely_affinely_if affine_affinely pure_impl_forall.
 Qed.
-Global Instance into_forall_wand_pure Ï† P Q :
-  FromPureT true P Ï† â†’ IntoForall (P -âˆ— Q) (Î» _ : Ï†, Q).
+Global Instance into_forall_wand_pure a Ï† P Q :
+  FromPureT a P Ï† â†’ IntoForall (P -âˆ— Q) (Î» _ : Ï†, Q).
 Proof.
   rewrite /FromPureT /FromPure /IntoForall=> -[Ï†' [-> <-]] /=.
-  apply forall_intro=>? /=.
+  apply forall_intro=>? /=. rewrite -affinely_affinely_if.
   by rewrite -(pure_intro _ True%I) // /bi_affinely right_id emp_wand.
 Qed.
 
diff --git a/theories/proofmode/class_instances_sbi.v b/theories/proofmode/class_instances_sbi.v
index 2748471ca..56586ce3a 100644
--- a/theories/proofmode/class_instances_sbi.v
+++ b/theories/proofmode/class_instances_sbi.v
@@ -37,9 +37,9 @@ Proof.
 Qed.
 
 (** FromPure *)
-Global Instance from_pure_internal_eq af {A : ofeT} (a b : A) :
-  @FromPure PROP af (a â‰¡ b) (a â‰¡ b).
-Proof. by rewrite /FromPure pure_internal_eq affinely_if_elim. Qed.
+Global Instance from_pure_internal_eq {A : ofeT} (a b : A) :
+  @FromPure PROP false (a â‰¡ b) (a â‰¡ b).
+Proof. by rewrite /FromPure pure_internal_eq. Qed.
 Global Instance from_pure_later a P Ï† : FromPure a P Ï† â†’ FromPure a (â–· P) Ï†.
 Proof. rewrite /FromPure=> ->. apply later_intro. Qed.
 Global Instance from_pure_laterN a n P Ï† : FromPure a P Ï† â†’ FromPure a (â–·^n P) Ï†.
diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index abd98b1a7..03dbb8b66 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -56,24 +56,20 @@ Proof. by exists Ï†. Qed.
 Hint Extern 0 (IntoPureT _ _) =>
   notypeclasses refine (into_pureT_hint _ _ _) : typeclass_instances.
 
-(** [FromPure] is used when introducing a pure assertion. It is used
-    by iPure, the "[%]" specialization pattern, and the [with "[%]"]
-    pattern when using [iAssert].
-
-    The [a] Boolean asserts whether we introduce the pure assertion in
-    an affine way or in an absorbing way. When [FromPure true P Ï†] is
-    derived, then [FromPure false P Ï†] can always be derived too. We
-    use [true] for specialization patterns and [false] for the
-    [iPureIntro] tactic.
-
-    This Boolean is not needed for [IntoPure], because in the case of
-    [IntoPure], we can have the same behavior by asking that [P] be
-    [Affine]. *)
+(** [FromPure] is used when introducing a pure assertion. It is used by
+[IntoPure] and the [[%]] specialization pattern.
+
+The Boolean [a] asserts whether we the pure assertion required the [emp]
+resource or not. Concretely, for [IntoPure] it specifies whether the spatial
+context should be empty or not.
+
+Note that this Boolean is not needed for [IntoPure], because in the case of
+[IntoPure], we can have the same behavior by asking that [P] be [Affine]. *)
 Class FromPure {PROP : bi} (a : bool) (P : PROP) (Ï† : Prop) :=
   from_pure : <affine>?a âŒœÏ†âŒ âŠ¢ P.
 Arguments FromPure {_} _ _%I _%type_scope : simpl never.
 Arguments from_pure {_} _ _%I _%type_scope {_}.
-Hint Mode FromPure + + ! - : typeclass_instances.
+Hint Mode FromPure + - ! - : typeclass_instances.
 
 Class FromPureT {PROP : bi} (a : bool) (P : PROP) (Ï† : Type) :=
   from_pureT : âˆƒ Ïˆ : Prop, Ï† = Ïˆ âˆ§ FromPure a P Ïˆ.
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 6291971cb..5513acd4b 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -104,14 +104,14 @@ Proof.
 Qed.
 
 (** * Pure *)
-(* This relies on the invariant that [FromPure false] implies
-   [FromPure true] *)
-Lemma tac_pure_intro Î” Q Ï† af :
-  env_spatial_is_nil Î” = af â†’ FromPure af Q Ï† â†’ Ï† â†’ envs_entails Î” Q.
-Proof.
-  intros ???. rewrite envs_entails_eq -(from_pure af Q). destruct af.
-  - rewrite env_spatial_is_nil_intuitionistically //= /bi_intuitionistically.
-    f_equiv. by apply pure_intro.
+Lemma tac_pure_intro Î” Q Ï† a :
+  FromPure a Q Ï† â†’
+  (if a then AffineEnv (env_spatial Î”) else TCTrue) â†’
+  Ï† â†’
+  envs_entails Î” Q.
+Proof.
+  intros ???. rewrite envs_entails_eq -(from_pure a Q). destruct a; simpl.
+  - by rewrite (affine (of_envs Î”)) pure_True // affinely_True_emp affinely_emp.
   - by apply pure_intro.
 Qed.
 
@@ -276,19 +276,18 @@ Proof.
   apply wand_intro_l. by rewrite assoc !wand_elim_r.
 Qed.
 
-Lemma tac_specialize_assert_pure Î” Î”' j q R P1 P2 Ï† Q :
+Lemma tac_specialize_assert_pure Î” Î”' j q a R P1 P2 Ï† Q :
   envs_lookup j Î” = Some (q, R) â†’
   IntoWand q true R P1 P2 â†’
-  FromPure true P1 Ï† â†’
+  FromPure a P1 Ï† â†’
   envs_simple_replace j q (Esnoc Enil j P2) Î” = Some Î”' â†’
   Ï† â†’ envs_entails Î”' Q â†’ envs_entails Î” Q.
 Proof.
   rewrite envs_entails_eq=> ????? <-. rewrite envs_simple_replace_singleton_sound //=.
   rewrite -intuitionistically_if_idemp (into_wand q true) /=.
-  rewrite -(from_pure true P1) /bi_intuitionistically.
-  rewrite pure_True //= persistently_affinely_elim persistently_pure
-          affinely_True_emp affinely_emp.
-  by rewrite emp_wand wand_elim_r.
+  rewrite -(from_pure a P1) pure_True //.
+  rewrite -affinely_affinely_if affinely_True_emp affinely_emp.
+  by rewrite intuitionistically_emp left_id wand_elim_r.
 Qed.
 
 Lemma tac_specialize_assert_intuitionistic Î” Î”' Î”'' j q P1 P1' P2 R Q :
diff --git a/theories/proofmode/frame_instances.v b/theories/proofmode/frame_instances.v
index 63e837fcd..f9c8cd921 100644
--- a/theories/proofmode/frame_instances.v
+++ b/theories/proofmode/frame_instances.v
@@ -26,10 +26,20 @@ Proof.
   apply sep_elim_l, _.
 Qed.
 
-Global Instance frame_here_pure p Ï† Q : FromPure false Q Ï† â†’ Frame p âŒœÏ†âŒ Q True.
+Global Instance frame_here_pure_persistent a Ï† Q :
+  FromPure a Q Ï† â†’ Frame true âŒœÏ†âŒ Q emp.
 Proof.
-  rewrite /FromPure /Frame=> <-.
-  by rewrite intuitionistically_if_elim sep_elim_l.
+  rewrite /FromPure /Frame /= => <-. rewrite right_id.
+  by rewrite -affinely_affinely_if intuitionistically_affinely.
+Qed.
+Global Instance frame_here_pure a Ï† Q :
+  FromPure a Q Ï† â†’
+  TCOr (TCEq a false) (BiAffine PROP) â†’
+  Frame false âŒœÏ†âŒ Q emp.
+Proof.
+  rewrite /FromPure /Frame => <- [->|?] /=.
+  - by rewrite right_id.
+  - by rewrite right_id -affinely_affinely_if affine_affinely.
 Qed.
 
 Global Instance make_embed_pure `{BiEmbed PROP PROP'} Ï† :
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index bb9c0726b..8b61e7173 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -300,10 +300,11 @@ Tactic Notation "iEmpIntro" :=
 Tactic Notation "iPureIntro" :=
   iStartProof;
   eapply tac_pure_intro;
-    [pm_reflexivity
-    |iSolveTC ||
+    [iSolveTC ||
      let P := match goal with |- FromPure _ ?P _ => P end in
      fail "iPureIntro:" P "not pure"
+    |pm_reduce; iSolveTC ||
+     fail "iPureIntro: spatial context contains non-affine hypotheses"
     |].
 
 (** Framing *)
@@ -780,7 +781,7 @@ Ltac iSpecializePat_go H1 pats :=
              fail "iSpecialize: cannot instantiate" P "with" Q
             |pm_reflexivity|iSpecializePat_go H1 pats]]
     | SPureGoal ?d :: ?pats =>
-       notypeclasses refine (tac_specialize_assert_pure _ _ H1 _ _ _ _ _ _ _ _ _ _ _ _);
+       notypeclasses refine (tac_specialize_assert_pure _ _ H1 _ _ _ _ _ _ _ _ _ _ _ _ _);
          [pm_reflexivity ||
           let H1 := pretty_ident H1 in
           fail "iSpecialize:" H1 "not found"
diff --git a/theories/proofmode/monpred.v b/theories/proofmode/monpred.v
index 185eaf989..0c9e1e9f3 100644
--- a/theories/proofmode/monpred.v
+++ b/theories/proofmode/monpred.v
@@ -202,8 +202,8 @@ Global Instance from_pure_monPred_at a P Ï† i : FromPure a P Ï† â†’ FromPure a (
 Proof. rewrite /FromPure=><-. by rewrite monPred_at_affinely_if monPred_at_pure. Qed.
 Global Instance into_pure_monPred_in i j : @IntoPure PROP (monPred_in i j) (i âŠ‘ j).
 Proof. by rewrite /IntoPure monPred_at_in. Qed.
-Global Instance from_pure_monPred_in i j af : @FromPure PROP af (monPred_in i j) (i âŠ‘ j).
-Proof. by rewrite /FromPure monPred_at_in bi.affinely_if_elim. Qed.
+Global Instance from_pure_monPred_in i j : @FromPure PROP false (monPred_in i j) (i âŠ‘ j).
+Proof. by rewrite /FromPure monPred_at_in. Qed.
 
 Global Instance into_persistent_monPred_at p P Q ð“  i :
   IntoPersistent p P Q â†’ MakeMonPredAt i Q ð“  â†’ IntoPersistent p (P i) ð“  | 0.
-- 
GitLab