Commit d7cada37 authored by Dan Frumin's avatar Dan Frumin

A common rel_pure_l/r tactic utilizing typeclass search

- The typeclass `PureExec e1 e2` controls pure deterministic
  reductions
- General tactics rel_pure_l and rel_pure_r that depend on that typeclass
- The same typeclass can be used for WP tactics and tp tactics, potentially
parent 7b70c9db
......@@ -159,7 +159,7 @@ Section CG_Counter.
iMod ("Hrev" with "[HR Hx]").
{ iExists _. iFrame. } iModIntro. simpl.
rel_rec_l.
rel_op_l. simpl.
rel_op_l.
rel_bind_l (CAS _ _ _).
iApply (bin_log_related_cas_l); auto.
iMod "H2" as (n') "[Hx [HR HQ]]". iModIntro. simpl.
......@@ -285,15 +285,18 @@ Section CG_Counter.
iApply (bin_log_related_pair _ with "[]").
- rel_rec_l.
{ unfold FG_increment. unlock. simpl_subst/=. solve_closed. }
unfold CG_increment. unlock.
rel_rec_r.
unfold CG_increment. unlock; simpl_subst/=.
rel_rec_r.
replace (λ: <>, acquire #l ;; #cnt' <- 1 + (! #cnt');; release #l)%E
with (CG_increment $/ LocV cnt' $/ LocV l)%E; last first.
{ unfold CG_increment. unlock; simpl_subst/=. reflexivity. }
iApply (FG_CG_increment_refinement with "Hinv").
- rel_rec_l.
{ unfold counter_read. unlock. simpl_subst/=. solve_closed. }
rel_rec_r.
{ unfold counter_read. unlock. simpl_subst/=. solve_closed. }
iApply (counter_read_refinement with "Hinv").
Qed.
End CG_Counter.
......
From iris_logrel.F_mu_ref_conc.proofmode Require Export tactics rel_tactics.
From iris_logrel.F_mu_ref_conc Require Export fundamental_binary logrel_binary.
From iris.proofmode Require Import tactics.
From iris_logrel.F_mu_ref_conc Require Import rules_binary hax.
From iris.program_logic Require Import ectx_lifting.
Class PureExec (P : Prop) (e1 e2 : expr) := {
pure_exec_safe : P -> σ, head_reducible e1 σ;
pure_exec_puredet : P -> σ1 e2' σ2 efs, head_step e1 σ1 e2' σ2 efs -> σ1=σ2 /\ e2=e2' /\ [] = efs;
}.
Instance pure_binop op e1 v1 e2 v2 v `(to_val e1 = Some v1) `(to_val e2 = Some v2):
PureExec (binop_eval op v1 v2 = Some v)
(BinOp op e1 e2)
(of_val v).
Proof.
split; intros Hval.
- intros. do 3 eexists. econstructor; eauto using to_of_val.
- intros. by inv_head_step.
Qed.
Instance pure_rec f x e1 e2 v2 `{Closed (x :b: f :b: ) e1} `(to_val e2 = Some v2) :
PureExec True
(App (Rec f x e1) e2)
(subst' f (Rec f x e1) (subst' x e2 e1)).
Proof.
split; intros ?.
- intros. do 3 eexists. econstructor; eauto using to_of_val.
- intros. by inv_head_step.
Qed.
(* TODO: give this one a correct priority? *)
Instance pure_rec_locked e f x e1 e2 v2 `(to_val e2 = Some v2) `(e = Rec f x e1) `{Closed (x :b: f :b: ) e1} :
PureExec True
(App e e2)
(e $/ v2) | 100.
Proof.
split; intros ?; subst.
- intros. do 3 eexists. econstructor; eauto using to_of_val.
- intros. destruct f; by inv_head_step.
Qed.
Instance pure_fst e1 v1 e2 v2 `(to_val e1 = Some v1) `(to_val e2 = Some v2) :
PureExec True (Fst (e1, e2)) e1.
Proof.
split; intros ?.
- intros. do 3 eexists. econstructor; eauto using to_of_val.
- intros. by inv_head_step.
Qed.
Instance pure_snd e1 v1 e2 v2 `(to_val e1 = Some v1) `(to_val e2 = Some v2) :
PureExec True (Snd (e1, e2)) e2.
Proof.
split; intros ?.
- intros. do 3 eexists. econstructor; eauto using to_of_val.
- intros. by inv_head_step.
Qed.
Instance pure_unfold e1 v1 `(to_val e1 = Some v1) :
PureExec True (Unfold (Fold e1)) e1.
Proof.
split; intros ?.
- intros. do 3 eexists. econstructor; eauto using to_of_val.
- intros. by inv_head_step.
Qed.
Instance pure_if_true e1 e2 `{Closed e1} `{Closed e2} :
PureExec True (If true e1 e2) e1.
Proof.
split; intros ?.
- intros. do 3 eexists. econstructor; eauto using to_of_val.
- intros. by inv_head_step.
Qed.
Instance pure_if_false e1 e2 `{Closed e1} `{Closed e2} :
PureExec True (If false e1 e2) e2.
Proof.
split; intros ?.
- intros. do 3 eexists. econstructor; eauto using to_of_val.
- intros. by inv_head_step.
Qed.
Instance pure_case_inl e0 v `(to_val e0 = Some v) e1 e2 `{Closed e1} `{Closed e2} :
PureExec True (Case (InjL e0) e1 e2) (e1 e0).
Proof.
split; intros ?.
- intros. do 3 eexists. econstructor; eauto using to_of_val.
- intros. by inv_head_step.
Qed.
Instance pure_case_inr e0 v `(to_val e0 = Some v) e1 e2 `{Closed e1} `{Closed e2} :
PureExec True (Case (InjR e0) e1 e2) (e2 e0).
Proof.
split; intros ?.
- intros. do 3 eexists. econstructor; eauto using to_of_val.
- intros. by inv_head_step.
Qed.
......@@ -81,6 +81,21 @@ Tactic Notation "wp_bind" open_constr(efoc) :=
| _ => fail "wp_bind: not a 'wp'"
end.
(* * Tactics for solving specific goals *)
(* Applied to goals that are equalities of expressions. Will try to unlock the
LHS once if necessary, to get rid of the lock added by the syntactic sugar. *)
Ltac solve_of_val_unlock := try apply of_val_unlock; fast_done.
Hint Extern 0 (of_val _ = _) => solve_of_val_unlock : typeclass_instances.
Ltac tac_rel_done := split_and?; try
lazymatch goal with
| [ |- of_val _ = _ ] => solve_of_val_unlock
| [ |- Closed _ _ ] => solve_closed
| [ |- to_val _ = Some _ ] => solve_to_val
| [ |- is_Some (to_val _)] => solve_to_val
end.
(* * TP tactics *)
(* ** bind *)
......
......@@ -239,6 +239,8 @@ Ltac solve_to_val :=
let e' := R.of_expr e in change (is_Some (to_val (R.to_expr e')));
apply R.to_val_is_Some, (bool_decide_unpack _); vm_compute; exact I
end.
Hint Extern 0 (to_val _ = Some _) => solve_to_val : typeclass_instances.
Hint Extern 0 (is_Some (to_val _)) => solve_to_val : typeclass_instances.
Ltac solve_closed :=
match goal with
......
......@@ -530,7 +530,7 @@ Section properties.
(** ** Reductions on the right *)
(** Lifting of the pure reductions *)
Lemma bin_log_pure_r Δ Γ E1 E2 K' τ e e' t
Lemma bin_log_pure_r Δ Γ E1 E2 K' e e' t τ
(Hspec : nclose specN E1)
(Hclosed1 : Closed e)
(Hclosed2 : Closed e') :
......
......@@ -19,8 +19,10 @@ F_mu_ref_conc/fundamental_binary.v
F_mu_ref_conc/context_refinement.v
F_mu_ref_conc/adequacy.v
F_mu_ref_conc/soundness_binary.v
F_mu_ref_conc/tactics.v
F_mu_ref_conc/rel_tactics.v
F_mu_ref_conc/proofmode/classes.v
F_mu_ref_conc/proofmode/tactics.v
F_mu_ref_conc/proofmode/rel_tactics.v
F_mu_ref_conc/proofmode.v
F_mu_ref_conc/notation.v
F_mu_ref_conc/examples/lock.v
F_mu_ref_conc/examples/counter.v
......
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