Commit 5ac96435 by Dan Frumin

Move 'bin_log_related_spec_ctx' to the rules module

parent 6b01a6cf
......@@ -79,27 +79,6 @@ Section rules.
iApply binary_fundamental_masked; eauto with typeable.
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.
Definition shootInv `{oneshotG Σ} x γ : iProp Σ :=
(x ↦ᵢ #0 pending γ x ↦ᵢ #1 shot γ)%I.
Ltac close_shoot := iNext; (iLeft + iRight); by iFrame.
......
......@@ -79,6 +79,27 @@ Section properties.
by iApply interp_ret.
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