Commit 72f96ce6 authored by Dan Frumin's avatar Dan Frumin

Some experiments with `bin_log_related_arrow`

parent e86c76ff
From iris.proofmode Require Import tactics.
From iris_logrel Require Import logrel.
Section test.
Context `{logrelG Σ}.
(* TODO: interesting fact?
bin_log_related_arrow_val can be proved using bin_log_related_arrow
specifically, at some point we can update
{Δ; Γ} v1 log v2 : τ
τ Δ (v1, v2') for some value v2'
Lemma bin_log_related_arrow_val Δ Γ E (f x f' x' : binder) (e e' eb eb' : expr) (τ τ' : type) :
e = (rec: f x := eb)%E
e' = (rec: f' x' := eb')%E
Closed e
Closed e'
( v1 v2, τ Δ (v1, v2) -
{Δ;Γ} App e (of_val v1) log App e' (of_val v2) : τ') -
{E;Δ;Γ} e log e' : TArrow τ τ'.
iIntros (????) "#H".
iApply bin_log_related_arrow; eauto. iAlways.
iIntros (v1 v2) "#Hvv".
rewrite bin_log_related_eq.
iIntros (ρ vvs) "#Hspec #HΓ". simpl.
rewrite /env_subst. rewrite !Closed_subst_p_id.
rewrite /interp_expr.
iIntros (j K) "Hj /=".
tp_bind j v2.
iSpecialize ("Hvv" $! ρ vvs with "Hspec [HΓ]"); auto.
iSpecialize ("Hvv" $! j (AppRCtx (RecV f' x' eb') :: K)).
simpl. rewrite /env_subst !Closed_subst_p_id.
iMod ("Hvv" with "Hj") as "Hvv".
iMod (wp_value_inv with "Hvv") as (v') "[Hj Hvv]".
iSpecialize ("H" with "Hvv Hspec [HΓ]"); auto.
replace (rec: f x := eb)%E with (of_val (rec: f x := eb)) by (unlock;reflexivity).
replace (rec: f' x' := eb')%E with (of_val (rec: f' x' := eb')) by (unlock;reflexivity).
rewrite /env_subst /= !Closed_subst_p_id.
iSpecialize ("H" with "Hj").
End test.
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