From 6f8c17a53f74b791f09700e82d2f00a18091b437 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 19 Sep 2016 17:46:04 +0200
Subject: [PATCH] Definition of FromPure that is symmetric w.r.t. IntoPure.

---
 proofmode/class_instances.v | 11 +++++++----
 proofmode/classes.v         |  2 +-
 proofmode/coq_tactics.v     |  5 +++--
 proofmode/pviewshifts.v     |  2 +-
 4 files changed, 12 insertions(+), 8 deletions(-)

diff --git a/proofmode/class_instances.v b/proofmode/class_instances.v
index 753eec0ac..3a8790f91 100644
--- a/proofmode/class_instances.v
+++ b/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 :
diff --git a/proofmode/classes.v b/proofmode/classes.v
index 83c1f2e7c..ac65c81e3 100644
--- a/proofmode/classes.v
+++ b/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.
diff --git a/proofmode/coq_tactics.v b/proofmode/coq_tactics.v
index 0917c2769..0c73bba5a 100644
--- a/proofmode/coq_tactics.v
+++ b/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 :
diff --git a/proofmode/pviewshifts.v b/proofmode/pviewshifts.v
index e3641da1c..ecdc794a5 100644
--- a/proofmode/pviewshifts.v
+++ b/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.
-- 
GitLab