Documentation

Cslib.Languages.LambdaCalculus.Named.Untyped.Properties

λ-calculus #

The untyped λ-calculus, with a named representation of variables. This file contains properties of α-equivalence and capture-avoiding substitution.

Main results #

source
theorem Cslib.LambdaCalculus.Named.Untyped.Term.vars_either_fv_or_bv {Var : Type u} [DecidableEq Var] {m : Term Var} :
m.vars = m.fv ∪ m.bv

A variable in a term is either free or bound.

source
@[simp]
theorem Cslib.LambdaCalculus.Named.Untyped.Term.rename_unused {Var : Type u} [DecidableEq Var] {m : Term Var} {x y : Var} :
x ∉ m.vars → m.rename x y = m

Renaming an unused variable has no effect.

source
@[simp]
theorem Cslib.LambdaCalculus.Named.Untyped.Term.rename_same {Var : Type u} [DecidableEq Var] {m : Term Var} {x : Var} :
m.rename x x = m

Renaming a variable to itself has no effect.

source
theorem Cslib.LambdaCalculus.Named.Untyped.Term.rename_vars_used {Var : Type u} [DecidableEq Var] {m : Term Var} {x y : Var} :
x ∈ m.vars → (m.rename x y).vars = m.vars.erase x ∪ {y}

Renaming a used variable changes the set of variables.

source
theorem Cslib.LambdaCalculus.Named.Untyped.Term.rename_remove {Var : Type u} [DecidableEq Var] {m : Term Var} {x y : Var} :
x ≠ y → x ∉ (m.rename x y).vars

Renaming removes the variable.

source
@[simp]
theorem Cslib.LambdaCalculus.Named.Untyped.Term.rename_vars {Var : Type u} [DecidableEq Var] {m : Term Var} {x y : Var} :
(m.rename x y).vars = m.vars \ {x} ∪ if x ∈ m.vars then {y} else ∅

The set of variables after renaming.

source
theorem Cslib.LambdaCalculus.Named.Untyped.Term.rename_fv {Var : Type u} [DecidableEq Var] {m : Term Var} {x y : Var} :
y ∉ m.vars → (m.rename x y).fv = m.fv \ {x} ∪ if x ∈ m.fv then {y} else ∅

The set of free variables after renaming.

source
@[simp]
theorem Cslib.LambdaCalculus.Named.Untyped.Term.rename_concat {Var : Type u} [DecidableEq Var] {m : Term Var} {x y z : Var} :
y ∉ m.vars → (m.rename x y).rename y z = m.rename x z

Concatenation of renaming.

source
theorem Cslib.LambdaCalculus.Named.Untyped.Term.rename_comm_fresh {Var : Type u} [DecidableEq Var] {m : Term Var} {x y z w : Var} :
x ≠ z → y ∉ m.vars ∪ {x, z} → w ∉ m.vars ∪ {x, z} → (m.rename x y).rename z w = (m.rename z w).rename x y

Commutativity of renaming distinct variables.

source
theorem Cslib.LambdaCalculus.Named.Untyped.Term.rename_comm {Var : Type u} [DecidableEq Var] {m : Term Var} {x y z w : Var} :
y ∉ m.vars ∪ {x, z} → w ∉ m.vars ∪ {x, y, z} → (m.rename x y).rename (if z = x then y else z) w = (m.rename z w).rename x y

Commutativity of renaming.

source
theorem Cslib.LambdaCalculus.Named.Untyped.Term.induction_by_sizeOf {Var : Type u} {C : Term Var → Prop} (step : ∀ (m : Term Var), (∀ (m1 : Term Var), sizeOf m1 < sizeOf m → C m1) → C m) (m : Term Var) :
C m
source
theorem Cslib.LambdaCalculus.Named.Untyped.Term.AlphaEquiv.eq_sizeOf {Var : Type u} [DecidableEq Var] {m n : Term Var} :
m =α n → sizeOf m = sizeOf n

α-equivalent terms have the same size.

source
theorem Cslib.LambdaCalculus.Named.Untyped.Term.AlphaEquiv.same_fv {Var : Type u} [DecidableEq Var] {m n : Term Var} :
m =α n → m.fv = n.fv

α-equivalent terms have the same free variables.

source
theorem Cslib.LambdaCalculus.Named.Untyped.Term.AlphaEquiv.refl {Var : Type u} [DecidableEq Var] [HasFresh Var] (m : Term Var) :
m =α m

Reflexivity of α-equivalence.

source
theorem Cslib.LambdaCalculus.Named.Untyped.Term.AlphaEquiv.symm {Var : Type u} [DecidableEq Var] {m n : Term Var} :
m =α n → n =α m

Symmetry of α-equivalence.

source
theorem Cslib.LambdaCalculus.Named.Untyped.Term.AlphaEquiv.rename_preserve {Var : Type u} [DecidableEq Var] [HasFresh Var] (m n : Term Var) (x y : Var) :
y ∉ m.vars ∪ n.vars → m =α n → (m.rename x y) =α (n.rename x y)

Renaming α-equivalent terms produces α-equivalent terms.

