diff --git a/CHANGELOG.md b/CHANGELOG.md
index 6cdea08d79f189fdcb5962578a19da5586ac4c04..aff5d2f3f046f1c2f0702d843251c4b71765c5e4 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -5,6 +5,10 @@ Coq development, but not every API-breaking change is listed.  Changes marked
 
 ## Iris master
 
+Changes in and extensions of the theory:
+
+* [#] Weakestpre for total program correctness.
+
 Changes in Coq:
 
 * Rename `timelessP` -> `timeless` (projection of the `Timeless` class)
diff --git a/ProofMode.md b/ProofMode.md
index dc14b03b649684b623cf9de8da7a3f9c49b77f53..02aabe071b0533e754b3e7a0fd38a24305b6da21 100644
--- a/ProofMode.md
+++ b/ProofMode.md
@@ -150,11 +150,22 @@ Induction
   variables `x1 ... xn`, the hypotheses given by the selection pattern `selpat`,
   and the spatial context.
 
-Rewriting
----------
+Rewriting / simplification
+--------------------------
+
+- `iRewrite pm_trm` / `iRewrite pm_trm in "H"` : rewrite using an internal
+  equality in the proof mode goal / hypothesis `H`.
+- `iEval (tac)` / `iEval (tac) in H` : performs a tactic `tac` on the proof mode
+  goal / hypothesis `H`. The tactic `tac` should be a reduction or rewriting
+  tactic like `simpl`, `cbv`, `lazy`, `rewrite` or `setoid_rewrite`. The `iEval`
+  tactic is implemented by running `tac` on `?evar ⊢ P` / `P ⊢ ?evar` where `P`
+  is the proof goal / hypothesis `H`. After running `tac`, `?evar` is unified
+  with the resulting `P`, which in turn becomes the new proof mode goal /
+  hypothesis `H`.
+  Note that parentheses around `tac` are needed.
+- `iSimpl` / `iSimpl in H` : performs `simpl` on the proof mode goal /
+  hypothesis `H`. This is a shorthand for `iEval (simpl)`.
 
-- `iRewrite pm_trm` : rewrite an equality in the conclusion.
-- `iRewrite pm_trm in "H"` : rewrite an equality in the hypothesis `H`.
 
 Iris
 ----
diff --git a/theories/base_logic/lib/boxes.v b/theories/base_logic/lib/boxes.v
index 3c9580e0bffb1c21ef315e8b3fdf5e631652dc9d..3bda9e53e2224c24e6488aeef323aff5e1224565 100644
--- a/theories/base_logic/lib/boxes.v
+++ b/theories/base_logic/lib/boxes.v
@@ -208,7 +208,7 @@ Lemma box_fill E f P :
 Proof.
   iIntros (?) "H HP"; iDestruct "H" as (Φ) "[#HeqP Hf]".
   iExists Φ; iSplitR; first by rewrite big_opM_fmap.
-  rewrite internal_eq_iff later_iff big_sepM_later.
+  iEval (rewrite internal_eq_iff later_iff big_sepM_later) in "HeqP".
   iDestruct ("HeqP" with "HP") as "HP".
   iCombine "Hf" "HP" as "Hf".
   rewrite -big_opM_opM big_opM_fmap; iApply (fupd_big_sepM _ _ f).
diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index bd97cb7c9efcc4d6de157740a97c3dd37f413752..593f812d7e2263c7faf21bd2ead38e58c560151c 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -6,18 +6,19 @@ 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) :=
   iStartProof;
   try (first [eapply tac_wp_expr_eval|eapply tac_twp_expr_eval];
-       [t; reflexivity|]).
+       [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/program_logic/adequacy.v b/theories/program_logic/adequacy.v
index 81f9f1e30d5d2058c061eec0c6cc8243f39337af..e48ae659604aa0d99e2aafac2c6d6dca5fe7994b 100644
--- a/theories/program_logic/adequacy.v
+++ b/theories/program_logic/adequacy.v
@@ -128,7 +128,7 @@ Lemma wptp_result s n e1 t1 v2 t2 σ1 σ2 φ :
 Proof.
   intros. rewrite wptp_steps // laterN_later. apply: bupd_iter_laterN_mono.
   iDestruct 1 as (e2 t2' ?) "((Hw & HE & _) & H & _)"; simplify_eq.
-  iDestruct (wp_value_inv with "H") as "H". rewrite uPred_fupd_eq.
+  iDestruct (wp_value_inv' with "H") as "H". rewrite uPred_fupd_eq.
   iMod ("H" with "[Hw HE]") as ">(_ & _ & $)"; iFrame; auto.
 Qed.
 
diff --git a/theories/program_logic/total_weakestpre.v b/theories/program_logic/total_weakestpre.v
index b15adb301cfcb98c99d3b963f3a623875dfb8442..dd0d0628b0d4d8afdc661bf441e7c779d850583f 100644
--- a/theories/program_logic/total_weakestpre.v
+++ b/theories/program_logic/total_weakestpre.v
@@ -222,7 +222,7 @@ Qed.
 
 Lemma twp_value' s E Φ v : Φ v -∗ WP of_val v @ s; E [{ Φ }].
 Proof. iIntros "HΦ". rewrite twp_unfold /twp_pre to_of_val. auto. Qed.
-Lemma twp_value_inv s E Φ v : WP of_val v @ s; E [{ Φ }] ={E}=∗ Φ v.
+Lemma twp_value_inv' s E Φ v : WP of_val v @ s; E [{ Φ }] ={E}=∗ Φ v.
 Proof. by rewrite twp_unfold /twp_pre to_of_val. Qed.
 
 Lemma twp_strong_mono s1 s2 E1 E2 e Φ Ψ :
@@ -267,7 +267,7 @@ Proof.
     + iMod ("H" with "[$]") as "[H _]". iDestruct "H" as %(? & ? & ? & ?).
       by edestruct (atomic _ _ _ _ Hstep).
   - destruct (atomic _ _ _ _ Hstep) as [v <-%of_to_val].
-    iMod (twp_value_inv with "H") as ">H". iFrame "Hphy". by iApply twp_value'.
+    iMod (twp_value_inv' with "H") as ">H". iFrame "Hphy". by iApply twp_value'.
 Qed.
 
 Lemma twp_bind K `{!LanguageCtx K} s E e Φ :
@@ -348,6 +348,8 @@ Lemma twp_value_fupd' s E Φ v : (|={E}=> Φ v) -∗ WP of_val v @ s; E [{ Φ }]
 Proof. intros. by rewrite -twp_fupd -twp_value'. Qed.
 Lemma twp_value_fupd s E Φ e v `{!IntoVal e v} : (|={E}=> Φ v) -∗ WP e @ s; E [{ Φ }].
 Proof. intros. rewrite -twp_fupd -twp_value //. Qed.
+Lemma twp_value_inv s E Φ e v `{!IntoVal e v} : WP e @ s; E [{ Φ }] ={E}=∗ Φ v.
+Proof. intros; rewrite -(of_to_val e v) //; by apply twp_value_inv'. Qed.
 
 Lemma twp_frame_l s E e Φ R : R ∗ WP e @ s; E [{ Φ }] -∗ WP e @ s; E [{ v, R ∗ Φ v }].
 Proof. iIntros "[? H]". iApply (twp_strong_mono with "H"); auto with iFrame. Qed.
diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v
index b5cfd329d94f4504e41e46ec79a76d0a1c1452d2..05416490d0dd369e2240635a97905444572255b1 100644
--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
@@ -207,7 +207,7 @@ Qed.
 
 Lemma wp_value' s E Φ v : Φ v ⊢ WP of_val v @ s; E {{ Φ }}.
 Proof. iIntros "HΦ". rewrite wp_unfold /wp_pre to_of_val. auto. Qed.
-Lemma wp_value_inv s E Φ v : WP of_val v @ s; E {{ Φ }} ={E}=∗ Φ v.
+Lemma wp_value_inv' s E Φ v : WP of_val v @ s; E {{ Φ }} ={E}=∗ Φ v.
 Proof. by rewrite wp_unfold /wp_pre to_of_val. Qed.
 
 Lemma wp_strong_mono s1 s2 E1 E2 e Φ Ψ :
@@ -251,7 +251,7 @@ Proof.
     + iMod ("H" with "[$]") as "[H _]". iDestruct "H" as %(? & ? & ? & ?).
       by edestruct (atomic _ _ _ _ Hstep).
   - destruct (atomic _ _ _ _ Hstep) as [v <-%of_to_val].
-    iMod (wp_value_inv with "H") as ">H". iFrame "Hphy". by iApply wp_value'.
+    iMod (wp_value_inv' with "H") as ">H". iFrame "Hphy". by iApply wp_value'.
 Qed.
 
 Lemma wp_step_fupd s E1 E2 e P Φ :
@@ -321,6 +321,8 @@ Proof. intros. by rewrite -wp_fupd -wp_value'. Qed.
 Lemma wp_value_fupd s E Φ e v `{!IntoVal e v} :
   (|={E}=> Φ v) ⊢ WP e @ s; E {{ Φ }}.
 Proof. intros. rewrite -wp_fupd -wp_value //. Qed.
+Lemma wp_value_inv s E Φ e v `{!IntoVal e v} : WP e @ s; E {{ Φ }} ={E}=∗ Φ v.
+Proof. intros; rewrite -(of_to_val e v) //; by apply wp_value_inv'. Qed.
 
 Lemma wp_frame_l s E e Φ R : R ∗ WP e @ s; E {{ Φ }} ⊢ WP e @ s; E {{ v, R ∗ Φ v }}.
 Proof. iIntros "[? H]". iApply (wp_strong_mono with "H"); auto with iFrame. Qed.
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 9f94d98be364820abfb4452e78943e2d228d717b..a0f432a175b3fd5cc7e41c1a6d82cd2177dca775 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -460,9 +460,22 @@ 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.
+Proof. by intros <-. Qed.
+
+Lemma tac_eval_in Δ Δ' i p P P' Q :
+  envs_lookup i Δ = Some (p, P) →
+  (∀ (P'':=P'), P ⊢ P') →
+  envs_simple_replace i p (Esnoc Enil i P') Δ  = Some Δ' →
+  envs_entails Δ' Q → envs_entails Δ Q.
+Proof.
+  rewrite envs_entails_eq /=. intros ? HP ? <-.
+  rewrite envs_simple_replace_singleton_sound //; simpl.
+  by rewrite HP wand_elim_r.
+Qed.
 
 Class AffineEnv (Γ : env PROP) := affine_env : Forall Affine Γ.
 Global Instance affine_env_nil : AffineEnv Enil.
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 3755bba63b74ddd79cf2bb7ea8fd3a2a00112678..e915b21a8d60d50e496a1a72f3efcd95d0fb34ff 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -87,9 +87,29 @@ Tactic Notation "iStartProof" uconstr(PROP) :=
 
 (** * Simplification *)
 Tactic Notation "iEval" tactic(t) :=
-  iStartProof; try (eapply tac_eval; [t; reflexivity|]).
+  iStartProof;
+  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"
+    |let x := fresh in intros x; t; unfold x; reflexivity
+    |env_reflexivity
+    |].
 
 Tactic Notation "iSimpl" := iEval simpl.
+Tactic Notation "iSimpl" "in" constr(H) := iEval simpl in H.
+
+(* It would be nice to also have an `iSsrRewrite`, however, for this we need to
+pass arguments to Ssreflect's `rewrite` like `/= foo /bar` in Ltac, see:
+
+  https://sympa.inria.fr/sympa/arc/coq-club/2018-01/msg00000.html
+
+PMP told me (= Robbert) in person that this is not possible today, but may be
+possible in Ltac2. *)
 
 (** * Context manipulation *)
 Tactic Notation "iRename" constr(H1) "into" constr(H2) :=
diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index 41cbbb148de27fa7921c888bc26ca4f55fcbeca9..55f7f55abae02197b572095738fe11e1c0d05a47 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -314,4 +314,10 @@ Lemma test_assert_pure (φ : Prop) P :
   φ → P ⊢ P ∗ ⌜φ⌝.
 Proof. iIntros (Hφ). iAssert ⌜φ⌝%I with "[%]" as "$"; auto. Qed.
 
+Lemma test_iEval x y : ⌜ (y + x)%nat = 1 ⌝ -∗ ⌜ S (x + y) = 2%nat ⌝ : PROP.
+Proof.
+  iIntros (H).
+  iEval (rewrite (Nat.add_comm x y) // H).
+  done.
+Qed.
 End tests.