Commit 737361de authored by Dan Frumin's avatar Dan Frumin

Better notation for autosubst substitution and liftings

parent ab35b735
......@@ -250,7 +250,7 @@ Section proof.
Context `{!logrelG Σ, !msizeG Σ, !lockG Σ}.
Lemma eqKey_refinement Δ Γ γ :
{,;tableR γ :: Δ;Autosubst_Classes.subst (ren (+1)) <$> Γ}
{,;tableR γ :: Δ;Γ}
eqKey
log
eqKey : TArrow (TVar 0) (TArrow (TVar 0) TBool).
......
......@@ -338,7 +338,7 @@ Section masked.
Closed (dom _ Γ) e
Closed (dom _ Γ) e'
logrelN E
( (τi : D), ⌜∀ ww, Persistent (τi ww) ({E;(τi::Δ);Autosubst_Classes.subst (ren (+1)) <$> Γ} e log e' : τ)) -
( (τi : D), ⌜∀ ww, Persistent (τi ww) ({E;(τi::Δ);Γ} e log e' : τ)) -
{E;Δ;Γ} TLam e log TLam e' : TForall τ.
Proof.
rewrite bin_log_related_eq.
......@@ -376,7 +376,7 @@ Section masked.
Lemma bin_log_related_tapp (τi : D) Δ Γ e e' τ :
( ww, Persistent (τi ww))
{E;Δ;Γ} e log e' : TForall τ -
{E;τi::Δ;Autosubst_Classes.subst (ren (+1)) <$> Γ} TApp e log TApp e' : τ.
{E;τi::Δ;Γ} TApp e log TApp e' : τ.
Proof.
rewrite bin_log_related_eq.
iIntros (?) "IH".
......@@ -435,7 +435,7 @@ Section masked.
Lemma bin_log_related_pack (τi : D) Δ Γ e e' τ :
( ww, Persistent (τi ww))
{E;τi::Δ;Autosubst_Classes.subst (ren (+1)) <$> Γ} e log e' : τ -
{E;τi::Δ;Γ} e log e' : τ -
{E;Δ;Γ} Pack e log Pack e' : TExists τ.
Proof.
rewrite bin_log_related_eq.
......@@ -457,8 +457,8 @@ Section masked.
(Hmasked : logrelN E) :
{E;Δ;Γ} e1 log e1' : TExists τ -
( τi : D, ⌜∀ ww, Persistent (τi ww)
{E;τi::Δ;Autosubst_Classes.subst (ren (+1)) <$> Γ}
e2 log e2' : TArrow τ (Autosubst_Classes.subst (ren (+1)) τ2)) -
{E;τi::Δ;Γ}
e2 log e2' : TArrow τ (asubst (ren (+1)) τ2)) -
{E;Δ;Γ} Unpack e1 e2 log Unpack e1' e2' : τ2.
Proof.
rewrite bin_log_related_eq.
......@@ -630,7 +630,7 @@ Section masked.
- by iApply (bin_log_related_app with "[] []").
- assert (Closed (dom _ Γ) e).
{ apply typed_X_closed in Ht.
pose (K:=(dom_fmap (Autosubst_Classes.subst (ren (+1))) Γ (D:=stringset))).
pose (K:=(dom_fmap (asubst (ren (+1))) Γ (D:=stringset))).
fold_leibniz. by rewrite -K. }
iApply bin_log_related_tlam; eauto.
- by iApply bin_log_related_tapp'.
......
......@@ -139,7 +139,7 @@ Section interp_env_facts.
Qed.
Lemma interp_env_ren Δ (Γ : stringmap type) E1 E2 (vvs : stringmap (val * val)) (τi : D) :
interp_env (Autosubst_Classes.subst (ren (+1)) <$> Γ) E1 E2 (τi :: Δ) vvs
interp_env (Γ) E1 E2 (τi :: Δ) vvs
⊣⊢
interp_env Γ E1 E2 Δ vvs.
Proof.
......@@ -209,7 +209,7 @@ Section related_facts.
Lemma bin_log_related_weaken_2 τi Δ Γ e1 e2 τ :
{Δ;Γ} e1 log e2 : τ -
{τi::Δ;Autosubst_Classes.subst (ren (+1)) <$>Γ} e1 log e2 : τ.[ren (+1)].
{τi::Δ;Γ} e1 log e2 : τ.[ren (+1)].
Proof.
rewrite bin_log_related_eq /bin_log_related_def.
iIntros "Hlog" (vvs ρ) "#Hs #HΓ".
......
......@@ -40,3 +40,7 @@ Ltac properness :=
Reserved Notation "⟦ τ ⟧" (at level 0, τ at level 70).
Reserved Notation "⟦ τ ⟧ₑ" (at level 0, τ at level 70).
Reserved Notation "⟦ Γ ⟧*" (at level 0, Γ at level 70).
Notation asubst := Autosubst_Classes.subst.
Notation "⤉ Γ" := (asubst (ren (+1)) <$> Γ)
(at level 10, format "⤉ Γ").
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