Merge branch 'robbert/twp_vals_compare_safe' into 'master'

Also use `solve_vals_compare_safe` in TWP case of `wp_pure`.

See merge request iris/iris!444

tests/heap_lang.v

@@ -121,6 +121,23 @@ Section tests.
     ⊢ WP let: "x" := Pred #42 in Pred "x" @ E [{ v, ⌜v = #40⌝ }].
   Proof. iIntros "". wp_apply Pred_spec. by wp_apply Pred_spec. Qed.
 
+  Definition Id : val :=
+    rec: "go" "x" :=
+      if: "x" = #0 then #() else "go" ("x" - #1).
+
+  (** These tests specially test the handling of the [vals_compare_safe]
+  side-condition of the [=] operator. *)
+  Lemma Id_wp (n : nat) : ⊢ WP Id #n {{ v, ⌜ v = #() ⌝ }}.
+  Proof.
+    iInduction n as [|n] "IH"; wp_rec; wp_pures; first done.
+    by replace (S n - 1) with (n:Z) by lia.
+  Qed.
+  Lemma Id_twp (n : nat) : ⊢ WP Id #n [{ v, ⌜ v = #() ⌝ }].
+  Proof.
+    iInduction n as [|n] "IH"; wp_rec; wp_pures; first done.
+    by replace (S n - 1) with (n:Z) by lia.
+  Qed.
+
   Lemma wp_apply_evar e P :
     P -∗ (∀ Q Φ, Q -∗ WP e {{ Φ }}) -∗ WP e {{ _, True }}.
   Proof. iIntros "HP HW". wp_apply "HW". iExact "HP". Qed.

theories/heap_lang/proofmode.v

@@ -97,7 +97,7 @@ Tactic Notation "wp_pure" open_constr(efoc) :=
       unify e' efoc;
       eapply (tac_twp_pure _ _ _ (fill K e'));
       [iSolveTC                       (* PureExec *)
-      |try fast_done                  (* The pure condition for PureExec *)
+      |try solve_vals_compare_safe    (* The pure condition for PureExec *)
       |wp_finish                      (* new goal *)
       ])
     || fail "wp_pure: cannot find" efoc "in" e "or" efoc "is not a redex"