Definition of FromPure that is symmetric w.r.t. IntoPure.

proofmode/class_instances.v

@@ -30,13 +30,16 @@ Proof. by rewrite /IntoPure discrete_valid. Qed.
 
 (* FromPure *)
 Global Instance from_pure_pure φ : @FromPure M (■ φ) φ.
-Proof. intros ?. by apply pure_intro. Qed.
+Proof. done. Qed.
 Global Instance from_pure_eq {A : cofeT} (a b : A) : @FromPure M (a ≡ b) (a ≡ b).
-Proof. intros ->. apply eq_refl. Qed.
+Proof. rewrite /FromPure. eapply pure_elim; [done|]=> ->. apply eq_refl'. Qed.
 Global Instance from_pure_valid {A : cmraT} (a : A) : @FromPure M (✓ a) (✓ a).
-Proof. intros ?. by apply valid_intro. Qed.
+Proof.
+  rewrite /FromPure. eapply pure_elim; [done|]=> ?.
+  rewrite -valid_intro //. auto with I.
+Qed.
 Global Instance from_pure_rvs P φ : FromPure P φ → FromPure (|=r=> P) φ.
-Proof. intros ??. by rewrite -rvs_intro (from_pure P). Qed.
+Proof. rewrite /FromPure=> ->. apply rvs_intro. Qed.
 
 (* IntoPersistentP *)
 Global Instance into_persistentP_always_trans P Q :

proofmode/classes.v

@@ -11,7 +11,7 @@ Global Arguments from_assumption _ _ _ {_}.
 Class IntoPure (P : uPred M) (φ : Prop) := into_pure : P ⊢ ■ φ.
 Global Arguments into_pure : clear implicits.
 
-Class FromPure (P : uPred M) (φ : Prop) := from_pure : φ → True ⊢ P.
+Class FromPure (P : uPred M) (φ : Prop) := from_pure : ■ φ ⊢ P.
 Global Arguments from_pure : clear implicits.
 
 Class IntoPersistentP (P Q : uPred M) := into_persistentP : P ⊢ □ Q.

proofmode/coq_tactics.v

@@ -318,7 +318,7 @@ Proof. by rewrite -(False_elim Q). Qed.
 
 (** * Pure *)
 Lemma tac_pure_intro Δ Q (φ : Prop) : FromPure Q φ → φ → Δ ⊢ Q.
-Proof. intros ??. rewrite -(from_pure Q) //. apply True_intro. Qed.
+Proof. intros ??. rewrite -(from_pure Q). by apply pure_intro. Qed.
 
 Lemma tac_pure Δ Δ' i p P φ Q :
   envs_lookup_delete i Δ = Some (p, P, Δ') → IntoPure P φ →
@@ -495,7 +495,8 @@ Lemma tac_specialize_assert_pure Δ Δ' j q R P1 P2 φ Q :
   φ → (Δ' ⊢ Q) → Δ ⊢ Q.
 Proof.
   intros. rewrite envs_simple_replace_sound //; simpl.
-  by rewrite right_id (into_wand R) -(from_pure P1) // wand_True wand_elim_r.
+  rewrite right_id (into_wand R) -(from_pure P1) pure_equiv //.
+  by rewrite wand_True wand_elim_r.
 Qed.
 
 Lemma tac_specialize_assert_persistent Δ Δ' Δ'' j q P1 P2 R Q :

proofmode/pviewshifts.v

@@ -8,7 +8,7 @@ Context `{irisG Λ Σ}.
 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.
+Proof. rewrite /FromPure. intros <-. apply pvs_intro. Qed.
 
 Global Instance from_assumption_pvs E p P Q :
   FromAssumption p P (|=r=> Q) → FromAssumption p P (|={E}=> Q)%I.