source
theorem Cslib.LambdaCalculus.Named.Untyped.Term.AlphaEquiv.abs_elim {Var : Type u} [DecidableEq Var] [HasFresh Var] {m1 m2 : Term Var} {x1 x2 y : Var} :
y ∉ m1.vars ∪ m2.vars ∪ {x1, x2} → (Term.abs x1 m1) =α (Term.abs x2 m2) → (m1.rename x1 y) =α (m2.rename x2 y)

Elimination rule for α-equivalence of abstractions. It states that if two abstractions are α-equivalent, then their bodies can be renamed to any'' fresh variable y and remain α-equivalent. This is sometimes easier to use than using by_cases on the equivalence, which can only produce the claim for some'' fresh y.

source
theorem Cslib.LambdaCalculus.Named.Untyped.Term.AlphaEquiv.trans {Var : Type u} [DecidableEq Var] [HasFresh Var] {m n p : Term Var} :
m =α n → n =α p → m =α p

Transitivity of α-equivalence.

source
theorem Cslib.LambdaCalculus.Named.Untyped.Term.AlphaEquiv.rename_non_fv {Var : Type u} [DecidableEq Var] [HasFresh Var] {m : Term Var} {x y : Var} :
x ∉ m.fv → y ∉ m.vars → m =α (m.rename x y)

Renaming a non-free variable results in an α-equivalent term

source
theorem Cslib.LambdaCalculus.Named.Untyped.Term.AlphaEquiv.abs_non_fv {Var : Type u} [DecidableEq Var] [HasFresh Var] {m1 m2 : Term Var} {x1 x2 : Var} :
m1 =α m2 → x1 ∉ m1.fv → x2 ∉ m2.fv → (Term.abs x1 m1) =α (Term.abs x2 m2)

Abstracting over an arbitrary non-free variable results in the same term, modulo α-equivalence.

source
theorem Cslib.LambdaCalculus.Named.Untyped.Term.AlphaEquiv.abs_rename {Var : Type u} [DecidableEq Var] [HasFresh Var] {m : Term Var} {x y : Var} :
y ∉ m.vars ∪ {x} → (Term.abs x m) =α (Term.abs y (m.rename x y))

Renaming an abstraction leads to an α-equivalent term.

source
theorem Cslib.LambdaCalculus.Named.Untyped.Term.Context.complete {Var : Type u} (m : Term Var) :
∃ (c : Context Var) (x : Var), m = c.fill (var x)

Any Term can be obtained by filling a Context with a variable. This proves that Context completely captures the syntax of terms.

source
theorem Cslib.LambdaCalculus.Named.Untyped.Term.Context.fill_vars {Var : Type u} [DecidableEq Var] {c : Context Var} {m : Term Var} :
(c.fill m).vars = c.vars ∪ m.vars

The set of variables after filling a context.

source
theorem Cslib.LambdaCalculus.Named.Untyped.Term.AlphaEquiv.context {Var : Type u} [DecidableEq Var] [HasFresh Var] {m n : Term Var} {c : Context Var} :
m =α n → (c.fill m) =α (c.fill n)

α-equivalence is preserved under context filling.

source
theorem Cslib.LambdaCalculus.Named.Untyped.Term.Subst.function_to_relation {Var : Type u} [DecidableEq Var] [HasFresh Var] {m r : Term Var} {x : Var} :
m.Subst x r m[x := r]

The functional definition of substitution satisfies the relational definition of substitution.

source
theorem Cslib.LambdaCalculus.Named.Untyped.Term.subst.non_free {Var : Type u} [DecidableEq Var] [HasFresh Var] {m r : Term Var} {x : Var} :
x ∉ m.fv → m[x := r] =α m

Substituting a non-free variable has no effect.

source
theorem Cslib.LambdaCalculus.Named.Untyped.Term.subst.abs_fresh {Var : Type u} [DecidableEq Var] [HasFresh Var] {m r : Term Var} {x y z : Var} :
z ∉ m.vars ∪ r.vars ∪ {x, y} → (abs y m)[x := r] =α (abs z (m.rename y z)[x := r])

Modulo α-equivalence, substituting an abstraction falls back to the fresh variable case only. With this lemma, the three cases in the definition of subst can be reduced to one.

source
theorem Cslib.LambdaCalculus.Named.Untyped.Term.subst.preserve_AlphaEquiv {Var : Type u} [DecidableEq Var] [HasFresh Var] {m m' r r' : Term Var} {x : Var} :
m =α m' → r =α r' → m[x := r] =α m'[x := r']

Substituting α-equivalent terms produces α-equivalent terms.

source
theorem Cslib.LambdaCalculus.Named.Untyped.Term.Subst.relation_iff_function {Var : Type u} [DecidableEq Var] [HasFresh Var] {m n r : Term Var} {x : Var} :
m.Subst x r n ↔ n =α m[x := r]

The relational definition of substitution coincides with the functional definition of substitution, modulo α-equivalence.

source
theorem Cslib.LambdaCalculus.Named.Untyped.Term.subst.commutativity {Var : Type u} [DecidableEq Var] [HasFresh Var] {m r1 r2 : Term Var} {x y : Var} :
x ∉ r2.fv ∪ {y} → m[x := r1][y := r2] =α m[y := r2][x := r1[y := r2]]

Commutativity of substitution (a.k.a. the substitution lemma)