This file follows very closely its sibling CBVTyped.v
. It is recommended to read that
one first: the comments on this one will be quite more terse and focus on the differences.
As our framework is "well-typed well-scoped", when we mean untyped, we really mean
unityped, i.e., we will take the single element set as set of types. Although, the
typing rules will not be as uninteresting as it would seem. Indeed, as we adopt a
single-sided sequent-calculus style of presentation, we do give types to continuations
(formally negated types), and we thus have not one type, but two: the type of terms
β
and the type of continuations β
.
Typing contexts, terms, values, evaluation contexts and configurations work straightforwardly.
Variant ty : Type :=
| Left : ty
| Right : ty
.
Notation "β" := (Left) (at level 20) : ty_scope . Notation "β" := (Right) (at level 20) : ty_scope . Definition t_ctx : Type := Ctx.ctx ty . Bind Scope ctx_scope with t_ctx .
Note that is is the proper pure untyped lambda calculus: in constrast with our STLC example, the lambda is not recursive and there is no unit value nor base type, only functions.
Inductive term (Ξ : t_ctx) : Type :=
| Val : val Ξ -> term Ξ
| App : term Ξ -> term Ξ -> term Ξ
with val (Ξ : t_ctx) : Type :=
| Var : Ξ β β -> val Ξ
| Lam : term (Ξ βΆβ β) -> val Ξ
.
Inductive ev_ctx (Ξ : t_ctx) : Type :=
| K0 : Ξ β β -> ev_ctx Ξ
| K1 : term Ξ -> ev_ctx Ξ -> ev_ctx Ξ
| K2 : val Ξ -> ev_ctx Ξ -> ev_ctx Ξ
.
Variant state (Ξ : t_ctx) : Type :=
| Cut : term Ξ -> ev_ctx Ξ -> state Ξ
.
We introduce the sorted family of generalized values, together with the generalized variable.
Equations val_m : t_ctx -> ty -> Type := val_m Ξ (β) := val Ξ ; val_m Ξ (β) := ev_ctx Ξ . Equations a_id {Ξ} : Ξ =[val_m]> Ξ := a_id (β) i := Var i ; a_id (β) i := K0 i .
Equations t_rename {Ξ Ξ} : Ξ β Ξ -> term Ξ -> term Ξ := t_rename f (Val v) := Val (v_rename f v) ; t_rename f (App t1 t2) := App (t_rename f t1) (t_rename f t2) ; with v_rename {Ξ Ξ} : Ξ β Ξ -> val Ξ -> val Ξ := v_rename f (Var i) := Var (f _ i) ; v_rename f (Lam t) := Lam (t_rename (r_shift1 f) t) . Equations e_rename {Ξ Ξ} : Ξ β Ξ -> ev_ctx Ξ -> ev_ctx Ξ := e_rename f (K0 i) := K0 (f _ i) ; e_rename f (K1 t Ο) := K1 (t_rename f t) (e_rename f Ο) ; e_rename f (K2 v Ο) := K2 (v_rename f v) (e_rename f Ο) . Equations s_rename {Ξ Ξ} : Ξ β Ξ -> state Ξ -> state Ξ := s_rename f (Cut t Ο) := Cut (t_rename f t) (e_rename f Ο). Equations m_rename {Ξ Ξ} : Ξ β Ξ -> val_m Ξ βα΅’ val_m Ξ := m_rename f (β) v := v_rename f v ; m_rename f (β) Ο := e_rename f Ο .
Renaming an assigment on the left.
Definition a_ren {Ξ1 Ξ2 Ξ3} : Ξ1 =[val_m]> Ξ2 -> Ξ2 β Ξ3 -> Ξ1 =[val_m]> Ξ3 := fun f g _ i => m_rename g _ (f _ i) . Arguments a_ren _ _ _ /.
The following bunch of notations will help us to keep the code readable:
Notation "t ββα΅£ r" := (t_rename r%asgn t) (at level 14). Notation "v α΅₯βα΅£ r" := (v_rename r%asgn v) (at level 14). Notation "Ο ββα΅£ r" := (e_rename r%asgn Ο) (at level 14). Notation "v ββα΅£ r" := (m_rename r%asgn _ v) (at level 14). Notation "s ββα΅£ r" := (s_rename r%asgn s) (at level 14). Notation "a βα΅£ r" := (a_ren a%asgn r%asgn) (at level 14) : asgn_scope.
The weakenings we will need for substitution..
Definition t_shift1 {Ξ a} := @t_rename Ξ (Ξ βΆβ a) r_pop. Definition v_shift1 {Ξ a} := @v_rename Ξ (Ξ βΆβ a) r_pop. Definition m_shift1 {Ξ a} := @m_rename Ξ (Ξ βΆβ a) r_pop. Definition a_shift1 {Ξ Ξ a} (f : Ξ =[val_m]> Ξ) := [ a_map f m_shift1 ,β a_id a top ]%asgn .
Equations t_subst {Ξ Ξ} : Ξ =[val_m]> Ξ -> term Ξ -> term Ξ := t_subst f (Val v) := Val (v_subst f v) ; t_subst f (App t1 t2) := App (t_subst f t1) (t_subst f t2) ; with v_subst {Ξ Ξ} : Ξ =[val_m]> Ξ -> val Ξ -> val Ξ := v_subst f (Var i) := f _ i ; v_subst f (Lam t) := Lam (t_subst (a_shift1 f) t) . Equations e_subst {Ξ Ξ} : Ξ =[val_m]> Ξ -> ev_ctx Ξ -> ev_ctx Ξ := e_subst f (K0 i) := f _ i ; e_subst f (K1 t Ο) := K1 (t_subst f t) (e_subst f Ο) ; e_subst f (K2 v Ο) := K2 (v_subst f v) (e_subst f Ο) . Notation "t `ββ a" := (t_subst a%asgn t) (at level 30). Notation "v `α΅₯β a" := (v_subst a%asgn v) (at level 30). Notation "Ο `ββ a" := (e_subst a%asgn Ο) (at level 30). Equations m_subst : val_m ββ β¦ val_m , val_m β§β := m_subst _ (β) v _ f := v `α΅₯β f ; m_subst _ (β) Ο _ f := Ο `ββ f . Equations s_subst : state ββ β¦ val_m , state β§β := s_subst _ (Cut t Ο) _ f := Cut (t `ββ f) (Ο `ββ f) .
We can now instanciate the substitution monoid and module structures.
#[global] Instance val_m_monoid : subst_monoid val_m := {| v_var := @a_id ; v_sub := m_subst |} . #[global] Instance state_module : subst_module val_m state := {| c_sub := s_subst |} .
Single-variable substitution.
Definition assign1 {Ξ a} v : (Ξ βΆβ a) =[val_m]> Ξ := a_id βΆβ v . Definition t_subst1 {Ξ a} (t : term _) v := t `ββ @assign1 Ξ a v. Notation "t /[ v ]" := (t_subst1 t v) (at level 50, left associativity).
As before we define observations (copatterns), as there are only functions and
continuations there is exactly one pattern at each type. Knowing this, we could
have made this type (obs
) disappear, but it is kept here for the sake of being
more explicit.
Variant obs : ty -> Type :=
| ORet : obs (β)
| OApp : obs (β)
.
Observation still behave as binders, returning bind a term (what we are returning) and applying binds a term (the argument) and a continuation.
Equations obs_dom {a} : obs a -> t_ctx := obs_dom (@ORet) := β βΆβ β ; obs_dom (@OApp) := β βΆβ β βΆβ β . Definition obs_op : Oper ty t_ctx := {| o_op := obs ; o_dom := @obs_dom |} . Notation ORet' := (ORet : o_op obs_op _). Notation OApp' := (OApp : o_op obs_op _).
We now define applying an observation with arguments to a value.
Equations obs_app {Ξ a} (v : val_m Ξ a) (p : obs a) (Ξ³ : obs_dom p =[val_m]> Ξ) : state Ξ :=
obs_app v (OApp) Ξ³ := Cut (Val v) (K2 (Ξ³ _ (pop top)) (Ξ³ _ top)) ;
obs_app Ο (ORet) Ξ³ := Cut (Val (Ξ³ _ top)) Ο .
Normal forms take the exact same form as for ULC: a head variable and an observation on it, with arguments.
Definition nf := c_var β₯β (obs_op # val_m).
The evaluator as a state machine.
β¨ t1 t2 | Ο β© β β¨ t2 | t1 β
1 Ο β©
β¨ v | x β©
normalβ¨ v | t β
1 Ο β© β β¨ t | v β
2 Ο β©
β¨ x | v β
2 Ο β©
normalβ¨ Ξ»x.t | v β
2 Ο β© β β¨ t[xβ¦v] | Ο β©
Rules 1,3,5 step to a new configuration, while cases 2,4 are stuck on normal forms.
Equations eval_step {Ξ : t_ctx} : state Ξ -> (state Ξ + nf Ξ) := eval_step (Cut (App t1 t2) (Ο)) := inl (Cut t2 (K1 t1 Ο)) ; eval_step (Cut (Val v) (K0 i)) := inr (i β ORet' β¦ ! βΆβ v β¦) ; eval_step (Cut (Val v) (K1 t Ο)) := inl (Cut t (K2 v Ο)) ; eval_step (Cut (Val (Var i)) (K2 v Ο)) := inr (i β OApp' β¦ ! βΆβ v βΆβ Ο β¦) ; eval_step (Cut (Val (Lam t)) (K2 v Ο)) := inl (Cut (t /[ v ]) Ο) . Definition ulc_eval {Ξ : t_ctx} : state Ξ -> delay (nf Ξ) := iter_delay (ret_delay β eval_step).
We now tackle the basic syntactic lemmas on renaming and substitution. See you in 400 lines.
Scheme term_mut := Induction for term Sort Prop with val_mut := Induction for val Sort Prop . Record syn_ind_args (P_t : forall Ξ, term Ξ -> Prop) (P_v : forall Ξ, val Ξ -> Prop) (P_e : forall Ξ, ev_ctx Ξ -> Prop) := { ind_val {Ξ} v (_ : P_v Ξ v) : P_t Ξ (Val v) ; ind_app {Ξ} t1 (_ : P_t Ξ t1) t2 (_ : P_t Ξ t2) : P_t Ξ (App t1 t2) ; ind_var {Ξ} i : P_v Ξ (Var i) ; ind_lam {Ξ} t (_ : P_t _ t) : P_v Ξ (Lam t) ; ind_kvar {Ξ} i : P_e Ξ (K0 i) ; ind_kfun {Ξ} t (_ : P_t Ξ t) Ο (_ : P_e Ξ Ο) : P_e Ξ (K1 t Ο) ; ind_karg {Ξ} v (_ : P_v Ξ v) Ο (_ : P_e Ξ Ο) : P_e Ξ (K2 v Ο) } .destruct H; now apply (term_mut P_t P_v). Qed.P_t: forall Ξ : t_ctx, term Ξ -> Prop
P_v: forall Ξ : t_ctx, val Ξ -> Prop
P_e: forall Ξ : t_ctx, ev_ctx Ξ -> Prop
H: syn_ind_args P_t P_v P_e
Ξ: t_ctx
t: term ΞP_t Ξ tdestruct H; now apply (val_mut P_t P_v). Qed.P_t: forall Ξ : t_ctx, term Ξ -> Prop
P_v: forall Ξ : t_ctx, val Ξ -> Prop
P_e: forall Ξ : t_ctx, ev_ctx Ξ -> Prop
H: syn_ind_args P_t P_v P_e
Ξ: t_ctx
v: val ΞP_v Ξ vP_t: forall Ξ : t_ctx, term Ξ -> Prop
P_v: forall Ξ : t_ctx, val Ξ -> Prop
P_e: forall Ξ : t_ctx, ev_ctx Ξ -> Prop
H: syn_ind_args P_t P_v P_e
Ξ: t_ctx
Ο: ev_ctx ΞP_e Ξ ΟP_t: forall Ξ : t_ctx, term Ξ -> Prop
P_v: forall Ξ : t_ctx, val Ξ -> Prop
P_e: forall Ξ : t_ctx, ev_ctx Ξ -> Prop
H: syn_ind_args P_t P_v P_e
Ξ: t_ctx
c: Ξ β βP_e Ξ (K0 c)P_t: forall Ξ : t_ctx, term Ξ -> Prop
P_v: forall Ξ : t_ctx, val Ξ -> Prop
P_e: forall Ξ : t_ctx, ev_ctx Ξ -> Prop
H: syn_ind_args P_t P_v P_e
Ξ: t_ctx
t: term Ξ
Ο: ev_ctx Ξ
IHΟ: P_e Ξ ΟP_e Ξ (K1 t Ο)P_t: forall Ξ : t_ctx, term Ξ -> Prop
P_v: forall Ξ : t_ctx, val Ξ -> Prop
P_e: forall Ξ : t_ctx, ev_ctx Ξ -> Prop
H: syn_ind_args P_t P_v P_e
Ξ: t_ctx
v: val Ξ
Ο: ev_ctx Ξ
IHΟ: P_e Ξ ΟP_e Ξ (K2 v Ο)apply (ind_kvar _ _ _ H).P_t: forall Ξ : t_ctx, term Ξ -> Prop
P_v: forall Ξ : t_ctx, val Ξ -> Prop
P_e: forall Ξ : t_ctx, ev_ctx Ξ -> Prop
H: syn_ind_args P_t P_v P_e
Ξ: t_ctx
c: Ξ β βP_e Ξ (K0 c)apply (ind_kfun _ _ _ H); auto; apply (term_ind_mut _ _ _ H).P_t: forall Ξ : t_ctx, term Ξ -> Prop
P_v: forall Ξ : t_ctx, val Ξ -> Prop
P_e: forall Ξ : t_ctx, ev_ctx Ξ -> Prop
H: syn_ind_args P_t P_v P_e
Ξ: t_ctx
t: term Ξ
Ο: ev_ctx Ξ
IHΟ: P_e Ξ ΟP_e Ξ (K1 t Ο)apply (ind_karg _ _ _ H); auto; apply (val_ind_mut _ _ _ H). Qed.P_t: forall Ξ : t_ctx, term Ξ -> Prop
P_v: forall Ξ : t_ctx, val Ξ -> Prop
P_e: forall Ξ : t_ctx, ev_ctx Ξ -> Prop
H: syn_ind_args P_t P_v P_e
Ξ: t_ctx
v: val Ξ
Ο: ev_ctx Ξ
IHΟ: P_e Ξ ΟP_e Ξ (K2 v Ο)
Renaming respects pointwise equality of assignments.
Definition t_ren_proper_P Ξ (t : term Ξ) : Prop := forall Ξ (f1 f2 : Ξ β Ξ), f1 β‘β f2 -> t ββα΅£ f1 = t ββα΅£ f2 . Definition v_ren_proper_P Ξ (v : val Ξ) : Prop := forall Ξ (f1 f2 : Ξ β Ξ), f1 β‘β f2 -> v α΅₯βα΅£ f1 = v α΅₯βα΅£ f2 . Definition e_ren_proper_P Ξ (Ο : ev_ctx Ξ) : Prop := forall Ξ (f1 f2 : Ξ β Ξ), f1 β‘β f2 -> Ο ββα΅£ f1 = Ο ββα΅£ f2 .syn_ind_args t_ren_proper_P v_ren_proper_P e_ren_proper_Pforall (Ξ : t_ctx) (v : val Ξ), v_ren_proper_P Ξ v -> t_ren_proper_P Ξ (Val v)forall (Ξ : t_ctx) (t1 : term Ξ), t_ren_proper_P Ξ t1 -> forall t2 : term Ξ, t_ren_proper_P Ξ t2 -> t_ren_proper_P Ξ (App t1 t2)forall (Ξ : t_ctx) (i : Ξ β β), v_ren_proper_P Ξ (Var i)forall (Ξ : t_ctx) (t : term (Ξ βΆβ β)), t_ren_proper_P (Ξ βΆβ β) t -> v_ren_proper_P Ξ (Lam t)forall (Ξ : t_ctx) (i : Ξ β β), e_ren_proper_P Ξ (K0 i)forall (Ξ : t_ctx) (t : term Ξ), t_ren_proper_P Ξ t -> forall Ο : ev_ctx Ξ, e_ren_proper_P Ξ Ο -> e_ren_proper_P Ξ (K1 t Ο)forall (Ξ : t_ctx) (v : val Ξ), v_ren_proper_P Ξ v -> forall Ο : ev_ctx Ξ, e_ren_proper_P Ξ Ο -> e_ren_proper_P Ξ (K2 v Ο)forall (Ξ : t_ctx) (v : val Ξ), (forall (Ξ : t_ctx) (f1 f2 : Ξ β Ξ), f1 β‘β f2 -> v α΅₯βα΅£ f1 = v α΅₯βα΅£ f2) -> forall (Ξ : t_ctx) (f1 f2 : Ξ β Ξ), f1 β‘β f2 -> Val v ββα΅£ f1 = Val v ββα΅£ f2forall (Ξ : t_ctx) (t1 : term Ξ), (forall (Ξ : t_ctx) (f1 f2 : Ξ β Ξ), f1 β‘β f2 -> t1 ββα΅£ f1 = t1 ββα΅£ f2) -> forall t2 : term Ξ, (forall (Ξ : t_ctx) (f1 f2 : Ξ β Ξ), f1 β‘β f2 -> t2 ββα΅£ f1 = t2 ββα΅£ f2) -> forall (Ξ : t_ctx) (f1 f2 : Ξ β Ξ), f1 β‘β f2 -> App t1 t2 ββα΅£ f1 = App t1 t2 ββα΅£ f2forall (Ξ : t_ctx) (i : Ξ β β) (Ξ : t_ctx) (f1 f2 : Ξ β Ξ), f1 β‘β f2 -> Var i α΅₯βα΅£ f1 = Var i α΅₯βα΅£ f2forall (Ξ : t_ctx) (t : term (Ξ βΆβ β)), (forall (Ξ : t_ctx) (f1 f2 : (Ξ βΆβ β) β Ξ), f1 β‘β f2 -> t ββα΅£ f1 = t ββα΅£ f2) -> forall (Ξ : t_ctx) (f1 f2 : Ξ β Ξ), f1 β‘β f2 -> Lam t α΅₯βα΅£ f1 = Lam t α΅₯βα΅£ f2forall (Ξ : t_ctx) (i : Ξ β β) (Ξ : t_ctx) (f1 f2 : Ξ β Ξ), f1 β‘β f2 -> K0 i ββα΅£ f1 = K0 i ββα΅£ f2forall (Ξ : t_ctx) (t : term Ξ), (forall (Ξ : t_ctx) (f1 f2 : Ξ β Ξ), f1 β‘β f2 -> t ββα΅£ f1 = t ββα΅£ f2) -> forall Ο : ev_ctx Ξ, (forall (Ξ : t_ctx) (f1 f2 : Ξ β Ξ), f1 β‘β f2 -> Ο ββα΅£ f1 = Ο ββα΅£ f2) -> forall (Ξ : t_ctx) (f1 f2 : Ξ β Ξ), f1 β‘β f2 -> K1 t Ο ββα΅£ f1 = K1 t Ο ββα΅£ f2forall (Ξ : t_ctx) (v : val Ξ), (forall (Ξ : t_ctx) (f1 f2 : Ξ β Ξ), f1 β‘β f2 -> v α΅₯βα΅£ f1 = v α΅₯βα΅£ f2) -> forall Ο : ev_ctx Ξ, (forall (Ξ : t_ctx) (f1 f2 : Ξ β Ξ), f1 β‘β f2 -> Ο ββα΅£ f1 = Ο ββα΅£ f2) -> forall (Ξ : t_ctx) (f1 f2 : Ξ β Ξ), f1 β‘β f2 -> K2 v Ο ββα΅£ f1 = K2 v Ο ββα΅£ f2Ξ: t_ctx
i: Ξ β β
Ξ: t_ctx
f1, f2: Ξ β Ξ
H: f1 β‘β f2f1 (β) i = f2 (β) iΞ: t_ctx
t: term (Ξ βΆβ β)
H: forall (Ξ : t_ctx) (f1 f2 : (Ξ βΆβ β) β Ξ), f1 β‘β f2 -> t ββα΅£ f1 = t ββα΅£ f2
Ξ: t_ctx
f1, f2: Ξ β Ξ
H0: f1 β‘β f2t ββα΅£ r_shift1 f1 = t ββα΅£ r_shift1 f2Ξ: t_ctx
i: Ξ β β
Ξ: t_ctx
f1, f2: Ξ β Ξ
H: f1 β‘β f2f1 (β) i = f2 (β) inow apply r_shift1_eq. Qed.Ξ: t_ctx
t: term (Ξ βΆβ β)
H: forall (Ξ : t_ctx) (f1 f2 : (Ξ βΆβ β) β Ξ), f1 β‘β f2 -> t ββα΅£ f1 = t ββα΅£ f2
Ξ: t_ctx
f1, f2: Ξ β Ξ
H0: f1 β‘β f2r_shift1 f1 β‘β r_shift1 f2intros f1 f2 H1 x y ->; now apply (term_ind_mut _ _ _ ren_proper_prf). Qed.Ξ, Ξ: t_ctxProper (asgn_eq Ξ Ξ ==> eq ==> eq) t_renameintros f1 f2 H1 x y ->; now apply (val_ind_mut _ _ _ ren_proper_prf). Qed.Ξ, Ξ: t_ctxProper (asgn_eq Ξ Ξ ==> eq ==> eq) v_renameintros f1 f2 H1 x y ->; now apply (ctx_ind_mut _ _ _ ren_proper_prf). Qed.Ξ, Ξ: t_ctxProper (asgn_eq Ξ Ξ ==> eq ==> eq) e_renameintros ? ? H1 [] _ ? ->; cbn in *; now rewrite H1. Qed.Ξ, Ξ: t_ctxProper (asgn_eq Ξ Ξ ==> (ββ a, eq ==> eq)) m_renameintros ? ? H1 _ x ->; destruct x; cbn; now rewrite H1. Qed.Ξ, Ξ: t_ctxProper (asgn_eq Ξ Ξ ==> eq ==> eq) s_renameintros ?? H1 ?? H2 ??; apply (m_ren_eq _ _ H2), H1. Qed.Ξ1, Ξ2, Ξ3: t_ctxProper (asgn_eq Ξ1 Ξ2 ==> asgn_eq Ξ2 Ξ3 ==> asgn_eq Ξ1 Ξ3) a_renΞ, Ξ: t_ctx
x: tyProper (asgn_eq Ξ Ξ ==> asgn_eq (Ξ βΆβ x) (Ξ βΆβ x)) a_shift1now rewrite H. Qed.Ξ1: ctx ty
Ξ: t_ctx
y0: ty
x0, y: Ξ1 =[ val_m ]> Ξ
H: x0 β‘β y
a: ty
v: var a Ξ1m_shift1 a (x0 a v) = m_shift1 a (y a v)
Renaming-renaming assocativity.
Definition t_ren_ren_P Ξ1 (t : term Ξ1) : Prop := forall Ξ2 Ξ3 (f1 : Ξ1 β Ξ2) (f2 : Ξ2 β Ξ3), (t ββα΅£ f1) ββα΅£ f2 = t ββα΅£ (f1 α΅£β f2) . Definition v_ren_ren_P Ξ1 (v : val Ξ1) : Prop := forall Ξ2 Ξ3 (f1 : Ξ1 β Ξ2) (f2 : Ξ2 β Ξ3), (v α΅₯βα΅£ f1) α΅₯βα΅£ f2 = v α΅₯βα΅£ (f1 α΅£β f2) . Definition e_ren_ren_P Ξ1 (Ο : ev_ctx Ξ1) : Prop := forall Ξ2 Ξ3 (f1 : Ξ1 β Ξ2) (f2 : Ξ2 β Ξ3), (Ο ββα΅£ f1) ββα΅£ f2 = Ο ββα΅£ (f1 α΅£β f2) .syn_ind_args t_ren_ren_P v_ren_ren_P e_ren_ren_Pforall (Ξ : t_ctx) (v : val Ξ), v_ren_ren_P Ξ v -> t_ren_ren_P Ξ (Val v)forall (Ξ : t_ctx) (t1 : term Ξ), t_ren_ren_P Ξ t1 -> forall t2 : term Ξ, t_ren_ren_P Ξ t2 -> t_ren_ren_P Ξ (App t1 t2)forall (Ξ : t_ctx) (i : Ξ β β), v_ren_ren_P Ξ (Var i)forall (Ξ : t_ctx) (t : term (Ξ βΆβ β)), t_ren_ren_P (Ξ βΆβ β) t -> v_ren_ren_P Ξ (Lam t)forall (Ξ : t_ctx) (i : Ξ β β), e_ren_ren_P Ξ (K0 i)forall (Ξ : t_ctx) (t : term Ξ), t_ren_ren_P Ξ t -> forall Ο : ev_ctx Ξ, e_ren_ren_P Ξ Ο -> e_ren_ren_P Ξ (K1 t Ο)forall (Ξ : t_ctx) (v : val Ξ), v_ren_ren_P Ξ v -> forall Ο : ev_ctx Ξ, e_ren_ren_P Ξ Ο -> e_ren_ren_P Ξ (K2 v Ο)forall (Ξ : t_ctx) (v : val Ξ), (forall (Ξ2 Ξ3 : t_ctx) (f1 : Ξ β Ξ2) (f2 : Ξ2 β Ξ3), (v α΅₯βα΅£ f1) α΅₯βα΅£ f2 = v α΅₯βα΅£ (f1 α΅£β f2)) -> forall (Ξ2 Ξ3 : t_ctx) (f1 : Ξ β Ξ2) (f2 : Ξ2 β Ξ3), (Val v ββα΅£ f1) ββα΅£ f2 = Val v ββα΅£ (f1 α΅£β f2)forall (Ξ : t_ctx) (t1 : term Ξ), (forall (Ξ2 Ξ3 : t_ctx) (f1 : Ξ β Ξ2) (f2 : Ξ2 β Ξ3), (t1 ββα΅£ f1) ββα΅£ f2 = t1 ββα΅£ (f1 α΅£β f2)) -> forall t2 : term Ξ, (forall (Ξ2 Ξ3 : t_ctx) (f1 : Ξ β Ξ2) (f2 : Ξ2 β Ξ3), (t2 ββα΅£ f1) ββα΅£ f2 = t2 ββα΅£ (f1 α΅£β f2)) -> forall (Ξ2 Ξ3 : t_ctx) (f1 : Ξ β Ξ2) (f2 : Ξ2 β Ξ3), (App t1 t2 ββα΅£ f1) ββα΅£ f2 = App t1 t2 ββα΅£ (f1 α΅£β f2)forall (Ξ : t_ctx) (i : Ξ β β) (Ξ2 Ξ3 : t_ctx) (f1 : Ξ β Ξ2) (f2 : Ξ2 β Ξ3), (Var i α΅₯βα΅£ f1) α΅₯βα΅£ f2 = Var i α΅₯βα΅£ (f1 α΅£β f2)forall (Ξ : t_ctx) (t : term (Ξ βΆβ β)), (forall (Ξ2 Ξ3 : t_ctx) (f1 : (Ξ βΆβ β) β Ξ2) (f2 : Ξ2 β Ξ3), (t ββα΅£ f1) ββα΅£ f2 = t ββα΅£ (f1 α΅£β f2)) -> forall (Ξ2 Ξ3 : t_ctx) (f1 : Ξ β Ξ2) (f2 : Ξ2 β Ξ3), (Lam t α΅₯βα΅£ f1) α΅₯βα΅£ f2 = Lam t α΅₯βα΅£ (f1 α΅£β f2)forall (Ξ : t_ctx) (i : Ξ β β) (Ξ2 Ξ3 : t_ctx) (f1 : Ξ β Ξ2) (f2 : Ξ2 β Ξ3), (K0 i ββα΅£ f1) ββα΅£ f2 = K0 i ββα΅£ (f1 α΅£β f2)forall (Ξ : t_ctx) (t : term Ξ), (forall (Ξ2 Ξ3 : t_ctx) (f1 : Ξ β Ξ2) (f2 : Ξ2 β Ξ3), (t ββα΅£ f1) ββα΅£ f2 = t ββα΅£ (f1 α΅£β f2)) -> forall Ο : ev_ctx Ξ, (forall (Ξ2 Ξ3 : t_ctx) (f1 : Ξ β Ξ2) (f2 : Ξ2 β Ξ3), (Ο ββα΅£ f1) ββα΅£ f2 = Ο ββα΅£ (f1 α΅£β f2)) -> forall (Ξ2 Ξ3 : t_ctx) (f1 : Ξ β Ξ2) (f2 : Ξ2 β Ξ3), (K1 t Ο ββα΅£ f1) ββα΅£ f2 = K1 t Ο ββα΅£ (f1 α΅£β f2)forall (Ξ : t_ctx) (v : val Ξ), (forall (Ξ2 Ξ3 : t_ctx) (f1 : Ξ β Ξ2) (f2 : Ξ2 β Ξ3), (v α΅₯βα΅£ f1) α΅₯βα΅£ f2 = v α΅₯βα΅£ (f1 α΅£β f2)) -> forall Ο : ev_ctx Ξ, (forall (Ξ2 Ξ3 : t_ctx) (f1 : Ξ β Ξ2) (f2 : Ξ2 β Ξ3), (Ο ββα΅£ f1) ββα΅£ f2 = Ο ββα΅£ (f1 α΅£β f2)) -> forall (Ξ2 Ξ3 : t_ctx) (f1 : Ξ β Ξ2) (f2 : Ξ2 β Ξ3), (K2 v Ο ββα΅£ f1) ββα΅£ f2 = K2 v Ο ββα΅£ (f1 α΅£β f2)Ξ: t_ctx
t: term (Ξ βΆβ β)
H: forall (Ξ2 Ξ3 : t_ctx) (f1 : (Ξ βΆβ β) β Ξ2) (f2 : Ξ2 β Ξ3), (t ββα΅£ f1) ββα΅£ f2 = t ββα΅£ (f1 α΅£β f2)
Ξ2, Ξ3: t_ctx
f1: Ξ β Ξ2
f2: Ξ2 β Ξ3(t ββα΅£ r_shift1 f1) ββα΅£ r_shift1 f2 = t ββα΅£ r_shift1 (f1 α΅£β f2)intros ? h; dependent elimination h; auto. Qed.Ξ: t_ctx
t: term (Ξ βΆβ β)
H: forall (Ξ2 Ξ3 : t_ctx) (f1 : (Ξ βΆβ β) β Ξ2) (f2 : Ξ2 β Ξ3), (t ββα΅£ f1) ββα΅£ f2 = t ββα΅£ (f1 α΅£β f2)
Ξ2, Ξ3: t_ctx
f1: Ξ β Ξ2
f2: Ξ2 β Ξ3r_shift1 f1 α΅£β r_shift1 f2 β‘β r_shift1 (f1 α΅£β f2)now apply (term_ind_mut _ _ _ ren_ren_prf). Qed.Ξ1, Ξ2, Ξ3: ctx ty
f1: Ξ1 β Ξ2
f2: Ξ2 β Ξ3
t: term Ξ1(t ββα΅£ f1) ββα΅£ f2 = t ββα΅£ (f1 α΅£β f2)now apply (val_ind_mut _ _ _ ren_ren_prf). Qed.Ξ1, Ξ2, Ξ3: ctx ty
f1: Ξ1 β Ξ2
f2: Ξ2 β Ξ3
v: val Ξ1(v α΅₯βα΅£ f1) α΅₯βα΅£ f2 = v α΅₯βα΅£ (f1 α΅£β f2)now apply (ctx_ind_mut _ _ _ ren_ren_prf). Qed.Ξ1, Ξ2, Ξ3: ctx ty
f1: Ξ1 β Ξ2
f2: Ξ2 β Ξ3
Ο: ev_ctx Ξ1(Ο ββα΅£ f1) ββα΅£ f2 = Ο ββα΅£ (f1 α΅£β f2)destruct a; [ now apply v_ren_ren | now apply e_ren_ren ]. Qed.Ξ1, Ξ2, Ξ3: ctx ty
f1: Ξ1 β Ξ2
f2: Ξ2 β Ξ3
a: ty
v: val_m Ξ1 a(v ββα΅£ f1) ββα΅£ f2 = v ββα΅£ (f1 α΅£β f2)destruct s; apply (f_equal2 Cut); [ now apply t_ren_ren | now apply e_ren_ren ]. Qed.Ξ1, Ξ2, Ξ3: ctx ty
f1: Ξ1 β Ξ2
f2: Ξ2 β Ξ3
s: state Ξ1(s ββα΅£ f1) ββα΅£ f2 = s ββα΅£ (f1 α΅£β f2)
Left identity law of renaming.
Definition t_ren_id_l_P Ξ (t : term Ξ) : Prop := t ββα΅£ r_id = t . Definition v_ren_id_l_P Ξ (v : val Ξ) : Prop := v α΅₯βα΅£ r_id = v . Definition e_ren_id_l_P Ξ (Ο : ev_ctx Ξ) : Prop := Ο ββα΅£ r_id = Ο .syn_ind_args t_ren_id_l_P v_ren_id_l_P e_ren_id_l_Pforall (Ξ : t_ctx) (v : val Ξ), v_ren_id_l_P Ξ v -> t_ren_id_l_P Ξ (Val v)forall (Ξ : t_ctx) (t1 : term Ξ), t_ren_id_l_P Ξ t1 -> forall t2 : term Ξ, t_ren_id_l_P Ξ t2 -> t_ren_id_l_P Ξ (App t1 t2)forall (Ξ : t_ctx) (i : Ξ β β), v_ren_id_l_P Ξ (Var i)forall (Ξ : t_ctx) (t : term (Ξ βΆβ β)), t_ren_id_l_P (Ξ βΆβ β) t -> v_ren_id_l_P Ξ (Lam t)forall (Ξ : t_ctx) (i : Ξ β β), e_ren_id_l_P Ξ (K0 i)forall (Ξ : t_ctx) (t : term Ξ), t_ren_id_l_P Ξ t -> forall Ο : ev_ctx Ξ, e_ren_id_l_P Ξ Ο -> e_ren_id_l_P Ξ (K1 t Ο)forall (Ξ : t_ctx) (v : val Ξ), v_ren_id_l_P Ξ v -> forall Ο : ev_ctx Ξ, e_ren_id_l_P Ξ Ο -> e_ren_id_l_P Ξ (K2 v Ο)forall (Ξ : t_ctx) (v : val Ξ), v α΅₯βα΅£ r_id = v -> Val v ββα΅£ r_id = Val vforall (Ξ : t_ctx) (t1 : term Ξ), t1 ββα΅£ r_id = t1 -> forall t2 : term Ξ, t2 ββα΅£ r_id = t2 -> App t1 t2 ββα΅£ r_id = App t1 t2forall (Ξ : t_ctx) (i : Ξ β β), Var i α΅₯βα΅£ r_id = Var iforall (Ξ : t_ctx) (t : term (Ξ βΆβ β)), t ββα΅£ r_id = t -> Lam t α΅₯βα΅£ r_id = Lam tforall (Ξ : t_ctx) (i : Ξ β β), K0 i ββα΅£ r_id = K0 iforall (Ξ : t_ctx) (t : term Ξ), t ββα΅£ r_id = t -> forall Ο : ev_ctx Ξ, Ο ββα΅£ r_id = Ο -> K1 t Ο ββα΅£ r_id = K1 t Οforall (Ξ : t_ctx) (v : val Ξ), v α΅₯βα΅£ r_id = v -> forall Ο : ev_ctx Ξ, Ο ββα΅£ r_id = Ο -> K2 v Ο ββα΅£ r_id = K2 v ΟΞ: t_ctx
t: term (Ξ βΆβ β)
H: t ββα΅£ r_id = tt ββα΅£ r_shift1 r_id = tintros ? h; dependent elimination h; auto. Qed.Ξ: t_ctx
t: term (Ξ βΆβ β)
H: t ββα΅£ r_id = tr_shift1 r_id β‘β r_idnow apply (term_ind_mut _ _ _ ren_id_l_prf). Qed.Ξ: t_ctx
t: term Ξt ββα΅£ r_id = tnow apply (val_ind_mut _ _ _ ren_id_l_prf). Qed.Ξ: t_ctx
v: val Ξv α΅₯βα΅£ r_id = vnow apply (ctx_ind_mut _ _ _ ren_id_l_prf). Qed.Ξ: t_ctx
Ο: ev_ctx ΞΟ ββα΅£ r_id = Οdestruct a; [ now apply v_ren_id_l | now apply e_ren_id_l ]. Qed.Ξ: t_ctx
a: ty
v: val_m Ξ av ββα΅£ r_id = vdestruct s; apply (f_equal2 Cut); [ now apply t_ren_id_l | now apply e_ren_id_l ]. Qed.Ξ: t_ctx
s: state Ξs ββα΅£ r_id = snow destruct a. Qed.Ξ, Ξ: ctx ty
f: Ξ β Ξ
a: ty
i: Ξ β aa_id a i ββα΅£ f = a_id a (f a i)intros ??; now apply m_ren_id_r. Qed.Ξ, Ξ: ctx ty
f: Ξ β Ξa_id βα΅£ f β‘β f α΅£β a_idΞ: t_ctx
x: tya_shift1 a_id β‘β a_idexact (m_ren_id_r _ _). Qed.Ξ1: ctx ty
y, a: ty
v: var a Ξ1a_shift1 a_id a (pop v) = a_id a (pop v)
Lemma 5: shifting assigments commutes with left and right renaming.
intros ? v; dependent elimination v; auto. Qed.Ξ1, Ξ2: ctx ty
Ξ3: t_ctx
a: ty
f1: Ξ1 β Ξ2
f2: Ξ2 =[ val_m ]> Ξ3a_shift1 (f1 α΅£β f2) β‘β r_shift1 f1 α΅£β a_shift1 f2Ξ1, Ξ2, Ξ3: t_ctx
a: ty
f1: Ξ1 =[ val_m ]> Ξ2
f2: Ξ2 β Ξ3a_shift1 (f1 βα΅£ f2) β‘β a_shift1 f1 βα΅£ r_shift1 f2Ξ1, Ξ2, Ξ3: t_ctx
a: ty
f1: Ξ1 =[ val_m ]> Ξ2
f2: Ξ2 β Ξ3
a0: ty
v: Ξ1 βΆβ a β a0a_shift1 (f1 βα΅£ f2) a0 v = (a_shift1 f1 βα΅£ r_shift1 f2)%asgn a0 vΞ: ctx ty
Ξ2, Ξ3: t_ctx
a0: ty
f1: Ξ =[ val_m ]> Ξ2
f2: Ξ2 β Ξ3a_shift1 (f1 βα΅£ f2) a0 top = (a_shift1 f1 βα΅£ r_shift1 f2)%asgn a0 topΞ0: ctx ty
Ξ2, Ξ3: t_ctx
y: ty
f1: Ξ0 =[ val_m ]> Ξ2
f2: Ξ2 β Ξ3
a0: ty
v: var a0 Ξ0a_shift1 (f1 βα΅£ f2) a0 (pop v) = (a_shift1 f1 βα΅£ r_shift1 f2)%asgn a0 (pop v)cbn; unfold m_shift1, r_shift1; now rewrite 2 m_ren_ren. Qed.Ξ0: ctx ty
Ξ2, Ξ3: t_ctx
y: ty
f1: Ξ0 =[ val_m ]> Ξ2
f2: Ξ2 β Ξ3
a0: ty
v: var a0 Ξ0a_shift1 (f1 βα΅£ f2) a0 (pop v) = (a_shift1 f1 βα΅£ r_shift1 f2)%asgn a0 (pop v)
Lemma 6: substitution respects pointwise equality of assigments.
Definition t_sub_proper_P Ξ (t : term Ξ) : Prop := forall Ξ (f1 f2 : Ξ =[val_m]> Ξ), f1 β‘β f2 -> t `ββ f1 = t `ββ f2 . Definition v_sub_proper_P Ξ (v : val Ξ) : Prop := forall Ξ (f1 f2 : Ξ =[val_m]> Ξ), f1 β‘β f2 -> v `α΅₯β f1 = v `α΅₯β f2 . Definition e_sub_proper_P Ξ (Ο : ev_ctx Ξ) : Prop := forall Ξ (f1 f2 : Ξ =[val_m]> Ξ), f1 β‘β f2 -> Ο `ββ f1 = Ο `ββ f2.syn_ind_args t_sub_proper_P v_sub_proper_P e_sub_proper_Pforall (Ξ : t_ctx) (v : val Ξ), v_sub_proper_P Ξ v -> t_sub_proper_P Ξ (Val v)forall (Ξ : t_ctx) (t1 : term Ξ), t_sub_proper_P Ξ t1 -> forall t2 : term Ξ, t_sub_proper_P Ξ t2 -> t_sub_proper_P Ξ (App t1 t2)forall (Ξ : t_ctx) (i : Ξ β β), v_sub_proper_P Ξ (Var i)forall (Ξ : t_ctx) (t : term (Ξ βΆβ β)), t_sub_proper_P (Ξ βΆβ β) t -> v_sub_proper_P Ξ (Lam t)forall (Ξ : t_ctx) (i : Ξ β β), e_sub_proper_P Ξ (K0 i)forall (Ξ : t_ctx) (t : term Ξ), t_sub_proper_P Ξ t -> forall Ο : ev_ctx Ξ, e_sub_proper_P Ξ Ο -> e_sub_proper_P Ξ (K1 t Ο)forall (Ξ : t_ctx) (v : val Ξ), v_sub_proper_P Ξ v -> forall Ο : ev_ctx Ξ, e_sub_proper_P Ξ Ο -> e_sub_proper_P Ξ (K2 v Ο)forall (Ξ : t_ctx) (v : val Ξ), (forall (Ξ : t_ctx) (f1 f2 : Ξ =[ val_m ]> Ξ), f1 β‘β f2 -> v `α΅₯β f1 = v `α΅₯β f2) -> forall (Ξ : t_ctx) (f1 f2 : Ξ =[ val_m ]> Ξ), f1 β‘β f2 -> Val v `ββ f1 = Val v `ββ f2forall (Ξ : t_ctx) (t1 : term Ξ), (forall (Ξ : t_ctx) (f1 f2 : Ξ =[ val_m ]> Ξ), f1 β‘β f2 -> t1 `ββ f1 = t1 `ββ f2) -> forall t2 : term Ξ, (forall (Ξ : t_ctx) (f1 f2 : Ξ =[ val_m ]> Ξ), f1 β‘β f2 -> t2 `ββ f1 = t2 `ββ f2) -> forall (Ξ : t_ctx) (f1 f2 : Ξ =[ val_m ]> Ξ), f1 β‘β f2 -> App t1 t2 `ββ f1 = App t1 t2 `ββ f2forall (Ξ : t_ctx) (i : Ξ β β) (Ξ : t_ctx) (f1 f2 : Ξ =[ val_m ]> Ξ), f1 β‘β f2 -> Var i `α΅₯β f1 = Var i `α΅₯β f2forall (Ξ : t_ctx) (t : term (Ξ βΆβ β)), (forall (Ξ : t_ctx) (f1 f2 : (Ξ βΆβ β) =[ val_m ]> Ξ), f1 β‘β f2 -> t `ββ f1 = t `ββ f2) -> forall (Ξ : t_ctx) (f1 f2 : Ξ =[ val_m ]> Ξ), f1 β‘β f2 -> Lam t `α΅₯β f1 = Lam t `α΅₯β f2forall (Ξ : t_ctx) (i : Ξ β β) (Ξ : t_ctx) (f1 f2 : Ξ =[ val_m ]> Ξ), f1 β‘β f2 -> K0 i `ββ f1 = K0 i `ββ f2forall (Ξ : t_ctx) (t : term Ξ), (forall (Ξ : t_ctx) (f1 f2 : Ξ =[ val_m ]> Ξ), f1 β‘β f2 -> t `ββ f1 = t `ββ f2) -> forall Ο : ev_ctx Ξ, (forall (Ξ : t_ctx) (f1 f2 : Ξ =[ val_m ]> Ξ), f1 β‘β f2 -> Ο `ββ f1 = Ο `ββ f2) -> forall (Ξ : t_ctx) (f1 f2 : Ξ =[ val_m ]> Ξ), f1 β‘β f2 -> K1 t Ο `ββ f1 = K1 t Ο `ββ f2forall (Ξ : t_ctx) (v : val Ξ), (forall (Ξ : t_ctx) (f1 f2 : Ξ =[ val_m ]> Ξ), f1 β‘β f2 -> v `α΅₯β f1 = v `α΅₯β f2) -> forall Ο : ev_ctx Ξ, (forall (Ξ : t_ctx) (f1 f2 : Ξ =[ val_m ]> Ξ), f1 β‘β f2 -> Ο `ββ f1 = Ο `ββ f2) -> forall (Ξ : t_ctx) (f1 f2 : Ξ =[ val_m ]> Ξ), f1 β‘β f2 -> K2 v Ο `ββ f1 = K2 v Ο `ββ f2now apply H, a_shift_eq. Qed.Ξ: t_ctx
t: term (Ξ βΆβ β)
H: forall (Ξ : t_ctx) (f1 f2 : (Ξ βΆβ β) =[ val_m ]> Ξ), f1 β‘β f2 -> t `ββ f1 = t `ββ f2
Ξ: t_ctx
f1, f2: Ξ =[ val_m ]> Ξ
H0: f1 β‘β f2t `ββ a_shift1 f1 = t `ββ a_shift1 f2intros ? ? H1 _ ? ->; now apply (term_ind_mut _ _ _ sub_proper_prf). Qed.Ξ, Ξ: t_ctxProper (asgn_eq Ξ Ξ ==> eq ==> eq) t_substintros ? ? H1 _ ? ->; now apply (val_ind_mut _ _ _ sub_proper_prf). Qed.Ξ, Ξ: t_ctxProper (asgn_eq Ξ Ξ ==> eq ==> eq) v_substintros ? ? H1 _ ? ->; now apply (ctx_ind_mut _ _ _ sub_proper_prf). Qed.Ξ, Ξ: t_ctxProper (asgn_eq Ξ Ξ ==> eq ==> eq) e_substintros ? [] ?? -> ??? H1; cbn in *; now rewrite H1. Qed.Proper (ββ Ξ, (ββ a, eq ==> (ββ Ξ, asgn_eq Ξ Ξ ==> eq))) m_substintros ??[] -> ??? H1; cbn; now rewrite H1. Qed. (* #[global] Instance a_comp_eq {Ξ1 Ξ2 Ξ3} : Proper (ass_eq _ _ ==> ass_eq _ _ ==> ass_eq _ _) (@a_comp Ξ1 Ξ2 Ξ3). intros ? ? H1 ? ? H2 ? ?; unfold a_comp, s_map; now rewrite H1, H2. Qed. *)Proper (ββ Ξ, eq ==> (ββ Ξ, asgn_eq Ξ Ξ ==> eq)) s_subst
Lemma 7: renaming-substitution "associativity".
Definition t_ren_sub_P Ξ1 (t : term Ξ1) : Prop := forall Ξ2 Ξ3 (f1 : Ξ1 =[val_m]> Ξ2) (f2 : Ξ2 β Ξ3) , (t `ββ f1) ββα΅£ f2 = t `ββ (f1 βα΅£ f2) . Definition v_ren_sub_P Ξ1 (v : val Ξ1) : Prop := forall Ξ2 Ξ3 (f1 : Ξ1 =[val_m]> Ξ2) (f2 : Ξ2 β Ξ3) , (v `α΅₯β f1) α΅₯βα΅£ f2 = v `α΅₯β (f1 βα΅£ f2) . Definition e_ren_sub_P Ξ1 (Ο : ev_ctx Ξ1) : Prop := forall Ξ2 Ξ3 (f1 : Ξ1 =[val_m]> Ξ2) (f2 : Ξ2 β Ξ3) , (Ο `ββ f1) ββα΅£ f2 = Ο `ββ (f1 βα΅£ f2) .syn_ind_args t_ren_sub_P v_ren_sub_P e_ren_sub_Pforall (Ξ : t_ctx) (v : val Ξ), v_ren_sub_P Ξ v -> t_ren_sub_P Ξ (Val v)forall (Ξ : t_ctx) (t1 : term Ξ), t_ren_sub_P Ξ t1 -> forall t2 : term Ξ, t_ren_sub_P Ξ t2 -> t_ren_sub_P Ξ (App t1 t2)forall (Ξ : t_ctx) (i : Ξ β β), v_ren_sub_P Ξ (Var i)forall (Ξ : t_ctx) (t : term (Ξ βΆβ β)), t_ren_sub_P (Ξ βΆβ β) t -> v_ren_sub_P Ξ (Lam t)forall (Ξ : t_ctx) (i : Ξ β β), e_ren_sub_P Ξ (K0 i)forall (Ξ : t_ctx) (t : term Ξ), t_ren_sub_P Ξ t -> forall Ο : ev_ctx Ξ, e_ren_sub_P Ξ Ο -> e_ren_sub_P Ξ (K1 t Ο)forall (Ξ : t_ctx) (v : val Ξ), v_ren_sub_P Ξ v -> forall Ο : ev_ctx Ξ, e_ren_sub_P Ξ Ο -> e_ren_sub_P Ξ (K2 v Ο)forall (Ξ : t_ctx) (v : val Ξ), (forall (Ξ2 Ξ3 : t_ctx) (f1 : Ξ =[ val_m ]> Ξ2) (f2 : Ξ2 β Ξ3), (v `α΅₯β f1) α΅₯βα΅£ f2 = v `α΅₯β f1 βα΅£ f2) -> forall (Ξ2 Ξ3 : t_ctx) (f1 : Ξ =[ val_m ]> Ξ2) (f2 : Ξ2 β Ξ3), (Val v `ββ f1) ββα΅£ f2 = Val v `ββ f1 βα΅£ f2forall (Ξ : t_ctx) (t1 : term Ξ), (forall (Ξ2 Ξ3 : t_ctx) (f1 : Ξ =[ val_m ]> Ξ2) (f2 : Ξ2 β Ξ3), (t1 `ββ f1) ββα΅£ f2 = t1 `ββ f1 βα΅£ f2) -> forall t2 : term Ξ, (forall (Ξ2 Ξ3 : t_ctx) (f1 : Ξ =[ val_m ]> Ξ2) (f2 : Ξ2 β Ξ3), (t2 `ββ f1) ββα΅£ f2 = t2 `ββ f1 βα΅£ f2) -> forall (Ξ2 Ξ3 : t_ctx) (f1 : Ξ =[ val_m ]> Ξ2) (f2 : Ξ2 β Ξ3), (App t1 t2 `ββ f1) ββα΅£ f2 = App t1 t2 `ββ f1 βα΅£ f2forall (Ξ : t_ctx) (i : Ξ β β) (Ξ2 Ξ3 : t_ctx) (f1 : Ξ =[ val_m ]> Ξ2) (f2 : Ξ2 β Ξ3), (Var i `α΅₯β f1) α΅₯βα΅£ f2 = Var i `α΅₯β f1 βα΅£ f2forall (Ξ : t_ctx) (t : term (Ξ βΆβ β)), (forall (Ξ2 Ξ3 : t_ctx) (f1 : (Ξ βΆβ β) =[ val_m ]> Ξ2) (f2 : Ξ2 β Ξ3), (t `ββ f1) ββα΅£ f2 = t `ββ f1 βα΅£ f2) -> forall (Ξ2 Ξ3 : t_ctx) (f1 : Ξ =[ val_m ]> Ξ2) (f2 : Ξ2 β Ξ3), (Lam t `α΅₯β f1) α΅₯βα΅£ f2 = Lam t `α΅₯β f1 βα΅£ f2forall (Ξ : t_ctx) (i : Ξ β β) (Ξ2 Ξ3 : t_ctx) (f1 : Ξ =[ val_m ]> Ξ2) (f2 : Ξ2 β Ξ3), (K0 i `ββ f1) ββα΅£ f2 = K0 i `ββ f1 βα΅£ f2forall (Ξ : t_ctx) (t : term Ξ), (forall (Ξ2 Ξ3 : t_ctx) (f1 : Ξ =[ val_m ]> Ξ2) (f2 : Ξ2 β Ξ3), (t `ββ f1) ββα΅£ f2 = t `ββ f1 βα΅£ f2) -> forall Ο : ev_ctx Ξ, (forall (Ξ2 Ξ3 : t_ctx) (f1 : Ξ =[ val_m ]> Ξ2) (f2 : Ξ2 β Ξ3), (Ο `ββ f1) ββα΅£ f2 = Ο `ββ f1 βα΅£ f2) -> forall (Ξ2 Ξ3 : t_ctx) (f1 : Ξ =[ val_m ]> Ξ2) (f2 : Ξ2 β Ξ3), (K1 t Ο `ββ f1) ββα΅£ f2 = K1 t Ο `ββ f1 βα΅£ f2forall (Ξ : t_ctx) (v : val Ξ), (forall (Ξ2 Ξ3 : t_ctx) (f1 : Ξ =[ val_m ]> Ξ2) (f2 : Ξ2 β Ξ3), (v `α΅₯β f1) α΅₯βα΅£ f2 = v `α΅₯β f1 βα΅£ f2) -> forall Ο : ev_ctx Ξ, (forall (Ξ2 Ξ3 : t_ctx) (f1 : Ξ =[ val_m ]> Ξ2) (f2 : Ξ2 β Ξ3), (Ο `ββ f1) ββα΅£ f2 = Ο `ββ f1 βα΅£ f2) -> forall (Ξ2 Ξ3 : t_ctx) (f1 : Ξ =[ val_m ]> Ξ2) (f2 : Ξ2 β Ξ3), (K2 v Ο `ββ f1) ββα΅£ f2 = K2 v Ο `ββ f1 βα΅£ f2change (a_shift1 (fun x => _)) with (a_shift1 (a:=β) (f1 βα΅£ f2)); now rewrite a_shift1_a_ren. Qed.Ξ: t_ctx
t: term (Ξ βΆβ β)
H: forall (Ξ2 Ξ3 : t_ctx) (f1 : (Ξ βΆβ β) =[ val_m ]> Ξ2) (f2 : Ξ2 β Ξ3), (t `ββ f1) ββα΅£ f2 = t `ββ f1 βα΅£ f2
Ξ2, Ξ3: t_ctx
f1: Ξ =[ val_m ]> Ξ2
f2: Ξ2 β Ξ3(t `ββ a_shift1 f1) ββα΅£ r_shift1 f2 = t `ββ a_shift1 (fun x : ty => m_rename f2 x β f1 x)now apply (term_ind_mut _ _ _ ren_sub_prf). Qed.Ξ1, Ξ2, Ξ3: t_ctx
f1: Ξ1 =[ val_m ]> Ξ2
f2: Ξ2 β Ξ3
t: term Ξ1(t `ββ f1) ββα΅£ f2 = t `ββ f1 βα΅£ f2now apply (val_ind_mut _ _ _ ren_sub_prf). Qed.Ξ1, Ξ2, Ξ3: t_ctx
f1: Ξ1 =[ val_m ]> Ξ2
f2: Ξ2 β Ξ3
v: val Ξ1(v `α΅₯β f1) α΅₯βα΅£ f2 = v `α΅₯β f1 βα΅£ f2now apply (ctx_ind_mut _ _ _ ren_sub_prf). Qed.Ξ1, Ξ2, Ξ3: t_ctx
f1: Ξ1 =[ val_m ]> Ξ2
f2: Ξ2 β Ξ3
Ο: ev_ctx Ξ1(Ο `ββ f1) ββα΅£ f2 = Ο `ββ f1 βα΅£ f2destruct a; [ now apply v_ren_sub | now apply e_ren_sub ]. Qed.Ξ1, Ξ2, Ξ3: t_ctx
f1: Ξ1 =[ val_m ]> Ξ2
f2: Ξ2 β Ξ3
a: ty
v: val_m Ξ1 a(v α΅₯β f1) ββα΅£ f2 = v α΅₯β f1 βα΅£ f2destruct s; cbn; now rewrite t_ren_sub, e_ren_sub. Qed.Ξ1, Ξ2, Ξ3: t_ctx
f1: Ξ1 =[ val_m ]> Ξ2
f2: Ξ2 β Ξ3
s: state Ξ1(s ββ f1) ββα΅£ f2 = s ββ f1 βα΅£ f2
Lemma 8: substitution-renaming "associativity".
Definition t_sub_ren_P Ξ1 (t : term Ξ1) : Prop := forall Ξ2 Ξ3 (f1 : Ξ1 β Ξ2) (f2 : Ξ2 =[val_m]> Ξ3) , (t ββα΅£ f1) `ββ f2 = t `ββ (f1 α΅£β f2) . Definition v_sub_ren_P Ξ1 (v : val Ξ1) : Prop := forall Ξ2 Ξ3 (f1 : Ξ1 β Ξ2) (f2 : Ξ2 =[val_m]> Ξ3) , (v α΅₯βα΅£ f1) `α΅₯β f2 = v `α΅₯β (f1 α΅£β f2) . Definition e_sub_ren_P Ξ1 (Ο : ev_ctx Ξ1) : Prop := forall Ξ2 Ξ3 (f1 : Ξ1 β Ξ2) (f2 : Ξ2 =[val_m]> Ξ3) , (Ο ββα΅£ f1) `ββ f2 = Ο `ββ (f1 α΅£β f2) .syn_ind_args t_sub_ren_P v_sub_ren_P e_sub_ren_Pforall (Ξ : t_ctx) (v : val Ξ), v_sub_ren_P Ξ v -> t_sub_ren_P Ξ (Val v)forall (Ξ : t_ctx) (t1 : term Ξ), t_sub_ren_P Ξ t1 -> forall t2 : term Ξ, t_sub_ren_P Ξ t2 -> t_sub_ren_P Ξ (App t1 t2)forall (Ξ : t_ctx) (i : Ξ β β), v_sub_ren_P Ξ (Var i)forall (Ξ : t_ctx) (t : term (Ξ βΆβ β)), t_sub_ren_P (Ξ βΆβ β) t -> v_sub_ren_P Ξ (Lam t)forall (Ξ : t_ctx) (i : Ξ β β), e_sub_ren_P Ξ (K0 i)forall (Ξ : t_ctx) (t : term Ξ), t_sub_ren_P Ξ t -> forall Ο : ev_ctx Ξ, e_sub_ren_P Ξ Ο -> e_sub_ren_P Ξ (K1 t Ο)forall (Ξ : t_ctx) (v : val Ξ), v_sub_ren_P Ξ v -> forall Ο : ev_ctx Ξ, e_sub_ren_P Ξ Ο -> e_sub_ren_P Ξ (K2 v Ο)forall (Ξ : t_ctx) (v : val Ξ), (forall (Ξ2 Ξ3 : t_ctx) (f1 : Ξ β Ξ2) (f2 : Ξ2 =[ val_m ]> Ξ3), v α΅₯βα΅£ f1 `α΅₯β f2 = v `α΅₯β f1 α΅£β f2) -> forall (Ξ2 Ξ3 : t_ctx) (f1 : Ξ β Ξ2) (f2 : Ξ2 =[ val_m ]> Ξ3), Val v ββα΅£ f1 `ββ f2 = Val v `ββ f1 α΅£β f2forall (Ξ : t_ctx) (t1 : term Ξ), (forall (Ξ2 Ξ3 : t_ctx) (f1 : Ξ β Ξ2) (f2 : Ξ2 =[ val_m ]> Ξ3), t1 ββα΅£ f1 `ββ f2 = t1 `ββ f1 α΅£β f2) -> forall t2 : term Ξ, (forall (Ξ2 Ξ3 : t_ctx) (f1 : Ξ β Ξ2) (f2 : Ξ2 =[ val_m ]> Ξ3), t2 ββα΅£ f1 `ββ f2 = t2 `ββ f1 α΅£β f2) -> forall (Ξ2 Ξ3 : t_ctx) (f1 : Ξ β Ξ2) (f2 : Ξ2 =[ val_m ]> Ξ3), App t1 t2 ββα΅£ f1 `ββ f2 = App t1 t2 `ββ f1 α΅£β f2forall (Ξ : t_ctx) (i : Ξ β β) (Ξ2 Ξ3 : t_ctx) (f1 : Ξ β Ξ2) (f2 : Ξ2 =[ val_m ]> Ξ3), Var i α΅₯βα΅£ f1 `α΅₯β f2 = Var i `α΅₯β f1 α΅£β f2forall (Ξ : t_ctx) (t : term (Ξ βΆβ β)), (forall (Ξ2 Ξ3 : t_ctx) (f1 : (Ξ βΆβ β) β Ξ2) (f2 : Ξ2 =[ val_m ]> Ξ3), t ββα΅£ f1 `ββ f2 = t `ββ f1 α΅£β f2) -> forall (Ξ2 Ξ3 : t_ctx) (f1 : Ξ β Ξ2) (f2 : Ξ2 =[ val_m ]> Ξ3), Lam t α΅₯βα΅£ f1 `α΅₯β f2 = Lam t `α΅₯β f1 α΅£β f2forall (Ξ : t_ctx) (i : Ξ β β) (Ξ2 Ξ3 : t_ctx) (f1 : Ξ β Ξ2) (f2 : Ξ2 =[ val_m ]> Ξ3), K0 i ββα΅£ f1 `ββ f2 = K0 i `ββ f1 α΅£β f2forall (Ξ : t_ctx) (t : term Ξ), (forall (Ξ2 Ξ3 : t_ctx) (f1 : Ξ β Ξ2) (f2 : Ξ2 =[ val_m ]> Ξ3), t ββα΅£ f1 `ββ f2 = t `ββ f1 α΅£β f2) -> forall Ο : ev_ctx Ξ, (forall (Ξ2 Ξ3 : t_ctx) (f1 : Ξ β Ξ2) (f2 : Ξ2 =[ val_m ]> Ξ3), Ο ββα΅£ f1 `ββ f2 = Ο `ββ f1 α΅£β f2) -> forall (Ξ2 Ξ3 : t_ctx) (f1 : Ξ β Ξ2) (f2 : Ξ2 =[ val_m ]> Ξ3), K1 t Ο ββα΅£ f1 `ββ f2 = K1 t Ο `ββ f1 α΅£β f2forall (Ξ : t_ctx) (v : val Ξ), (forall (Ξ2 Ξ3 : t_ctx) (f1 : Ξ β Ξ2) (f2 : Ξ2 =[ val_m ]> Ξ3), v α΅₯βα΅£ f1 `α΅₯β f2 = v `α΅₯β f1 α΅£β f2) -> forall Ο : ev_ctx Ξ, (forall (Ξ2 Ξ3 : t_ctx) (f1 : Ξ β Ξ2) (f2 : Ξ2 =[ val_m ]> Ξ3), Ο ββα΅£ f1 `ββ f2 = Ο `ββ f1 α΅£β f2) -> forall (Ξ2 Ξ3 : t_ctx) (f1 : Ξ β Ξ2) (f2 : Ξ2 =[ val_m ]> Ξ3), K2 v Ο ββα΅£ f1 `ββ f2 = K2 v Ο `ββ f1 α΅£β f2now rewrite a_shift1_s_ren. Qed.Ξ: t_ctx
t: term (Ξ βΆβ β)
H: forall (Ξ2 Ξ3 : t_ctx) (f1 : (Ξ βΆβ β) β Ξ2) (f2 : Ξ2 =[ val_m ]> Ξ3), t ββα΅£ f1 `ββ f2 = t `ββ f1 α΅£β f2
Ξ2, Ξ3: t_ctx
f1: Ξ β Ξ2
f2: Ξ2 =[ val_m ]> Ξ3t ββα΅£ r_shift1 f1 `ββ a_shift1 f2 = t `ββ a_shift1 (f1 α΅£β f2)now apply (term_ind_mut _ _ _ sub_ren_prf). Qed.Ξ1, Ξ2: ctx ty
Ξ3: t_ctx
f1: Ξ1 β Ξ2
f2: Ξ2 =[ val_m ]> Ξ3
t: term Ξ1t ββα΅£ f1 `ββ f2 = t `ββ f1 α΅£β f2now apply (val_ind_mut _ _ _ sub_ren_prf). Qed.Ξ1, Ξ2: ctx ty
Ξ3: t_ctx
f1: Ξ1 β Ξ2
f2: Ξ2 =[ val_m ]> Ξ3
v: val Ξ1v α΅₯βα΅£ f1 `α΅₯β f2 = v `α΅₯β f1 α΅£β f2now apply (ctx_ind_mut _ _ _ sub_ren_prf). Qed.Ξ1, Ξ2: ctx ty
Ξ3: t_ctx
f1: Ξ1 β Ξ2
f2: Ξ2 =[ val_m ]> Ξ3
Ο: ev_ctx Ξ1Ο ββα΅£ f1 `ββ f2 = Ο `ββ f1 α΅£β f2destruct a; [ now apply v_sub_ren | now apply e_sub_ren ]. Qed.Ξ1, Ξ2: ctx ty
Ξ3: t_ctx
f1: Ξ1 β Ξ2
f2: Ξ2 =[ val_m ]> Ξ3
a: ty
v: val_m Ξ1 av ββα΅£ f1 α΅₯β f2 = v α΅₯β f1 α΅£β f2destruct s; cbn; now rewrite t_sub_ren, e_sub_ren. Qed.Ξ1, Ξ2: ctx ty
Ξ3: t_ctx
f1: Ξ1 β Ξ2
f2: Ξ2 =[ val_m ]> Ξ3
s: state Ξ1s ββα΅£ f1 ββ f2 = s ββ f1 α΅£β f2
Lemma 9: left identity law of substitution.
Definition t_sub_id_l_P Ξ (t : term Ξ) : Prop := t `ββ a_id = t . Definition v_sub_id_l_P Ξ (v : val Ξ) : Prop := v `α΅₯β a_id = v . Definition e_sub_id_l_P Ξ (Ο : ev_ctx Ξ) : Prop := Ο `ββ a_id = Ο .syn_ind_args t_sub_id_l_P v_sub_id_l_P e_sub_id_l_Pforall (Ξ : t_ctx) (v : val Ξ), v_sub_id_l_P Ξ v -> t_sub_id_l_P Ξ (Val v)forall (Ξ : t_ctx) (t1 : term Ξ), t_sub_id_l_P Ξ t1 -> forall t2 : term Ξ, t_sub_id_l_P Ξ t2 -> t_sub_id_l_P Ξ (App t1 t2)forall (Ξ : t_ctx) (i : Ξ β β), v_sub_id_l_P Ξ (Var i)forall (Ξ : t_ctx) (t : term (Ξ βΆβ β)), t_sub_id_l_P (Ξ βΆβ β) t -> v_sub_id_l_P Ξ (Lam t)forall (Ξ : t_ctx) (i : Ξ β β), e_sub_id_l_P Ξ (K0 i)forall (Ξ : t_ctx) (t : term Ξ), t_sub_id_l_P Ξ t -> forall Ο : ev_ctx Ξ, e_sub_id_l_P Ξ Ο -> e_sub_id_l_P Ξ (K1 t Ο)forall (Ξ : t_ctx) (v : val Ξ), v_sub_id_l_P Ξ v -> forall Ο : ev_ctx Ξ, e_sub_id_l_P Ξ Ο -> e_sub_id_l_P Ξ (K2 v Ο)forall (Ξ : t_ctx) (v : val Ξ), v `α΅₯β a_id = v -> Val v `ββ a_id = Val vforall (Ξ : t_ctx) (t1 : term Ξ), t1 `ββ a_id = t1 -> forall t2 : term Ξ, t2 `ββ a_id = t2 -> App t1 t2 `ββ a_id = App t1 t2forall (Ξ : t_ctx) (i : Ξ β β), Var i `α΅₯β a_id = Var iforall (Ξ : t_ctx) (t : term (Ξ βΆβ β)), t `ββ a_id = t -> Lam t `α΅₯β a_id = Lam tforall (Ξ : t_ctx) (i : Ξ β β), K0 i `ββ a_id = K0 iforall (Ξ : t_ctx) (t : term Ξ), t `ββ a_id = t -> forall Ο : ev_ctx Ξ, Ο `ββ a_id = Ο -> K1 t Ο `ββ a_id = K1 t Οforall (Ξ : t_ctx) (v : val Ξ), v `α΅₯β a_id = v -> forall Ο : ev_ctx Ξ, Ο `ββ a_id = Ο -> K2 v Ο `ββ a_id = K2 v Οnow rewrite a_shift_id. Qed.Ξ: t_ctx
t: term (Ξ βΆβ β)
H: t `ββ a_id = tt `ββ a_shift1 a_id = tnow apply (term_ind_mut _ _ _ sub_id_l_prf). Qed.Ξ: t_ctx
t: term Ξt `ββ a_id = tnow apply (val_ind_mut _ _ _ sub_id_l_prf). Qed.Ξ: t_ctx
v: val Ξv `α΅₯β a_id = vnow apply (ctx_ind_mut _ _ _ sub_id_l_prf). Qed.Ξ: t_ctx
Ο: ev_ctx ΞΟ `ββ a_id = Οdestruct a; [ now apply v_sub_id_l | now apply e_sub_id_l ]. Qed.Ξ: t_ctx
a: ty
v: val_m Ξ av α΅₯β a_id = vdestruct s; cbn; now rewrite t_sub_id_l, e_sub_id_l. Qed.Ξ: t_ctx
s: state Ξs ββ a_id = s
Lemma 9: right identity law of substitution. As for renaming, this one is mostly by definition.
now destruct a. Qed.Ξ1: ctx ty
Ξ2: t_ctx
a: ty
i: Ξ1 β a
f: Ξ1 =[ val_m ]> Ξ2a_id a i α΅₯β f = f a i
Lemma 10: shifting assigments respects composition.
Ξ1, Ξ2, Ξ3: t_ctx
a: ty
f1: Ξ1 =[ val_m ]> Ξ2
f2: Ξ2 =[ val_m ]> Ξ3a_shift1 (f1 β f2) β‘β a_shift1 f1 β a_shift1 f2Ξ: ctx ty
Ξ2, Ξ3: t_ctx
a0: ty
f1: Ξ =[ val_m ]> Ξ2
f2: Ξ2 =[ val_m ]> Ξ3a_id a0 top = m_subst (Ξ2 βΆβ a0) a0 (a_id a0 top) (Ξ3 βΆβ a0) (a_shift1 f2)Ξ0: ctx ty
Ξ2, Ξ3: t_ctx
y: ty
f1: Ξ0 =[ val_m ]> Ξ2
f2: Ξ2 =[ val_m ]> Ξ3
a0: ty
v: var a0 Ξ0m_shift1 a0 (m_subst Ξ2 a0 (f1 a0 v) Ξ3 f2) = m_subst (Ξ2 βΆβ y) a0 (m_shift1 a0 (f1 a0 v)) (Ξ3 βΆβ y) (a_shift1 f2)unfold m_shift1; now rewrite m_ren_sub, m_sub_ren. Qed.Ξ0: ctx ty
Ξ2, Ξ3: t_ctx
y: ty
f1: Ξ0 =[ val_m ]> Ξ2
f2: Ξ2 =[ val_m ]> Ξ3
a0: ty
v: var a0 Ξ0m_shift1 a0 (m_subst Ξ2 a0 (f1 a0 v) Ξ3 f2) = m_subst (Ξ2 βΆβ y) a0 (m_shift1 a0 (f1 a0 v)) (Ξ3 βΆβ y) (a_shift1 f2)
Lemma 11: substitution-substitution associativity, ie composition law.
Definition t_sub_sub_P Ξ1 (t : term Ξ1) : Prop := forall Ξ2 Ξ3 (f1 : Ξ1 =[val_m]> Ξ2) (f2 : Ξ2 =[val_m]> Ξ3) , t `ββ (f1 β f2) = (t `ββ f1) `ββ f2 . Definition v_sub_sub_P Ξ1 (v : val Ξ1) : Prop := forall Ξ2 Ξ3 (f1 : Ξ1 =[val_m]> Ξ2) (f2 : Ξ2 =[val_m]> Ξ3) , v `α΅₯β (f1 β f2) = (v `α΅₯β f1) `α΅₯β f2 . Definition e_sub_sub_P Ξ1 (Ο : ev_ctx Ξ1) : Prop := forall Ξ2 Ξ3 (f1 : Ξ1 =[val_m]> Ξ2) (f2 : Ξ2 =[val_m]> Ξ3) , Ο `ββ (f1 β f2) = (Ο `ββ f1) `ββ f2 .syn_ind_args t_sub_sub_P v_sub_sub_P e_sub_sub_Pforall (Ξ : t_ctx) (v : val Ξ), v_sub_sub_P Ξ v -> t_sub_sub_P Ξ (Val v)forall (Ξ : t_ctx) (t1 : term Ξ), t_sub_sub_P Ξ t1 -> forall t2 : term Ξ, t_sub_sub_P Ξ t2 -> t_sub_sub_P Ξ (App t1 t2)forall (Ξ : t_ctx) (i : Ξ β β), v_sub_sub_P Ξ (Var i)forall (Ξ : t_ctx) (t : term (Ξ βΆβ β)), t_sub_sub_P (Ξ βΆβ β) t -> v_sub_sub_P Ξ (Lam t)forall (Ξ : t_ctx) (i : Ξ β β), e_sub_sub_P Ξ (K0 i)forall (Ξ : t_ctx) (t : term Ξ), t_sub_sub_P Ξ t -> forall Ο : ev_ctx Ξ, e_sub_sub_P Ξ Ο -> e_sub_sub_P Ξ (K1 t Ο)forall (Ξ : t_ctx) (v : val Ξ), v_sub_sub_P Ξ v -> forall Ο : ev_ctx Ξ, e_sub_sub_P Ξ Ο -> e_sub_sub_P Ξ (K2 v Ο)forall (Ξ : t_ctx) (v : val Ξ), (forall (Ξ2 Ξ3 : t_ctx) (f1 : Ξ =[ val_m ]> Ξ2) (f2 : Ξ2 =[ val_m ]> Ξ3), v `α΅₯β f1 β f2 = (v `α΅₯β f1) `α΅₯β f2) -> forall (Ξ2 Ξ3 : t_ctx) (f1 : Ξ =[ val_m ]> Ξ2) (f2 : Ξ2 =[ val_m ]> Ξ3), Val v `ββ f1 β f2 = (Val v `ββ f1) `ββ f2forall (Ξ : t_ctx) (t1 : term Ξ), (forall (Ξ2 Ξ3 : t_ctx) (f1 : Ξ =[ val_m ]> Ξ2) (f2 : Ξ2 =[ val_m ]> Ξ3), t1 `ββ f1 β f2 = (t1 `ββ f1) `ββ f2) -> forall t2 : term Ξ, (forall (Ξ2 Ξ3 : t_ctx) (f1 : Ξ =[ val_m ]> Ξ2) (f2 : Ξ2 =[ val_m ]> Ξ3), t2 `ββ f1 β f2 = (t2 `ββ f1) `ββ f2) -> forall (Ξ2 Ξ3 : t_ctx) (f1 : Ξ =[ val_m ]> Ξ2) (f2 : Ξ2 =[ val_m ]> Ξ3), App t1 t2 `ββ f1 β f2 = (App t1 t2 `ββ f1) `ββ f2forall (Ξ : t_ctx) (i : Ξ β β) (Ξ2 Ξ3 : t_ctx) (f1 : Ξ =[ val_m ]> Ξ2) (f2 : Ξ2 =[ val_m ]> Ξ3), Var i `α΅₯β f1 β f2 = (Var i `α΅₯β f1) `α΅₯β f2forall (Ξ : t_ctx) (t : term (Ξ βΆβ β)), (forall (Ξ2 Ξ3 : t_ctx) (f1 : (Ξ βΆβ β) =[ val_m ]> Ξ2) (f2 : Ξ2 =[ val_m ]> Ξ3), t `ββ f1 β f2 = (t `ββ f1) `ββ f2) -> forall (Ξ2 Ξ3 : t_ctx) (f1 : Ξ =[ val_m ]> Ξ2) (f2 : Ξ2 =[ val_m ]> Ξ3), Lam t `α΅₯β f1 β f2 = (Lam t `α΅₯β f1) `α΅₯β f2forall (Ξ : t_ctx) (i : Ξ β β) (Ξ2 Ξ3 : t_ctx) (f1 : Ξ =[ val_m ]> Ξ2) (f2 : Ξ2 =[ val_m ]> Ξ3), K0 i `ββ f1 β f2 = (K0 i `ββ f1) `ββ f2forall (Ξ : t_ctx) (t : term Ξ), (forall (Ξ2 Ξ3 : t_ctx) (f1 : Ξ =[ val_m ]> Ξ2) (f2 : Ξ2 =[ val_m ]> Ξ3), t `ββ f1 β f2 = (t `ββ f1) `ββ f2) -> forall Ο : ev_ctx Ξ, (forall (Ξ2 Ξ3 : t_ctx) (f1 : Ξ =[ val_m ]> Ξ2) (f2 : Ξ2 =[ val_m ]> Ξ3), Ο `ββ f1 β f2 = (Ο `ββ f1) `ββ f2) -> forall (Ξ2 Ξ3 : t_ctx) (f1 : Ξ =[ val_m ]> Ξ2) (f2 : Ξ2 =[ val_m ]> Ξ3), K1 t Ο `ββ f1 β f2 = (K1 t Ο `ββ f1) `ββ f2forall (Ξ : t_ctx) (v : val Ξ), (forall (Ξ2 Ξ3 : t_ctx) (f1 : Ξ =[ val_m ]> Ξ2) (f2 : Ξ2 =[ val_m ]> Ξ3), v `α΅₯β f1 β f2 = (v `α΅₯β f1) `α΅₯β f2) -> forall Ο : ev_ctx Ξ, (forall (Ξ2 Ξ3 : t_ctx) (f1 : Ξ =[ val_m ]> Ξ2) (f2 : Ξ2 =[ val_m ]> Ξ3), Ο `ββ f1 β f2 = (Ο `ββ f1) `ββ f2) -> forall (Ξ2 Ξ3 : t_ctx) (f1 : Ξ =[ val_m ]> Ξ2) (f2 : Ξ2 =[ val_m ]> Ξ3), K2 v Ο `ββ f1 β f2 = (K2 v Ο `ββ f1) `ββ f2now rewrite a_shift1_comp. Qed.Ξ: t_ctx
t: term (Ξ βΆβ β)
H: forall (Ξ2 Ξ3 : t_ctx) (f1 : (Ξ βΆβ β) =[ val_m ]> Ξ2) (f2 : Ξ2 =[ val_m ]> Ξ3), t `ββ f1 β f2 = (t `ββ f1) `ββ f2
Ξ2, Ξ3: t_ctx
f1: Ξ =[ val_m ]> Ξ2
f2: Ξ2 =[ val_m ]> Ξ3t `ββ a_shift1 (f1 β f2) = (t `ββ a_shift1 f1) `ββ a_shift1 f2now apply (term_ind_mut _ _ _ sub_sub_prf). Qed.Ξ1, Ξ2, Ξ3: t_ctx
f1: Ξ1 =[ val_m ]> Ξ2
f2: Ξ2 =[ val_m ]> Ξ3
t: term Ξ1t `ββ f1 β f2 = (t `ββ f1) `ββ f2now apply (val_ind_mut _ _ _ sub_sub_prf). Qed.Ξ1, Ξ2, Ξ3: t_ctx
f1: Ξ1 =[ val_m ]> Ξ2
f2: Ξ2 =[ val_m ]> Ξ3
v: val Ξ1v `α΅₯β f1 β f2 = (v `α΅₯β f1) `α΅₯β f2now apply (ctx_ind_mut _ _ _ sub_sub_prf). Qed.Ξ1, Ξ2, Ξ3: t_ctx
f1: Ξ1 =[ val_m ]> Ξ2
f2: Ξ2 =[ val_m ]> Ξ3
Ο: ev_ctx Ξ1Ο `ββ f1 β f2 = (Ο `ββ f1) `ββ f2destruct a; [ now apply v_sub_sub | now apply e_sub_sub ]. Qed.Ξ1, Ξ2, Ξ3: t_ctx
a: ty
v: val_m Ξ1 a
f1: Ξ1 =[ val_m ]> Ξ2
f2: Ξ2 =[ val_m ]> Ξ3v α΅₯β f1 β f2 = (v α΅₯β f1) α΅₯β f2destruct s; cbn; now rewrite t_sub_sub, e_sub_sub. Qed.Ξ1, Ξ2, Ξ3: t_ctx
s: state Ξ1
f1: Ξ1 =[ val_m ]> Ξ2
f2: Ξ2 =[ val_m ]> Ξ3s ββ f1 β f2 = (s ββ f1) ββ f2Ξ, Ξ: t_ctx
a: ty
f: Ξ =[ val_m ]> Ξ
v: val_m Ξ aa_shift1 f β assign1 (v α΅₯β f) β‘β assign1 v β fΞ0: ctx ty
Ξ: t_ctx
a0: ty
f: Ξ0 =[ val_m ]> Ξ
v: val_m Ξ0 a0m_subst (Ξ βΆβ a0) a0 (a_id a0 top) Ξ (assign1 (m_subst Ξ0 a0 v Ξ f)) = m_subst Ξ0 a0 v Ξ fΞ1: ctx ty
Ξ: t_ctx
y: ty
f: Ξ1 =[ val_m ]> Ξ
v: val_m Ξ1 y
a0: ty
v0: var a0 Ξ1m_subst (Ξ βΆβ y) a0 (m_shift1 a0 (f a0 v0)) Ξ (assign1 (m_subst Ξ1 y v Ξ f)) = m_subst Ξ1 a0 (a_id a0 v0) Ξ funfold m_shift1; rewrite m_sub_ren, m_sub_id_r; now apply m_sub_id_l. Qed.Ξ1: ctx ty
Ξ: t_ctx
y: ty
f: Ξ1 =[ val_m ]> Ξ
v: val_m Ξ1 y
a0: ty
v0: var a0 Ξ1m_subst (Ξ βΆβ y) a0 (m_shift1 a0 (f a0 v0)) Ξ (assign1 (m_subst Ξ1 y v Ξ f)) = m_subst Ξ1 a0 (a_id a0 v0) Ξ funfold t_subst1; now rewrite <- 2 t_sub_sub, a_sub1_sub. Qed.Ξ, Ξ: t_ctx
x: ty
f: Ξ =[ val_m ]> Ξ
t: term (Ξ βΆβ x)
v: val_m Ξ xt `ββ a_shift1 f /[ v α΅₯β f] = (t /[ v]) `ββ f
We can now instanciate the generic OGS construction.
#[global] Instance ulc_val_laws : subst_monoid_laws val_m := {| v_sub_proper := @m_sub_eq ; v_sub_var := @m_sub_id_r ; v_var_sub := @m_sub_id_l ; Subst.v_sub_sub := @m_sub_sub |} . #[global] Instance ulc_conf_laws : subst_module_laws val_m state := {| c_sub_proper := @s_sub_eq ; c_var_sub := @s_sub_id_l ; c_sub_sub := @s_sub_sub |} .var_assumptions val_mforall (Ξ : t_ctx) (x : ty), injective (Subst.a_id (x:=x))forall (Ξ : t_ctx) (x : ty) (v : val_m Ξ x), decidable (is_var v)forall (Ξ1 Ξ2 : t_ctx) (x : ty) (v : val_m Ξ1 x) (r : Ξ1 β Ξ2), is_var (v_ren v r) -> is_var vintros ? [] ?? H; now dependent destruction H.forall (Ξ : t_ctx) (x : ty), injective (Subst.a_id (x:=x))forall (Ξ : t_ctx) (x : ty) (v : val_m Ξ x), decidable (is_var v)all: apply No; intro H; dependent destruction H.Ξ: t_ctx
t: term (Ξ βΆβ β)decidable (is_var (Lam t))Ξ: t_ctx
t: term Ξ
e: ev_ctx Ξdecidable (is_var (K1 t e))Ξ: t_ctx
v: val Ξ
e: ev_ctx Ξdecidable (is_var (K2 v e))intros ?? [] v r H; induction v; dependent destruction H; exact (Vvar _). Qed. #[global] Instance ulc_machine : machine val_m state obs_op := {| eval := @ulc_eval ; oapp := @obs_app |} . From Coinduction Require Import coinduction lattice rel tactics. From OGS.ITree Require Import Eq. Ltac refold_eval := change (Structure.iter _ _ ?a) with (ulc_eval a); change (Structure.subst (fun pat : T1 => let 'T1_0 := pat in ?f) T1_0 ?u) with (bind_delay' u f).forall (Ξ1 Ξ2 : t_ctx) (x : ty) (v : val_m Ξ1 x) (r : Ξ1 β Ξ2), is_var (v_ren v r) -> is_var vmachine_laws val_m state obs_opΞ: t_ctx
x: ty
v: val_m Ξ x
o: obs xProper (asgn_eq (obs_dom o) Ξ ==> eq) (obs_app v o)Ξ1, Ξ2: t_ctx
x: ty
v: val_m Ξ1 x
o: obs x
a: obs_dom o =[ val_m ]> Ξ1
b: Ξ1 =[ val_m ]> Ξ2s_subst Ξ1 (obs_app v o a) Ξ2 b = obs_app (m_subst Ξ1 x v Ξ2 b) o (a β b)Ξ, Ξ: t_ctx
c: state Ξ
a: Ξ =[ val_m ]> Ξulc_eval (s_subst Ξ c Ξ a) β bind_delay' (ulc_eval c) (fun n : Obs.nf obs_op val_m Ξ => ulc_eval (s_subst Ξ (obs_app (a_id (nf_ty n) (nf_var n)) (nf_obs n) (nf_args n)) Ξ a))Ξ: t_ctx
u: Obs.nf obs_op val_m Ξulc_eval (obs_app (a_id (nf_ty u) (nf_var u)) (nf_obs u) (nf_args u)) β ret_delay uwell_founded head_inst_nostepintros ?? H1; dependent elimination o; cbn; repeat (f_equal; auto).Ξ: t_ctx
x: ty
v: val_m Ξ x
o: obs xProper (asgn_eq (obs_dom o) Ξ ==> eq) (obs_app v o)destruct x; dependent elimination o; cbn; f_equal.Ξ1, Ξ2: t_ctx
x: ty
v: val_m Ξ1 x
o: obs x
a: obs_dom o =[ val_m ]> Ξ1
b: Ξ1 =[ val_m ]> Ξ2s_subst Ξ1 (obs_app v o a) Ξ2 b = obs_app (m_subst Ξ1 x v Ξ2 b) o (a β b)Ξ, Ξ: t_ctx
c: state Ξ
a: Ξ =[ val_m ]> Ξulc_eval (s_subst Ξ c Ξ a) β bind_delay' (ulc_eval c) (fun n : Obs.nf obs_op val_m Ξ => ulc_eval (s_subst Ξ (obs_app (a_id (nf_ty n) (nf_var n)) (nf_obs n) (nf_args n)) Ξ a))Ξ, Ξ: t_ctx
R: relα΅’ (itree Event.emptyβ (fun _ : T1 => Obs.nf obs_op val_m Ξ)) (itree Event.emptyβ (fun _ : T1 => Obs.nf obs_op val_m Ξ))
CIH: forall (c : state Ξ) (a : Ξ =[ val_m ]> Ξ), it_eq_t Event.emptyβ (fun _ : T1 => nf_eq) R T1_0 (ulc_eval (s_subst Ξ c Ξ a)) (bind_delay' (ulc_eval c) (fun n : Obs.nf obs_op val_m Ξ => ulc_eval (s_subst Ξ (obs_app (a_id (nf_ty n) (nf_var n)) (nf_obs n) (nf_args n)) Ξ a)))
c: state Ξ
e: Ξ =[ val_m ]> Ξit_eq_bt Event.emptyβ (fun _ : T1 => nf_eq) R T1_0 (ulc_eval (s_subst Ξ c Ξ e)) (bind_delay' (ulc_eval c) (fun n : Obs.nf obs_op val_m Ξ => ulc_eval (s_subst Ξ (obs_app (a_id (nf_ty n) (nf_var n)) (nf_obs n) (nf_args n)) Ξ e)))Ξ: t_ctx
v: val Ξ
i: Ξ β β
Ξ: t_ctx
R: relα΅’ (itree Event.emptyβ (fun _ : T1 => Obs.nf obs_op val_m Ξ)) (itree Event.emptyβ (fun _ : T1 => Obs.nf obs_op val_m Ξ))
CIH: forall (c : state Ξ) (a : Ξ =[ val_m ]> Ξ), it_eq_t Event.emptyβ (fun _ : T1 => nf_eq) R T1_0 (ulc_eval (s_subst Ξ c Ξ a)) (bind_delay' (ulc_eval c) (fun n : Obs.nf obs_op val_m Ξ => ulc_eval (s_subst Ξ (obs_app (a_id (nf_ty n) (nf_var n)) (nf_obs n) (nf_args n)) Ξ a)))
e: Ξ =[ val_m ]> Ξ
H: {| pr1 := ORet; pr2 := (! βΆβ v)%asgn |} = {| pr1 := ORet; pr2 := (! βΆβ v)%asgn |}it_eqF Event.emptyβ (fun _ : T1 => nf_eq) (it_eq_t Event.emptyβ (fun _ : T1 => nf_eq) R) T1_0 match match e (β) i with | K0 c => inr (c β ORet β¦ ! βΆβ (v `α΅₯β e) β¦) | K1 t e0 => inl (Cut t (K2 (v `α΅₯β e) e0)) | K2 v0 e0 => match v `α΅₯β e with | Var c => fun (v1 : val Ξ) (e1 : ev_ctx Ξ) => inr (c β OApp β¦ (! βΆβ v1) βΆβ e1 β¦) | Lam t => fun v1 : val Ξ => inl β Cut (t /[ v1]) end v0 e0 end with | inl x => TauF (Structure.iter (fun pat : T1 => let 'T1_0 as x0 := pat return (state Ξ -> itree Event.emptyβ ((fun _ : T1 => state Ξ) +α΅’ (fun _ : T1 => nf Ξ)) x0) in ret_delay β eval_step) T1_0 x) | inr y => RetF y end match match e (β) i with | K0 c => inr (c β ORet β¦ ! βΆβ (v `α΅₯β e) β¦) | K1 t e0 => inl (Cut t (K2 (v `α΅₯β e) e0)) | K2 v0 e0 => match v `α΅₯β e with | Var c => fun (v1 : val Ξ) (e1 : ev_ctx Ξ) => inr (c β OApp β¦ (! βΆβ v1) βΆβ e1 β¦) | Lam t => fun v1 : val Ξ => inl β Cut (t /[ v1]) end v0 e0 end with | inl x => TauF (Structure.iter (fun pat : T1 => let 'T1_0 as x0 := pat return (state Ξ -> itree Event.emptyβ ((fun _ : T1 => state Ξ) +α΅’ (fun _ : T1 => nf Ξ)) x0) in ret_delay β eval_step) T1_0 x) | inr y => RetF y endΞ: t_ctx
v: val Ξ
t: term Ξ
Ο: ev_ctx Ξ
Ξ: t_ctx
R: relα΅’ (itree Event.emptyβ (fun _ : T1 => Obs.nf obs_op val_m Ξ)) (itree Event.emptyβ (fun _ : T1 => Obs.nf obs_op val_m Ξ))
CIH: forall (c : state Ξ) (a : Ξ =[ val_m ]> Ξ), it_eq_t Event.emptyβ (fun _ : T1 => nf_eq) R T1_0 (ulc_eval (s_subst Ξ c Ξ a)) (bind_delay' (ulc_eval c) (fun n : Obs.nf obs_op val_m Ξ => ulc_eval (s_subst Ξ (obs_app (a_id (nf_ty n) (nf_var n)) (nf_obs n) (nf_args n)) Ξ a)))
e: Ξ =[ val_m ]> Ξ
H: Cut t (K2 v Ο) = Cut t (K2 v Ο)it_eqF Event.emptyβ (fun _ : T1 => nf_eq) (it_eq_t Event.emptyβ (fun _ : T1 => nf_eq) R) T1_0 (TauF (Structure.iter (fun pat : T1 => let 'T1_0 as x := pat return (state Ξ -> itree Event.emptyβ ((fun _ : T1 => state Ξ) +α΅’ (fun _ : T1 => nf Ξ)) x) in ret_delay β eval_step) T1_0 (Cut (t `ββ e) (K2 (v `α΅₯β e) (Ο `ββ e))))) (TauF (Structure.subst (fun pat : T1 => let 'T1_0 as x := pat return (Obs.nf obs_op val_m Ξ -> itree Event.emptyβ (fun _ : T1 => Obs.nf obs_op val_m Ξ) x) in fun y : Obs.nf obs_op val_m Ξ => ulc_eval (s_subst Ξ (obs_app (a_id (nf_ty y) (nf_var y)) (nf_obs y) (nf_args y)) Ξ e)) T1_0 (Structure.iter (fun pat : T1 => let 'T1_0 as x := pat return (state Ξ -> itree Event.emptyβ ((fun _ : T1 => state Ξ) +α΅’ (fun _ : T1 => nf Ξ)) x) in ret_delay β eval_step) T1_0 (Cut t (K2 v Ο)))))Ξ: t_ctx
i: Ξ β β
v: val Ξ
Ο: ev_ctx Ξ
Ξ: t_ctx
R: relα΅’ (itree Event.emptyβ (fun _ : T1 => Obs.nf obs_op val_m Ξ)) (itree Event.emptyβ (fun _ : T1 => Obs.nf obs_op val_m Ξ))
CIH: forall (c : state Ξ) (a : Ξ =[ val_m ]> Ξ), it_eq_t Event.emptyβ (fun _ : T1 => nf_eq) R T1_0 (ulc_eval (s_subst Ξ c Ξ a)) (bind_delay' (ulc_eval c) (fun n : Obs.nf obs_op val_m Ξ => ulc_eval (s_subst Ξ (obs_app (a_id (nf_ty n) (nf_var n)) (nf_obs n) (nf_args n)) Ξ a)))
e: Ξ =[ val_m ]> Ξ
H: {| pr1 := OApp; pr2 := ((! βΆβ v) βΆβ Ο)%asgn |} = {| pr1 := OApp; pr2 := ((! βΆβ v) βΆβ Ο)%asgn |}it_eqF Event.emptyβ (fun _ : T1 => nf_eq) (it_eq_t Event.emptyβ (fun _ : T1 => nf_eq) R) T1_0 match match e (β) i with | Var c => fun (v0 : val Ξ) (e0 : ev_ctx Ξ) => inr (c β OApp β¦ (! βΆβ v0) βΆβ e0 β¦) | Lam t => fun v0 : val Ξ => inl β Cut (t /[ v0]) end (v `α΅₯β e) (Ο `ββ e) with | inl x => TauF (Structure.iter (fun pat : T1 => let 'T1_0 as x0 := pat return (state Ξ -> itree Event.emptyβ ((fun _ : T1 => state Ξ) +α΅’ (fun _ : T1 => nf Ξ)) x0) in ret_delay β eval_step) T1_0 x) | inr y => RetF y end match match e (β) i with | Var c => fun (v0 : val Ξ) (e0 : ev_ctx Ξ) => inr (c β OApp β¦ (! βΆβ v0) βΆβ e0 β¦) | Lam t => fun v0 : val Ξ => inl β Cut (t /[ v0]) end (v `α΅₯β e) (Ο `ββ e) with | inl x => TauF (Structure.iter (fun pat : T1 => let 'T1_0 as x0 := pat return (state Ξ -> itree Event.emptyβ ((fun _ : T1 => state Ξ) +α΅’ (fun _ : T1 => nf Ξ)) x0) in ret_delay β eval_step) T1_0 x) | inr y => RetF y endΞ: t_ctx
t: term (Ξ βΆβ β)
v: val Ξ
Ο: ev_ctx Ξ
Ξ: t_ctx
R: relα΅’ (itree Event.emptyβ (fun _ : T1 => Obs.nf obs_op val_m Ξ)) (itree Event.emptyβ (fun _ : T1 => Obs.nf obs_op val_m Ξ))
CIH: forall (c : state Ξ) (a : Ξ =[ val_m ]> Ξ), it_eq_t Event.emptyβ (fun _ : T1 => nf_eq) R T1_0 (ulc_eval (s_subst Ξ c Ξ a)) (bind_delay' (ulc_eval c) (fun n : Obs.nf obs_op val_m Ξ => ulc_eval (s_subst Ξ (obs_app (a_id (nf_ty n) (nf_var n)) (nf_obs n) (nf_args n)) Ξ a)))
e: Ξ =[ val_m ]> Ξ
H: Cut (t /[ v]) Ο = Cut (t /[ v]) Οit_eqF Event.emptyβ (fun _ : T1 => nf_eq) (it_eq_t Event.emptyβ (fun _ : T1 => nf_eq) R) T1_0 (TauF (Structure.iter (fun pat : T1 => let 'T1_0 as x := pat return (state Ξ -> itree Event.emptyβ ((fun _ : T1 => state Ξ) +α΅’ (fun _ : T1 => nf Ξ)) x) in ret_delay β eval_step) T1_0 (Cut (t `ββ a_shift1 e /[ v `α΅₯β e]) (Ο `ββ e)))) (TauF (Structure.subst (fun pat : T1 => let 'T1_0 as x := pat return (Obs.nf obs_op val_m Ξ -> itree Event.emptyβ (fun _ : T1 => Obs.nf obs_op val_m Ξ) x) in fun y : Obs.nf obs_op val_m Ξ => ulc_eval (s_subst Ξ (obs_app (a_id (nf_ty y) (nf_var y)) (nf_obs y) (nf_args y)) Ξ e)) T1_0 (Structure.iter (fun pat : T1 => let 'T1_0 as x := pat return (state Ξ -> itree Event.emptyβ ((fun _ : T1 => state Ξ) +α΅’ (fun _ : T1 => nf Ξ)) x) in ret_delay β eval_step) T1_0 (Cut (t /[ v]) Ο))))Ξ: t_ctx
t1, t2: term Ξ
Ο: ev_ctx Ξ
Ξ: t_ctx
R: relα΅’ (itree Event.emptyβ (fun _ : T1 => Obs.nf obs_op val_m Ξ)) (itree Event.emptyβ (fun _ : T1 => Obs.nf obs_op val_m Ξ))
CIH: forall (c : state Ξ) (a : Ξ =[ val_m ]> Ξ), it_eq_t Event.emptyβ (fun _ : T1 => nf_eq) R T1_0 (ulc_eval (s_subst Ξ c Ξ a)) (bind_delay' (ulc_eval c) (fun n : Obs.nf obs_op val_m Ξ => ulc_eval (s_subst Ξ (obs_app (a_id (nf_ty n) (nf_var n)) (nf_obs n) (nf_args n)) Ξ a)))
e: Ξ =[ val_m ]> Ξ
H: Cut t2 (K1 t1 Ο) = Cut t2 (K1 t1 Ο)it_eqF Event.emptyβ (fun _ : T1 => nf_eq) (it_eq_t Event.emptyβ (fun _ : T1 => nf_eq) R) T1_0 (TauF (Structure.iter (fun pat : T1 => let 'T1_0 as x := pat return (state Ξ -> itree Event.emptyβ ((fun _ : T1 => state Ξ) +α΅’ (fun _ : T1 => nf Ξ)) x) in ret_delay β eval_step) T1_0 (Cut (t2 `ββ e) (K1 (t1 `ββ e) (Ο `ββ e))))) (TauF (Structure.subst (fun pat : T1 => let 'T1_0 as x := pat return (Obs.nf obs_op val_m Ξ -> itree Event.emptyβ (fun _ : T1 => Obs.nf obs_op val_m Ξ) x) in fun y : Obs.nf obs_op val_m Ξ => ulc_eval (s_subst Ξ (obs_app (a_id (nf_ty y) (nf_var y)) (nf_obs y) (nf_args y)) Ξ e)) T1_0 (Structure.iter (fun pat : T1 => let 'T1_0 as x := pat return (state Ξ -> itree Event.emptyβ ((fun _ : T1 => state Ξ) +α΅’ (fun _ : T1 => nf Ξ)) x) in ret_delay β eval_step) T1_0 (Cut t2 (K1 t1 Ο)))))Ξ: t_ctx
v: val Ξ
i: Ξ β β
Ξ: t_ctx
R: relα΅’ (itree Event.emptyβ (fun _ : T1 => Obs.nf obs_op val_m Ξ)) (itree Event.emptyβ (fun _ : T1 => Obs.nf obs_op val_m Ξ))
CIH: forall (c : state Ξ) (a : Ξ =[ val_m ]> Ξ), it_eq_t Event.emptyβ (fun _ : T1 => nf_eq) R T1_0 (ulc_eval (s_subst Ξ c Ξ a)) (bind_delay' (ulc_eval c) (fun n : Obs.nf obs_op val_m Ξ => ulc_eval (s_subst Ξ (obs_app (a_id (nf_ty n) (nf_var n)) (nf_obs n) (nf_args n)) Ξ a)))
e: Ξ =[ val_m ]> Ξ
H: {| pr1 := ORet; pr2 := (! βΆβ v)%asgn |} = {| pr1 := ORet; pr2 := (! βΆβ v)%asgn |}it_eqF Event.emptyβ (fun _ : T1 => nf_eq) (it_eq_t Event.emptyβ (fun _ : T1 => nf_eq) R) T1_0 match match e (β) i with | K0 c => inr (c β ORet β¦ ! βΆβ (v `α΅₯β e) β¦) | K1 t e0 => inl (Cut t (K2 (v `α΅₯β e) e0)) | K2 v0 e0 => match v `α΅₯β e with | Var c => fun (v1 : val Ξ) (e1 : ev_ctx Ξ) => inr (c β OApp β¦ (! βΆβ v1) βΆβ e1 β¦) | Lam t => fun v1 : val Ξ => inl β Cut (t /[ v1]) end v0 e0 end with | inl x => TauF (Structure.iter (fun pat : T1 => let 'T1_0 as x0 := pat return (state Ξ -> itree Event.emptyβ ((fun _ : T1 => state Ξ) +α΅’ (fun _ : T1 => nf Ξ)) x0) in ret_delay β eval_step) T1_0 x) | inr y => RetF y end match match e (β) i with | K0 c => inr (c β ORet β¦ ! βΆβ (v `α΅₯β e) β¦) | K1 t e0 => inl (Cut t (K2 (v `α΅₯β e) e0)) | K2 v0 e0 => match v `α΅₯β e with | Var c => fun (v1 : val Ξ) (e1 : ev_ctx Ξ) => inr (c β OApp β¦ (! βΆβ v1) βΆβ e1 β¦) | Lam t => fun v1 : val Ξ => inl β Cut (t /[ v1]) end v0 e0 end with | inl x => TauF (Structure.iter (fun pat : T1 => let 'T1_0 as x0 := pat return (state Ξ -> itree Event.emptyβ ((fun _ : T1 => state Ξ) +α΅’ (fun _ : T1 => nf Ξ)) x0) in ret_delay β eval_step) T1_0 x) | inr y => RetF y endΞ: t_ctx
v: val Ξ
i: Ξ β β
Ξ: t_ctx
R: relα΅’ (itree Event.emptyβ (fun _ : T1 => Obs.nf obs_op val_m Ξ)) (itree Event.emptyβ (fun _ : T1 => Obs.nf obs_op val_m Ξ))
CIH: forall (c : state Ξ) (a : Ξ =[ val_m ]> Ξ), it_eq_t Event.emptyβ (fun _ : T1 => nf_eq) R T1_0 (ulc_eval (s_subst Ξ c Ξ a)) (bind_delay' (ulc_eval c) (fun n : Obs.nf obs_op val_m Ξ => ulc_eval (s_subst Ξ (obs_app (a_id (nf_ty n) (nf_var n)) (nf_obs n) (nf_args n)) Ξ a)))
e: Ξ =[ val_m ]> Ξ
H: {| pr1 := ORet; pr2 := (! βΆβ v)%asgn |} = {| pr1 := ORet; pr2 := (! βΆβ v)%asgn |}
v0: val Ξ
v1: ev_ctx Ξit_eqF Event.emptyβ (fun _ : T1 => nf_eq) (it_eq_t Event.emptyβ (fun _ : T1 => nf_eq) R) T1_0 match match v `α΅₯β e with | Var c => fun (v0 : val Ξ) (e0 : ev_ctx Ξ) => inr (c β OApp β¦ (! βΆβ v0) βΆβ e0 β¦) | Lam t => fun v0 : val Ξ => inl β Cut (t /[ v0]) end v0 v1 with | inl x => TauF (Structure.iter (fun pat : T1 => let 'T1_0 as x0 := pat return (state Ξ -> itree Event.emptyβ ((fun _ : T1 => state Ξ) +α΅’ (fun _ : T1 => nf Ξ)) x0) in ret_delay β eval_step) T1_0 x) | inr y => RetF y end match match v `α΅₯β e with | Var c => fun (v0 : val Ξ) (e0 : ev_ctx Ξ) => inr (c β OApp β¦ (! βΆβ v0) βΆβ e0 β¦) | Lam t => fun v0 : val Ξ => inl β Cut (t /[ v0]) end v0 v1 with | inl x => TauF (Structure.iter (fun pat : T1 => let 'T1_0 as x0 := pat return (state Ξ -> itree Event.emptyβ ((fun _ : T1 => state Ξ) +α΅’ (fun _ : T1 => nf Ξ)) x0) in ret_delay β eval_step) T1_0 x) | inr y => RetF y enddependent elimination v'; cbn; auto.Ξ: t_ctx
i: Ξ β β
Ξ: t_ctx
R: relα΅’ (itree Event.emptyβ (fun _ : T1 => Obs.nf obs_op val_m Ξ)) (itree Event.emptyβ (fun _ : T1 => Obs.nf obs_op val_m Ξ))
CIH: forall (c : state Ξ) (a : Ξ =[ val_m ]> Ξ), it_eq_t Event.emptyβ (fun _ : T1 => nf_eq) R T1_0 (ulc_eval (s_subst Ξ c Ξ a)) (bind_delay' (ulc_eval c) (fun n : Obs.nf obs_op val_m Ξ => ulc_eval (s_subst Ξ (obs_app (a_id (nf_ty n) (nf_var n)) (nf_obs n) (nf_args n)) Ξ a)))
e: Ξ =[ val_m ]> Ξ
v0: val Ξ
v1: ev_ctx Ξ
v': val Ξit_eqF Event.emptyβ (fun _ : T1 => nf_eq) (it_eq_t Event.emptyβ (fun _ : T1 => nf_eq) R) T1_0 match match v' with | Var c => fun (v0 : val Ξ) (e0 : ev_ctx Ξ) => inr (c β OApp β¦ (! βΆβ v0) βΆβ e0 β¦) | Lam t => fun v0 : val Ξ => inl β Cut (t /[ v0]) end v0 v1 with | inl x => TauF (Structure.iter (fun pat : T1 => let 'T1_0 as x0 := pat return (state Ξ -> itree Event.emptyβ ((fun _ : T1 => state Ξ) +α΅’ (fun _ : T1 => nf Ξ)) x0) in ret_delay β eval_step) T1_0 x) | inr y => RetF y end match match v' with | Var c => fun (v0 : val Ξ) (e0 : ev_ctx Ξ) => inr (c β OApp β¦ (! βΆβ v0) βΆβ e0 β¦) | Lam t => fun v0 : val Ξ => inl β Cut (t /[ v0]) end v0 v1 with | inl x => TauF (Structure.iter (fun pat : T1 => let 'T1_0 as x0 := pat return (state Ξ -> itree Event.emptyβ ((fun _ : T1 => state Ξ) +α΅’ (fun _ : T1 => nf Ξ)) x0) in ret_delay β eval_step) T1_0 x) | inr y => RetF y endeconstructor; refold_eval; apply CIH.Ξ: t_ctx
v: val Ξ
t: term Ξ
Ο: ev_ctx Ξ
Ξ: t_ctx
R: relα΅’ (itree Event.emptyβ (fun _ : T1 => Obs.nf obs_op val_m Ξ)) (itree Event.emptyβ (fun _ : T1 => Obs.nf obs_op val_m Ξ))
CIH: forall (c : state Ξ) (a : Ξ =[ val_m ]> Ξ), it_eq_t Event.emptyβ (fun _ : T1 => nf_eq) R T1_0 (ulc_eval (s_subst Ξ c Ξ a)) (bind_delay' (ulc_eval c) (fun n : Obs.nf obs_op val_m Ξ => ulc_eval (s_subst Ξ (obs_app (a_id (nf_ty n) (nf_var n)) (nf_obs n) (nf_args n)) Ξ a)))
e: Ξ =[ val_m ]> Ξ
H: Cut t (K2 v Ο) = Cut t (K2 v Ο)it_eqF Event.emptyβ (fun _ : T1 => nf_eq) (it_eq_t Event.emptyβ (fun _ : T1 => nf_eq) R) T1_0 (TauF (Structure.iter (fun pat : T1 => let 'T1_0 as x := pat return (state Ξ -> itree Event.emptyβ ((fun _ : T1 => state Ξ) +α΅’ (fun _ : T1 => nf Ξ)) x) in ret_delay β eval_step) T1_0 (Cut (t `ββ e) (K2 (v `α΅₯β e) (Ο `ββ e))))) (TauF (Structure.subst (fun pat : T1 => let 'T1_0 as x := pat return (Obs.nf obs_op val_m Ξ -> itree Event.emptyβ (fun _ : T1 => Obs.nf obs_op val_m Ξ) x) in fun y : Obs.nf obs_op val_m Ξ => ulc_eval (s_subst Ξ (obs_app (a_id (nf_ty y) (nf_var y)) (nf_obs y) (nf_args y)) Ξ e)) T1_0 (Structure.iter (fun pat : T1 => let 'T1_0 as x := pat return (state Ξ -> itree Event.emptyβ ((fun _ : T1 => state Ξ) +α΅’ (fun _ : T1 => nf Ξ)) x) in ret_delay β eval_step) T1_0 (Cut t (K2 v Ο)))))Ξ: t_ctx
i: Ξ β β
v: val Ξ
Ο: ev_ctx Ξ
Ξ: t_ctx
R: relα΅’ (itree Event.emptyβ (fun _ : T1 => Obs.nf obs_op val_m Ξ)) (itree Event.emptyβ (fun _ : T1 => Obs.nf obs_op val_m Ξ))
CIH: forall (c : state Ξ) (a : Ξ =[ val_m ]> Ξ), it_eq_t Event.emptyβ (fun _ : T1 => nf_eq) R T1_0 (ulc_eval (s_subst Ξ c Ξ a)) (bind_delay' (ulc_eval c) (fun n : Obs.nf obs_op val_m Ξ => ulc_eval (s_subst Ξ (obs_app (a_id (nf_ty n) (nf_var n)) (nf_obs n) (nf_args n)) Ξ a)))
e: Ξ =[ val_m ]> Ξ
H: {| pr1 := OApp; pr2 := ((! βΆβ v) βΆβ Ο)%asgn |} = {| pr1 := OApp; pr2 := ((! βΆβ v) βΆβ Ο)%asgn |}it_eqF Event.emptyβ (fun _ : T1 => nf_eq) (it_eq_t Event.emptyβ (fun _ : T1 => nf_eq) R) T1_0 match match e (β) i with | Var c => fun (v0 : val Ξ) (e0 : ev_ctx Ξ) => inr (c β OApp β¦ (! βΆβ v0) βΆβ e0 β¦) | Lam t => fun v0 : val Ξ => inl β Cut (t /[ v0]) end (v `α΅₯β e) (Ο `ββ e) with | inl x => TauF (Structure.iter (fun pat : T1 => let 'T1_0 as x0 := pat return (state Ξ -> itree Event.emptyβ ((fun _ : T1 => state Ξ) +α΅’ (fun _ : T1 => nf Ξ)) x0) in ret_delay β eval_step) T1_0 x) | inr y => RetF y end match match e (β) i with | Var c => fun (v0 : val Ξ) (e0 : ev_ctx Ξ) => inr (c β OApp β¦ (! βΆβ v0) βΆβ e0 β¦) | Lam t => fun v0 : val Ξ => inl β Cut (t /[ v0]) end (v `α΅₯β e) (Ο `ββ e) with | inl x => TauF (Structure.iter (fun pat : T1 => let 'T1_0 as x0 := pat return (state Ξ -> itree Event.emptyβ ((fun _ : T1 => state Ξ) +α΅’ (fun _ : T1 => nf Ξ)) x0) in ret_delay β eval_step) T1_0 x) | inr y => RetF y enddependent elimination vv; cbn; auto.Ξ: t_ctx
v: val Ξ
Ο: ev_ctx Ξ
Ξ: t_ctx
R: relα΅’ (itree Event.emptyβ (fun _ : T1 => Obs.nf obs_op val_m Ξ)) (itree Event.emptyβ (fun _ : T1 => Obs.nf obs_op val_m Ξ))
CIH: forall (c : state Ξ) (a : Ξ =[ val_m ]> Ξ), it_eq_t Event.emptyβ (fun _ : T1 => nf_eq) R T1_0 (ulc_eval (s_subst Ξ c Ξ a)) (bind_delay' (ulc_eval c) (fun n : Obs.nf obs_op val_m Ξ => ulc_eval (s_subst Ξ (obs_app (a_id (nf_ty n) (nf_var n)) (nf_obs n) (nf_args n)) Ξ a)))
e: Ξ =[ val_m ]> Ξ
vv: val_m Ξ (β)it_eqF Event.emptyβ (fun _ : T1 => nf_eq) (it_eq_t Event.emptyβ (fun _ : T1 => nf_eq) R) T1_0 match match vv with | Var c => fun (v0 : val Ξ) (e0 : ev_ctx Ξ) => inr (c β OApp β¦ (! βΆβ v0) βΆβ e0 β¦) | Lam t => fun v0 : val Ξ => inl β Cut (t /[ v0]) end (v `α΅₯β e) (Ο `ββ e) with | inl x => TauF (Structure.iter (fun pat : T1 => let 'T1_0 as x0 := pat return (state Ξ -> itree Event.emptyβ ((fun _ : T1 => state Ξ) +α΅’ (fun _ : T1 => nf Ξ)) x0) in ret_delay β eval_step) T1_0 x) | inr y => RetF y end match match vv with | Var c => fun (v0 : val Ξ) (e0 : ev_ctx Ξ) => inr (c β OApp β¦ (! βΆβ v0) βΆβ e0 β¦) | Lam t => fun v0 : val Ξ => inl β Cut (t /[ v0]) end (v `α΅₯β e) (Ο `ββ e) with | inl x => TauF (Structure.iter (fun pat : T1 => let 'T1_0 as x0 := pat return (state Ξ -> itree Event.emptyβ ((fun _ : T1 => state Ξ) +α΅’ (fun _ : T1 => nf Ξ)) x0) in ret_delay β eval_step) T1_0 x) | inr y => RetF y endΞ: t_ctx
t: term (Ξ βΆβ β)
v: val Ξ
Ο: ev_ctx Ξ
Ξ: t_ctx
R: relα΅’ (itree Event.emptyβ (fun _ : T1 => Obs.nf obs_op val_m Ξ)) (itree Event.emptyβ (fun _ : T1 => Obs.nf obs_op val_m Ξ))
CIH: forall (c : state Ξ) (a : Ξ =[ val_m ]> Ξ), it_eq_t Event.emptyβ (fun _ : T1 => nf_eq) R T1_0 (ulc_eval (s_subst Ξ c Ξ a)) (bind_delay' (ulc_eval c) (fun n : Obs.nf obs_op val_m Ξ => ulc_eval (s_subst Ξ (obs_app (a_id (nf_ty n) (nf_var n)) (nf_obs n) (nf_args n)) Ξ a)))
e: Ξ =[ val_m ]> Ξ
H: Cut (t /[ v]) Ο = Cut (t /[ v]) Οit_eqF Event.emptyβ (fun _ : T1 => nf_eq) (it_eq_t Event.emptyβ (fun _ : T1 => nf_eq) R) T1_0 (TauF (Structure.iter (fun pat : T1 => let 'T1_0 as x := pat return (state Ξ -> itree Event.emptyβ ((fun _ : T1 => state Ξ) +α΅’ (fun _ : T1 => nf Ξ)) x) in ret_delay β eval_step) T1_0 (Cut (t `ββ a_shift1 e /[ v `α΅₯β e]) (Ο `ββ e)))) (TauF (Structure.subst (fun pat : T1 => let 'T1_0 as x := pat return (Obs.nf obs_op val_m Ξ -> itree Event.emptyβ (fun _ : T1 => Obs.nf obs_op val_m Ξ) x) in fun y : Obs.nf obs_op val_m Ξ => ulc_eval (s_subst Ξ (obs_app (a_id (nf_ty y) (nf_var y)) (nf_obs y) (nf_args y)) Ξ e)) T1_0 (Structure.iter (fun pat : T1 => let 'T1_0 as x := pat return (state Ξ -> itree Event.emptyβ ((fun _ : T1 => state Ξ) +α΅’ (fun _ : T1 => nf Ξ)) x) in ret_delay β eval_step) T1_0 (Cut (t /[ v]) Ο))))Ξ: t_ctx
t: term (Ξ βΆβ β)
v: val Ξ
Ο: ev_ctx Ξ
Ξ: t_ctx
R: relα΅’ (itree Event.emptyβ (fun _ : T1 => Obs.nf obs_op val_m Ξ)) (itree Event.emptyβ (fun _ : T1 => Obs.nf obs_op val_m Ξ))
CIH: forall (c : state Ξ) (a : Ξ =[ val_m ]> Ξ), it_eq_t Event.emptyβ (fun _ : T1 => nf_eq) R T1_0 (ulc_eval (s_subst Ξ c Ξ a)) (bind_delay' (ulc_eval c) (fun n : Obs.nf obs_op val_m Ξ => ulc_eval (s_subst Ξ (obs_app (a_id (nf_ty n) (nf_var n)) (nf_obs n) (nf_args n)) Ξ a)))
e: Ξ =[ val_m ]> Ξ
H: Cut (t /[ v]) Ο = Cut (t /[ v]) Οit_eq_t Event.emptyβ (fun _ : T1 => nf_eq) R T1_0 (ulc_eval (Cut (t `ββ a_shift1 e /[ (v : val_m Ξ (β)) α΅₯β e]) (Ο `ββ e))) (bind_delay' (ulc_eval (Cut (t /[ v]) Ο)) (fun y : Obs.nf obs_op val_m Ξ => ulc_eval (s_subst Ξ (obs_app (a_id (nf_ty y) (nf_var y)) (nf_obs y) (nf_args y)) Ξ e)))apply CIH.Ξ: t_ctx
t: term (Ξ βΆβ β)
v: val Ξ
Ο: ev_ctx Ξ
Ξ: t_ctx
R: relα΅’ (itree Event.emptyβ (fun _ : T1 => Obs.nf obs_op val_m Ξ)) (itree Event.emptyβ (fun _ : T1 => Obs.nf obs_op val_m Ξ))
CIH: forall (c : state Ξ) (a : Ξ =[ val_m ]> Ξ), it_eq_t Event.emptyβ (fun _ : T1 => nf_eq) R T1_0 (ulc_eval (s_subst Ξ c Ξ a)) (bind_delay' (ulc_eval c) (fun n : Obs.nf obs_op val_m Ξ => ulc_eval (s_subst Ξ (obs_app (a_id (nf_ty n) (nf_var n)) (nf_obs n) (nf_args n)) Ξ a)))
e: Ξ =[ val_m ]> Ξ
H: Cut (t /[ v]) Ο = Cut (t /[ v]) Οit_eq_t Event.emptyβ (fun _ : T1 => nf_eq) R T1_0 (ulc_eval (Cut ((t /[ v]) `ββ e) (Ο `ββ e))) (bind_delay' (ulc_eval (Cut (t /[ v]) Ο)) (fun y : Obs.nf obs_op val_m Ξ => ulc_eval (s_subst Ξ (obs_app (a_id (nf_ty y) (nf_var y)) (nf_obs y) (nf_args y)) Ξ e)))econstructor; refold_eval; apply CIH.Ξ: t_ctx
t1, t2: term Ξ
Ο: ev_ctx Ξ
Ξ: t_ctx
R: relα΅’ (itree Event.emptyβ (fun _ : T1 => Obs.nf obs_op val_m Ξ)) (itree Event.emptyβ (fun _ : T1 => Obs.nf obs_op val_m Ξ))
CIH: forall (c : state Ξ) (a : Ξ =[ val_m ]> Ξ), it_eq_t Event.emptyβ (fun _ : T1 => nf_eq) R T1_0 (ulc_eval (s_subst Ξ c Ξ a)) (bind_delay' (ulc_eval c) (fun n : Obs.nf obs_op val_m Ξ => ulc_eval (s_subst Ξ (obs_app (a_id (nf_ty n) (nf_var n)) (nf_obs n) (nf_args n)) Ξ a)))
e: Ξ =[ val_m ]> Ξ
H: Cut t2 (K1 t1 Ο) = Cut t2 (K1 t1 Ο)it_eqF Event.emptyβ (fun _ : T1 => nf_eq) (it_eq_t Event.emptyβ (fun _ : T1 => nf_eq) R) T1_0 (TauF (Structure.iter (fun pat : T1 => let 'T1_0 as x := pat return (state Ξ -> itree Event.emptyβ ((fun _ : T1 => state Ξ) +α΅’ (fun _ : T1 => nf Ξ)) x) in ret_delay β eval_step) T1_0 (Cut (t2 `ββ e) (K1 (t1 `ββ e) (Ο `ββ e))))) (TauF (Structure.subst (fun pat : T1 => let 'T1_0 as x := pat return (Obs.nf obs_op val_m Ξ -> itree Event.emptyβ (fun _ : T1 => Obs.nf obs_op val_m Ξ) x) in fun y : Obs.nf obs_op val_m Ξ => ulc_eval (s_subst Ξ (obs_app (a_id (nf_ty y) (nf_var y)) (nf_obs y) (nf_args y)) Ξ e)) T1_0 (Structure.iter (fun pat : T1 => let 'T1_0 as x := pat return (state Ξ -> itree Event.emptyβ ((fun _ : T1 => state Ξ) +α΅’ (fun _ : T1 => nf Ξ)) x) in ret_delay β eval_step) T1_0 (Cut t2 (K1 t1 Ο)))))Ξ: t_ctx
u: Obs.nf obs_op val_m Ξulc_eval (obs_app (a_id (nf_ty u) (nf_var u)) (nf_obs u) (nf_args u)) β ret_delay uΞ: t_ctx
a: ty
i: Ξ β a
p: obs_op a
Ξ³: dom p =[ val_m ]> Ξulc_eval (obs_app (a_id a i) p (nf_args (i β p β¦ Ξ³ β¦))) β ret_delay (i β p β¦ Ξ³ β¦)Ξ: t_ctx
i: Ξ β β
Ξ³: dom ORet =[ val_m ]> Ξulc_eval (Cut (Val (Ξ³ (β) Ctx.top)) (K0 i)) β ret_delay (i β ORet β¦ Ξ³ β¦)Ξ: t_ctx
i: Ξ β β
Ξ³: dom OApp =[ val_m ]> Ξulc_eval (Cut (Val (Var i)) (K2 (Ξ³ (β) (pop Ctx.top)) (Ξ³ (β) Ctx.top))) β ret_delay (i β OApp β¦ Ξ³ β¦)all: econstructor; intros ? v; do 3 (dependent elimination v; auto).Ξ: t_ctx
i: Ξ β β
Ξ³: dom ORet =[ val_m ]> Ξnf_eq (i β ORet β¦ ! βΆβ Ξ³ (β) Ctx.top β¦) (i β ORet β¦ Ξ³ β¦)Ξ: t_ctx
i: Ξ β β
Ξ³: dom OApp =[ val_m ]> Ξnf_eq (i β OApp β¦ (! βΆβ Ξ³ (β) (pop Ctx.top)) βΆβ Ξ³ (β) Ctx.top β¦) (i β OApp β¦ Ξ³ β¦)well_founded head_inst_nostepx: ty
p: obs xAcc head_inst_nostep (x,' p)forall y : {x : ty & obs x}, head_inst_nostep y (β,' OApp) -> Acc head_inst_nostep yforall y : {x : ty & obs x}, head_inst_nostep y (β,' ORet) -> Acc head_inst_nostep yforall y : {x : ty & obs x}, head_inst_nostep y (β,' OApp) -> Acc head_inst_nostep yz: ty
p: obs z
H: head_inst_nostep (z,' p) (β,' OApp)Acc head_inst_nostep (z,' p)Ξ: t_ctx
v: val_m Ξ (β)
a: dom OApp =[ val_m ]> Ξ
i: Ξ β projT1 (β,' ORet)
t0: Β¬ (is_var v)
i0: evalβ (v β OApp β¦ a β¦) β ret_delay (i β projT2 (β,' ORet))Acc head_inst_nostep (β,' ORet)Ξ: t_ctx
v: val_m Ξ (β)
a: dom OApp =[ val_m ]> Ξ
i: Ξ β projT1 (β,' OApp)
t0: Β¬ (is_var v)
i0: evalβ (v β OApp β¦ a β¦) β ret_delay (i β projT2 (β,' OApp))Acc head_inst_nostep (β,' OApp)all: apply it_eq_step in i0; now inversion i0.Ξ: t_ctx
t1: term (Ξ βΆβ β)
a: dom OApp =[ val_m ]> Ξ
i: Ξ β projT1 (β,' ORet)
t0: Β¬ (is_var (Lam t1))
i0: evalβ (Lam t1 β OApp β¦ a β¦) β ret_delay (i β projT2 (β,' ORet))Acc head_inst_nostep (β,' ORet)Ξ: t_ctx
t1: term (Ξ βΆβ β)
a: dom OApp =[ val_m ]> Ξ
i: Ξ β projT1 (β,' OApp)
t0: Β¬ (is_var (Lam t1))
i0: evalβ (Lam t1 β OApp β¦ a β¦) β ret_delay (i β projT2 (β,' OApp))Acc head_inst_nostep (β,' OApp)forall y : {x : ty & obs x}, head_inst_nostep y (β,' ORet) -> Acc head_inst_nostep yz: ty
p: obs z
H: head_inst_nostep (z,' p) (β,' ORet)Acc head_inst_nostep (z,' p)Ξ: t_ctx
v: ev_ctx Ξ
a: (β β βΆβ β) =[ val_m ]> Ξ
i: cvar Ξ (β)
t0: Β¬ (is_var v)
i0: evalβ (Cut (Val (a (β) Ctx.top)) v) β ret_delay (i β ORet)Acc head_inst_nostep (β,' ORet)Ξ: t_ctx
v: ev_ctx Ξ
a: (β β βΆβ β) =[ val_m ]> Ξ
i: cvar Ξ (β)
t0: Β¬ (is_var v)
i0: evalβ (Cut (Val (a (β) Ctx.top)) v) β ret_delay (i β OApp)Acc head_inst_nostep (β,' OApp)Ξ: t_ctx
t1: term Ξ
e: ev_ctx Ξ
a: (β β βΆβ β) =[ val_m ]> Ξ
i: cvar Ξ (β)
t0: Β¬ (is_var (K1 t1 e))
i0: evalβ (Cut (Val (a (β) Ctx.top)) (K1 t1 e)) β ret_delay (i β ORet)Acc head_inst_nostep (β,' ORet)Ξ: t_ctx
v: val Ξ
e0: ev_ctx Ξ
a: (β β βΆβ β) =[ val_m ]> Ξ
i: cvar Ξ (β)
t0: Β¬ (is_var (K2 v e0))
i0: evalβ (Cut (Val (a (β) Ctx.top)) (K2 v e0)) β ret_delay (i β ORet)Acc head_inst_nostep (β,' ORet)Ξ: t_ctx
v: ev_ctx Ξ
a: (β β βΆβ β) =[ val_m ]> Ξ
i: cvar Ξ (β)
t0: Β¬ (is_var v)
i0: evalβ (Cut (Val (a (β) Ctx.top)) v) β ret_delay (i β OApp)Acc head_inst_nostep (β,' OApp)apply it_eq_step in i0; now inversion i0.Ξ: t_ctx
t1: term Ξ
e: ev_ctx Ξ
a: (β β βΆβ β) =[ val_m ]> Ξ
i: cvar Ξ (β)
t0: Β¬ (is_var (K1 t1 e))
i0: evalβ (Cut (Val (a (β) Ctx.top)) (K1 t1 e)) β ret_delay (i β ORet)Acc head_inst_nostep (β,' ORet)Ξ: t_ctx
v: val Ξ
e0: ev_ctx Ξ
a: (β β βΆβ β) =[ val_m ]> Ξ
i: cvar Ξ (β)
t0: Β¬ (is_var (K2 v e0))
i0: evalβ (Cut (Val (a (β) Ctx.top)) (K2 v e0)) β ret_delay (i β ORet)Acc head_inst_nostep (β,' ORet)Ξ: t_ctx
v: val Ξ
e0: ev_ctx Ξ
i: cvar Ξ (β)
t0: Β¬ (is_var (K2 v e0))
vv: val_m Ξ (β)
i0: evalβ (Cut (Val vv) (K2 v e0)) β ret_delay (i β ORet)Acc head_inst_nostep (β,' ORet)inversion r_rel.Ξ: t_ctx
v: val Ξ
e0: ev_ctx Ξ
i: cvar Ξ (β)
t0: Β¬ (is_var (K2 v e0))
c: Ξ β β
r_rel: eqα΅’ (fun _ : T1 => obs_op β Ξ) T1_0 (c β OApp β¦ (! βΆβ v) βΆβ e0 β¦) (i β ORet)Acc head_inst_nostep (β,' ORet)Ξ: t_ctx
v: ev_ctx Ξ
a: (β β βΆβ β) =[ val_m ]> Ξ
i: cvar Ξ (β)
t0: Β¬ (is_var v)
i0: evalβ (Cut (Val (a (β) Ctx.top)) v) β ret_delay (i β OApp)Acc head_inst_nostep (β,' OApp)Ξ: t_ctx
v: ev_ctx Ξ
a: (β β βΆβ β) =[ val_m ]> Ξ
i: cvar Ξ (β)
t0: Β¬ (is_var v)
i0: evalβ (Cut (Val (a (β) Ctx.top)) v) β ret_delay (i β OApp)
z: ty
p: obs z
H: head_inst_nostep (z,' p) (β,' OApp)Acc head_inst_nostep (z,' p)Ξ: t_ctx
v: ev_ctx Ξ
a: (β β βΆβ β) =[ val_m ]> Ξ
i: cvar Ξ (β)
t0: Β¬ (is_var v)
i0: evalβ (Cut (Val (a (β) Ctx.top)) v) β ret_delay (i β OApp)
Ξ0: t_ctx
v0: val_m Ξ0 (β)
a0: dom OApp =[ val_m ]> Ξ0
i1: Ξ0 β projT1 (β,' ORet)
t1: Β¬ (is_var v0)
i2: evalβ (v0 β OApp β¦ a0 β¦) β ret_delay (i1 β projT2 (β,' ORet))Acc head_inst_nostep (β,' ORet)Ξ: t_ctx
v: ev_ctx Ξ
a: (β β βΆβ β) =[ val_m ]> Ξ
i: cvar Ξ (β)
t0: Β¬ (is_var v)
i0: evalβ (Cut (Val (a (β) Ctx.top)) v) β ret_delay (i β OApp)
Ξ0: t_ctx
v0: val_m Ξ0 (β)
a0: dom OApp =[ val_m ]> Ξ0
i1: Ξ0 β projT1 (β,' OApp)
t1: Β¬ (is_var v0)
i2: evalβ (v0 β OApp β¦ a0 β¦) β ret_delay (i1 β projT2 (β,' OApp))Acc head_inst_nostep (β,' OApp)all: apply it_eq_step in i2; now inversion i2. Qed.Ξ: t_ctx
v: ev_ctx Ξ
a: (β β βΆβ β) =[ val_m ]> Ξ
i: cvar Ξ (β)
t0: Β¬ (is_var v)
i0: evalβ (Cut (Val (a (β) Ctx.top)) v) β ret_delay (i β OApp)
Ξ0: t_ctx
t2: term (Ξ0 βΆβ β)
a0: dom OApp =[ val_m ]> Ξ0
i1: Ξ0 β projT1 (β,' ORet)
t1: Β¬ (is_var (Lam t2))
i2: evalβ (Lam t2 β OApp β¦ a0 β¦) β ret_delay (i1 β projT2 (β,' ORet))Acc head_inst_nostep (β,' ORet)Ξ: t_ctx
v: ev_ctx Ξ
a: (β β βΆβ β) =[ val_m ]> Ξ
i: cvar Ξ (β)
t0: Β¬ (is_var v)
i0: evalβ (Cut (Val (a (β) Ctx.top)) v) β ret_delay (i β OApp)
Ξ0: t_ctx
t2: term (Ξ0 βΆβ β)
a0: dom OApp =[ val_m ]> Ξ0
i1: Ξ0 β projT1 (β,' OApp)
t1: Β¬ (is_var (Lam t2))
i2: evalβ (Lam t2 β OApp β¦ a0 β¦) β ret_delay (i1 β projT2 (β,' OApp))Acc head_inst_nostep (β,' OApp)
Definition subst_eq Ξ {Ξ} : relation (state Ξ) := fun u v => forall Ο : Ξ =[val_m]> Ξ, evalβ (u ββ Ο) β evalβ (v ββ Ο) . Notation "x ββ¦sub Ξ β§β y" := (subst_eq Ξ x y) (at level 10).exact (ogs_correction Ξ x y). Qed.Ξ, Ξ: t_ctx
x, y: state Ξx ββ¦ogs Ξ β§β y -> x ββ¦sub Ξ β§β y
Definition ciu_eq Ξ {Ξ} : relation (term Ξ) := fun u v => forall (Ο : Ξ =[val_m]> Ξ) (Ο : ev_ctx Ξ), evalβ (Cut (u `ββ Ο) Ο) β evalβ (Cut (v `ββ Ο) Ο) . Notation "x ββ¦ciu Ξ β§β y" := (ciu_eq Ξ x y) (at level 10). Definition c_init {Ξ} (t : term Ξ) : state (Ξ βΆβ β) := Cut (t_shift1 t) (K0 Ctx.top) . Definition a_of_sk {Ξ Ξ} (Ο : Ξ =[val_m]> Ξ) (Ο : ev_ctx Ξ) : (Ξ βΆβ β) =[val_m]> Ξ := Ο βΆβ (Ο : val_m _ (β)) .cbn; unfold t_shift1; now rewrite t_sub_ren. Qed.Ξ, Ξ: t_ctx
t: term Ξ
Ο: Ξ =[ val_m ]> Ξ
Ο: ev_ctx ΞCut (t `ββ Ο) Ο = c_init t ββ a_of_sk Ο Ο
We can now obtain a correctness theorem with respect to standard CIU-equivalence by embedding terms into states. Proving that CIU-equivalence entails our substitution equivalence is left to the reader!
Ξ, Ξ: t_ctx
x, y: term Ξc_init x ββ¦ogs Ξ β§β c_init y -> x ββ¦ciu Ξ β§β ynow apply ulc_subst_correct. Qed.Ξ, Ξ: t_ctx
x, y: term Ξ
H: c_init x ββ¦ogs Ξ β§β c_init y
Ο: Ξ =[ val_m ]> Ξ
k: ev_ctx Ξevalβ (c_init x ββ a_of_sk Ο k) β evalβ (c_init y ββ a_of_sk Ο k)
Following a trick by Conor McBride we provide a cool notation for writing terms without any DeBruijn indices, instead leveraging Coq's binders. For this we need a bit of infrastructure, for manipulating terms that only have term variables.
Equations n_ctx : nat -> t_ctx := n_ctx O := β ; n_ctx (S n) := n_ctx n βΆβ β . Notation var' n := (n_ctx n β β). Notation term' n := (term (n_ctx n)). Equations v_emb (n : nat) : var' (S n) := v_emb O := Ctx.top ; v_emb (S n) := pop (v_emb n) . Equations v_lift {n} : var' n -> var' (S n) := @v_lift (S _) Ctx.top := Ctx.top ; @v_lift (S _) (pop i) := pop (v_lift i) .
Here starts the magic.
Equations mk_var (m : nat) : forall n, var' (m + S n) := mk_var O := v_emb ; mk_var (S m) := v_lift β mk_var m . Definition mk_lam {m : nat} (f : (forall n, term' (m + S n)) -> term' (S m)) : term' m := Val (Lam (f (Val β Var β mk_var m))). Arguments mk_lam {_} & _ .
Now a bit of syntactic sugar.
Declare Custom Entry lambda. Notation "β¨ e β¨" := (e : term' 0) (e custom lambda at level 2). Notation "x" := (x _) (in custom lambda at level 0, x ident). Notation "( x )" := x (in custom lambda at level 0, x at level 2). Notation "x y" := (App x y) (in custom lambda at level 1, left associativity). Notation "'Ξ»' x .. y β U" := (mk_lam (fun x => .. (mk_lam (fun y => U)) ..)) (in custom lambda at level 1, x binder, y binder, U at level 2).
Aren't these beautiful?
Definition Delta := β¨ (Ξ» x β x x) β¨ . Definition Omega := β¨ (Ξ» x β x x) (Ξ» x β x x) β¨ . Definition Upsilon := β¨ Ξ» f β (Ξ» x β f (x x)) (Ξ» x β f (x x)) β¨. Definition Theta := β¨ (Ξ» x f β f (x x f)) (Ξ» x f β f (x x f)) β¨.
You can check the actual lambda-term they unwrap to by running eg: