From f7643c59ba1db0ed7124bc0e45001a2a4c0403d6 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 20 Feb 2016 19:44:27 +0100
Subject: [PATCH] =?UTF-8?q?generalize=20the=20l=C3=B6b-part=20of=20the=20w?=
=?UTF-8?q?p=5Frec=20tactic?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
---
heap_lang/tests.v | 6 +++---
heap_lang/wp_tactics.v | 47 ++++++++++++++++++++++++------------------
2 files changed, 30 insertions(+), 23 deletions(-)
diff --git a/heap_lang/tests.v b/heap_lang/tests.v
index 4b98b3e3e..d687c9051 100644
--- a/heap_lang/tests.v
+++ b/heap_lang/tests.v
@@ -63,10 +63,10 @@ Section LiftingTests.
Proof.
wp_lam>; apply later_mono; wp_op=> ?; wp_if.
- wp_op. wp_op.
- ewp apply FindPred_spec.
- apply and_intro; first auto with I omega.
+ (* TODO: Can we use the wp tactic again here? *)
+ wp_focus (FindPred _ _). rewrite -FindPred_spec; last by omega.
wp_op. by replace (n - 1) with (- (-n + 2 - 1)) by omega.
- - ewp apply FindPred_spec. auto with I omega.
+ - rewrite -FindPred_spec; eauto with omega.
Qed.
Lemma Pred_user E :
diff --git a/heap_lang/wp_tactics.v b/heap_lang/wp_tactics.v
index fc828cb31..ee6117c9e 100644
--- a/heap_lang/wp_tactics.v
+++ b/heap_lang/wp_tactics.v
@@ -36,6 +36,31 @@ Ltac uRevert_all :=
apply wand_elim_l'
end.
+(** This starts on a goal of the form ∀ ..., ?0... → ?1 ⊑ ?2.
+ It applies löb where all the Coq assumptions have been turned into logical
+ 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;
+ (* We now have a goal for the form True ⊑ P, with the "original" conclusion
+ being locked. *)
+ apply löb_strong; etransitivity;
+ first (apply equiv_spec; symmetry; apply (left_id _ _ _); reflexivity);
+ (* Now introduce again all the things that we reverted, and at the bottom, do the work *)
+ let rec go :=
+ lazymatch goal with
+ | |- _ ⊑ (∀ _, _) => apply forall_intro;
+ let H := fresh in intro H; go; revert H
+ | |- _ ⊑ (■_ → _) => apply impl_intro_l, const_elim_l;
+ let H := fresh in intro H; go; revert H
+ | |- ▷ ?R ⊑ (?L -★ locked _) => apply wand_intro_l;
+ (* TODO: Do sth. more robust than rewriting. *)
+ trans (▷ (L ★ R))%I; first (rewrite later_sep -(later_intro L); reflexivity );
+ unlock; tac
+ end
+ in go.
+
Ltac wp_bind K :=
lazymatch eval hnf in K with
| [] => idtac
@@ -55,23 +80,7 @@ Ltac wp_finish :=
end in simpl; revert_intros go.
Tactic Notation "wp_rec" :=
- uLock_goal; uRevert_all;
- (* We now have a goal for the form True ⊑ P, with the "original" conclusion
- being locked. *)
- apply löb_strong; etransitivity;
- first (apply equiv_spec; symmetry; apply (left_id _ _ _)); [];
- (* Now introduce again all the things that we reverted, and at the bottom, do the work *)
- let rec go :=
- lazymatch goal with
- | |- _ ⊑ (∀ _, _) => apply forall_intro;
- let H := fresh in intro H; go; revert H
- | |- _ ⊑ (■_ → _) => apply impl_intro_l, const_elim_l;
- let H := fresh in intro H; go; revert H
- | |- ▷ ?R ⊑ (?L -★ locked _) => apply wand_intro_l;
- (* TODO: Do sth. more robust than rewriting. *)
- trans (▷ (L ★ R))%I; first (rewrite later_sep -(later_intro L); reflexivity );
- unlock;
- (* Find the redex and apply wp_rec *)
+ uLö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
@@ -79,9 +88,7 @@ Tactic Notation "wp_rec" :=
wp_bind K; etrans; [|eapply wp_rec; reflexivity]; wp_finish
end)
end;
- apply later_mono
- end
- in go.
+ apply later_mono).
Tactic Notation "wp_lam" ">" :=
match goal with
--
GitLab