def Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.multiApp {Var : Type u} (f : Term Var) : List (Term Var) → Term Var

multiApp f [x₁, x₂, ..., xₙ] applies the arguments x₁, x₂, ..., xₙ to f in left-associative order, i.e. as (((f x₁) x₂) ... xₙ).

Equations

• f.multiApp [] = f
• f.multiApp (a :: as) = (f.multiApp as).app a

inductive Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.ListFullBeta {Var : Type u} : List (Term Var) → List (Term Var) → Prop

A list of arguments performs a single reduction step

[x₁, ..., xᵢ ..., xₙ] ⭢βᶠ [x₁, ..., xᵢ', ..., xₙ]

if one of the arguments performs a single step xᵢ ⭢βᶠ xᵢ' and the rest of the arguments are locally closed.

• step {Var : Type u} {N N' : Term Var} {Ns : List (Term Var)} : N.FullBeta N' → (∀ N ∈ Ns, N.LC) → ListFullBeta (N :: Ns) (N' :: Ns)

  head of the list performs a single reduction step, the rest are locally closed

• cons {Var : Type u} {N : Term Var} {Ns Ns' : List (Term Var)} : N.LC → ListFullBeta Ns Ns' → ListFullBeta (N :: Ns) (N :: Ns')

  given a list that already contains a step, we can add locally closed terms to the front

def Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.«term_⭢Lβᶠ_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.«term_↠Lβᶠ_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.multiApp_lc {Var : Type u} {M : Term Var} {Ns : List (Term Var)} : (M.multiApp Ns).LC ↔ M.LC ∧ ∀ N ∈ Ns, N.LC

A term resulting from a multi-application is locally closed if and only if the leftmost term and all arguments applied to it are locally closed

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.step_multiApp_l {Var : Type u} {M M' : Term Var} {Ns : List (Term Var)} (steps : M.FullBeta M') (lc_Ns : ∀ N ∈ Ns, N.LC) : (M.multiApp Ns).FullBeta (M'.multiApp Ns)

Just like ordinary beta reduction, the left-hand side of a multi-application step is locally closed

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.steps_multiApp_l {Var : Type u} {M M' : Term Var} {Ns : List (Term Var)} (steps : Relation.ReflTransGen FullBeta M M') (lc_Ns : ∀ N ∈ Ns, N.LC) : Relation.ReflTransGen FullBeta (M.multiApp Ns) (M'.multiApp Ns)

Congruence lemma for multi reduction of the left most term of a multi-application

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.step_multiApp_r {Var : Type u} {M : Term Var} {Ns Ns' : List (Term Var)} (steps : ListFullBeta Ns Ns') (lc_M : M.LC) : (M.multiApp Ns).FullBeta (M.multiApp Ns')

Congruence lemma for single reduction of one of the arguments of a multi-application

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.steps_multiApp_r {Var : Type u} {M : Term Var} {Ns Ns' : List (Term Var)} (steps : Relation.ReflTransGen ListFullBeta Ns Ns') (lc_M : M.LC) : Relation.ReflTransGen FullBeta (M.multiApp Ns) (M.multiApp Ns')

Congruence lemma for multiple reduction of one of the arguments of a multi-application

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.invert_abs_multiApp_st {Var : Type u} {Ps : List (Term Var)} {M N Q : Term Var} (h_red : ((M.abs.app N).multiApp Ps).FullBeta Q) : (∃ (M' : Term Var), M.abs.FullBeta M'.abs ∧ Q = (M'.abs.app N).multiApp Ps) ∨ (∃ (N' : Term Var), N.FullBeta N' ∧ Q = (M.abs.app N').multiApp Ps) ∨ (∃ (Ps' : List (Term Var)), ListFullBeta Ps Ps' ∧ Q = (M.abs.app N).multiApp Ps') ∨ Q = (M.open' N).multiApp Ps

If a term (λ M) N P_1 ... P_n reduces in a single step to Q, then Q must be one of the following forms:

Q = (λ M') N P₁ ... Pₙ where M ⭢βᶠ M' or Q = (λ M) N' P₁ ... Pₙ where N ⭢βᶠ N' or Q = (λ M) N P₁' ... Pₙ' where P_i ⭢βᶠ P_i' for some i or Q = (M ^ N) P₁ ... Pₙ

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.invert_abs_multiApp_mst {Var : Type u} {Ps : List (Term Var)} {M N Q : Term Var} (h_red : Relation.ReflTransGen FullBeta ((M.abs.app N).multiApp Ps) Q) : ∃ (M' : Term Var) (N' : Term Var) (Ns' : List (Term Var)), Relation.ReflTransGen FullBeta M.abs M'.abs ∧ Relation.ReflTransGen FullBeta N N' ∧ Relation.ReflTransGen ListFullBeta Ps Ns' ∧ (Q = (M'.abs.app N').multiApp Ns' ∨ Relation.ReflTransGen FullBeta ((M.abs.app N).multiApp Ps) ((M'.open' N').multiApp Ns') ∧ Relation.ReflTransGen FullBeta ((M'.open' N').multiApp Ns') Q)

If a term (λ M) N P₁ ... Pₙ reduces in multiple steps to Q, then either Q if of the form

Q = (λ M') N' P'₁ ... P'ₙ

or

we first reach an intermediate term of this shape,

(λ M) N P₁ ... Pₙ ↠βᶠ (λ M') N' P'₁ ... P'ₙ

then perform a beta reduction and reduce further to Q

(λ M') N' P'₁ ... P'ₙ ↠βᶠ M' ^ N' P'_₁ ... P'_ₙ ↠βᶠ Q

where M ↠βᶠ M' and N ↠βᶠ N' and P_i ↠βᶠ P_i' for all i

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.multiApp_step_lc_r {Var : Type u} {Ns Ns' : List (Term Var)} [DecidableEq Var] [HasFresh Var] (step : ListFullBeta Ns Ns') (N : Term Var) : N ∈ Ns' → N.LC

Just like ordinary beta reduction, the right-hand side of a multi-application step is locally closed

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.multiApp_steps_lc {Var : Type u} {Ns Ns' : List (Term Var)} [DecidableEq Var] [HasFresh Var] (step : Relation.ReflTransGen ListFullBeta Ns Ns') (H : ∀ N ∈ Ns, N.LC) (N : Term Var) : N ∈ Ns' → N.LC

Just like ordinary beta reduction, multiple steps of a argument list preserves local closure