From 6a086fc67cc07bd01d58a99c6d587e5329101258 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Mon, 12 Feb 2018 23:59:15 +0100
Subject: [PATCH] Make FromPure depend on an affinity parameter.

---
 theories/base_logic/base_logic.v     |   6 +-
 theories/proofmode/class_instances.v | 156 ++++++++++++++++-----------
 theories/proofmode/classes.v         |  27 ++---
 theories/proofmode/coq_tactics.v     |  17 +--
 theories/proofmode/monpred.v         |   8 +-
 theories/proofmode/tactics.v         |  10 +-
 theories/tests/proofmode.v           |  14 +++
 7 files changed, 145 insertions(+), 93 deletions(-)

diff --git a/theories/base_logic/base_logic.v b/theories/base_logic/base_logic.v
index bcc18e6fd..5a947722e 100644
--- a/theories/base_logic/base_logic.v
+++ b/theories/base_logic/base_logic.v
@@ -31,10 +31,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} (a : A) :
-  @FromPure (uPredI M) (âœ“ a) (âœ“ a).
+Global Instance from_pure_cmra_valid {A : cmraT} af (a : A) :
+  @FromPure (uPredI M) af (âœ“ a) (âœ“ a).
 Proof.
-  rewrite /FromPure. eapply bi.pure_elim; [done|]=> ?.
+  rewrite /FromPure. eapply bi.pure_elim; [by apply affinely_if_elim|]=> ?.
   rewrite -cmra_valid_intro //. by apply pure_intro.
 Qed.
 
diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index 52e0daac8..93383cc92 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -138,8 +138,8 @@ Global Instance into_pure_pure_or (Ï†1 Ï†2 : Prop) P1 P2 :
   IntoPure P1 Ï†1 â†’ IntoPure P2 Ï†2 â†’ IntoPure (P1 âˆ¨ P2) (Ï†1 âˆ¨ Ï†2).
 Proof. rewrite /IntoPure pure_or. by intros -> ->. Qed.
 Global Instance into_pure_pure_impl (Ï†1 Ï†2 : Prop) P1 P2 :
-  FromPure P1 Ï†1 â†’ IntoPure P2 Ï†2 â†’ IntoPure (P1 â†’ P2) (Ï†1 â†’ Ï†2).
-Proof. rewrite /FromPure /IntoPure pure_impl. by intros -> ->. Qed.
+  FromPure false P1 Ï†1 â†’ IntoPure P2 Ï†2 â†’ IntoPure (P1 â†’ P2) (Ï†1 â†’ Ï†2).
+Proof. rewrite /FromPure /IntoPure pure_impl=> <- -> //. Qed.
 
 Global Instance into_pure_exist {A} (Î¦ : A â†’ PROP) (Ï† : A â†’ Prop) :
   (âˆ€ x, IntoPure (Î¦ x) (Ï† x)) â†’ IntoPure (âˆƒ x, Î¦ x) (âˆƒ x, Ï† x).
@@ -152,8 +152,13 @@ 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 P1 Ï†1 â†’ IntoPure P2 Ï†2 â†’ IntoPure (P1 -âˆ— P2) (Ï†1 â†’ Ï†2).
-Proof. rewrite /FromPure /IntoPure=> <- ->. by rewrite pure_impl impl_wand_2. Qed.
+  FromPure true 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 //.
+Qed.
 
 Global Instance into_pure_affinely P Ï† :
   IntoPure P Ï† â†’ IntoPure (bi_affinely P) Ï†.
@@ -170,53 +175,83 @@ Global Instance into_pure_embed `{BiEmbedding PROP PROP'} P Ï† :
 Proof. rewrite /IntoPure=> ->. by rewrite bi_embed_pure. Qed.
 
 (* FromPure *)
-Global Instance from_pure_pure Ï† : @FromPure PROP âŒœÏ†âŒ Ï†.
-Proof. by rewrite /FromPure. Qed.
-Global Instance from_pure_pure_and (Ï†1 Ï†2 : Prop) P1 P2 :
-  FromPure P1 Ï†1 â†’ FromPure P2 Ï†2 â†’ FromPure (P1 âˆ§ P2) (Ï†1 âˆ§ Ï†2).
-Proof. rewrite /FromPure pure_and. by intros -> ->. Qed.
-Global Instance from_pure_pure_or (Ï†1 Ï†2 : Prop) P1 P2 :
-  FromPure P1 Ï†1 â†’ FromPure P2 Ï†2 â†’ FromPure (P1 âˆ¨ P2) (Ï†1 âˆ¨ Ï†2).
-Proof. rewrite /FromPure pure_or. by intros -> ->. Qed.
-Global Instance from_pure_pure_impl (Ï†1 Ï†2 : Prop) P1 P2 :
-  IntoPure P1 Ï†1 â†’ FromPure P2 Ï†2 â†’ FromPure (P1 â†’ P2) (Ï†1 â†’ Ï†2).
-Proof. rewrite /FromPure /IntoPure pure_impl. by intros -> ->. Qed.
-
-Global Instance from_pure_exist {A} (Î¦ : A â†’ PROP) (Ï† : A â†’ Prop) :
-  (âˆ€ x, FromPure (Î¦ x) (Ï† x)) â†’ FromPure (âˆƒ x, Î¦ x) (âˆƒ x, Ï† x).
-Proof. rewrite /FromPure=>Hx. rewrite pure_exist. by setoid_rewrite Hx. Qed.
-Global Instance from_pure_forall {A} (Î¦ : A â†’ PROP) (Ï† : A â†’ Prop) :
-  (âˆ€ x, FromPure (Î¦ x) (Ï† x)) â†’ FromPure (âˆ€ x, Î¦ x) (âˆ€ x, Ï† x).
-Proof. rewrite /FromPure=>Hx. rewrite pure_forall. by setoid_rewrite Hx. Qed.
-
-Global Instance from_pure_pure_sep (Ï†1 Ï†2 : Prop) P1 P2 :
-  FromPure P1 Ï†1 â†’ FromPure P2 Ï†2 â†’ FromPure (P1 âˆ— P2) (Ï†1 âˆ§ Ï†2).
-Proof. rewrite /FromPure=> <- <-. by rewrite pure_and persistent_and_sep_1. Qed.
-Global Instance from_pure_pure_wand (Ï†1 Ï†2 : Prop) P1 P2 :
-  IntoPure P1 Ï†1 â†’ FromPure P2 Ï†2 â†’ FromPure (P1 -âˆ— P2) (Ï†1 â†’ Ï†2).
-Proof.
-  rewrite /FromPure /IntoPure=> -> <-.
-  by rewrite pure_wand_forall pure_impl pure_impl_forall.
+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_pure_impl a (Ï†1 Ï†2 : Prop) P1 P2 :
+  IntoPure P1 Ï†1 â†’ FromPure a P2 Ï†2 â†’ FromPure a (P1 â†’ P2) (Ï†1 â†’ Ï†2).
+Proof.
+  rewrite /FromPure /IntoPure pure_impl=> -> <-. destruct a=>//=.
+  apply bi.impl_intro_l. by rewrite affinely_and_r bi.impl_elim_r.
+Qed.
+
+Global Instance from_pure_exist {A} a (Î¦ : A â†’ PROP) (Ï† : A â†’ Prop) :
+  (âˆ€ x, FromPure a (Î¦ x) (Ï† x)) â†’ FromPure a (âˆƒ x, Î¦ x) (âˆƒ x, Ï† x).
+Proof.
+  rewrite /FromPure=>Hx. rewrite pure_exist affinely_if_exist.
+  by setoid_rewrite Hx.
+Qed.
+Global Instance from_pure_forall {A} a (Î¦ : A â†’ PROP) (Ï† : A â†’ Prop) :
+  (âˆ€ x, FromPure a (Î¦ x) (Ï† x)) â†’ FromPure a (âˆ€ x, Î¦ x) (âˆ€ x, Ï† x).
+Proof.
+  rewrite /FromPure=>Hx. rewrite pure_forall. setoid_rewrite <-Hx.
+  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).
+Proof.
+  rewrite /FromPure=> <- <- /=. by rewrite -persistent_and_affinely_sep_l pure_and.
+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).
+Proof.
+  rewrite /FromPure /IntoPure=> -> <- /=.
+  by rewrite bi.affinely_if_elim pure_wand_forall pure_impl pure_impl_forall.
 Qed.
 
 Global Instance from_pure_plainly P Ï† :
-  FromPure P Ï† â†’ FromPure (bi_plainly P) Ï†.
+  FromPure false P Ï† â†’ FromPure false (bi_plainly P) Ï†.
 Proof. rewrite /FromPure=> <-. by rewrite plainly_pure. Qed.
-Global Instance from_pure_persistently P Ï† :
-  FromPure P Ï† â†’ FromPure (bi_persistently P) Ï†.
-Proof. rewrite /FromPure=> <-. by rewrite persistently_pure. Qed.
-Global Instance from_pure_affinely P Ï† `{!Affine P} :
-  FromPure P Ï† â†’ FromPure (bi_affinely P) Ï†.
-Proof. by rewrite /FromPure affine_affinely. Qed.
-Global Instance from_pure_absorbingly P Ï† : FromPure P Ï† â†’ FromPure (bi_absorbingly P) Ï†.
-Proof. rewrite /FromPure=> <-. by rewrite absorbingly_pure. Qed.
-Global Instance from_pure_embed `{BiEmbedding PROP PROP'} P Ï† :
-  FromPure P Ï† â†’ FromPure âŽ¡PâŽ¤ Ï†.
-Proof. rewrite /FromPure=> <-. by rewrite bi_embed_pure. Qed.
-
-Global Instance from_pure_bupd `{BUpdFacts PROP} P Ï† :
-  FromPure P Ï† â†’ FromPure (|==> P) Ï†.
-Proof. rewrite /FromPure=> ->. apply bupd_intro. Qed.
+Global Instance from_pure_persistently P a Ï† :
+  FromPure true P Ï† â†’ FromPure a (bi_persistently P) Ï†.
+Proof.
+  rewrite /FromPure=> <- /=.
+  by rewrite persistently_affinely affinely_if_elim persistently_pure.
+Qed.
+Global Instance from_pure_affinely_true P Ï† :
+  FromPure true P Ï† â†’ FromPure true (bi_affinely P) Ï†.
+Proof. rewrite /FromPure=><- /=. by rewrite affinely_idemp. Qed.
+Global Instance from_pure_affinely_false P Ï† `{!Affine P} :
+  FromPure false P Ï† â†’ FromPure false (bi_affinely P) Ï†.
+Proof. rewrite /FromPure /= affine_affinely //. Qed.
+
+Global Instance from_pure_absorbingly P Ï† :
+  FromPure true P Ï† â†’ FromPure false (bi_absorbingly P) Ï†.
+Proof. rewrite /FromPure=> <- /=. apply persistent_absorbingly_affinely, _. Qed.
+Global Instance from_pure_embed `{BiEmbedding PROP PROP'} a P Ï† :
+  FromPure a P Ï† â†’ FromPure a âŽ¡PâŽ¤ Ï†.
+Proof. rewrite /FromPure=> <-. by rewrite bi_embed_affinely_if bi_embed_pure. Qed.
+
+Global Instance from_pure_bupd `{BUpdFacts PROP} a P Ï† :
+  FromPure a P Ï† â†’ FromPure a (|==> P) Ï†.
+Proof. rewrite /FromPure=> <-. apply bupd_intro. Qed.
 
 (* IntoPersistent *)
 Global Instance into_persistent_persistently p P Q :
@@ -857,7 +892,7 @@ Proof.
   intros. by rewrite /Frame affinely_persistently_if_elim affinely_elim sep_elim_l.
 Qed.
 
-Global Instance frame_here_pure p Ï† Q : FromPure Q Ï† â†’ Frame p âŒœÏ†âŒ Q True.
+Global Instance frame_here_pure p Ï† Q : FromPure false Q Ï† â†’ Frame p âŒœÏ†âŒ Q True.
 Proof.
   rewrite /FromPure /Frame=> <-. by rewrite affinely_persistently_if_elim sep_elim_l.
 Qed.
@@ -1126,17 +1161,17 @@ Global Instance from_assumption_fupd `{FUpdFacts PROP} E p P Q :
 Proof. rewrite /FromAssumption=>->. apply bupd_fupd. Qed.
 
 (* FromPure *)
-Global Instance from_pure_internal_eq {A : ofeT} (a b : A) :
-  @FromPure PROP (a â‰¡ b) (a â‰¡ b).
-Proof. by rewrite /FromPure pure_internal_eq. Qed.
-Global Instance from_pure_later P Ï† : FromPure P Ï† â†’ FromPure (â–· P) Ï†.
+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_later a P Ï† : FromPure a P Ï† â†’ FromPure a (â–· P) Ï†.
 Proof. rewrite /FromPure=> ->. apply later_intro. Qed.
-Global Instance from_pure_laterN n P Ï† : FromPure P Ï† â†’ FromPure (â–·^n P) Ï†.
+Global Instance from_pure_laterN a n P Ï† : FromPure a P Ï† â†’ FromPure a (â–·^n P) Ï†.
 Proof. rewrite /FromPure=> ->. apply laterN_intro. Qed.
-Global Instance from_pure_except_0 P Ï† : FromPure P Ï† â†’ FromPure (â—‡ P) Ï†.
+Global Instance from_pure_except_0 a P Ï† : FromPure a P Ï† â†’ FromPure a (â—‡ P) Ï†.
 Proof. rewrite /FromPure=> ->. apply except_0_intro. Qed.
-Global Instance from_pure_fupd `{FUpdFacts PROP} E P Ï† :
-  FromPure P Ï† â†’ FromPure (|={E}=> P) Ï†.
+Global Instance from_pure_fupd `{FUpdFacts PROP} a E P Ï† :
+  FromPure a P Ï† â†’ FromPure a (|={E}=> P) Ï†.
 Proof. rewrite /FromPure. intros <-. apply fupd_intro. Qed.
 
 (* IntoPure *)
@@ -1333,16 +1368,17 @@ Global Instance into_forall_except_0 {A} P (Î¦ : A â†’ PROP) :
   IntoForall P Î¦ â†’ IntoForall (â—‡ P) (Î» a, â—‡ (Î¦ a))%I.
 Proof. rewrite /IntoForall=> HP. by rewrite HP except_0_forall. Qed.
 Global Instance into_forall_impl_pure Ï† P Q :
-  FromPureT P Ï† â†’ IntoForall (P â†’ Q) (Î» _ : Ï†, Q).
+  FromPureT false P Ï† â†’ IntoForall (P â†’ Q) (Î» _ : Ï†, Q).
 Proof.
   rewrite /FromPureT /FromPure /IntoForall=> -[Ï†' [-> <-]].
   by rewrite pure_impl_forall.
 Qed.
 Global Instance into_forall_wand_pure Ï† P Q :
-  Absorbing Q â†’ FromPureT P Ï† â†’ IntoForall (P -âˆ— Q) (Î» _ : Ï†, Q).
+  FromPureT true P Ï† â†’ IntoForall (P -âˆ— Q) (Î» _ : Ï†, Q).
 Proof.
-  rewrite /FromPureT /FromPure /IntoForall=> ? -[Ï†' [-> <-]].
-  by rewrite pure_wand_forall.
+  rewrite /FromPureT /FromPure /IntoForall=> -[Ï†' [-> <-]] /=.
+  apply forall_intro=>? /=.
+  by rewrite -(pure_intro True%I) // /bi_affinely right_id emp_wand.
 Qed.
 
 (* FromForall *)
diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index 5c2efcaf6..25e01bcbf 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -43,18 +43,19 @@ Proof. by exists Ï†. Qed.
 Hint Extern 0 (IntoPureT _ _) =>
   notypeclasses refine (into_pureT_hint _ _ _) : typeclass_instances.
 
-Class FromPure {PROP : bi} (P : PROP) (Ï† : Prop) :=
-  from_pure : âŒœÏ†âŒ âŠ¢ P.
-Arguments FromPure {_} _%I _%type_scope : simpl never.
-Arguments from_pure {_} _%I _%type_scope {_}.
-Hint Mode FromPure + ! - : typeclass_instances.
-
-Class FromPureT {PROP : bi} (P : PROP) (Ï† : Type) :=
-  from_pureT : âˆƒ Ïˆ : Prop, Ï† = Ïˆ âˆ§ FromPure P Ïˆ.
-Lemma from_pureT_hint {PROP : bi} (P : PROP) (Ï† : Prop) : FromPure P Ï† â†’ FromPureT P Ï†.
+Class FromPure {PROP : bi} (a : bool) (P : PROP) (Ï† : Prop) :=
+  from_pure : bi_affinely_if a âŒœÏ†âŒ âŠ¢ P.
+Arguments FromPure {_} _ _%I _%type_scope : simpl never.
+Arguments from_pure {_} _ _%I _%type_scope {_}.
+Hint Mode FromPure + + ! - : typeclass_instances.
+
+Class FromPureT {PROP : bi} (a : bool) (P : PROP) (Ï† : Type) :=
+  from_pureT : âˆƒ Ïˆ : Prop, Ï† = Ïˆ âˆ§ FromPure a P Ïˆ.
+Lemma from_pureT_hint {PROP : bi} (a : bool) (P : PROP) (Ï† : Prop) :
+  FromPure a P Ï† â†’ FromPureT a P Ï†.
 Proof. by exists Ï†. Qed.
-Hint Extern 0 (FromPureT _ _) =>
-  notypeclasses refine (from_pureT_hint _ _ _) : typeclass_instances.
+Hint Extern 0 (FromPureT _ _ _) =>
+  notypeclasses refine (from_pureT_hint _ _ _ _) : typeclass_instances.
 
 Class IntoInternalEq {PROP : sbi} {A : ofeT} (P : PROP) (x y : A) :=
   into_internal_eq : P âŠ¢ x â‰¡ y.
@@ -448,8 +449,8 @@ with the exception of:
 *)
 Instance into_pure_tc_opaque {PROP : bi} (P : PROP) Ï† :
   IntoPure P Ï† â†’ IntoPure (tc_opaque P) Ï† := id.
-Instance from_pure_tc_opaque {PROP : bi} (P : PROP) Ï† :
-  FromPure P Ï† â†’ FromPure (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) :
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 376a0806e..498e6f55b 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -520,8 +520,8 @@ Proof.
 Qed.
 
 (** * Pure *)
-Lemma tac_pure_intro Î” Q Ï† : FromPure Q Ï† â†’ Ï† â†’ envs_entails Î” Q.
-Proof. intros ??. rewrite /envs_entails -(from_pure Q). by apply pure_intro. Qed.
+Lemma tac_pure_intro Î” Q Ï† : FromPure false Q Ï† â†’ Ï† â†’ envs_entails Î” Q.
+Proof. intros ??. rewrite /envs_entails -(from_pure _ Q). by apply pure_intro. Qed.
 
 Lemma tac_pure Î” Î”' i p P Ï† Q :
   envs_lookup_delete i Î” = Some (p, P, Î”') â†’
@@ -821,13 +821,14 @@ Qed.
 Lemma tac_specialize_assert_pure Î” Î”' j q R P1 P2 Ï† Q :
   envs_lookup j Î” = Some (q, R) â†’
   IntoWand q true R P1 P2 â†’
-  FromPure P1 Ï† â†’
+  FromPure true P1 Ï† â†’
   envs_simple_replace j q (Esnoc Enil j P2) Î” = Some Î”' â†’
   Ï† â†’ envs_entails Î”' Q â†’ envs_entails Î” Q.
 Proof.
   rewrite /envs_entails=> ????? <-. rewrite envs_simple_replace_singleton_sound //=.
-  rewrite -affinely_persistently_if_idemp into_wand /= -(from_pure P1).
-  rewrite pure_True // persistently_pure affinely_True_emp affinely_emp.
+  rewrite -affinely_persistently_if_idemp into_wand /= -(from_pure _ P1).
+  rewrite pure_True //= persistently_affinely persistently_pure
+          affinely_True_emp affinely_emp.
   by rewrite emp_wand wand_elim_r.
 Qed.
 
@@ -926,14 +927,14 @@ Proof.
 Qed.
 
 Lemma tac_assert_pure Î” Î”' j P P' Ï† Q :
-  FromPure P Ï† â†’
+  FromPure true P Ï† â†’
   FromAffinely P' P â†’
   envs_app false (Esnoc Enil j P') Î” = Some Î”' â†’
   Ï† â†’ envs_entails Î”' Q â†’ envs_entails Î” Q.
 Proof.
   rewrite /envs_entails => ???? <-. rewrite envs_app_singleton_sound //=.
-  rewrite -(from_affinely P') -(from_pure P) pure_True //.
-  by rewrite affinely_True_emp affinely_emp emp_wand.
+  rewrite -(from_affinely P') -(from_pure _ P) pure_True //.
+  by rewrite affinely_idemp affinely_True_emp affinely_emp emp_wand.
 Qed.
 
 Lemma tac_pose_proof Î” Î”' j P Q :
diff --git a/theories/proofmode/monpred.v b/theories/proofmode/monpred.v
index f9461af7e..116f30b5d 100644
--- a/theories/proofmode/monpred.v
+++ b/theories/proofmode/monpred.v
@@ -157,12 +157,12 @@ Qed.
 
 Global Instance into_pure_monPred_at P Ï† i : IntoPure P Ï† â†’ IntoPure (P i) Ï†.
 Proof. rewrite /IntoPure=>->. by rewrite monPred_at_pure. Qed.
-Global Instance from_pure_monPred_at P Ï† i : FromPure P Ï† â†’ FromPure (P i) Ï†.
-Proof. rewrite /FromPure=><-. by rewrite monPred_at_pure. Qed.
+Global Instance from_pure_monPred_at a P Ï† i : FromPure a P Ï† â†’ FromPure a (P i) Ï†.
+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 : @FromPure PROP (monPred_in i j) (i âŠ‘ j).
-Proof. by rewrite /FromPure 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 into_persistent_monPred_at p P Q ð“  i :
   IntoPersistent p P Q â†’ MakeMonPredAt i Q ð“  â†’ IntoPersistent p (P i) ð“  | 0.
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 5d9765b17..12f7c8c5a 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -230,7 +230,7 @@ Tactic Notation "iPureIntro" :=
   iStartProof;
   eapply tac_pure_intro;
     [apply _ ||
-     let P := match goal with |- FromPure ?P _ => P end in
+     let P := match goal with |- FromPure _ ?P _ => P end in
      fail "iPureIntro:" P "not pure"
     |].
 
@@ -494,7 +494,7 @@ Local Tactic Notation "iSpecializePat" open_constr(H) constr(pat) :=
          [env_reflexivity || fail "iSpecialize:" H1 "not found"
          |solve_to_wand H1
          |apply _ ||
-          let Q := match goal with |- FromPure ?Q _ => Q end in
+          let Q := match goal with |- FromPure _ ?Q _ => Q end in
           fail "iSpecialize:" Q "not pure"
          |env_reflexivity
          |done_if d (*goal*)
@@ -1663,10 +1663,10 @@ Tactic Notation "iAssertCore" open_constr(Q)
   let Hs := spec_pat.parse Hs in
   lazymatch Hs with
   | [SPureGoal ?d] =>
-     eapply tac_assert_pure with _ H Q _;
-       [env_reflexivity
-       |apply _ || fail "iAssert:" Q "not pure"
+     eapply tac_assert_pure with _ H Q _ _;
+       [apply _ || fail "iAssert:" Q "not pure"
        |apply _
+       |env_reflexivity
        |done_if d (*goal*)
        |tac H]
   | [SGoal (SpecGoal GPersistent _ ?Hs_frame [] ?d)] =>
diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index 7389faf69..41cbbb148 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -300,4 +300,18 @@ Lemma test_iNext_later_laterN P n : â–·^n â–· P âŠ¢ â–· â–·^n P.
 Proof. iIntros "H". iNext. by iNext. Qed.
 Lemma test_iNext_laterN_laterN P n1 n2 : â–· â–·^n1 â–·^n2 P âŠ¢ â–·^n1 â–·^n2 â–· P.
 Proof. iIntros "H". iNext. iNext. by iNext. Qed.
+
+Lemma test_specialize_affine_pure (Ï† : Prop) P :
+  Ï† â†’ (bi_affinely âŒœÏ†âŒ -âˆ— P) âŠ¢ P.
+Proof.
+  iIntros (HÏ†) "H". by iSpecialize ("H" with "[% //]").
+Qed.
+
+Lemma test_assert_affine_pure (Ï† : Prop) P :
+  Ï† â†’ P âŠ¢ P âˆ— bi_affinely âŒœÏ†âŒ.
+Proof. iIntros (HÏ†). iAssert (bi_affinely âŒœÏ†âŒ) with "[%]" as "$"; auto. Qed.
+Lemma test_assert_pure (Ï† : Prop) P :
+  Ï† â†’ P âŠ¢ P âˆ— âŒœÏ†âŒ.
+Proof. iIntros (HÏ†). iAssert âŒœÏ†âŒ%I with "[%]" as "$"; auto. Qed.
+
 End tests.
-- 
GitLab