Split IsPure into IntoPure and FromPure.

This tweak allows us to declare pvs as an instance of FromPure (it is not
an instance of IntoPure), making some tactics (like iPureIntro and done)
work with pvs too.

proofmode/classes.v

@@ -17,15 +17,24 @@ Global Instance from_assumption_always_r P Q :
   FromAssumption true P Q → FromAssumption true P (□ Q).
 Proof. rewrite /FromAssumption=><-. by rewrite always_always. Qed.
 
-Class IsPure (P : uPred M) (φ : Prop) := is_pure : P ⊣⊢ ■ φ.
-Global Arguments is_pure : clear implicits.
-Global Instance is_pure_pure φ : IsPure (■ φ) φ.
+Class IntoPure (P : uPred M) (φ : Prop) := into_pure : P ⊢ ■ φ.
+Global Arguments into_pure : clear implicits.
+Global Instance into_pure_pure φ : IntoPure (■ φ) φ.
 Proof. done. Qed.
-Global Instance is_pure_eq {A : cofeT} (a b : A) :
-  Timeless a → IsPure (a ≡ b) (a ≡ b).
-Proof. intros; red. by rewrite timeless_eq. Qed.
-Global Instance is_pure_valid `{CMRADiscrete A} (a : A) : IsPure (✓ a) (✓ a).
-Proof. intros; red. by rewrite discrete_valid. Qed.
+Global Instance into_pure_eq {A : cofeT} (a b : A) :
+  Timeless a → IntoPure (a ≡ b) (a ≡ b).
+Proof. intros. by rewrite /IntoPure timeless_eq. Qed.
+Global Instance into_pure_valid `{CMRADiscrete A} (a : A) : IntoPure (✓ a) (✓ a).
+Proof. by rewrite /IntoPure discrete_valid. Qed.
+
+Class FromPure (P : uPred M) (φ : Prop) := from_pure : φ → True ⊢ P.
+Global Arguments from_pure : clear implicits.
+Global Instance from_pure_pure φ : FromPure (■ φ) φ.
+Proof. intros ?. by apply pure_intro. Qed.
+Global Instance from_pure_eq {A : cofeT} (a b : A) : FromPure (a ≡ b) (a ≡ b).
+Proof. intros ->. apply eq_refl. Qed.
+Global Instance from_pure_valid {A : cmraT} (a : A) : FromPure (✓ a) (✓ a).
+Proof. intros ?. by apply valid_intro. Qed.
 
 Class IntoPersistentP (P Q : uPred M) := into_persistentP : P ⊢ □ Q.
 Global Arguments into_persistentP : clear implicits.

proofmode/coq_tactics.v

@@ -316,15 +316,15 @@ Lemma tac_ex_falso Δ Q : (Δ ⊢ False) → Δ ⊢ Q.
 Proof. by rewrite -(False_elim Q). Qed.
 
 (** * Pure *)
-Lemma tac_pure_intro Δ Q (φ : Prop) : IsPure Q φ → φ → Δ ⊢ Q.
-Proof. intros ->. apply pure_intro. Qed.
+Lemma tac_pure_intro Δ Q (φ : Prop) : FromPure Q φ → φ → Δ ⊢ Q.
+Proof. intros ??. rewrite -(from_pure Q) //. apply True_intro. Qed.
 
 Lemma tac_pure Δ Δ' i p P φ Q :
