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

@@ -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.

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.

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
     |].
 

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. *)
 (*