Simply typed lambda calculus
InductiveSimple types#✓fully proved
Given a type \(B\) of base types, the simple types over \(B\) are generated by two rules: every base type \(b \in B\) is a simple type, and for simple types \(A\) and \(C\) the function type \(A \Rightarrow C\) is a simple type.
inductive Ty (Base : Type u) where
| base : Base → Ty Base
| arr : Ty Base → Ty Base → Ty Base
deriving DecidableEq, ReprUsed by 315
InductiveTyped de Bruijn variables of the simply typed lambda calculus#✓fully proved
For a context \(\Gamma\) (a list of simple types) and a simple type \(A\), the variables of type \(A\) in \(\Gamma\) are generated by two rules: the variable \(0\) is a variable of type \(A\) in the context \(A :: \Gamma\) obtained by prepending \(A\) to \(\Gamma\), and if \(x\) is a variable of type \(A\) in \(\Gamma\), then for every simple type \(B\) the successor of \(x\) is a variable of type \(A\) in \(B :: \Gamma\).
inductive Var {Base : Type u} : List (Ty Base) → Ty Base → Type u where
| zero {A : Ty Base} {Γ : List (Ty Base)} : Var (A :: Γ) A
| succ {A B : Ty Base} {Γ : List (Ty Base)} : Var Γ A → Var (B :: Γ) Ainductive Ty (Base : Type u) where
| base : Base → Ty Base
| arr : Ty Base → Ty Base → Ty Base
deriving DecidableEq, ReprCSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Syntax.lean:36
Uses 1 · Used by 154
InductiveIntrinsically typed terms of the simply typed lambda calculus#✓fully proved
Let \(A\) and \(B\) range over simple types and \(\Gamma\) over contexts (lists of simple types); write \(A \Rightarrow B\) for the function type from \(A\) to \(B\) and \(A :: \Gamma\) for the context obtained by prepending \(A\) to \(\Gamma\). The terms of type \(A\) in context \(\Gamma\) are generated by three rules: every variable of type \(A\) in \(\Gamma\) is a term of type \(A\) in context \(\Gamma\); if \(f\) is a term of type \(A \Rightarrow B\) and \(a\) is a term of type \(A\), both in context \(\Gamma\), then the application \(f\,a\) is a term of type \(B\) in context \(\Gamma\); and if \(t\) is a term of type \(B\) in the context \(A :: \Gamma\), then the abstraction \(\lambda t\) is a term of type \(A \Rightarrow B\) in context \(\Gamma\).
inductive Tm {Base : Type u} : List (Ty Base) → Ty Base → Type u where
| var {A : Ty Base} {Γ : List (Ty Base)} : Var Γ A → Tm Γ A
| app {A B : Ty Base} {Γ : List (Ty Base)} : Tm Γ (A ⇒ B) → Tm Γ A → Tm Γ B
| lam {A B : Ty Base} {Γ : List (Ty Base)} : Tm (A :: Γ) B → Tm Γ (A ⇒ B)inductive Ty (Base : Type u) where
| base : Base → Ty Base
| arr : Ty Base → Ty Base → Ty Base
deriving DecidableEq, ReprCSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Syntax.lean:36
inductive Var {Base : Type u} : List (Ty Base) → Ty Base → Type u where
| zero {A : Ty Base} {Γ : List (Ty Base)} : Var (A :: Γ) A
| succ {A B : Ty Base} {Γ : List (Ty Base)} : Var Γ A → Var (B :: Γ) ACSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Syntax.lean:56
Uses 2 · Used by 188
AbbreviationRenamings of simply typed contexts#✓fully proved
For contexts \(\Gamma\) and \(\Delta\) (lists of simple types), a renaming from \(\Gamma\) to \(\Delta\) assigns to every simple type \(A\) and every variable of type \(A\) in \(\Gamma\) a variable of type \(A\) in \(\Delta\).
abbrev Ren {Base : Type u} (Γ Δ : List (Ty Base)) := ∀ {A}, Var Γ A → Var Δ Ainductive Ty (Base : Type u) where
| base : Base → Ty Base
| arr : Ty Base → Ty Base → Ty Base
deriving DecidableEq, ReprCSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Syntax.lean:36
inductive Var {Base : Type u} : List (Ty Base) → Ty Base → Type u where
| zero {A : Ty Base} {Γ : List (Ty Base)} : Var (A :: Γ) A
| succ {A B : Ty Base} {Γ : List (Ty Base)} : Var Γ A → Var (B :: Γ) ACSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Syntax.lean:56
Uses 2 · Used by 44
AbbreviationSimultaneous substitutions of simply typed contexts#✓fully proved
For contexts \(\Gamma\) and \(\Delta\) (lists of simple types), a substitution from \(\Gamma\) to \(\Delta\) assigns to every simple type \(A\) and every variable of type \(A\) in \(\Gamma\) a term of type \(A\) in context \(\Delta\).
abbrev Sub {Base : Type u} (Γ Δ : List (Ty Base)) := ∀ {A}, Var Γ A → Tm Δ Ainductive Ty (Base : Type u) where
| base : Base → Ty Base
| arr : Ty Base → Ty Base → Ty Base
deriving DecidableEq, ReprCSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Syntax.lean:36
inductive Var {Base : Type u} : List (Ty Base) → Ty Base → Type u where
| zero {A : Ty Base} {Γ : List (Ty Base)} : Var (A :: Γ) A
| succ {A B : Ty Base} {Γ : List (Ty Base)} : Var Γ A → Var (B :: Γ) ACSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Syntax.lean:56
inductive Tm {Base : Type u} : List (Ty Base) → Ty Base → Type u where
| var {A : Ty Base} {Γ : List (Ty Base)} : Var Γ A → Tm Γ A
| app {A B : Ty Base} {Γ : List (Ty Base)} : Tm Γ (A ⇒ B) → Tm Γ A → Tm Γ B
| lam {A B : Ty Base} {Γ : List (Ty Base)} : Tm (A :: Γ) B → Tm Γ (A ⇒ B)CSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Syntax.lean:61
Uses 3 · Used by 36
DefinitionIdentity renaming of a simply typed context#✓fully proved
For every context \(\Gamma\), the identity renaming from \(\Gamma\) to \(\Gamma\) sends each variable to itself.
def id : Ren Γ Γ := fun x ↦ xabbrev Ren {Base : Type u} (Γ Δ : List (Ty Base)) := ∀ {A}, Var Γ A → Var Δ ACSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Syntax.lean:71
Uses 3 · Used by 9
DefinitionComposition of renamings of simply typed contexts#✓fully proved
For contexts \(\Gamma\), \(\Delta\) and \(\Xi\), a renaming \(\rho\) from \(\Gamma\) to \(\Delta\) and a renaming \(\sigma\) from \(\Delta\) to \(\Xi\), the composite of \(\rho\) followed by \(\sigma\) is the renaming from \(\Gamma\) to \(\Xi\) that sends each variable \(x\) to \(\sigma(\rho(x))\).
def comp (ρ : Ren Γ Δ) (σ : Ren Δ Ξ) : Ren Γ Ξ := fun x ↦ σ (ρ x)abbrev Ren {Base : Type u} (Γ Δ : List (Ty Base)) := ∀ {A}, Var Γ A → Var Δ ACSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Syntax.lean:71
Uses 3 · Used by 5
DefinitionLifting a renaming under a binder#✓fully proved
Let \(\rho\) be a renaming from a context \(\Gamma\) to a context \(\Delta\) and let \(A\) be a simple type, and write \(A :: \Gamma\) for the context obtained by prepending \(A\) to \(\Gamma\). The lift of \(\rho\) is the renaming from \(A :: \Gamma\) to \(A :: \Delta\) that sends the variable \(0\) to \(0\) and sends the successor of a variable \(x\) of \(\Gamma\) to the successor of \(\rho(x)\).
def lift (ρ : Ren Γ Δ) : Ren (A :: Γ) (A :: Δ)
| _, .zero => .zero
| _, .succ x => .succ (ρ x)abbrev Ren {Base : Type u} (Γ Δ : List (Ty Base)) := ∀ {A}, Var Γ A → Var Δ ACSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Syntax.lean:71
Uses 3 · Used by 30
DefinitionRenaming a simply typed term#✓fully proved
For a renaming \(\rho\) from a context \(\Gamma\) to a context \(\Delta\), the renaming \(t[\rho]\) of a term \(t\) of type \(A\) in context \(\Gamma\) is the term of type \(A\) in context \(\Delta\) defined by recursion on \(t\): \(x[\rho] = \rho(x)\) for a variable \(x\), \((f\,a)[\rho] = f[\rho]\,a[\rho]\) for an application, and \((\lambda s)[\rho] = \lambda (s[\rho^{\uparrow}])\) for an abstraction, where \(\rho^{\uparrow}\) is the lift of \(\rho\) under one binder.
def rename : {Γ Δ : List (Ty Base)} → Ren Γ Δ → {A : Ty Base} → Tm Γ A → Tm Δ A
| _, _, ρ, _, .var x => .var (ρ x)
| _, _, ρ, _, .app f a => .app (rename ρ f) (rename ρ a)
| _, _, ρ, _, .lam body => .lam (rename (Var.lift ρ) body)inductive Ty (Base : Type u) where
| base : Base → Ty Base
| arr : Ty Base → Ty Base → Ty Base
deriving DecidableEq, ReprCSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Syntax.lean:36
abbrev Ren {Base : Type u} (Γ Δ : List (Ty Base)) := ∀ {A}, Var Γ A → Var Δ ACSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Syntax.lean:71
inductive Tm {Base : Type u} : List (Ty Base) → Ty Base → Type u where
| var {A : Ty Base} {Γ : List (Ty Base)} : Var Γ A → Tm Γ A
| app {A B : Ty Base} {Γ : List (Ty Base)} : Tm Γ (A ⇒ B) → Tm Γ A → Tm Γ B
| lam {A B : Ty Base} {Γ : List (Ty Base)} : Tm (A :: Γ) B → Tm Γ (A ⇒ B)CSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Syntax.lean:61
def lift (ρ : Ren Γ Δ) : Ren (A :: Γ) (A :: Δ)
| _, .zero => .zero
| _, .succ x => .succ (ρ x)CSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Syntax.lean:85
Uses 5 · Used by 23
DefinitionWeakening a simply typed term#✓fully proved
For a term \(t\) of type \(A\) in a context \(\Gamma\) and a simple type \(B\), write \(B :: \Gamma\) for the context obtained by prepending \(B\) to \(\Gamma\). The weakening of \(t\) is the term of type \(A\) in the context \(B :: \Gamma\) obtained by renaming \(t\) along the renaming that sends each variable of \(\Gamma\) to its successor in \(B :: \Gamma\).
def weaken (t : Tm Γ A) : Tm (B :: Γ) A := rename .succ tinductive Tm {Base : Type u} : List (Ty Base) → Ty Base → Type u where
| var {A : Ty Base} {Γ : List (Ty Base)} : Var Γ A → Tm Γ A
| app {A B : Ty Base} {Γ : List (Ty Base)} : Tm Γ (A ⇒ B) → Tm Γ A → Tm Γ B
| lam {A B : Ty Base} {Γ : List (Ty Base)} : Tm (A :: Γ) B → Tm Γ (A ⇒ B)CSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Syntax.lean:61
def rename : {Γ Δ : List (Ty Base)} → Ren Γ Δ → {A : Ty Base} → Tm Γ A → Tm Δ A
| _, _, ρ, _, .var x => .var (ρ x)
| _, _, ρ, _, .app f a => .app (rename ρ f) (rename ρ a)
| _, _, ρ, _, .lam body => .lam (rename (Var.lift ρ) body)CSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Syntax.lean:105
Uses 4 · Used by 36
DefinitionIdentity substitution (simply typed lambda calculus)#✓fully proved
For a context \(\Gamma\), the identity substitution from \(\Gamma\) to \(\Gamma\) sends each variable of \(\Gamma\) to the term consisting of that variable alone.
def id : Sub Γ Γ := fun x ↦ .var xabbrev Sub {Base : Type u} (Γ Δ : List (Ty Base)) := ∀ {A}, Var Γ A → Tm Δ ACSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Syntax.lean:74
DefinitionSubstitution induced by a renaming (simply typed lambda calculus)#✓fully proved
For contexts \(\Gamma\) and \(\Delta\) and a type-preserving renaming \(\rho\) from \(\Gamma\) to \(\Delta\), the induced substitution from \(\Gamma\) to \(\Delta\) sends each variable \(x\) of \(\Gamma\) to the term consisting of the variable \(\rho(x)\) alone.
def ofRen (ρ : Ren Γ Δ) : Sub Γ Δ := fun x ↦ .var (ρ x)abbrev Ren {Base : Type u} (Γ Δ : List (Ty Base)) := ∀ {A}, Var Γ A → Var Δ ACSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Syntax.lean:71
abbrev Sub {Base : Type u} (Γ Δ : List (Ty Base)) := ∀ {A}, Var Γ A → Tm Δ ACSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Syntax.lean:74
DefinitionLifting a substitution under a binder (simply typed lambda calculus)#✓fully proved
Write \(A :: \Gamma\) for the context \(\Gamma\) extended by a newest variable of type \(A\). Given a substitution \(\sigma\) from a context \(\Gamma\) to a context \(\Delta\) and a type \(A\), its lift is the substitution from \(A :: \Gamma\) to \(A :: \Delta\) that sends the newest variable to the term consisting of the newest variable alone, and sends the successor of each variable \(x\) of \(\Gamma\) to the weakening of the term \(\sigma(x)\) into the context \(A :: \Delta\).
def lift (σ : Sub Γ Δ) : Sub (A :: Γ) (A :: Δ)
| _, .zero => .var .zero
| _, .succ x => Tm.weaken (σ x)abbrev Sub {Base : Type u} (Γ Δ : List (Ty Base)) := ∀ {A}, Var Γ A → Tm Δ ACSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Syntax.lean:74
def weaken (t : Tm Γ A) : Tm (B :: Γ) A := rename .succ tCSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Syntax.lean:156
Uses 5 · Used by 20
DefinitionSingle-variable substitution (simply typed lambda calculus)#✓fully proved
Write \(A :: \Gamma\) for the context \(\Gamma\) extended by a newest variable of type \(A\). Given a term \(a\) of type \(A\) in context \(\Gamma\), the single-variable substitution for \(a\) is the substitution from \(A :: \Gamma\) to \(\Gamma\) that sends the newest variable to \(a\) and sends the successor of each variable \(x\) of \(\Gamma\) to the term consisting of the variable \(x\) alone.
def single (a : Tm Γ A) : Sub (A :: Γ) Γ
| _, .zero => a
| _, .succ x => .var xinductive Tm {Base : Type u} : List (Ty Base) → Ty Base → Type u where
| var {A : Ty Base} {Γ : List (Ty Base)} : Var Γ A → Tm Γ A
| app {A B : Ty Base} {Γ : List (Ty Base)} : Tm Γ (A ⇒ B) → Tm Γ A → Tm Γ B
| lam {A B : Ty Base} {Γ : List (Ty Base)} : Tm (A :: Γ) B → Tm Γ (A ⇒ B)CSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Syntax.lean:61
abbrev Sub {Base : Type u} (Γ Δ : List (Ty Base)) := ∀ {A}, Var Γ A → Tm Δ ACSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Syntax.lean:74
Uses 4 · Used by 15
DefinitionSimultaneous substitution (simply typed lambda calculus)#✓fully proved
Given a substitution \(\sigma\) from a context \(\Gamma\) to a context \(\Delta\), the result \(t[\sigma]\) of applying \(\sigma\) to a term \(t\) of type \(A\) in context \(\Gamma\) is the term of type \(A\) in context \(\Delta\) defined by recursion on \(t\): \(x[\sigma] = \sigma(x)\) for a variable \(x\), \((f\,a)[\sigma] = f[\sigma]\,a[\sigma]\) for an application, and \((\lambda u)[\sigma] = \lambda\,(u[\sigma'])\) for an abstraction with body \(u\), where \(\sigma'\) is the lift of \(\sigma\) under the binder. Because variables are de Bruijn indices, this substitution is capture-avoiding.
def subst : {Γ Δ : List (Ty Base)} → Sub Γ Δ → {A : Ty Base} → Tm Γ A → Tm Δ A
| _, _, σ, _, .var x => σ x
| _, _, σ, _, .app f a => .app (subst σ f) (subst σ a)
| _, _, σ, _, .lam body => .lam (subst (Sub.lift σ) body)inductive Ty (Base : Type u) where
| base : Base → Ty Base
| arr : Ty Base → Ty Base → Ty Base
deriving DecidableEq, ReprCSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Syntax.lean:36
abbrev Sub {Base : Type u} (Γ Δ : List (Ty Base)) := ∀ {A}, Var Γ A → Tm Δ ACSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Syntax.lean:74
inductive Tm {Base : Type u} : List (Ty Base) → Ty Base → Type u where
| var {A : Ty Base} {Γ : List (Ty Base)} : Var Γ A → Tm Γ A
| app {A B : Ty Base} {Γ : List (Ty Base)} : Tm Γ (A ⇒ B) → Tm Γ A → Tm Γ B
| lam {A B : Ty Base} {Γ : List (Ty Base)} : Tm (A :: Γ) B → Tm Γ (A ⇒ B)CSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Syntax.lean:61
def lift (σ : Sub Γ Δ) : Sub (A :: Γ) (A :: Δ)
| _, .zero => .var .zero
| _, .succ x => Tm.weaken (σ x)CSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Substitution.lean:50
Uses 5 · Used by 26
DefinitionInstantiating a binder body (simply typed lambda calculus)#✓fully proved
Write \(A :: \Gamma\) for the context \(\Gamma\) extended by a newest variable of type \(A\). Given a term \(t\) of type \(B\) in context \(A :: \Gamma\) and a term \(a\) of type \(A\) in context \(\Gamma\), the instantiation of \(t\) with \(a\) is the term of type \(B\) in context \(\Gamma\) obtained by applying to \(t\) the single-variable substitution for \(a\), which replaces the newest variable by \(a\) and leaves the older variables unchanged.
def instantiate (body : Tm (A :: Γ) B) (a : Tm Γ A) : Tm Γ B :=
subst (Sub.single a) bodyinductive Tm {Base : Type u} : List (Ty Base) → Ty Base → Type u where
| var {A : Ty Base} {Γ : List (Ty Base)} : Var Γ A → Tm Γ A
| app {A B : Ty Base} {Γ : List (Ty Base)} : Tm Γ (A ⇒ B) → Tm Γ A → Tm Γ B
| lam {A B : Ty Base} {Γ : List (Ty Base)} : Tm (A :: Γ) B → Tm Γ (A ⇒ B)CSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Syntax.lean:61
def subst : {Γ Δ : List (Ty Base)} → Sub Γ Δ → {A : Ty Base} → Tm Γ A → Tm Δ A
| _, _, σ, _, .var x => σ x
| _, _, σ, _, .app f a => .app (subst σ f) (subst σ a)
| _, _, σ, _, .lam body => .lam (subst (Sub.lift σ) body)CSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Substitution.lean:74
def single (a : Tm Γ A) : Sub (A :: Γ) Γ
| _, .zero => a
| _, .succ x => .var xCSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Substitution.lean:55
Uses 4 · Used by 30
DefinitionExtension of a simply typed substitution#✓fully proved
Given a term \(a\) of type \(A\) in a context \(\Delta\) and a substitution \(\sigma\) from \(\Gamma\) to \(\Delta\), the extension of \(\sigma\) by \(a\) is the substitution from the context \(\Gamma\) extended by a newest variable of type \(A\) to \(\Delta\) that sends the newest variable to \(a\) and each older variable \(x\) of \(\Gamma\) to \(\sigma(x)\).
def cons (a : Tm Δ A) (σ : Sub Γ Δ) : Sub (A :: Γ) Δ
| _, .zero => a
| _, .succ x => σ xinductive Tm {Base : Type u} : List (Ty Base) → Ty Base → Type u where
| var {A : Ty Base} {Γ : List (Ty Base)} : Var Γ A → Tm Γ A
| app {A B : Ty Base} {Γ : List (Ty Base)} : Tm Γ (A ⇒ B) → Tm Γ A → Tm Γ B
| lam {A B : Ty Base} {Γ : List (Ty Base)} : Tm (A :: Γ) B → Tm Γ (A ⇒ B)CSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Syntax.lean:61
abbrev Sub {Base : Type u} (Γ Δ : List (Ty Base)) := ∀ {A}, Var Γ A → Tm Δ ACSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Syntax.lean:74
Uses 4 · Used by 6
DefinitionComposition of simply typed substitutions#✓fully proved
For substitutions \(\sigma\) from a context \(\Gamma\) to \(\Delta\) and \(\tau\) from \(\Delta\) to \(\Xi\), the composite of \(\sigma\) followed by \(\tau\) is the substitution from \(\Gamma\) to \(\Xi\) that sends each variable \(x\) of \(\Gamma\) to the term obtained by applying \(\tau\) to \(\sigma(x)\).
def comp (σ : Sub Γ Δ) (τ : Sub Δ Ξ) : Sub Γ Ξ := fun x ↦ Tm.subst τ (σ x)abbrev Sub {Base : Type u} (Γ Δ : List (Ty Base)) := ∀ {A}, Var Γ A → Tm Δ ACSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Syntax.lean:74
def subst : {Γ Δ : List (Ty Base)} → Sub Γ Δ → {A : Ty Base} → Tm Γ A → Tm Δ A
| _, _, σ, _, .var x => σ x
| _, _, σ, _, .app f a => .app (subst σ f) (subst σ a)
| _, _, σ, _, .lam body => .lam (subst (Sub.lift σ) body)CSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Substitution.lean:74
Uses 4 · Used by 6
TheoremRenaming commutes with weakening for intrinsically typed STLC terms#✓fully proved
Let \(\rho\) be a renaming from the typing context \(\Gamma\) to the typing context \(\Delta\), \(t\) a term of type \(A\) in context \(\Gamma\), and \(B\) a type. Weakening \(t\) by a new newest variable of type \(B\) and then renaming by the lift of \(\rho\) under that variable gives the same term as renaming \(t\) by \(\rho\) and then weakening by a new newest variable of type \(B\).
theorem rename_weaken (ρ : Ren Γ Δ) (t : Tm Γ A) :
rename (Var.lift (A := B) ρ) (weaken (B := B) t) = weaken (B := B) (rename ρ t)abbrev Ren {Base : Type u} (Γ Δ : List (Ty Base)) := ∀ {A}, Var Γ A → Var Δ ACSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Syntax.lean:71
inductive Tm {Base : Type u} : List (Ty Base) → Ty Base → Type u where
| var {A : Ty Base} {Γ : List (Ty Base)} : Var Γ A → Tm Γ A
| app {A B : Ty Base} {Γ : List (Ty Base)} : Tm Γ (A ⇒ B) → Tm Γ A → Tm Γ B
| lam {A B : Ty Base} {Γ : List (Ty Base)} : Tm (A :: Γ) B → Tm Γ (A ⇒ B)CSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Syntax.lean:61
def rename : {Γ Δ : List (Ty Base)} → Ren Γ Δ → {A : Ty Base} → Tm Γ A → Tm Δ A
| _, _, ρ, _, .var x => .var (ρ x)
| _, _, ρ, _, .app f a => .app (rename ρ f) (rename ρ a)
| _, _, ρ, _, .lam body => .lam (rename (Var.lift ρ) body)CSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Syntax.lean:105
def lift (ρ : Ren Γ Δ) : Ren (A :: Γ) (A :: Δ)
| _, .zero => .zero
| _, .succ x => .succ (ρ x)CSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Syntax.lean:85
def weaken (t : Tm Γ A) : Tm (B :: Γ) A := rename .succ tCSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Syntax.lean:156
Uses 8 · Used by 4
TheoremRenaming after substitution in the simply typed calculus#✓fully proved
Let \(\sigma\) be a substitution from \(\Gamma\) to \(\Delta\), \(\rho\) a renaming from \(\Delta\) to \(\Xi\) and \(t\) a term of type \(A\) in \(\Gamma\). Renaming by \(\rho\) the result of applying \(\sigma\) to \(t\) gives the result of applying to \(t\) the substitution that sends each variable \(x\) of \(\Gamma\) to \(\sigma(x)\) renamed by \(\rho\).
theorem rename_subst (ρ : Ren Δ Ξ) (σ : Sub Γ Δ) (t : Tm Γ A) :
rename ρ (subst σ t) = subst (fun x ↦ rename ρ (σ x)) tabbrev Ren {Base : Type u} (Γ Δ : List (Ty Base)) := ∀ {A}, Var Γ A → Var Δ ACSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Syntax.lean:71
abbrev Sub {Base : Type u} (Γ Δ : List (Ty Base)) := ∀ {A}, Var Γ A → Tm Δ ACSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Syntax.lean:74
inductive Tm {Base : Type u} : List (Ty Base) → Ty Base → Type u where
| var {A : Ty Base} {Γ : List (Ty Base)} : Var Γ A → Tm Γ A
| app {A B : Ty Base} {Γ : List (Ty Base)} : Tm Γ (A ⇒ B) → Tm Γ A → Tm Γ B
| lam {A B : Ty Base} {Γ : List (Ty Base)} : Tm (A :: Γ) B → Tm Γ (A ⇒ B)CSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Syntax.lean:61
def rename : {Γ Δ : List (Ty Base)} → Ren Γ Δ → {A : Ty Base} → Tm Γ A → Tm Δ A
| _, _, ρ, _, .var x => .var (ρ x)
| _, _, ρ, _, .app f a => .app (rename ρ f) (rename ρ a)
| _, _, ρ, _, .lam body => .lam (rename (Var.lift ρ) body)CSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Syntax.lean:105
def subst : {Γ Δ : List (Ty Base)} → Sub Γ Δ → {A : Ty Base} → Tm Γ A → Tm Δ A
| _, _, σ, _, .var x => σ x
| _, _, σ, _, .app f a => .app (subst σ f) (subst σ a)
| _, _, σ, _, .lam body => .lam (subst (Sub.lift σ) body)CSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Substitution.lean:74
Uses 11 · Used by 2
TheoremRenaming then substituting an intrinsically typed STLC term#✓fully proved
Let \(\rho\) be a renaming from the typing context \(\Gamma\) to the typing context \(\Delta\), \(\sigma\) a substitution from \(\Delta\) to the typing context \(\Xi\), and \(t\) a term of type \(A\) in context \(\Gamma\). Renaming \(t\) by \(\rho\) and then applying \(\sigma\) gives the same term as applying to \(t\) the substitution that sends each variable \(x\) of \(\Gamma\) to \(\sigma(\rho(x))\).
theorem subst_rename (σ : Sub Δ Ξ) (ρ : Ren Γ Δ) (t : Tm Γ A) :
subst σ (rename ρ t) = subst (fun x ↦ σ (ρ x)) tabbrev Sub {Base : Type u} (Γ Δ : List (Ty Base)) := ∀ {A}, Var Γ A → Tm Δ ACSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Syntax.lean:74
abbrev Ren {Base : Type u} (Γ Δ : List (Ty Base)) := ∀ {A}, Var Γ A → Var Δ ACSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Syntax.lean:71
inductive Tm {Base : Type u} : List (Ty Base) → Ty Base → Type u where
| var {A : Ty Base} {Γ : List (Ty Base)} : Var Γ A → Tm Γ A
| app {A B : Ty Base} {Γ : List (Ty Base)} : Tm Γ (A ⇒ B) → Tm Γ A → Tm Γ B
| lam {A B : Ty Base} {Γ : List (Ty Base)} : Tm (A :: Γ) B → Tm Γ (A ⇒ B)CSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Syntax.lean:61
def subst : {Γ Δ : List (Ty Base)} → Sub Γ Δ → {A : Ty Base} → Tm Γ A → Tm Δ A
| _, _, σ, _, .var x => σ x
| _, _, σ, _, .app f a => .app (subst σ f) (subst σ a)
| _, _, σ, _, .lam body => .lam (subst (Sub.lift σ) body)CSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Substitution.lean:74
def rename : {Γ Δ : List (Ty Base)} → Ren Γ Δ → {A : Ty Base} → Tm Γ A → Tm Δ A
| _, _, ρ, _, .var x => .var (ρ x)
| _, _, ρ, _, .app f a => .app (rename ρ f) (rename ρ a)
| _, _, ρ, _, .lam body => .lam (rename (Var.lift ρ) body)CSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Syntax.lean:105
Uses 10 · Used by 4
TheoremLifted substitution commutes with weakening for intrinsically typed STLC terms#✓fully proved
Let \(\sigma\) be a substitution from the typing context \(\Gamma\) to the typing context \(\Delta\), \(t\) a term of type \(A\) in context \(\Gamma\), and \(B\) a type. Weakening \(t\) by a new newest variable of type \(B\) and then applying the lift of \(\sigma\) under that variable gives the same term as applying \(\sigma\) to \(t\) and then weakening by a new newest variable of type \(B\).
theorem subst_lift_weaken (σ : Sub Γ Δ) (t : Tm Γ A) :
subst (Sub.lift (A := B) σ) (weaken (B := B) t) = weaken (B := B) (subst σ t)abbrev Sub {Base : Type u} (Γ Δ : List (Ty Base)) := ∀ {A}, Var Γ A → Tm Δ ACSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Syntax.lean:74
inductive Tm {Base : Type u} : List (Ty Base) → Ty Base → Type u where
| var {A : Ty Base} {Γ : List (Ty Base)} : Var Γ A → Tm Γ A
| app {A B : Ty Base} {Γ : List (Ty Base)} : Tm Γ (A ⇒ B) → Tm Γ A → Tm Γ B
| lam {A B : Ty Base} {Γ : List (Ty Base)} : Tm (A :: Γ) B → Tm Γ (A ⇒ B)CSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Syntax.lean:61
def subst : {Γ Δ : List (Ty Base)} → Sub Γ Δ → {A : Ty Base} → Tm Γ A → Tm Δ A
| _, _, σ, _, .var x => σ x
| _, _, σ, _, .app f a => .app (subst σ f) (subst σ a)
| _, _, σ, _, .lam body => .lam (subst (Sub.lift σ) body)CSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Substitution.lean:74
def lift (σ : Sub Γ Δ) : Sub (A :: Γ) (A :: Δ)
| _, .zero => .var .zero
| _, .succ x => Tm.weaken (σ x)CSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Substitution.lean:50
def weaken (t : Tm Γ A) : Tm (B :: Γ) A := rename .succ tCSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Syntax.lean:156
Uses 10 · Used by 5
TheoremComposition of substitutions for intrinsically typed STLC terms#✓fully proved
Let \(\sigma\) be a substitution from the typing context \(\Gamma\) to the typing context \(\Delta\), \(\tau\) a substitution from \(\Delta\) to the typing context \(\Xi\), and \(t\) a term of type \(A\) in context \(\Gamma\). Applying \(\sigma\) to \(t\) and then applying \(\tau\) gives the same term as applying to \(t\) the composite substitution, which sends each variable \(x\) of \(\Gamma\) to the result of applying \(\tau\) to \(\sigma(x)\).
theorem subst_subst (σ : Sub Γ Δ) (τ : Sub Δ Ξ) (t : Tm Γ A) :
subst τ (subst σ t) = subst (Sub.comp σ τ) tabbrev Sub {Base : Type u} (Γ Δ : List (Ty Base)) := ∀ {A}, Var Γ A → Tm Δ ACSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Syntax.lean:74
inductive Tm {Base : Type u} : List (Ty Base) → Ty Base → Type u where
| var {A : Ty Base} {Γ : List (Ty Base)} : Var Γ A → Tm Γ A
| app {A B : Ty Base} {Γ : List (Ty Base)} : Tm Γ (A ⇒ B) → Tm Γ A → Tm Γ B
| lam {A B : Ty Base} {Γ : List (Ty Base)} : Tm (A :: Γ) B → Tm Γ (A ⇒ B)CSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Syntax.lean:61
def subst : {Γ Δ : List (Ty Base)} → Sub Γ Δ → {A : Ty Base} → Tm Γ A → Tm Δ A
| _, _, σ, _, .var x => σ x
| _, _, σ, _, .app f a => .app (subst σ f) (subst σ a)
| _, _, σ, _, .lam body => .lam (subst (Sub.lift σ) body)CSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Substitution.lean:74
def comp (σ : Sub Γ Δ) (τ : Sub Δ Ξ) : Sub Γ Ξ := fun x ↦ Tm.subst τ (σ x)CSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/SubstitutionLaws.lean:61
Uses 9 · Used by 2
TheoremRight identity law for composition of substitutions#✓fully proved
For every simultaneous substitution \(\sigma\) from a context \(\Gamma\) to a context \(\Delta\) and every variable \(x\) of type \(A\) in \(\Gamma\), the composite of \(\sigma\) followed by the identity substitution on \(\Delta\) sends \(x\) to \(\sigma(x)\).
@[simp] theorem comp_id_apply (σ : Sub Γ Δ) (x : Var Γ A) :
comp σ (id : Sub Δ Δ) x = σ xabbrev Sub {Base : Type u} (Γ Δ : List (Ty Base)) := ∀ {A}, Var Γ A → Tm Δ ACSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Syntax.lean:74
inductive Var {Base : Type u} : List (Ty Base) → Ty Base → Type u where
| zero {A : Ty Base} {Γ : List (Ty Base)} : Var (A :: Γ) A
| succ {A B : Ty Base} {Γ : List (Ty Base)} : Var Γ A → Var (B :: Γ) ACSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Syntax.lean:56
def comp (σ : Sub Γ Δ) (τ : Sub Δ Ξ) : Sub Γ Ξ := fun x ↦ Tm.subst τ (σ x)CSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/SubstitutionLaws.lean:61
def id : Sub Γ Γ := fun x ↦ .var xCSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Substitution.lean:44
Uses 9
DefinitionRenaming the images of a substitution#✓fully proved
Given a substitution \(\sigma\) from the typing context \(\Gamma\) to the typing context \(\Delta\) and a renaming \(\rho\) from \(\Delta\) to the typing context \(\Xi\), the substitution from \(\Gamma\) to \(\Xi\) obtained by renaming images sends each variable \(x\) of \(\Gamma\) to the renaming of the term \(\sigma(x)\) by \(\rho\).
def rename (σ : Sub Γ Δ) (ρ : Ren Δ Ξ) : Sub Γ Ξ := fun x ↦ Tm.rename ρ (σ x)abbrev Sub {Base : Type u} (Γ Δ : List (Ty Base)) := ∀ {A}, Var Γ A → Tm Δ ACSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Syntax.lean:74
abbrev Ren {Base : Type u} (Γ Δ : List (Ty Base)) := ∀ {A}, Var Γ A → Var Δ ACSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Syntax.lean:71
def rename : {Γ Δ : List (Ty Base)} → Ren Γ Δ → {A : Ty Base} → Tm Γ A → Tm Δ A
| _, _, ρ, _, .var x => .var (ρ x)
| _, _, ρ, _, .app f a => .app (rename ρ f) (rename ρ a)
| _, _, ρ, _, .lam body => .lam (rename (Var.lift ρ) body)CSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Syntax.lean:105
TheoremLifting commutes with renaming substitution images#✓fully proved
Let \(\sigma\) be a substitution from \(\Gamma\) to \(\Delta\) and \(\rho\) a renaming from \(\Delta\) to \(\Xi\). Lift \(\sigma\) under a binder of type \(A\) and rename each of its images by the lift of \(\rho\) under the same binder. At every variable \(x\) of the context \(\Gamma\) extended by a newest variable of type \(A\), this gives the same term as the lift under that binder of the substitution that renames each image of \(\sigma\) by \(\rho\).
theorem rename_lift_apply (σ : Sub Γ Δ) (ρ : Ren Δ Ξ) (x : Var (A :: Γ) B) :
rename (lift σ) (Var.lift ρ) x = lift (rename σ ρ) xabbrev Sub {Base : Type u} (Γ Δ : List (Ty Base)) := ∀ {A}, Var Γ A → Tm Δ ACSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Syntax.lean:74
abbrev Ren {Base : Type u} (Γ Δ : List (Ty Base)) := ∀ {A}, Var Γ A → Var Δ ACSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Syntax.lean:71
inductive Var {Base : Type u} : List (Ty Base) → Ty Base → Type u where
| zero {A : Ty Base} {Γ : List (Ty Base)} : Var (A :: Γ) A
| succ {A B : Ty Base} {Γ : List (Ty Base)} : Var Γ A → Var (B :: Γ) ACSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Syntax.lean:56
def rename (σ : Sub Γ Δ) (ρ : Ren Δ Ξ) : Sub Γ Ξ := fun x ↦ Tm.rename ρ (σ x)CSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/SubstitutionLaws.lean:186
def lift (σ : Sub Γ Δ) : Sub (A :: Γ) (A :: Δ)
| _, .zero => .var .zero
| _, .succ x => Tm.weaken (σ x)CSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Substitution.lean:50
def lift (ρ : Ren Γ Δ) : Ren (A :: Γ) (A :: Δ)
| _, .zero => .zero
| _, .succ x => .succ (ρ x)CSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Syntax.lean:85
Uses 9
TheoremComposing a single substitution with a substitution#✓fully proved
Let \(a\) be a term of type \(A\) in a context \(\Gamma\) and \(\sigma\) a substitution from \(\Gamma\) to \(\Delta\), and write \(a[\sigma]\) for the result of applying \(\sigma\) to \(a\). The composite of the single substitution of \(a\) for the newest variable followed by \(\sigma\) agrees, at every variable \(x\) of the context \(\Gamma\) extended by a newest variable of type \(A\), with the extension of \(\sigma\) that sends the newest variable to \(a[\sigma]\).
theorem comp_single_apply (a : Tm Γ A) (σ : Sub Γ Δ) (x : Var (A :: Γ) B) :
comp (single a) σ x = cons (Tm.subst σ a) σ xinductive Tm {Base : Type u} : List (Ty Base) → Ty Base → Type u where
| var {A : Ty Base} {Γ : List (Ty Base)} : Var Γ A → Tm Γ A
| app {A B : Ty Base} {Γ : List (Ty Base)} : Tm Γ (A ⇒ B) → Tm Γ A → Tm Γ B
| lam {A B : Ty Base} {Γ : List (Ty Base)} : Tm (A :: Γ) B → Tm Γ (A ⇒ B)CSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Syntax.lean:61
abbrev Sub {Base : Type u} (Γ Δ : List (Ty Base)) := ∀ {A}, Var Γ A → Tm Δ ACSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Syntax.lean:74
inductive Var {Base : Type u} : List (Ty Base) → Ty Base → Type u where
| zero {A : Ty Base} {Γ : List (Ty Base)} : Var (A :: Γ) A
| succ {A B : Ty Base} {Γ : List (Ty Base)} : Var Γ A → Var (B :: Γ) ACSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Syntax.lean:56
def comp (σ : Sub Γ Δ) (τ : Sub Δ Ξ) : Sub Γ Ξ := fun x ↦ Tm.subst τ (σ x)CSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/SubstitutionLaws.lean:61
def single (a : Tm Γ A) : Sub (A :: Γ) Γ
| _, .zero => a
| _, .succ x => .var xCSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Substitution.lean:55
def cons (a : Tm Δ A) (σ : Sub Γ Δ) : Sub (A :: Γ) Δ
| _, .zero => a
| _, .succ x => σ xCSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/SubstitutionLaws.lean:51
def subst : {Γ Δ : List (Ty Base)} → Sub Γ Δ → {A : Ty Base} → Tm Γ A → Tm Δ A
| _, _, σ, _, .var x => σ x
| _, _, σ, _, .app f a => .app (subst σ f) (subst σ a)
| _, _, σ, _, .lam body => .lam (subst (Sub.lift σ) body)CSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Substitution.lean:74
Uses 8
TheoremLifting followed by single substitution#✓fully proved
Let \(\sigma\) be a substitution from \(\Gamma\) to \(\Delta\) and \(a\) a term of type \(A\) in \(\Delta\). The composite of the lift of \(\sigma\) under a binder of type \(A\) followed by the single substitution of \(a\) for the newest variable agrees, at every variable \(x\) of the context \(\Gamma\) extended by a newest variable of type \(A\), with the extension of \(\sigma\) that sends the newest variable to \(a\) and each older variable \(y\) to \(\sigma(y)\).
theorem lift_single_apply (σ : Sub Γ Δ) (a : Tm Δ A) (x : Var (A :: Γ) B) :
comp (lift σ) (single a) x = cons a σ xabbrev Sub {Base : Type u} (Γ Δ : List (Ty Base)) := ∀ {A}, Var Γ A → Tm Δ ACSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Syntax.lean:74
inductive Tm {Base : Type u} : List (Ty Base) → Ty Base → Type u where
| var {A : Ty Base} {Γ : List (Ty Base)} : Var Γ A → Tm Γ A
| app {A B : Ty Base} {Γ : List (Ty Base)} : Tm Γ (A ⇒ B) → Tm Γ A → Tm Γ B
| lam {A B : Ty Base} {Γ : List (Ty Base)} : Tm (A :: Γ) B → Tm Γ (A ⇒ B)CSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Syntax.lean:61
inductive Var {Base : Type u} : List (Ty Base) → Ty Base → Type u where
| zero {A : Ty Base} {Γ : List (Ty Base)} : Var (A :: Γ) A
| succ {A B : Ty Base} {Γ : List (Ty Base)} : Var Γ A → Var (B :: Γ) ACSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Syntax.lean:56
def comp (σ : Sub Γ Δ) (τ : Sub Δ Ξ) : Sub Γ Ξ := fun x ↦ Tm.subst τ (σ x)CSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/SubstitutionLaws.lean:61
def lift (σ : Sub Γ Δ) : Sub (A :: Γ) (A :: Δ)
| _, .zero => .var .zero
| _, .succ x => Tm.weaken (σ x)CSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Substitution.lean:50
def single (a : Tm Γ A) : Sub (A :: Γ) Γ
| _, .zero => a
| _, .succ x => .var xCSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Substitution.lean:55
def cons (a : Tm Δ A) (σ : Sub Γ Δ) : Sub (A :: Γ) Δ
| _, .zero => a
| _, .succ x => σ xCSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/SubstitutionLaws.lean:51
Uses 13 · Used by 1
TheoremSingle substitution cancels weakening#✓fully proved
Let \(t\) be a term of type \(A\) in the typing context \(\Gamma\) and \(a\) a term of type \(B\) in context \(\Gamma\). Weakening \(t\) by a new newest variable of type \(B\) and then applying the substitution that replaces the newest variable by \(a\) and leaves every older variable unchanged gives back \(t\).
@[simp] theorem subst_single_weaken (a : Tm Γ B) (t : Tm Γ A) :
subst (Sub.single a) (weaken (B := B) t) = tinductive Tm {Base : Type u} : List (Ty Base) → Ty Base → Type u where
| var {A : Ty Base} {Γ : List (Ty Base)} : Var Γ A → Tm Γ A
| app {A B : Ty Base} {Γ : List (Ty Base)} : Tm Γ (A ⇒ B) → Tm Γ A → Tm Γ B
| lam {A B : Ty Base} {Γ : List (Ty Base)} : Tm (A :: Γ) B → Tm Γ (A ⇒ B)CSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Syntax.lean:61
def subst : {Γ Δ : List (Ty Base)} → Sub Γ Δ → {A : Ty Base} → Tm Γ A → Tm Δ A
| _, _, σ, _, .var x => σ x
| _, _, σ, _, .app f a => .app (subst σ f) (subst σ a)
| _, _, σ, _, .lam body => .lam (subst (Sub.lift σ) body)CSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Substitution.lean:74
def single (a : Tm Γ A) : Sub (A :: Γ) Γ
| _, .zero => a
| _, .succ x => .var xCSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Substitution.lean:55
def weaken (t : Tm Γ A) : Tm (B :: Γ) A := rename .succ tCSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Syntax.lean:156
Uses 11 · Used by 6
TheoremInstantiating a weakened term#✓fully proved
For terms \(b\) of type \(B\) and \(a\) of type \(A\) in a context \(\Gamma\), weakening \(b\) to the context \(\Gamma\) extended by a newest variable of type \(A\) and then instantiating that newest variable by \(a\) gives back \(b\).
@[simp] theorem instantiate_weaken (body : Tm Γ B) (a : Tm Γ A) :
instantiate (weaken (B := A) body) a = bodyinductive Tm {Base : Type u} : List (Ty Base) → Ty Base → Type u where
| var {A : Ty Base} {Γ : List (Ty Base)} : Var Γ A → Tm Γ A
| app {A B : Ty Base} {Γ : List (Ty Base)} : Tm Γ (A ⇒ B) → Tm Γ A → Tm Γ B
| lam {A B : Ty Base} {Γ : List (Ty Base)} : Tm (A :: Γ) B → Tm Γ (A ⇒ B)CSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Syntax.lean:61
def instantiate (body : Tm (A :: Γ) B) (a : Tm Γ A) : Tm Γ B :=
subst (Sub.single a) bodyCSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Substitution.lean:124
def weaken (t : Tm Γ A) : Tm (B :: Γ) A := rename .succ tCSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Syntax.lean:156
TheoremRenaming commutes with instantiation#✓fully proved
Let \(\rho\) be a renaming from \(\Gamma\) to \(\Delta\), \(b\) a term of type \(B\) in the context \(\Gamma\) extended by a newest variable of type \(A\), and \(a\) a term of type \(A\) in \(\Gamma\). Renaming by \(\rho\) the instantiation of the newest variable of \(b\) by \(a\) gives the instantiation of the newest variable of \(b'\) by \(a'\), where \(b'\) is \(b\) renamed by the lift of \(\rho\) under the binder and \(a'\) is \(a\) renamed by \(\rho\).
theorem rename_instantiate (ρ : Ren Γ Δ) (body : Tm (A :: Γ) B) (a : Tm Γ A) :
rename ρ (instantiate body a) =
instantiate (rename (Var.lift ρ) body) (rename ρ a)abbrev Ren {Base : Type u} (Γ Δ : List (Ty Base)) := ∀ {A}, Var Γ A → Var Δ ACSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Syntax.lean:71
inductive Tm {Base : Type u} : List (Ty Base) → Ty Base → Type u where
| var {A : Ty Base} {Γ : List (Ty Base)} : Var Γ A → Tm Γ A
| app {A B : Ty Base} {Γ : List (Ty Base)} : Tm Γ (A ⇒ B) → Tm Γ A → Tm Γ B
| lam {A B : Ty Base} {Γ : List (Ty Base)} : Tm (A :: Γ) B → Tm Γ (A ⇒ B)CSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Syntax.lean:61
def rename : {Γ Δ : List (Ty Base)} → Ren Γ Δ → {A : Ty Base} → Tm Γ A → Tm Δ A
| _, _, ρ, _, .var x => .var (ρ x)
| _, _, ρ, _, .app f a => .app (rename ρ f) (rename ρ a)
| _, _, ρ, _, .lam body => .lam (rename (Var.lift ρ) body)CSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Syntax.lean:105
def instantiate (body : Tm (A :: Γ) B) (a : Tm Γ A) : Tm Γ B :=
subst (Sub.single a) bodyCSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Substitution.lean:124
def lift (ρ : Ren Γ Δ) : Ren (A :: Γ) (A :: Δ)
| _, .zero => .zero
| _, .succ x => .succ (ρ x)CSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Syntax.lean:85
Uses 14
TheoremSubstitution commutes with instantiation for intrinsically typed STLC terms#✓fully proved
Let \(\sigma\) be a substitution from the typing context \(\Gamma\) to the typing context \(\Delta\), \(s\) a term of type \(B\) in the context \(\Gamma\) extended by a newest variable of type \(A\), and \(a\) a term of type \(A\) in context \(\Gamma\). Replacing the newest variable of \(s\) by \(a\) and then applying \(\sigma\) gives the same term as applying the lift of \(\sigma\) to \(s\) and then replacing the newest variable of the result by the term obtained by applying \(\sigma\) to \(a\).
theorem subst_instantiate (σ : Sub Γ Δ) (body : Tm (A :: Γ) B) (a : Tm Γ A) :
subst σ (instantiate body a) =
instantiate (subst (Sub.lift σ) body) (subst σ a)abbrev Sub {Base : Type u} (Γ Δ : List (Ty Base)) := ∀ {A}, Var Γ A → Tm Δ ACSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Syntax.lean:74
inductive Tm {Base : Type u} : List (Ty Base) → Ty Base → Type u where
| var {A : Ty Base} {Γ : List (Ty Base)} : Var Γ A → Tm Γ A
| app {A B : Ty Base} {Γ : List (Ty Base)} : Tm Γ (A ⇒ B) → Tm Γ A → Tm Γ B
| lam {A B : Ty Base} {Γ : List (Ty Base)} : Tm (A :: Γ) B → Tm Γ (A ⇒ B)CSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Syntax.lean:61
def subst : {Γ Δ : List (Ty Base)} → Sub Γ Δ → {A : Ty Base} → Tm Γ A → Tm Δ A
| _, _, σ, _, .var x => σ x
| _, _, σ, _, .app f a => .app (subst σ f) (subst σ a)
| _, _, σ, _, .lam body => .lam (subst (Sub.lift σ) body)CSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Substitution.lean:74
def instantiate (body : Tm (A :: Γ) B) (a : Tm Γ A) : Tm Γ B :=
subst (Sub.single a) bodyCSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Substitution.lean:124
def lift (σ : Sub Γ Δ) : Sub (A :: Γ) (A :: Δ)
| _, .zero => .var .zero
| _, .succ x => Tm.weaken (σ x)CSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Substitution.lean:50
Uses 12
TheoremSubstituting by an extended substitution, via lifting#✓fully proved
Let \(\sigma\) be a substitution from the typing context \(\Gamma\) to the typing context \(\Delta\), \(s\) a term of type \(B\) in the context \(\Gamma\) extended by a newest variable of type \(A\), and \(a\) a term of type \(A\) in context \(\Delta\). Applying to \(s\) the extension of \(\sigma\) that sends the newest variable to \(a\) gives the same term as applying the lift of \(\sigma\) to \(s\) and then replacing the newest variable of the result by \(a\).
theorem subst_cons (σ : Sub Γ Δ) (body : Tm (A :: Γ) B) (a : Tm Δ A) :
subst (Sub.cons a σ) body = instantiate (subst (Sub.lift σ) body) aabbrev Sub {Base : Type u} (Γ Δ : List (Ty Base)) := ∀ {A}, Var Γ A → Tm Δ ACSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Syntax.lean:74
inductive Tm {Base : Type u} : List (Ty Base) → Ty Base → Type u where
| var {A : Ty Base} {Γ : List (Ty Base)} : Var Γ A → Tm Γ A
| app {A B : Ty Base} {Γ : List (Ty Base)} : Tm Γ (A ⇒ B) → Tm Γ A → Tm Γ B
| lam {A B : Ty Base} {Γ : List (Ty Base)} : Tm (A :: Γ) B → Tm Γ (A ⇒ B)CSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Syntax.lean:61
def subst : {Γ Δ : List (Ty Base)} → Sub Γ Δ → {A : Ty Base} → Tm Γ A → Tm Δ A
| _, _, σ, _, .var x => σ x
| _, _, σ, _, .app f a => .app (subst σ f) (subst σ a)
| _, _, σ, _, .lam body => .lam (subst (Sub.lift σ) body)CSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Substitution.lean:74
def cons (a : Tm Δ A) (σ : Sub Γ Δ) : Sub (A :: Γ) Δ
| _, .zero => a
| _, .succ x => σ xCSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/SubstitutionLaws.lean:51
def instantiate (body : Tm (A :: Γ) B) (a : Tm Γ A) : Tm Γ B :=
subst (Sub.single a) bodyCSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Substitution.lean:124
def lift (σ : Sub Γ Δ) : Sub (A :: Γ) (A :: Δ)
| _, .zero => .var .zero
| _, .succ x => Tm.weaken (σ x)CSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Substitution.lean:50
Uses 13 · Used by 1
TheoremInstantiation is substitution by an extended identity#✓fully proved
Let \(b\) be a term of type \(B\) in the context \(\Gamma\) extended by a newest variable of type \(A\), and \(a\) a term of type \(A\) in \(\Gamma\). Instantiating the newest variable of \(b\) by \(a\) gives the same term as applying to \(b\) the substitution that sends the newest variable to \(a\) and each older variable to itself, that is, the extension of the identity substitution on \(\Gamma\) by \(a\).
theorem instantiate_eq_subst_cons (body : Tm (A :: Γ) B) (a : Tm Γ A) :
instantiate body a = subst (Sub.cons a Sub.id) bodyinductive Tm {Base : Type u} : List (Ty Base) → Ty Base → Type u where
| var {A : Ty Base} {Γ : List (Ty Base)} : Var Γ A → Tm Γ A
| app {A B : Ty Base} {Γ : List (Ty Base)} : Tm Γ (A ⇒ B) → Tm Γ A → Tm Γ B
| lam {A B : Ty Base} {Γ : List (Ty Base)} : Tm (A :: Γ) B → Tm Γ (A ⇒ B)CSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Syntax.lean:61
def instantiate (body : Tm (A :: Γ) B) (a : Tm Γ A) : Tm Γ B :=
subst (Sub.single a) bodyCSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Substitution.lean:124
def subst : {Γ Δ : List (Ty Base)} → Sub Γ Δ → {A : Ty Base} → Tm Γ A → Tm Δ A
| _, _, σ, _, .var x => σ x
| _, _, σ, _, .app f a => .app (subst σ f) (subst σ a)
| _, _, σ, _, .lam body => .lam (subst (Sub.lift σ) body)CSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Substitution.lean:74
def cons (a : Tm Δ A) (σ : Sub Γ Δ) : Sub (A :: Γ) Δ
| _, .zero => a
| _, .succ x => σ xCSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/SubstitutionLaws.lean:51
def id : Sub Γ Γ := fun x ↦ .var xCSLibExt/Languages/LambdaCalculus/DeBruijn/Stlc/Substitution.lean:44
Uses 11
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.