Commit 9357c013 authored by Dan Frumin's avatar Dan Frumin

Move the -val-arrow rule to rules.v

parent 7bf3e041
...@@ -47,6 +47,33 @@ Section properties. ...@@ -47,6 +47,33 @@ Section properties.
rewrite /env_subst. rewrite !Closed_subst_p_id. done. rewrite /env_subst. rewrite !Closed_subst_p_id. done.
Qed. Qed.
Notation "P ∗-∗ Q" := ((P - Q) (Q - P))%I (at level 50).
Lemma interp_val_arrow τ σ Δ (v v' : val) ρ :
spec_ctx ρ -
τ σ Δ (v, v')
-
( ( (w w' : val), τ Δ (w, w')
- {Δ;} v w log v' w' : σ))%I.
Proof.
iIntros "#Hspec".
iSplitL.
- iIntros "/= #Hvv !#".
iIntros (w w') "#Hw".
iApply related_ret.
iApply ("Hvv" $! (w, w') with "Hw").
- iIntros "#Hvv /= !#".
iIntros ([w w']) "#Hww /=".
iSpecialize ("Hvv" with "Hww").
rewrite bin_log_related_eq /bin_log_related_def.
iIntros (j K) "Hj /=".
iSpecialize ("Hvv" $! ρ with "Hspec []").
{ iAlways. by iApply interp_env_nil. }
rewrite /interp_expr /=.
iSpecialize ("Hvv" $! j K).
rewrite /env_subst !fmap_empty !subst_p_empty.
by iMod ("Hvv" with "Hj").
Qed.
Lemma bin_log_related_weaken_2 τi E Δ Γ e1 e2 (τ : type) : Lemma bin_log_related_weaken_2 τi E Δ Γ e1 e2 (τ : type) :
{E;Δ;Γ} e1 log e2 : τ - {E;Δ;Γ} e1 log e2 : τ -
{E;τi::Δ;⤉Γ} e1 log e2 : τ.[ren (+1)]. {E;τi::Δ;⤉Γ} e1 log e2 : τ.[ren (+1)].
......
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