-  envs_lookup_delete i Δ = Some (p, P, Δ') → IsPure P φ →
+  envs_lookup_delete i Δ = Some (p, P, Δ') → IntoPure P φ →
   (φ → Δ' ⊢ Q) → Δ ⊢ Q.
 Proof.
   intros ?? HQ. rewrite envs_lookup_delete_sound' //; simpl.
-  rewrite (is_pure P); by apply pure_elim_sep_l.
+  rewrite (into_pure P); by apply pure_elim_sep_l.
 Qed.
 
 Lemma tac_pure_revert Δ φ Q : (Δ ⊢ ■ φ → Q) → (φ → Δ ⊢ Q).
@@ -405,9 +405,9 @@ Proof.
   intros ?? HQ. rewrite envs_app_sound //; simpl. apply impl_intro_l.
   by rewrite right_id {1}(into_persistentP P) always_and_sep_l wand_elim_r.
 Qed.
-Lemma tac_impl_intro_pure Δ P φ Q : IsPure P φ → (φ → Δ ⊢ Q) → Δ ⊢ P → Q.
+Lemma tac_impl_intro_pure Δ P φ Q : IntoPure P φ → (φ → Δ ⊢ Q) → Δ ⊢ P → Q.
 Proof.
-  intros. by apply impl_intro_l; rewrite (is_pure P); apply pure_elim_l.
+  intros. by apply impl_intro_l; rewrite (into_pure P); apply pure_elim_l.
 Qed.
 
 Lemma tac_wand_intro Δ Δ' i P Q :
@@ -423,9 +423,9 @@ Proof.
   intros. rewrite envs_app_sound //; simpl.
   rewrite right_id. by apply wand_mono.
 Qed.
-Lemma tac_wand_intro_pure Δ P φ Q : IsPure P φ → (φ → Δ ⊢ Q) → Δ ⊢ P -★ Q.
+Lemma tac_wand_intro_pure Δ P φ Q : IntoPure P φ → (φ → Δ ⊢ Q) → Δ ⊢ P -★ Q.
 Proof.
-  intros. by apply wand_intro_l; rewrite (is_pure P); apply pure_elim_sep_l.
+  intros. by apply wand_intro_l; rewrite (into_pure P); apply pure_elim_sep_l.
 Qed.
 
 (* This is pretty much [tac_specialize_assert] with [js:=[j]] and [tac_exact],
@@ -476,12 +476,12 @@ Qed.
 
 Lemma tac_specialize_pure Δ Δ' j q R P1 P2 φ Q :
   envs_lookup j Δ = Some (q, R) →
-  IntoWand R P1 P2 → IsPure P1 φ →
+  IntoWand R P1 P2 → FromPure P1 φ →
   envs_simple_replace j q (Esnoc Enil j P2) Δ = Some Δ' →
   φ → (Δ' ⊢ Q) → Δ ⊢ Q.
 Proof.
   intros. rewrite envs_simple_replace_sound //; simpl.
-  by rewrite right_id (into_wand R) (is_pure P1) pure_equiv // wand_True wand_elim_r.
+  by rewrite right_id (into_wand R) -(from_pure P1) // wand_True wand_elim_r.
 Qed.
 
 Lemma tac_specialize_persistent Δ Δ' Δ'' j q P1 P2 R Q :

proofmode/pviewshifts.v

@@ -7,6 +7,8 @@ Section pvs.
 Context {Λ : language} {Σ : iFunctor}.
 Implicit Types P Q : iProp Λ Σ.
 
+Global Instance from_pure_pvs E P φ : FromPure P φ → FromPure (|={E}=> P) φ.
+Proof. intros ??. by rewrite -pvs_intro (from_pure P). Qed.
 Global Instance from_assumption_pvs E p P Q :
   FromAssumption p P Q → FromAssumption p P (|={E}=> Q)%I.
 Proof. rewrite /FromAssumption=>->. apply pvs_intro. Qed.

proofmode/tactics.v

@@ -112,13 +112,13 @@ Local Tactic Notation "iPersistent" constr(H) :=
 Local Tactic Notation "iPure" constr(H) "as" simple_intropattern(pat) :=
   eapply tac_pure with _ H _ _ _; (* (i:=H1) *)
     [env_cbv; reflexivity || fail "iPure:" H "not found"
-    |let P := match goal with |- IsPure ?P _ => P end in
+    |let P := match goal with |- IntoPure ?P _ => P end in
      apply _ || fail "iPure:" H ":" P "not pure"
     |intros pat].
 
 Tactic Notation "iPureIntro" :=
   eapply tac_pure_intro;
-    [let P := match goal with |- IsPure ?P _ => P end in
+    [let P := match goal with |- FromPure ?P _ => P end in
      apply _ || fail "iPureIntro:" P "not pure"|].
 
 (** * Specialize *)
@@ -184,7 +184,7 @@ Local Tactic Notation "iSpecializePat" constr(H) constr(pat) :=
        eapply tac_specialize_pure with _ H1 _ _ _ _ _;
          [env_cbv; reflexivity || fail "iSpecialize:" H1 "not found"
          |solve_to_wand H1
-         |let Q := match goal with |- IsPure ?Q _ => Q end in
+         |let Q := match goal with |- FromPure ?Q _ => Q end in
           apply _ || fail "iSpecialize:" Q "not pure"
          |env_cbv; reflexivity
          |(*goal*)
@@ -505,11 +505,11 @@ Tactic Notation "iNext":=
 Local Tactic Notation "iIntro" "{" simple_intropattern(x) "}" := first
   [ (* (∀ _, _) *) apply tac_forall_intro; intros x
   | (* (?P → _) *) eapply tac_impl_intro_pure;
-     [let P := match goal with |- IsPure ?P _ => P end in
+     [let P := match goal with |- IntoPure ?P _ => P end in
       apply _ || fail "iIntro:" P "not pure"
      |intros x]
   | (* (?P -★ _) *) eapply tac_wand_intro_pure;
-     [let P := match goal with |- IsPure ?P _ => P end in
+     [let P := match goal with |- IntoPure ?P _ => P end in
       apply _ || fail "iIntro:" P "not pure"
      |intros x]
   |intros x].

tests/one_shot.v

@@ -71,7 +71,7 @@ Proof.
       + iSplit. iRight; iExists m; by iSplitL "Hl". eauto. }
     wp_let. iPvsIntro. iIntros "!". wp_seq.
     iDestruct "Hv" as "[%|Hv]"; last iDestruct "Hv" as {m} "[% Hγ']"; subst.
-    { wp_match. by iPvsIntro. }
+    { by wp_match. }
     wp_match. wp_focus (! _)%E.
     iInv> N as "[[Hl Hγ]|Hinv]"; last iDestruct "Hinv" as {m'} "[Hl Hγ]".
     { iCombine "Hγ" "Hγ'" as "Hγ". by iDestruct (own_valid with "Hγ") as "%". }

tests/proofmode.v

-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import tactics notation.
 From iris.proofmode Require Import pviewshifts invariants.
 
 Lemma demo_0 {M : ucmraT} (P Q : uPred M) :
@@ -103,6 +103,6 @@ Section iris.
     iApply ("H" with "[#] HP |==>[HQ] |==>").
     - done.
     - by iApply inv_alloc.
-    - by iPvsIntro.
+    - done.
   Qed.
 End iris.