Commit 3c109f48 authored by Dan Frumin's avatar Dan Frumin

Generalize `bin_log_related_arrow` a bit

parent 241c86c6
......@@ -26,26 +26,35 @@ Section hax.
Notation D := (prodC valC valC -n> iProp Σ).
Implicit Types Δ : listC D.
Lemma bin_log_related_arrow Γ (f x f' x' : binder) (e e' : expr) (τ τ' : type)
Lemma bin_log_related_arrow Γ E (f x f' x' : binder) (e e' : expr) (τ τ' : type)
(Hclosed : Closed (rec: f x := e)%E )
(Hclosed' : Closed (rec: f' x' := e')%E) :
( Δ vv, τ Δ vv -
App (Rec f x e) (of_val (vv.1)) log App (Rec f' x' e') (of_val (vv.2)) : τ') -
Γ (Rec f x e) log (Rec f' x' e') : TArrow τ τ'.
Γ App (Rec f x e) (of_val (vv.1)) log App (Rec f' x' e') (of_val (vv.2)) : τ') -
{E,E;Γ} (Rec f x e) log (Rec f' x' e') : TArrow τ τ'.
Proof.
iIntros "#H".
iIntros (Δ vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj".
cbn-[subst_p]. rewrite /env_subst !Closed_subst_p_id.
iModIntro. iApply wp_value; auto.
cbn-[subst_p].
iModIntro.
rewrite {2}/env_subst Closed_subst_p_id.
iApply wp_value.
{ simpl. erewrite decide_left. done. }
iExists (RecV f' x' e'). simpl.
rewrite /env_subst Closed_subst_p_id.
iExists (RecV f' x' e').
iFrame "Hj". iAlways. iIntros (vv) "Hvv".
iSpecialize ("H" $! Δ vv with "Hvv").
iSpecialize ("H" $! Δ with "Hs []").
{ iAlways. iApply interp_env_nil. }
rewrite !fmap_empty /env_subst !subst_p_empty. done.
Unshelve. all: rewrite /Closed /= in Hclosed Hclosed'; eauto.
{ iAlways. iApply "HΓ". }
Unshelve. all: trivial.
assert (Closed ((rec: f x := e) (vv.1))%E).
{ revert Hclosed. unfold Closed. simpl.
intros. split_and?; auto. apply of_val_closed. }
assert (Closed ((rec: f' x' := e') (vv.2))%E).
{ revert Hclosed'. unfold Closed. simpl.
intros. split_and?; auto. apply of_val_closed. }
rewrite /env_subst. rewrite !Closed_subst_p_id. done.
Qed.
Lemma weird_bind e Q :
......
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