Commit 1b172b22 authored by Ralf Jung's avatar Ralf Jung

move generic upred tactics from wp_tactics to upred_tactics

parent 0ef28164
From algebra Require Export upred.
From algebra Require Export upred_big_op.
Import uPred.
Module upred_reflection. Section upred_reflection.
Context {M : cmraT}.
......@@ -89,7 +90,7 @@ Module upred_reflection. Section upred_reflection.
Proof.
intros ??. rewrite !eval_flatten.
rewrite (flatten_cancel e1 e1' ns) // (flatten_cancel e2 e2' ns) //; csimpl.
rewrite !fmap_app !big_sep_app. apply uPred.sep_mono_r.
rewrite !fmap_app !big_sep_app. apply sep_mono_r.
Qed.
Class Quote (Σ1 Σ2 : list (uPred M)) (P : uPred M) (e : expr) := {}.
......@@ -144,3 +145,98 @@ Tactic Notation "ecancel" open_constr(Ps) :=
| |- @uPred_entails ?M _ _ =>
close Ps (@nil (uPred M)) ltac:(fun Qs => cancel Qs)
end.
(* Some more generic uPred tactics.
TODO: Naming. *)
Ltac revert_intros tac :=
lazymatch goal with
| |- _, _ => let H := fresh in intro H; revert_intros tac; revert H
| |- _ => tac
end.
(** Assumes a goal of the shape P Q. Alterantively, if Q
is built of , , with in all branches; that will work, too.
Will turn this goal into P Q and strip in P below , , . *)
Ltac u_strip_later :=
let rec strip :=
lazymatch goal with
| |- (_ _) _ =>
etrans; last (eapply equiv_entails_sym, later_sep);
apply sep_mono; strip
| |- (_ _) _ =>
etrans; last (eapply equiv_entails_sym, later_and);
apply sep_mono; strip
| |- (_ _) _ =>
etrans; last (eapply equiv_entails_sym, later_or);
apply sep_mono; strip
| |- _ _ => apply later_mono; reflexivity
| |- _ _ => apply later_intro; reflexivity
end
in let rec shape_Q :=
lazymatch goal with
| |- _ (_ _) =>
(* Force the later on the LHS to be top-level, matching laters
below on the RHS *)
etrans; first (apply equiv_entails, later_sep; reflexivity);
(* Match the arm recursively *)
apply sep_mono; shape_Q
| |- _ (_ _) =>
etrans; first (apply equiv_entails, later_and; reflexivity);
apply sep_mono; shape_Q
| |- _ (_ _) =>
etrans; first (apply equiv_entails, later_or; reflexivity);
apply sep_mono; shape_Q
| |- _ _ => apply later_mono; reflexivity
(* We fail if we don't find laters in all branches. *)
end
in revert_intros ltac:(etrans; [|shape_Q];
etrans; last eapply later_mono; first solve [ strip ]).
(** Transforms a goal of the form ..., ?0... ?1 ?2
into True ..., ?0... ?1 ?2, applies tac, and
the moves all the assumptions back. *)
Ltac u_revert_all :=
lazymatch goal with
| |- _, _ => 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. *)
first [ apply (const_intro_impl _ _ _ H); clear H
| revert H; apply forall_elim']
| |- ?C _ => trans (True C)%I;
first (apply equiv_entails_sym, left_id, _; reflexivity);
apply impl_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,
but with an additional assumption -ed to the context *)
Ltac u_löb tac :=
u_revert_all;
(* Add a box *)
etrans; last (eapply always_elim; reflexivity);
(* We now have a goal for the form True P, with the "original" conclusion
being locked. *)
apply löb_strong; etransitivity;
first (apply equiv_entails, left_id, _; reflexivity);
apply: always_intro;
(* 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
(* This is the "bottom" of the goal, where we see the impl introduced
by u_revert_all as well as the from löb_strong and the we added. *)
| |- ?R (?L _) => apply impl_intro_l;
trans (L R)%I;
first (eapply equiv_entails, always_and_sep_r, _; reflexivity);
tac
end
in go.
From algebra Require Export upred_tactics.
From heap_lang Require Export tactics substitution.
Import uPred.
(* TODO: The next few 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
| |- _ => tac
end.
(** Assumes a goal of the shape P Q. Alterantively, if Q
is built of , , with in all branches; that will work, too.
Will turn this goal into P Q and strip in P below , , . *)
Ltac u_strip_later :=
let rec strip :=
lazymatch goal with
| |- (_ _) _ =>
etrans; last (eapply equiv_entails_sym, later_sep);
apply sep_mono; strip
| |- (_ _) _ =>
etrans; last (eapply equiv_entails_sym, later_and);
apply sep_mono; strip
| |- (_ _) _ =>
etrans; last (eapply equiv_entails_sym, later_or);
apply sep_mono; strip
| |- _ _ => apply later_mono; reflexivity
| |- _ _ => apply later_intro; reflexivity
end
in let rec shape_Q :=
lazymatch goal with
| |- _ (_ _) =>
(* Force the later on the LHS to be top-level, matching laters
below on the RHS *)
etrans; first (apply equiv_entails, later_sep; reflexivity);
(* Match the arm recursively *)
apply sep_mono; shape_Q
| |- _ (_ _) =>
etrans; first (apply equiv_entails, later_and; reflexivity);
apply sep_mono; shape_Q
| |- _ (_ _) =>
etrans; first (apply equiv_entails, later_or; reflexivity);
apply sep_mono; shape_Q
| |- _ _ => apply later_mono; reflexivity
(* We fail if we don't find laters in all branches. *)
end
in revert_intros ltac:(etrans; [|shape_Q];
etrans; last eapply later_mono; first solve [ strip ]).
(** Transforms a goal of the form ..., ?0... ?1 ?2
into True ..., ?0... ?1 ?2, applies tac, and
the moves all the assumptions back. *)
Ltac u_revert_all :=
lazymatch goal with
| |- _, _ => 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. *)
first [ apply (const_intro_impl _ _ _ H); clear H
| revert H; apply forall_elim']
| |- ?C _ => trans (True C)%I;
first (apply equiv_entails_sym, left_id, _; reflexivity);
apply impl_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,
but with an additional assumption -ed to the context *)
Ltac u_löb tac :=
u_revert_all;
(* Add a box *)
etrans; last (eapply always_elim; reflexivity);
(* We now have a goal for the form True P, with the "original" conclusion
being locked. *)
apply löb_strong; etransitivity;
first (apply equiv_entails, left_id, _; reflexivity);
apply: always_intro;
(* 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
(* This is the "bottom" of the goal, where we see the impl introduced
by u_revert_all as well as the from löb_strong and the we added. *)
| |- ?R (?L _) => apply impl_intro_l;
trans (L R)%I;
first (eapply equiv_entails, always_and_sep_r, _; reflexivity);
tac
end
in go.
(** wp-specific helper tactics *)
(* First try to productively strip off laters; if that fails, at least
cosmetically get rid of laters in the conclusion. *)
......
Markdown is supported
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