From 6428df9193a30b1851d9f347610e5740da69ca8a Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 20 Feb 2016 20:38:33 +0100
Subject: [PATCH] write a tactic to strip away laters
---
barrier/barrier.v | 19 ++++++-------------
heap_lang/wp_tactics.v | 33 +++++++++++++++++++++++++++------
2 files changed, 33 insertions(+), 19 deletions(-)
diff --git a/barrier/barrier.v b/barrier/barrier.v
index c38926871..2b1c3de33 100644
--- a/barrier/barrier.v
+++ b/barrier/barrier.v
@@ -214,10 +214,8 @@ Section proof.
apply forall_intro=>-[p I]. apply wand_intro_l. rewrite -!assoc.
apply const_elim_sep_l=>Hs. destruct p; last done.
rewrite {1}/barrier_inv =>/={Hs}. rewrite later_sep.
- eapply wp_store; eauto with I ndisj.
- rewrite -!assoc. apply sep_mono_r. etrans; last eapply later_mono.
- { (* Is this really the best way to strip the later? *)
- erewrite later_sep. apply sep_mono_r. apply later_intro. }
+ eapply wp_store; eauto with I ndisj.
+ rewrite -!assoc. apply sep_mono_r. u_strip_later.
apply wand_intro_l. rewrite -(exist_intro (State High I)).
rewrite -(exist_intro ∅). rewrite const_equiv /=; last first.
{ apply rtc_once. constructor; first constructor;
@@ -249,9 +247,7 @@ Section proof.
apply const_elim_sep_l=>Hs.
rewrite {1}/barrier_inv =>/=. rewrite later_sep.
eapply wp_load; eauto with I ndisj.
- rewrite -!assoc. apply sep_mono_r. etrans; last eapply later_mono.
- { (* Is this really the best way to strip the later? *)
- erewrite later_sep. apply sep_mono_r, later_intro. }
+ rewrite -!assoc. apply sep_mono_r. u_strip_later.
apply wand_intro_l. destruct p.
{ (* a Low state. The comparison fails, and we recurse. *)
rewrite -(exist_intro (State Low I)) -(exist_intro {[ Change i ]}).
@@ -261,7 +257,8 @@ Section proof.
wp_op; first done. intros _. wp_if. rewrite !assoc.
rewrite -{2}pvs_wp. apply pvs_wand_r.
rewrite -(exist_intro γ) -(exist_intro P) -(exist_intro Q) -(exist_intro i).
- rewrite !assoc. do 3 (rewrite -pvs_frame_r; apply sep_mono_l).
+ rewrite !assoc.
+ do 3 (rewrite -pvs_frame_r; apply sep_mono; last (try apply later_intro; reflexivity)).
rewrite [(_ ★ heap_ctx _)%I]comm -!assoc -pvs_frame_l. apply sep_mono_r.
rewrite comm -pvs_frame_l. apply sep_mono_r.
apply sts_ownS_weaken; eauto using sts.up_subseteq. }
@@ -285,11 +282,7 @@ Section proof.
apply wand_intro_l. rewrite [(heap_ctx _ ★ _)%I]sep_elim_r.
rewrite [(sts_own _ _ _ ★ _)%I]sep_elim_r [(sts_ctx _ _ _ ★ _)%I]sep_elim_r.
rewrite !assoc [(_ ★ saved_prop_own i Q)%I]comm !assoc saved_prop_agree.
- wp_op>; last done. intros _.
- etrans; last eapply later_mono.
- { (* Is this really the best way to strip the later? *)
- erewrite later_sep. apply sep_mono; last apply later_intro.
- rewrite ->later_sep. apply sep_mono_l. rewrite ->later_sep. done. }
+ wp_op>; last done. intros _. u_strip_later.
wp_if.
eapply wand_apply_r; [done..|]. eapply wand_apply_r; [done..|].
apply: (eq_rewrite Q' Q (λ x, x)%I); last by eauto with I.
diff --git a/heap_lang/wp_tactics.v b/heap_lang/wp_tactics.v
index 1ecf5771d..ecc90fbf0 100644
--- a/heap_lang/wp_tactics.v
+++ b/heap_lang/wp_tactics.v
@@ -1,6 +1,8 @@
From heap_lang Require Export tactics substitution.
Import uPred.
+(* TODO: The next 6 tactics are not wp-specific at all. They should move elsewhere. *)
+
Ltac revert_intros tac :=
lazymatch goal with
| |- ∀ _, _ => let H := fresh in intro H; revert_intros tac; revert H
@@ -15,17 +17,36 @@ Ltac wp_strip_later :=
end
in revert_intros ltac:(etrans; [|go]).
+(** Assumes a goal of the shape P ⊑ ▷ Q.
+ Will get rid of ▷ in P below ★, ∧ and ∨. *)
+Ltac u_strip_later :=
+ let rec strip :=
+ match goal with
+ | |- (_ ★ _) ⊑ ▷ _ =>
+ etrans; last (eapply equiv_spec, later_sep);
+ apply sep_mono; strip
+ | |- (_ ∧ _) ⊑ ▷ _ =>
+ etrans; last (eapply equiv_spec, later_and);
+ apply sep_mono; strip
+ | |- (_ ∨ _) ⊑ ▷ _ =>
+ etrans; last (eapply equiv_spec, later_or);
+ apply sep_mono; strip
+ | |- ▷ _ ⊑ ▷ _ => apply later_mono; reflexivity
+ | |- _ ⊑ ▷ _ => apply later_intro; reflexivity
+ end
+ in etrans; last eapply later_mono; first solve [ strip ].
+
(* ssreflect-locks the part after the ⊑ *)
(* FIXME: I tried doing a lazymatch to only apply the tactic if the goal has shape ⊑,
bit the match is executed *before* doing the recursion... WTF? *)
-Ltac uLock_goal := revert_intros ltac:(apply uPred_lock_conclusion).
+Ltac u_lock_goal := revert_intros ltac:(apply uPred_lock_conclusion).
(** Transforms a goal of the form ∀ ..., ?0... → ?1 ⊑ ?2
into True ⊑ ∀..., ■?0... → ?1 → ?2, applies tac, and
the moves all the assumptions back. *)
-Ltac uRevert_all :=
+Ltac u_revert_all :=
lazymatch goal with
- | |- ∀ _, _ => let H := fresh in intro H; uRevert_all;
+ | |- ∀ _, _ => let H := fresh in intro H; u_revert_all;
(* TODO: Really, we should distinguish based on whether this is a
dependent function type or not. Right now, we distinguish based
on the sort of the argument, which is suboptimal. *)
@@ -41,8 +62,8 @@ Ltac uRevert_all :=
assumptions, then moves all the Coq assumptions back out to the context,
applies [tac] on the goal (now of the form _ ⊑ _), and then reverts the Coq
assumption so that we end up with the same shape as where we started. *)
-Ltac uLöb tac :=
- uLock_goal; uRevert_all;
+Ltac u_löb tac :=
+ u_lock_goal; u_revert_all;
(* We now have a goal for the form True ⊑ P, with the "original" conclusion
being locked. *)
apply löb_strong; etransitivity;
@@ -81,7 +102,7 @@ Ltac wp_finish :=
end in simpl; revert_intros go.
Tactic Notation "wp_rec" :=
- uLöb ltac:((* Find the redex and apply wp_rec *)
+ u_löb ltac:((* Find the redex and apply wp_rec *)
match goal with
| |- _ ⊑ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
match eval cbv in e' with
--
GitLab