Generalize `iPureIntro` to support non-empty spatial contexts with just affine hypotheses.

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.

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.
 

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.
 

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) φ.

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 ψ.

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 :

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'} φ :

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"

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.