Commit 4ed33744 authored by Ralf Jung's avatar Ralf Jung
Browse files

prove a tactic for canceling with pattern matching, and use it in a few (test-)places

parent 50c0f2be
......@@ -127,3 +127,16 @@ Tactic Notation "cancel" constr(Ps) :=
[cbv; reflexivity|cbv; reflexivity|simpl]
Tactic Notation "ecancel" open_constr(Ps) :=
let rec close Ps Qs tac :=
lazymatch Ps with
| [] => tac Qs
| ?P :: ?Ps =>
find_pat P ltac:(fun Q => close Ps (Q :: Qs) tac)
lazymatch goal with
| |- @uPred_entails ?M _ _ =>
close Ps (@nil (uPred M)) ltac:(fun Qs => cancel Qs)
......@@ -131,7 +131,7 @@ Section heap.
rewrite -(exist_intro (op {[ l := Excl v ]})).
repeat erewrite <-exist_intro by apply _; simpl.
rewrite -of_heap_insert left_id right_id.
cancel [auth_own heap_name {[l := Excl v]} - Φ (LocV l)]%I.
ecancel [_ - Φ _]%I.
rewrite -(map_insert_singleton_op h); last by apply of_heap_None.
rewrite const_equiv ?left_id; last by apply (map_insert_valid h).
apply later_intro.
......@@ -298,6 +298,14 @@ Tactic Notation "feed" "destruct" constr(H) :=
Tactic Notation "feed" "destruct" constr(H) "as" simple_intropattern(IP) :=
feed (fun p => let H':=fresh in pose proof p as H'; destruct H' as IP) H.
(** The following tactic can be used to add support for patterns to tactic notation:
It will search for the first subterm of the goal matching [pat], and then call [tac]
with that subterm. *)
Ltac find_pat pat tac :=
match goal with |- context [?x] => unify pat x; tac x || fail 2
(** Coq's [firstorder] tactic fails or loops on rather small goals already. In
particular, on those generated by the tactic [unfold_elem_ofs] which is used
to solve propositions on collections. The [naive_solver] tactic implements an
......@@ -56,7 +56,7 @@ Section auth.
rewrite sep_exist_l. apply exist_elim=>γ. rewrite -(exist_intro γ).
trans ( auth_inv γ φ auth_own γ a)%I.
{ rewrite /auth_inv -(exist_intro a) later_sep.
rewrite const_equiv // left_id. cancel [▷ φ a]%I.
rewrite const_equiv // left_id. ecancel [▷ φ _]%I.
by rewrite -later_intro /auth_own -own_op auth_both_op. }
rewrite (inv_alloc N) /auth_ctx pvs_frame_r. apply pvs_mono.
by rewrite always_and_sep_l.
......@@ -85,7 +85,7 @@ Section sts.
rewrite sep_exist_l. apply exist_elim=>γ. rewrite -(exist_intro γ).
trans ( sts_inv γ φ sts_own γ s ( sts.tok s))%I.
{ rewrite /sts_inv -(exist_intro s) later_sep.
cancel [ φ s]%I.
ecancel [ φ _]%I.
by rewrite -later_intro -own_op sts_op_auth_frag_up; last set_solver. }
rewrite (inv_alloc N) /sts_ctx pvs_frame_r.
by rewrite always_and_sep_l.
......@@ -114,7 +114,7 @@ Section sts.
intros Hstep. rewrite /sts_inv /sts_own -(exist_intro s') later_sep.
(* TODO it would be really nice to use cancel here *)
rewrite [(_ ▷φ _)%I]comm -assoc.
rewrite [(_ φ _)%I]comm -assoc.
rewrite -pvs_frame_l. apply sep_mono_r. rewrite -later_intro.
rewrite own_valid_l discrete_validI. apply const_elim_sep_l=>Hval.
trans (|={E}=> own γ (sts_auth s' T'))%I.
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