Commit 6b0f9777 authored by Dan Frumin's avatar Dan Frumin

Obtain (∃ ρ, spec_ctx ρ) from the relational interpretation

parent 3d60cf9e
......@@ -53,7 +53,7 @@ Section properties.
iMod "HP". iApply ("HI" with "HP").
Qed.
Lemma bin_log_related_val Δ Γ E τ e e' v v' :
Lemma bin_log_related_val Δ Γ E e e' τ v v' :
to_val e = Some v
to_val e' = Some v'
(|={E}=> interp τ Δ (v, v')) {E,E;Δ;Γ} e log e' : τ.
......@@ -68,6 +68,27 @@ 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.
Proof.
intros Hp.
rewrite bin_log_related_eq /bin_log_related_def.
iIntros "Hctx". iIntros (vvs ρ') "#Hspec".
rewrite (persistentP (spec_ctx _)).
rewrite (uPred.always_sep_dup' (spec_ctx _)).
iDestruct "Hspec" as "#[Hspec #Hspec']".
iRevert "Hspec'".
rewrite (uPred.always_elim (spec_ctx _)).
iAssert ( ρ, spec_ctx ρ)%I as "Hρ".
{ eauto. }
iClear "Hspec".
iRevert (vvs ρ').
fold (bin_log_related_def E1 E2 Δ Γ e e' τ).
rewrite -bin_log_related_eq.
iApply (Hp with "Hctx Hρ").
Qed.
(** ** Reductions on the left *)
(** *** Lifting of the pure reductions *)
Lemma bin_log_pure_l Δ (Γ : stringmap type) (E : coPset)
......
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