Commit df22adc1 authored by Dan Frumin's avatar Dan Frumin

Get rid of the closedness conditions for pure reductions

parent e57bb39a
......@@ -67,15 +67,12 @@ Lemma tac_rel_pure_l `{logrelG Σ} K e1 ℶ E1 E2 Δ Γ e e2 eres ϕ t τ (b : b
e = fill K e1
PureExec ϕ e1 e2
ϕ
Closed e1
((b = true E1 = E2) b = false)
eres = fill K e2
( ?b bin_log_related E1 E2 Δ Γ eres t τ)
( bin_log_related E1 E2 Δ Γ e t τ).
Proof.
intros Hfill Hpure Hϕ ? Hb ? Hp. subst.
assert (Closed e2).
{ eapply PureExec_Closed; eauto. }
intros Hfill Hpure Hϕ Hb ? Hp. subst.
destruct b.
- destruct Hb as [[_ ?] | Hb']; last by inversion Hb'. subst.
rewrite -(bin_log_pure_l Δ Γ E2 K e1 e2 t τ).
......@@ -96,7 +93,6 @@ Tactic Notation "rel_pure_l" open_constr(ef) :=
[tac_bind_helper (* e = fill K e1' *)
|apply _ (* PureExec ϕ e1 e2 *)
|try (exact I || reflexivity || tac_rel_done)
|try (simpl; solve_closed) (* Closed e1 *)
|first [left; split; reflexivity | right; reflexivity] (* E1 = E2? *)
|simpl; reflexivity (* eres = fill K e2 *)
|try iNext; simpl_subst/= (* new goal *)])
......@@ -122,15 +118,12 @@ Lemma tac_rel_pure_r `{logrelG Σ} K e1 ℶ E1 E2 Δ Γ e e2 eres ϕ t τ :
e = fill K e1
PureExec ϕ e1 e2
ϕ
Closed e1
nclose specN E1
eres = fill K e2
( bin_log_related E1 E2 Δ Γ t (fill K e2) τ)
( bin_log_related E1 E2 Δ Γ t e τ).
Proof.
intros Hfill Hpure Hϕ ??? Hp. subst.
assert (Closed e2).
{ eapply PureExec_Closed; eauto. }
intros Hfill Hpure Hϕ ?? Hp. subst.
rewrite -(bin_log_pure_r Δ Γ E1 E2 K e1 e2 t τ).
{ exact Hp. }
{ assumption. }
......@@ -149,7 +142,6 @@ Tactic Notation "rel_pure_r" open_constr(ef) :=
[tac_bind_helper (* e = fill K e1 *)
|apply _ (* PureExec ϕ e1 e2 *)
|try (exact I || reflexivity || tac_rel_done) (* φ *)
|try (simpl; solve_closed) (* Closed e1 *)
|solve_ndisj (* specN E1 *)
|simpl; reflexivity (* eres = fill K e2 *)
|try iNext; simpl_subst/= (* new goal *)])
......
From iris_logrel.F_mu_ref_conc Require Export fundamental_binary logrel_binary.
From iris_logrel.F_mu_ref_conc Require Export logrel_binary.
From iris.proofmode Require Import tactics.
From iris_logrel.F_mu_ref_conc Require Import rules_binary tactics.
From iris.program_logic Require Import ectx_lifting.
......@@ -68,9 +68,9 @@ Section properties.
iModIntro. iApply wp_value; eauto.
Qed.
Lemma bin_log_related_spec_ctx Δ Γ E1 E2 e e' τ :
( ( ρ, spec_ctx ρ) - {E1,E2;Δ;Γ} e log e' : τ)%I
( {E1,E2;Δ;Γ} e log e' : τ)%I.
Lemma bin_log_related_spec_ctx Δ Γ E1 E2 e e' τ :
( ( ρ, spec_ctx ρ) - {E1,E2;Δ;Γ} e log e' : τ)%I
( {E1,E2;Δ;Γ} e log e' : τ)%I.
Proof.
intros Hp.
rewrite bin_log_related_eq /bin_log_related_def.
......@@ -93,27 +93,29 @@ Section properties.
(** *** Lifting of the pure reductions *)
Lemma bin_log_pure_l Δ (Γ : stringmap type) (E : coPset)
(K' : list ectx_item) (e e' t : expr) (τ : type)
(Hclosed : Closed e)
(Hclosed' : Closed e')
(Hsafe : σ, head_reducible e σ) :
( σ1 e2 σ2 efs, head_step e σ1 e2 σ2 efs -> σ1=σ2 /\ e'=e2 /\ [] = efs)
(Hsafe' : σ, head_reducible e σ)
(Hdet' : σ1 e2 σ2 efs, head_step e σ1 e2 σ2 efs -> σ1=σ2 /\ e'=e2 /\ [] = efs) :
({E,E;Δ;Γ} fill K' e' log t : τ)
{E,E;Δ;Γ} fill K' e log t : τ.
Proof.
rewrite bin_log_related_eq.
assert (to_val e = None) as Hval.
{ destruct (Hsafe ) as [e2 [σ2 [efs Hs]]].
by eapply val_stuck. }
iIntros (Hstep) "IH".
iIntros "IH".
iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
rewrite /env_subst.
rewrite fill_subst. iModIntro.
assert (Hsafe : σ, head_reducible (subst_p (fst <$> vvs) e) σ).
{ intros. by apply subst_p_safe. }
assert (to_val (subst_p (fst <$> vvs) e) = None) as Hval.
{ destruct (Hsafe ) as [e2 [σ2 [efs Hs]]].
by eapply val_stuck. }
iApply (wp_bind (subst_ctx (fst <$> vvs) K')).
rewrite Closed_subst_p_id.
iApply wp_lift_pure_det_head_step_no_fork'; eauto. iNext.
iSpecialize ("IH" with "Hs [HΓ] Hj"); auto. simpl.
iApply wp_lift_pure_det_head_step_no_fork'; eauto.
{ apply subst_p_det; eauto.
intros σ. destruct (Hsafe' σ) as (e2' & σ2' & efs & Hsafez).
destruct (Hdet' _ _ _ _ Hsafez) as (?&?&?).
by simplify_eq. }
iNext. iSpecialize ("IH" with "Hs [HΓ] Hj"); auto. simpl.
rewrite /env_subst fill_subst.
rewrite Closed_subst_p_id.
iApply wp_bind_inv.
{ (* TODO: how to get rid of this? *)
change lang with (ectx_lang expr).
......@@ -124,28 +126,30 @@ Section properties.
Lemma bin_log_pure_masked_l (Δ : list D) (Γ : stringmap type) (E1 E2 : coPset)
(K' : list ectx_item) (e e' t : expr) (τ : type)
(Hclosed : Closed e)
(Hclosed' : Closed e')
(Hsafe : σ, head_reducible e σ) :
( σ1 e2 σ2 efs, head_step e σ1 e2 σ2 efs -> σ1=σ2 /\ e'=e2 /\ [] = efs)
(Hsafe' : σ, head_reducible e σ)
(Hdet': σ1 e2 σ2 efs, head_step e σ1 e2 σ2 efs -> σ1=σ2 /\ e'=e2 /\ [] = efs) :
{E1,E2;Δ;Γ} fill K' e' log t : τ
{E1,E2;Δ;Γ} fill K' e log t : τ.
Proof.
rewrite bin_log_related_eq.
assert (to_val e = None) as Hval.
iIntros "IH".
iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
rewrite /env_subst fill_subst.
assert (Hsafe : σ, head_reducible (subst_p (fst <$> vvs) e) σ).
{ intros. by apply subst_p_safe. }
assert (to_val (subst_p (fst <$> vvs) e) = None) as Hval.
{ destruct (Hsafe ) as [e2 [σ2 [efs Hs]]].
by eapply val_stuck. }
iIntros (Hstep) "IH".
iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
rewrite /env_subst fill_subst.
rewrite Closed_subst_p_id.
iApply (wp_bind (subst_ctx _ K')).
iMod ("IH" with "Hs [HΓ] Hj") as "IH"; auto.
iModIntro.
iApply wp_lift_pure_det_head_step_no_fork; eauto. iModIntro.
iNext.
iApply wp_lift_pure_det_head_step_no_fork; eauto.
{ apply subst_p_det; eauto.
intros σ. destruct (Hsafe' σ) as (e2' & σ2' & efs & Hsafez).
destruct (Hdet' _ _ _ _ Hsafez) as (?&?&?).
by simplify_eq. }
iModIntro. iNext.
rewrite /env_subst fill_subst /=.
rewrite Closed_subst_p_id.
iApply wp_bind_inv.
{ (* TODO: how to get rid of this? *)
change lang with (ectx_lang expr).
......@@ -182,15 +186,6 @@ Section properties.
Proof.
iIntros (?) "Hlog".
iApply (bin_log_pure_l with "Hlog"); auto; intros; simpl.
- rewrite /Closed; cbn.
split_and?; eauto. rewrite -(of_to_val e' v); auto.
by apply of_val_closed.
- replace (rec: f x := e)%E with (of_val (rec: f x := e)%V) by (unlock; done).
replace e' with (of_val v) by (by rewrite (of_to_val e' v)).
rewrite -subst_p_rec /=.
eapply subst_p_closes; eauto.
destruct f, x; cbn-[union]; rewrite ?dom_insert ?dom_singleton ?dom_empty;
set_solver. (* TODO: kinda slow, dom_insert_binder *)
- do 3 eexists. econstructor; eauto.
- by inv_head_step.
Qed.
......@@ -552,9 +547,7 @@ Section properties.
(** ** Reductions on the right *)
(** Lifting of the pure reductions *)
Lemma bin_log_pure_r Δ Γ E1 E2 K' e e' t τ
(Hspec : nclose specN E1)
(Hclosed1 : Closed e)
(Hclosed2 : Closed e') :
(Hspec : nclose specN E1) :
( σ, head_step e σ e' σ [])
{E1,E2;Δ;Γ} t log fill K' e' : τ
{E1,E2;Δ;Γ} t log fill K' e : τ.
......@@ -563,9 +556,12 @@ Section properties.
iIntros (Hstep) "Hlog".
iIntros (vvs ρ) "#Hs #HΓ".
iIntros (j K) "Hj /=".
assert (Hsafe : σ, head_step (subst_p (snd <$> vvs) e) σ (subst_p (snd <$> vvs) e') σ []).
{ intros.
rewrite -(fmap_nil (subst_p (snd <$> vvs))).
by apply subst_p_head_step. }
rewrite /env_subst fill_subst -fill_app.
iMod (step_pure _ _ _ _ (subst_p _ e) (env_subst (snd <$> vvs) e') with "[Hs Hj]") as "Hj"; eauto.
{ rewrite /env_subst. rewrite_closed. }
rewrite fill_app -fill_subst.
iDestruct ("Hlog" with "Hs [HΓ] Hj") as "Hlog"; auto.
Qed.
......@@ -579,14 +575,7 @@ Section properties.
Proof.
iIntros (?) "Hlog".
iApply (bin_log_pure_r with "Hlog"); auto; intros.
{ rewrite_closed. }
{ replace (rec: f x := e)%E with (of_val (rec: f x := e)%V) by (unlock; done).
replace e' with (of_val v') by (by rewrite (of_to_val e' v')).
rewrite -subst_p_rec /=.
eapply subst_p_closes; eauto.
destruct f, x; cbn-[union]; rewrite ?dom_insert ?dom_singleton ?dom_empty;
set_solver. (* TODO: slow af *) }
{ econstructor; eauto. }
econstructor; eauto.
Qed.
Lemma bin_log_related_tlam_r Δ Γ E1 E2 K e t τ
......
......@@ -324,6 +324,14 @@ Proof.
by apply Closed_subst_p_id.
Qed.
Lemma to_val_subst_p (e : expr) (v : val) (es : stringmap val) :
to_val e = Some v subst_p es e = e.
Proof.
intros Htv.
rewrite -(of_to_val _ _ Htv).
apply of_val_subst_p.
Qed.
(** Relation between [subst_p] and [subst] *)
Lemma subst_p_insert (x : binder) v (m : stringmap val) e :
subst_p (<[x:=v]>m) e =
......@@ -392,6 +400,90 @@ Proof.
by rewrite subst_p_empty.
Qed.
Lemma elem_of_rec_lookup (x f : binder) (es : stringmap val) :
z : string, z x :b: f :b: delete x (delete f es) !! z = None.
Proof.
intros z.
destruct x as [|x],f as [|f]; cbn-[union singleton];
[ rewrite elem_of_empty; inversion 1
| rewrite right_id ?elem_of_union !elem_of_singleton.. ].
* intros; subst.
apply lookup_delete.
* intros; subst.
apply lookup_delete.
* intros [[] | []];
[ apply lookup_delete | rewrite delete_commute ; apply lookup_delete ].
Qed.
Lemma subst_p_head_step e e' vs efs σ σ' :
head_step e σ e' σ' efs
head_step (subst_p vs e) σ (subst_p vs e') σ' (subst_p vs <$> efs).
Proof.
intros Hst.
generalize dependent vs.
inversion Hst; subst; simpl;
intros vs;
repeat lazymatch goal with
| [ H : to_val ?e = Some ?v |- _ ] =>
rewrite -!(of_to_val e v H);
clear H
end;
rewrite ?of_val_subst_p;
try by (econstructor; eauto using to_of_val).
- econstructor; eauto using to_of_val.
+ eapply subst_p_closes; eauto.
set_solver.
+ rewrite !subst_p_delete.
rewrite !(delete_commute_binder _ f x).
rewrite (Closed_subst_p_id' _ _ e1); eauto.
apply elem_of_rec_lookup.
- econstructor. by rewrite Closed_subst_p_id.
Qed.
Lemma subst_p_safe e es :
( σ, head_reducible e σ) ( σ, head_reducible (subst_p es e) σ).
Proof.
rewrite /head_reducible.
intros Hsafe.
intros σ. destruct (Hsafe σ) as (e' & σ' & efs & Hstep).
do 3 eexists. apply subst_p_head_step; eauto.
Qed.
Lemma subst_p_det e e' es :
( σ, head_step e σ e' σ [])
( σ1 e2 σ2 efs, head_step e σ1 e2 σ2 efs -> σ1=σ2 /\ e'=e2 /\ [] = efs)
( σ1 e2 σ2 efs, head_step (subst_p es e) σ1 e2 σ2 efs -> σ1=σ2 /\ (subst_p es e')=e2 /\ [] = efs).
Proof.
intros Hstep Hdet σ1 e2 σ2 efs Hst.
specialize (Hdet σ1).
specialize (Hstep σ1).
inversion Hstep; subst; simplify_eq/=;
simpl in Hst; inversion Hst; simplify_eq/=; eauto;
repeat lazymatch goal with
| [ H : to_val ?e = Some ?v, H' : to_val (subst_p es ?e) = Some ?v2 |- _ ] =>
rewrite -(of_to_val _ _ H) in H';
rewrite of_val_subst_p in H';
rewrite to_of_val in H'
| [ H : to_val ?e = Some ?v, H' : context[subst_p _ ?e] |- _ ] =>
rewrite -(of_to_val _ _ H) in H';
rewrite of_val_subst_p in H';
rewrite (of_to_val _ _ H) in H'
end; simplify_eq/=;
rewrite ?of_val_subst_p;
split_and !; eauto.
- rewrite !subst_p_delete.
rewrite !(delete_commute_binder _ f x).
rewrite (Closed_subst_p_id' _ _ e1); eauto.
rewrite (to_val_subst_p e0 v0 _); eauto.
apply elem_of_rec_lookup.
- destruct (Hdet _ _ _ Hst) as (?&?&?).
by simplify_eq.
- destruct (Hdet _ _ _ Hst) as (?&?&?).
by simplify_eq.
- destruct (Hdet _ _ _ Hst) as (?&?&?).
by simplify_eq.
Qed.
(** Properties of the context substitution *)
Lemma fill_item_subst_p (es : stringmap val) (Ki : ectx_item) (e : expr) :
subst_p es (fill_item Ki e) = fill_item (subst_ctx_item es Ki) (subst_p es 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