From 48ccc2900523cd749172d12015eab59cd06ae229 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 16 Feb 2016 00:01:39 +0100
Subject: [PATCH] Preliminary version of tactics for automatically applying wp
rules.
---
_CoqProject | 1 +
heap_lang/tests.v | 45 +++++++++--------------------
heap_lang/wp_tactics.v | 64 ++++++++++++++++++++++++++++++++++++++++++
3 files changed, 79 insertions(+), 31 deletions(-)
create mode 100644 heap_lang/wp_tactics.v
diff --git a/_CoqProject b/_CoqProject
index fc0dbb510..4691c835f 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -70,6 +70,7 @@ program_logic/auth.v
program_logic/sts.v
heap_lang/heap_lang.v
heap_lang/tactics.v
+heap_lang/wp_tactics.v
heap_lang/lifting.v
heap_lang/derived.v
heap_lang/heap.v
diff --git a/heap_lang/tests.v b/heap_lang/tests.v
index 70ef55fff..bc0495c23 100644
--- a/heap_lang/tests.v
+++ b/heap_lang/tests.v
@@ -1,6 +1,6 @@
(** This file is essentially a bunch of testcases. *)
From program_logic Require Import ownership.
-From heap_lang Require Import substitution tactics heap notation.
+From heap_lang Require Import wp_tactics heap notation.
Import uPred.
Section LangTests.
@@ -62,48 +62,31 @@ Section LiftingTests.
revert n1; apply löb_all_1=>n1.
rewrite (comm uPred_and (â– _)%I) assoc; apply const_elim_r=>?.
(* first need to do the rec to get a later *)
- rewrite -(wp_bindi (AppLCtx _)) /=.
- rewrite -wp_rec // =>-/=; rewrite -wp_value //=.
+ wp_rec!.
(* FIXME: ssr rewrite fails with "Error: _pattern_value_ is used in conclusion." *)
- rewrite ->(later_intro (Q _)).
- rewrite -!later_and; apply later_mono.
- (* Go on *)
- rewrite -wp_let //= -later_intro.
- rewrite -(wp_bindi (LetCtx _ _)) -wp_bin_op //= -wp_let' //= -!later_intro.
- rewrite -(wp_bindi (IfCtx _ _)) /=.
- apply wp_lt=> ?.
- - rewrite -wp_if_true -!later_intro.
- rewrite (forall_elim (n1 + 1)) const_equiv; last omega.
+ rewrite ->(later_intro (Q _)); rewrite -!later_and; apply later_mono.
+ wp_rec. wp_bin_op. wp_rec. wp_bin_op=> ?.
+ - wp_if. rewrite (forall_elim (n1 + 1)) const_equiv; last omega.
by rewrite left_id impl_elim_l.
- assert (n1 = n2 - 1) as -> by omega.
- rewrite -wp_if_false -!later_intro.
- by rewrite -wp_value // and_elim_r.
+ wp_if. wp_value. auto with I.
Qed.
Lemma Pred_spec n E Q : ▷ Q (LitV (n - 1)) ⊑ wp E (Pred 'n)%L Q.
Proof.
- rewrite -wp_lam //=.
- rewrite -(wp_bindi (IfCtx _ _)) /=.
- apply later_mono, wp_le=> Hn.
- - rewrite -wp_if_true.
- rewrite -(wp_bindi (UnOpCtx _)) /=.
- rewrite -(wp_bind [AppLCtx _; AppRCtx _]) /=.
- rewrite -(wp_bindi (BinOpLCtx _ _)) /=.
- rewrite -wp_un_op //=.
- rewrite -wp_bin_op //= -!later_intro.
- rewrite -FindPred_spec. apply and_intro; first by (apply const_intro; omega).
- rewrite -wp_un_op //= -later_intro.
- by assert (n - 1 = - (- n + 2 - 1)) as -> by omega.
- - rewrite -wp_if_false -!later_intro.
- rewrite -FindPred_spec.
- auto using and_intro, const_intro with omega.
+ wp_rec!; apply later_mono; wp_bin_op=> ?.
+ - wp_if. wp_un_op. wp_bin_op.
+ wp_focus (FindPred _ _); rewrite -FindPred_spec.
+ apply and_intro; first auto with I omega.
+ wp_un_op. by replace (n - 1) with (- (-n + 2 - 1)) by omega.
+ - wp_if. rewrite -FindPred_spec. auto with I omega.
Qed.
Goal ∀ E,
True ⊑ wp (Σ:=globalF Σ) E (let: "x" := Pred '42 in Pred "x") (λ v, v = '40).
Proof.
intros E.
- rewrite -(wp_bindi (LetCtx _ _)) -Pred_spec //= -wp_let' //=.
- by rewrite -Pred_spec -!later_intro /=.
+ wp_focus (Pred '42); rewrite -Pred_spec -later_intro.
+ wp_rec. rewrite -Pred_spec -later_intro; auto with I.
Qed.
End LiftingTests.
diff --git a/heap_lang/wp_tactics.v b/heap_lang/wp_tactics.v
new file mode 100644
index 000000000..5d0b89a6d
--- /dev/null
+++ b/heap_lang/wp_tactics.v
@@ -0,0 +1,64 @@
+From heap_lang Require Export tactics substitution.
+Import uPred.
+
+Ltac wp_strip_later :=
+ match goal with
+ | |- ∀ _, _ => let H := fresh in intro H; wp_strip_later; revert H
+ | |- _ ⊑ ▷ _ => etransitivity; [|apply later_intro]
+ end.
+Ltac wp_bind K :=
+ lazymatch eval hnf in K with
+ | [] => idtac
+ | _ => etransitivity; [|apply (wp_bind K)]; simpl
+ end.
+
+Tactic Notation "wp_value" :=
+ match goal with
+ | |- _ ⊑ wp ?E ?e ?Q => etransitivity; [|by eapply wp_value]; simpl
+ end.
+Tactic Notation "wp_rec" "!" :=
+ repeat wp_value;
+ match goal with
+ | |- _ ⊑ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
+ match eval cbv in e' with
+ | App (Rec _ _ _) _ => wp_bind K; etransitivity; [|by eapply wp_rec]; simpl
+ end)
+ end.
+Tactic Notation "wp_rec" := wp_rec!; wp_strip_later.
+Tactic Notation "wp_bin_op" "!" :=
+ repeat wp_value;
+ match goal with
+ | |- _ ⊑ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
+ match eval cbv in e' with
+ | BinOp LtOp _ _ => wp_bind K; apply wp_lt; [|]
+ | BinOp LeOp _ _ => wp_bind K; apply wp_le; [|]
+ | BinOp EqOp _ _ => wp_bind K; apply wp_eq; [|]
+ | BinOp _ _ _ => wp_bind K; etransitivity; [|by eapply wp_bin_op]; simpl
+ end)
+ end.
+
+Tactic Notation "wp_bin_op" := wp_bin_op!; wp_strip_later.
+Tactic Notation "wp_un_op" "!" :=
+ repeat wp_value;
+ match goal with
+ | |- _ ⊑ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
+ match eval cbv in e' with
+ | UnOp _ _ => wp_bind K; etransitivity; [|by eapply wp_un_op]; simpl
+ end)
+ end.
+Tactic Notation "wp_un_op" := wp_un_op!; wp_strip_later.
+Tactic Notation "wp_if" "!" :=
+ repeat wp_value;
+ match goal with
+ | |- _ ⊑ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
+ match eval cbv in e' with
+ | If _ _ _ =>
+ wp_bind K; etransitivity; [|by apply wp_if_true || by apply wp_if_false]
+ end)
+ end.
+Tactic Notation "wp_if" := wp_if!; wp_strip_later.
+Tactic Notation "wp_focus" open_constr(efoc) :=
+ match goal with
+ | |- _ ⊑ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
+ match e' with efoc => unify e' efoc; wp_bind K end)
+ end.
--
GitLab