From f5a3065b21789315c0e71ac55eef33803a45b990 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 16 Jan 2018 21:15:42 +0100
Subject: [PATCH] Make `iEval` more robust by using a let binding internally.

This is to make sure that e.g. `//` in `iEval (rewrite .. // ..)` does
not immediately close the goal by reflexivity.
---
 theories/heap_lang/proofmode.v   | 12 +++++++-----
 theories/proofmode/coq_tactics.v |  6 ++++--
 theories/proofmode/tactics.v     |  5 +++--
 theories/tests/proofmode.v       |  7 +++++++
 4 files changed, 21 insertions(+), 9 deletions(-)

diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index 24a22025c..e8513242c 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -6,18 +6,20 @@ Set Default Proof Using "Type".
 Import uPred.
 
 Lemma tac_wp_expr_eval `{heapG Σ} Δ s E Φ e e' :
-  e = e' →
+  (∀ (e'':=e'), e = e'') →
   envs_entails Δ (WP e' @ s; E {{ Φ }}) → envs_entails Δ (WP e @ s; E {{ Φ }}).
 Proof. by intros ->. Qed.
 Lemma tac_twp_expr_eval `{heapG Σ} Δ s E Φ e e' :
-  e = e' →
+  (∀ (e'':=e'), e = e'') →
   envs_entails Δ (WP e' @ s; E [{ Φ }]) → envs_entails Δ (WP e @ s; E [{ Φ }]).
 Proof. by intros ->. Qed.
 
 Tactic Notation "wp_expr_eval" tactic(t) :=
-  try iStartProof;
-  try (first [eapply tac_wp_expr_eval|eapply tac_twp_expr_eval];
-       [t; reflexivity|]).
+  try (
+    iStartProof;
+    first [eapply tac_wp_expr_eval|eapply tac_twp_expr_eval];
+      [let x := fresh in intros x; t; unfold x; reflexivity
+      |]).
 
 Ltac wp_expr_simpl := wp_expr_eval simpl.
 Ltac wp_expr_simpl_subst := wp_expr_eval simpl_subst.
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index ac28a1a1b..73503b361 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -414,13 +414,15 @@ Qed.
 
 (** * Basic rules *)
 Lemma tac_eval Δ Q Q' :
-  (Q' ⊢ Q) →
+  (∀ (Q'':=Q'), Q'' ⊢ Q) → (* We introduce [Q''] as a let binding so that
+    tactics like `reflexivity` as called by [rewrite //] do not eagerly unify
+    it with [Q]. See [test_iEval] in [tests/proofmode]. *)
   envs_entails Δ Q' → envs_entails Δ Q.
 Proof. by intros <-. Qed.
 
 Lemma tac_eval_in Δ Δ' i p P P' Q :
   envs_lookup i Δ = Some (p, P) →
-  (P ⊢ P') →
+  (∀ (P'':=P'), P ⊢ P') →
   envs_simple_replace i p (Esnoc Enil i P') Δ  = Some Δ' →
   envs_entails Δ' Q → envs_entails Δ Q.
 Proof.
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 444ed4069..d09938c84 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -83,13 +83,14 @@ Ltac iStartProof :=
 (** * Simplification *)
 Tactic Notation "iEval" tactic(t) :=
   iStartProof;
-  eapply tac_eval; [t; reflexivity|].
+  eapply tac_eval;
+    [let x := fresh in intros x; t; unfold x; reflexivity|].
 
 Tactic Notation "iEval" tactic(t) "in" constr(H) :=
   iStartProof;
   eapply tac_eval_in with _ H _ _ _;
     [env_reflexivity || fail "iEval:" H "not found"
-    |t; reflexivity
+    |let x := fresh in intros x; t; unfold x; reflexivity
     |env_reflexivity
     |].
 
diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index caaabaec9..f257ff719 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -285,6 +285,13 @@ Proof. iIntros "H". iNext. by iNext. Qed.
 Lemma test_iNext_laterN_laterN P n1 n2 : ▷ ▷^n1 ▷^n2 P ⊢ ▷^n1 ▷^n2 ▷ P.
 Proof. iIntros "H". iNext. iNext. by iNext. Qed.
 
+Lemma test_iEval x y : ⌜ (y + x)%nat = 1 ⌝ -∗ ⌜ S (x + y) = 2%nat ⌝ : uPred M.
+Proof.
+  iIntros (H).
+  iEval (rewrite (Nat.add_comm x y) // H).
+  done.
+Qed.
+
 (* TODO: This test is broken in Coq 8.6. Should be restored once we drop Coq
 8.6 support. See also issue #108. *)
 (*
-- 
GitLab