Commit f638d4f9 authored by Dan Frumin's avatar Dan Frumin

Monadic operations for the relational intrepretation

- Define several versios of bind and return for the relational
  interpretation
- Use those operations to prove some compatibility lemmas
  without unfolding the definitions
- Get rid of the definition unfolding in a part of the stack
  refinement proof
parent 2961c9a7
......@@ -297,11 +297,8 @@ Section Stack_refinement.
by iApply "IH".
+ clear.
iClear "IH Histk HLK_tail HLK HLK' Hτ".
rewrite bin_log_related_eq.
rewrite /bin_log_related_def.
iIntros (vvs ρ) "#Hs #HΓ".
rewrite /env_subst /= !Closed_subst_p_id.
iAssumption.
iApply related_ret.
iApply "Hff".
Qed.
End Stack_refinement.
......
This diff is collapsed.
......@@ -394,3 +394,55 @@ Notation "'{' E1 ',' E2 ';' Γ '}' ⊨ e '≤log≤' e' : τ" :=
( Δ, bin_log_related E1 E2 Δ Γ e%E e'%E τ)%I (at level 74, E1,E2, e, e', τ at next level).
Notation "Γ ⊨ e '≤log≤' e' : τ" :=
( Δ, bin_log_related Δ Γ e%E e'%E τ)%I (at level 74, e, e', τ at next level).
Section monadic.
Context `{logrelG Σ}.
Lemma related_ret τ Δ e1 e2 Γ `{Closed e1} `{Closed e2} E :
interp_expr E E τ Δ (e1,e2) - {E,E;Δ;Γ} e1 log e2 : τ%I.
Proof.
iIntros "Hτ".
rewrite bin_log_related_eq /bin_log_related_def.
iIntros (vvs ρ) "#Hs #HΓ".
by rewrite /env_subst !Closed_subst_p_id.
Qed.
Lemma interp_ret τ Δ e1 e2 v1 v2 E :
to_val e1 = Some v1
to_val e2 = Some v2
τ Δ (v1,v2) - interp_expr E E τ Δ (e1,e2).
Proof.
iIntros (Hv1 Hv2) "Hτ".
unfold interp_expr. iIntros (j K) "Hj /=".
rewrite -(of_to_val e2 v2 Hv2).
iModIntro.
iApply wp_value; eauto.
Qed.
Lemma related_bind Δ Γ (e1 e2 : expr) (τ τ' : type) (K K' : list ectx_item) E :
({E,E;Δ;Γ} e1 log e2 : τ) -
( vv, τ Δ vv - {E,E;Δ;Γ} fill K (of_val (vv.1)) log fill K' (of_val (vv.2)) : τ') -
({E,E;Δ;Γ} fill K e1 log fill K' e2 : τ').
Proof.
iIntros "Hm Hf".
rewrite bin_log_related_eq /bin_log_related_def.
iIntros (vvs ρ) "#Hs #HΓ".
iIntros (j L) "Hj /=".
iSpecialize ("Hm" with "Hs HΓ").
rewrite /env_subst !fill_subst -fill_app.
iMod ("Hm" with "Hj") as "Hm /=".
iModIntro.
iApply wp_bind.
iApply (wp_wand with "Hm").
iIntros (v1). iDestruct 1 as (v2) "[Hj Hvv]".
rewrite fill_app.
replace (of_val v1) with (subst_p (fst <$> vvs) (of_val v1))
by (apply Closed_subst_p_id; done).
replace (of_val v2) with (subst_p (snd <$> vvs) (of_val v2))
by (apply Closed_subst_p_id; done).
rewrite -!fill_subst.
iApply fupd_wp. iApply (fupd_mask_mono E); eauto.
iMod ("Hf" with "Hvv Hs HΓ Hj") as "Hf /=".
done.
Qed.
End monadic.
......@@ -8,31 +8,6 @@ Set Default Proof Using "Type".
Import lang.
(** General tactics *)
Lemma tac_rel_bind_l `{logrelG Σ} e' K E1 E2 Δ Γ e t τ :
e = fill K e'
( bin_log_related E1 E2 Δ Γ (fill K e') t τ)
( bin_log_related E1 E2 Δ Γ e t τ).
Proof. intros. subst. eauto. Qed.
Lemma tac_rel_bind_r `{logrelG Σ} t' K E1 E2 Δ Γ e t τ :
t = fill K t'
( bin_log_related E1 E2 Δ Γ e (fill K t') τ)
( bin_log_related E1 E2 Δ Γ e t τ).
Proof. intros. subst. eauto. Qed.
Ltac tac_bind_helper :=
lazymatch goal with
| |- fill ?K ?e = fill _ ?efoc =>
reshape_expr e ltac:(fun K' e' =>
unify e' efoc;
let K'' := eval cbn[app] in (K' ++ K) in
replace (fill K e) with (fill K'' e') by (by rewrite ?fill_app))
| |- ?e = fill _ ?efoc =>
reshape_expr e ltac:(fun K' e' =>
unify e' efoc;
replace e with (fill K' e') by (by rewrite ?fill_app))
end; reflexivity.
Ltac rel_reshape_cont_r tac :=
lazymatch goal with
| |- _ bin_log_related _ _ _ _ _ (fill ?K ?e) _ =>
......@@ -51,25 +26,11 @@ Ltac rel_reshape_cont_l tac :=
reshape_expr e ltac:(fun K' e' => tac K' e')
end.
Tactic Notation "rel_bind_l" open_constr(efoc) :=
iStartProof;
eapply (tac_rel_bind_l efoc);
[ tac_bind_helper
| (* new goal *)
].
Ltac rel_bind_ctx_l K :=
eapply (tac_rel_bind_l _ K);
[reflexivity || tac_bind_helper
|].
Tactic Notation "rel_bind_r" open_constr(efoc) :=
iStartProof;
eapply (tac_rel_bind_r efoc);
[tac_bind_helper
| (* new goal *)
].
Ltac rel_bind_ctx_r K :=
eapply (tac_rel_bind_r _ K);
[reflexivity || tac_bind_helper
......
......@@ -2,7 +2,7 @@ From iris.program_logic Require Export weakestpre.
From iris.proofmode Require Import coq_tactics sel_patterns.
From iris.proofmode Require Export tactics.
From iris_logrel.F_mu_ref_conc Require Import rules rules_binary.
From iris_logrel.F_mu_ref_conc Require Export lang reflection proofmode.classes.
From iris_logrel.F_mu_ref_conc Require Export lang reflection proofmode.classes logrel_binary.
Set Default Proof Using "Type".
Import lang.
......@@ -96,9 +96,56 @@ Ltac tac_rel_done := split_and?; try
| [ |- is_Some (to_val _)] => solve_to_val
end.
(* * TP tactics *)
(** * Bind tactics for the relational interpretation *)
(* TODO: where should those tactics go? *)
Lemma tac_rel_bind_l `{logrelG Σ} e' K E1 E2 Δ Γ e t τ :
e = fill K e'
( bin_log_related E1 E2 Δ Γ (fill K e') t τ)
( bin_log_related E1 E2 Δ Γ e t τ).
Proof. intros. subst. eauto. Qed.
Lemma tac_rel_bind_r `{logrelG Σ} t' K E1 E2 Δ Γ e t τ :
t = fill K t'
( bin_log_related E1 E2 Δ Γ e (fill K t') τ)
( bin_log_related E1 E2 Δ Γ e t τ).
Proof. intros. subst. eauto. Qed.
Ltac tac_bind_helper :=
lazymatch goal with
| |- fill ?K ?e = fill _ ?efoc =>
reshape_expr e ltac:(fun K' e' =>
unify e' efoc;
let K'' := eval cbn[app] in (K' ++ K) in
replace (fill K e) with (fill K'' e') by (by rewrite ?fill_app))
| |- ?e = fill _ ?efoc =>
reshape_expr e ltac:(fun K' e' =>
unify e' efoc;
replace e with (fill K' e') by (by rewrite ?fill_app))
end; reflexivity.
Tactic Notation "rel_bind_l" open_constr(efoc) :=
iStartProof;
eapply (tac_rel_bind_l efoc);
[ tac_bind_helper
| (* new goal *)
].
Ltac rel_bind_ctx_l K :=
eapply (tac_rel_bind_l _ K);
[reflexivity || tac_bind_helper
|].
Tactic Notation "rel_bind_r" open_constr(efoc) :=
iStartProof;
eapply (tac_rel_bind_r efoc);
[tac_bind_helper
| (* new goal *)
].
(** * TP tactics *)
(* ** bind *)
(** ** bind *)
Lemma tac_tp_bind_gen `{logrelG Σ} j Δ Δ' i p e e' Q :
envs_lookup i Δ = Some (p, j e)%I
e = e'
......
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