Commit a15dc76f authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Put heap_lang tactics in better order.

parent 335c29dd
...@@ -26,6 +26,7 @@ Tactic Notation "wp_expr_eval" tactic3(t) := ...@@ -26,6 +26,7 @@ Tactic Notation "wp_expr_eval" tactic3(t) :=
[let x := fresh in intros x; t; unfold x; notypeclasses refine eq_refl|] [let x := fresh in intros x; t; unfold x; notypeclasses refine eq_refl|]
| _ => fail "wp_expr_eval: not a 'wp'" | _ => fail "wp_expr_eval: not a 'wp'"
end. end.
Ltac wp_expr_simpl := wp_expr_eval simpl.
Lemma tac_wp_pure `{!heapG Σ} Δ Δ' s E K e1 e2 φ n Φ : Lemma tac_wp_pure `{!heapG Σ} Δ Δ' s E K e1 e2 φ n Φ :
PureExec φ n e1 e2 PureExec φ n e1 e2
...@@ -65,8 +66,6 @@ Lemma tac_twp_value `{!heapG Σ} Δ s E (Φ : val → iPropI Σ) v : ...@@ -65,8 +66,6 @@ Lemma tac_twp_value `{!heapG Σ} Δ s E (Φ : val → iPropI Σ) v :
envs_entails Δ (|={E}=> Φ v) envs_entails Δ (WP (Val v) @ s; E [{ Φ }]). envs_entails Δ (|={E}=> Φ v) envs_entails Δ (WP (Val v) @ s; E [{ Φ }]).
Proof. rewrite envs_entails_eq=> ->. by rewrite twp_value_fupd. Qed. Proof. rewrite envs_entails_eq=> ->. by rewrite twp_value_fupd. Qed.
Ltac wp_expr_simpl := wp_expr_eval simpl.
(** Simplify the goal if it is [WP] of a value. (** Simplify the goal if it is [WP] of a value.
If the postcondition already allows a fupd, do not add a second one. If the postcondition already allows a fupd, do not add a second one.
But otherwise, *do* add a fupd. This ensures that all the lemmas applied But otherwise, *do* add a fupd. This ensures that all the lemmas applied
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment