diff --git a/tests/heap_lang.ref b/tests/heap_lang.ref
index 93e269e73fa8ba8423d143d3914f2e238794b36f..4a88fed5e105a649a4bf3022ac3dba5191bcfe1f 100644
--- a/tests/heap_lang.ref
+++ b/tests/heap_lang.ref
@@ -30,6 +30,28 @@
WP let: "x" := #l in let: "y" := ref #1 in "x" <- ! "x" + #1;; ! "x"
@ E [{ v, ⌜v = #2⌠}]
+"heap_e7_spec"
+ : string
+1 subgoal
+
+ Σ : gFunctors
+ H : heapG Σ
+ l : loc
+ ============================
+ _ : ▷ l ↦ #0
+ --------------------------------------∗
+ WP CAS #l #0 #1 {{ _, l ↦ #1 }}
+
+1 subgoal
+
+ Σ : gFunctors
+ H : heapG Σ
+ l : loc
+ ============================
+ _ : l ↦ #1
+ --------------------------------------∗
+ l ↦ #1
+
1 subgoal
Σ : gFunctors
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index 082649a8d3f0c0945daccfbefc99284e105af643..0ab4a6b4d2fc6ac2214562329bd427653eb17bd1 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -80,9 +80,13 @@ Section tests.
Definition heap_e7 : val := λ: "v", CAS "v" #0 #1.
- Lemma heap_e7_spec l : l ↦ #0 -∗ WP heap_e7 #l [{_, l ↦ #1 }].
+ Lemma heap_e7_spec_total l : l ↦ #0 -∗ WP heap_e7 #l [{_, l ↦ #1 }].
Proof. iIntros. wp_lam. wp_cas_suc. auto. Qed.
+ Check "heap_e7_spec".
+ Lemma heap_e7_spec l : ▷^2 l ↦ #0 -∗ WP heap_e7 #l {{_, l ↦ #1 }}.
+ Proof. iIntros. wp_lam. Show. wp_cas_suc. Show. auto. Qed.
+
Definition FindPred : val :=
rec: "pred" "x" "y" :=
let: "yp" := "y" + #1 in
diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index eb9ef069b83dad24a299e4cdf97a0232d957b92c..05eb1b56e759f5c1c5c787e33212a2640711f028 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -27,8 +27,6 @@ Tactic Notation "wp_expr_eval" tactic(t) :=
| _ => fail "wp_expr_eval: not a 'wp'"
end.
-Ltac wp_expr_simpl := wp_expr_eval simpl.
-
Lemma tac_wp_pure `{heapG Σ} Δ Δ' s E e1 e2 φ n Φ :
PureExec φ n e1 e2 →
φ →
@@ -55,8 +53,16 @@ Lemma tac_twp_value `{heapG Σ} Δ s E Φ v :
envs_entails Δ (Φ v) → envs_entails Δ (WP (Val v) @ s; E [{ Φ }]).
Proof. rewrite envs_entails_eq=> ->. by apply twp_value. Qed.
+Ltac wp_expr_simpl := wp_expr_eval simpl.
+
Ltac wp_value_head :=
- first [eapply tac_wp_value || eapply tac_twp_value]; reduction.pm_prettify.
+ first [eapply tac_wp_value || eapply tac_twp_value].
+
+Ltac wp_finish :=
+ wp_expr_simpl; (* simplify occurences of subst/fill *)
+ try wp_value_head; (* in case we have reached a value, get rid of the WP *)
+ pm_prettify. (* prettify â–·s caused by [MaybeIntoLaterNEnvs] and
+ λs caused by wp_value *)
Tactic Notation "wp_pure" open_constr(efoc) :=
iStartProof;
@@ -69,7 +75,7 @@ Tactic Notation "wp_pure" open_constr(efoc) :=
[iSolveTC (* PureExec *)
|try fast_done (* The pure condition for PureExec *)
|iSolveTC (* IntoLaters *)
- |wp_expr_simpl; try wp_value_head (* new goal *)
+ |wp_finish (* new goal *)
])
|| fail "wp_pure: cannot find" efoc "in" e "or" efoc "is not a redex"
| |- envs_entails _ (twp ?s ?E ?e ?Q) =>
@@ -79,7 +85,7 @@ Tactic Notation "wp_pure" open_constr(efoc) :=
eapply (tac_twp_pure _ _ _ (fill K e'));
[iSolveTC (* PureExec *)
|try fast_done (* The pure condition for PureExec *)
- |wp_expr_simpl; try wp_value_head (* new goal *)
+ |wp_finish (* new goal *)
])
|| fail "wp_pure: cannot find" efoc "in" e "or" efoc "is not a redex"
| _ => fail "wp_pure: not a 'wp'"
@@ -373,7 +379,7 @@ Tactic Notation "wp_alloc" ident(l) "as" constr(H) :=
first [intros l | fail 1 "wp_alloc:" l "not fresh"];
eexists; split;
[pm_reflexivity || fail "wp_alloc:" H "not fresh"
- |iDestructHyp Htmp as H; wp_expr_simpl; try wp_value_head] in
+ |iDestructHyp Htmp as H; wp_finish] in
wp_pures;
lazymatch goal with
| |- envs_entails _ (wp ?s ?E ?e ?Q) =>
@@ -405,13 +411,13 @@ Tactic Notation "wp_load" :=
|fail 1 "wp_load: cannot find 'Load' in" e];
[iSolveTC
|solve_mapsto ()
- |wp_expr_simpl; try wp_value_head]
+ |wp_finish]
| |- envs_entails _ (twp ?s ?E ?e ?Q) =>
first
[reshape_expr e ltac:(fun K e' => eapply (tac_twp_load _ _ _ _ K))
|fail 1 "wp_load: cannot find 'Load' in" e];
[solve_mapsto ()
- |wp_expr_simpl; try wp_value_head]
+ |wp_finish]
| _ => fail "wp_load: not a 'wp'"
end.
@@ -419,8 +425,6 @@ Tactic Notation "wp_store" :=
let solve_mapsto _ :=
let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
iAssumptionCore || fail "wp_store: cannot find" l "↦ ?" in
- let finish _ :=
- wp_expr_simpl; try first [wp_seq|wp_value_head] in
wp_pures;
lazymatch goal with
| |- envs_entails _ (wp ?s ?E ?e ?Q) =>
@@ -430,14 +434,14 @@ Tactic Notation "wp_store" :=
[iSolveTC
|solve_mapsto ()
|pm_reflexivity
- |finish ()]
+ |first [wp_seq|wp_finish]]
| |- envs_entails _ (twp ?s ?E ?e ?Q) =>
first
[reshape_expr e ltac:(fun K e' => eapply (tac_twp_store _ _ _ _ _ K))
|fail 1 "wp_store: cannot find 'Store' in" e];
[solve_mapsto ()
|pm_reflexivity
- |finish ()]
+ |first [wp_seq|wp_finish]]
| _ => fail "wp_store: not a 'wp'"
end.
@@ -455,8 +459,8 @@ Tactic Notation "wp_cas" "as" simple_intropattern(H1) "|" simple_intropattern(H2
|solve_mapsto ()
|pm_reflexivity
|try (fast_done || (left; fast_done) || (right; fast_done)) (* vals_cas_compare_safe *)
- |intros H1; wp_expr_simpl; try wp_value_head
- |intros H2; wp_expr_simpl; try wp_value_head]
+ |intros H1; wp_finish
+ |intros H2; wp_finish]
| |- envs_entails _ (twp ?E ?e ?Q) =>
first
[reshape_expr e ltac:(fun K e' => eapply (tac_twp_cas _ _ _ _ _ K))
@@ -464,8 +468,8 @@ Tactic Notation "wp_cas" "as" simple_intropattern(H1) "|" simple_intropattern(H2
[solve_mapsto ()
|pm_reflexivity
|try (fast_done || (left; fast_done) || (right; fast_done)) (* vals_cas_compare_safe *)
- |intros H1; wp_expr_simpl; try wp_value_head
- |intros H2; wp_expr_simpl; try wp_value_head]
+ |intros H1; wp_finish
+ |intros H2; wp_finish]
| _ => fail "wp_cas: not a 'wp'"
end.
@@ -483,7 +487,7 @@ Tactic Notation "wp_cas_fail" :=
|solve_mapsto ()
|try congruence
|try (fast_done || (left; fast_done) || (right; fast_done)) (* vals_cas_compare_safe *)
- |wp_expr_simpl; try wp_value_head]
+ |wp_finish]
| |- envs_entails _ (twp ?s ?E ?e ?Q) =>
first
[reshape_expr e ltac:(fun K e' => eapply (tac_twp_cas_fail _ _ _ _ K))
@@ -491,7 +495,7 @@ Tactic Notation "wp_cas_fail" :=
[solve_mapsto ()
|try congruence
|try (fast_done || (left; fast_done) || (right; fast_done)) (* vals_cas_compare_safe *)
- |wp_expr_simpl; try wp_value_head]
+ |wp_finish]
| _ => fail "wp_cas_fail: not a 'wp'"
end.
@@ -510,7 +514,7 @@ Tactic Notation "wp_cas_suc" :=
|pm_reflexivity
|try congruence
|try fast_done (* vals_cas_compare_safe *)
- |wp_expr_simpl; try wp_value_head]
+ |wp_finish]
| |- envs_entails _ (twp ?s ?E ?e ?Q) =>
first
[reshape_expr e ltac:(fun K e' => eapply (tac_twp_cas_suc _ _ _ _ _ K))
@@ -519,7 +523,7 @@ Tactic Notation "wp_cas_suc" :=
|pm_reflexivity
|try congruence
|try fast_done (* vals_cas_compare_safe *)
- |wp_expr_simpl; try wp_value_head]
+ |wp_finish]
| _ => fail "wp_cas_suc: not a 'wp'"
end.
@@ -536,13 +540,13 @@ Tactic Notation "wp_faa" :=
[iSolveTC
|solve_mapsto ()
|pm_reflexivity
- |wp_expr_simpl; try wp_value_head]
+ |wp_finish]
| |- envs_entails _ (twp ?s ?E ?e ?Q) =>
first
[reshape_expr e ltac:(fun K e' => eapply (tac_twp_faa _ _ _ _ _ K))
|fail 1 "wp_faa: cannot find 'CAS' in" e];
[solve_mapsto ()
|pm_reflexivity
- |wp_expr_simpl; try wp_value_head]
+ |wp_finish]
| _ => fail "wp_faa: not a 'wp'"
end.