From 37675f7b8b2127b4cee79457028f9731ec511db4 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 4 May 2016 22:21:31 +0200
Subject: [PATCH] Make iPureIntro also work with uPred_valid and uPred_eq.

---
 proofmode/coq_tactics.v | 8 ++++----
 proofmode/tactics.v     | 7 +++++--
 tests/proofmode.v       | 5 +++--
 3 files changed, 12 insertions(+), 8 deletions(-)

diff --git a/proofmode/coq_tactics.v b/proofmode/coq_tactics.v
index 29882b430..77406583c 100644
--- a/proofmode/coq_tactics.v
+++ b/proofmode/coq_tactics.v
@@ -292,10 +292,7 @@ Lemma tac_ex_falso Δ Q : Δ ⊢ False → Δ ⊢ Q.
 Proof. by rewrite -(False_elim Q). Qed.
 
 (** * Pure *)
-Lemma tac_pure_intro Δ (φ : Prop) : φ → Δ ⊢ ■ φ.
-Proof. apply const_intro. Qed.
-
-Class ToPure (P : uPred M) (φ : Prop) := to_pure : P ⊢ ■ φ.
+Class ToPure (P : uPred M) (φ : Prop) := to_pure : P ⊣⊢ ■ φ.
 Arguments to_pure : clear implicits.
 Global Instance to_pure_const φ : ToPure (■ φ) φ.
 Proof. done. Qed.
@@ -305,6 +302,9 @@ Proof. intros; red. by rewrite timeless_eq. Qed.
 Global Instance to_pure_valid `{CMRADiscrete A} (a : A) : ToPure (✓ a) (✓ a).
 Proof. intros; red. by rewrite discrete_valid. Qed.
 
+Lemma tac_pure_intro Δ Q (φ : Prop) : ToPure Q φ → φ → Δ ⊢ Q.
+Proof. intros ->. apply const_intro. Qed.
+
 Lemma tac_pure Δ Δ' i p P φ Q :
   envs_lookup_delete i Δ = Some (p, P, Δ') → ToPure P φ →
   (φ → Δ' ⊢ Q) → Δ ⊢ Q.
diff --git a/proofmode/tactics.v b/proofmode/tactics.v
index 222ae275c..4bfb81df0 100644
--- a/proofmode/tactics.v
+++ b/proofmode/tactics.v
@@ -113,7 +113,10 @@ Local Tactic Notation "iPure" constr(H) "as" simple_intropattern(pat) :=
      apply _ || fail "iPure:" H ":" P "not pure"
     |intros pat].
 
-Tactic Notation "iPureIntro" := apply uPred.const_intro.
+Tactic Notation "iPureIntro" :=
+  eapply tac_pure_intro;
+    [let P := match goal with |- ToPure ?P _ => P end in
+     apply _ || fail "iPureIntro:" P "not pure"|].
 
 (** * Specialize *)
 Record iTrm {X As} :=
@@ -751,5 +754,5 @@ Tactic Notation "iRewrite" "-" open_constr(t) "in" constr(H) :=
   iRewriteCore true t in H.
 
 (* Make sure that by and done solve trivial things in proof mode *)
-Hint Extern 0 (of_envs _ ⊢ _) => by apply tac_pure_intro.
+Hint Extern 0 (of_envs _ ⊢ _) => by iPureIntro.
 Hint Extern 0 (of_envs _ ⊢ _) => iAssumption.
diff --git a/tests/proofmode.v b/tests/proofmode.v
index b5e863c38..8146ab115 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -72,9 +72,10 @@ Proof.
 Qed.
 
 Lemma demo_6 (M : cmraT) (P Q : uPred M) :
-  True ⊢ (∀ x y z, x = 0 → y = 0 → z = 0 → P → □ Q → foo False).
+  True ⊢ (∀ x y z : nat,
+    x = plus 0 x → y = 0 → z = 0 → P → □ Q → foo (x ≡ x)).
 Proof.
   iIntros {a} "*".
   iIntros "#Hfoo **".
-  by iIntros "%".
+  by iIntros "# _".
 Qed.
-- 
GitLab