Type checking for the simply typed lambda calculus

InductiveRaw lambda terms#✓fully proved

Raw terms are extrinsic de Bruijn syntax over a given type of base types: a raw term is either a variable given by a natural-number index \(n\), an application \(f\,a\) of two raw terms \(f\) and \(a\), or a lambda abstraction \(\lambda A.\,t\) consisting of a simple type \(A\) over the base types (the parameter type) and a raw term \(t\) (the body). Variables and applications carry no type information.

inductive RawTm (Base : Type u) where
  | var : Nat → RawTm Base
  | app : RawTm Base → RawTm Base → RawTm Base
  | lam : Ty Base → RawTm Base → RawTm Base
  deriving DecidableEq, Repr

Uses 1 · Used by 54

Statement usesSimple types

Used byVariables captured by a lambda · Closure conversion of a program · Correctness of closure conversion in the empty environment · Flat closure conversion of a program · Correctness of flat closure conversion for closed programs · Flat closure conversion of a closed term is well scoped · Closure conversion of a closed term is well scoped · Closure conversion with accessors · Correctness of closure conversion · Flat closure conversion · Correctness of flat closure conversion · Flat closure conversion preserves scoping · Converted terms are well scoped · Source evaluation is deterministic · Big-step semantics of the closure-conversion source · Accessors implementing the free variables of a term · Flat accessors implement the variables of a closure body · Flat value relation · Free variables one binder deeper · Value relation for closure conversion · Source values of closure conversion · Embedding of raw STLC terms into the calculus with references · Typing is preserved by the embedding of raw STLC terms · Type checking for raw STLC terms · Closed raw terms · Elaboration of raw STLC terms · Completeness of elaboration · Elaboration inverts erasure · Elaboration preserves the input syntax · Soundness of elaboration · Erasure of intrinsically typed terms · Erasure preserves typing · Erasure is injective · Erasure commutes with renaming · Erasure of a weakened term · Free indices of a raw term · Declarative typing of raw terms · Declarative typing agrees with elaboration · Indices occurring in a raw term · Type inference for raw terms · Type inference is sound and complete · Normalization of raw terms · Raw normalization of an erased term · Raw normalization produces well-typed terms · Raw normalization is idempotent · Raw normalization reports the inferred type · Renaming of raw terms · Composition of renamings of raw terms · Agreeing numerical renamings coincide on erased terms · Shifting raw terms · Size of a raw term · Renaming preserves the size of a raw term · Shifting preserves the size of a raw term · Uniqueness of types for raw terms

DefinitionSize of a raw term#✓fully proved

Writing \(|t|\) for the size of a raw term \(t\), the size counts the syntax nodes of \(t\): a variable has size \(1\), an application \(f\,a\) has size \(|f| + |a| + 1\), and a lambda abstraction \(\lambda A.\,t\) has size \(|t| + 1\), so the type annotation \(A\) is not counted.

def size : RawTm Base → Nat
  | .var _ => 1
  | .app f a => f.size + a.size + 1
  | .lam _ body => body.size + 1

Uses 2 · Used by 2

Statement usesRaw lambda terms · Simple types

Used byRenaming preserves the size of a raw term · Shifting preserves the size of a raw term

DefinitionShifting raw terms#✓fully proved

For natural numbers \(k\) (the amount) and \(c\) (the cutoff, \(0\) by default), shifting a raw term by \(k\) at cutoff \(c\) replaces a variable index \(n\) by \(n + k\) if \(c \le n\) and leaves it unchanged otherwise, shifts both sides of an application by \(k\) at cutoff \(c\), and sends \(\lambda A.\,t\) to \(\lambda A.\,t'\), where \(t'\) is \(t\) shifted by \(k\) at cutoff \(c + 1\).

def shift (amount : Nat) (cutoff : Nat := 0) : RawTm Base → RawTm Base
  | .var n => .var (if cutoff ≤ n then n + amount else n)
  | .app f a => .app (f.shift amount cutoff) (a.shift amount cutoff)
  | .lam A body => .lam A (body.shift amount (cutoff + 1))

Uses 2 · Used by 1

Statement usesRaw lambda terms · Simple types

Used byShifting preserves the size of a raw term

DefinitionVariable lookup#✓fully proved

Given a context \(\Gamma\), a list of types, and a natural number \(n\), looking up the de Bruijn index \(n\) in \(\Gamma\) either fails or returns a type \(A\) together with an intrinsic variable of type \(A\) in \(\Gamma\). It is defined by recursion: lookup fails in the empty context; index \(0\) in the context \(A :: \Gamma\), obtained by adding \(A\) at the front of \(\Gamma\), returns \(A\) with the zero variable; and index \(n + 1\) in \(B :: \Gamma\) looks up \(n\) in \(\Gamma\), fails if that fails, and otherwise returns the same type with the successor of the variable found.

def lookupVar : (Γ : List (Ty Base)) → Nat →
    Option (Sigma fun A => Var Γ A)
  | [], _ => none
  | A :: _, 0 => some ⟨A, .zero⟩
  | _ :: Γ, n + 1 => do
      let ⟨A, x⟩ ← lookupVar Γ n
      pure ⟨A, .succ x⟩

Uses 2 · Used by 11

Statement usesSimple types · Typed de Bruijn variables of the simply typed lambda calculus

Used byTyping is preserved by the embedding of raw STLC terms · Elaboration of raw STLC terms · Completeness of elaboration · Elaboration inverts erasure · Elaboration preserves the input syntax · Soundness of elaboration · Erasure preserves typing · Declarative typing of raw terms · Lookup returns a variable with the queried index · Lookup recovers an intrinsic variable from its index · Uniqueness of types for raw terms

DefinitionIndex of a typed variable#✓fully proved

For a context \(\Gamma\) and a type \(A\), a well-typed de Bruijn variable of type \(A\) in \(\Gamma\) is sent to its natural-number index, forgetting its type: the variable for the first entry of the context has index \(0\), and the successor of a variable \(x\) has the index of \(x\) plus \(1\).

def Var.toNat {Base : Type u} {Γ : List (Ty Base)} {A : Ty Base} : Var Γ A → Nat
  | .zero => 0
  | .succ x => x.toNat + 1

Uses 2 · Used by 12

Statement usesSimple types · Typed de Bruijn variables of the simply typed lambda calculus

Used byTyping is preserved by the embedding of raw STLC terms · Agreement of renamings is preserved by composition · Elaboration inverts erasure · Elaboration preserves the input syntax · Erasure of intrinsically typed terms · Erasure preserves typing · Erasure commutes with renaming · Erasure of a weakened term · Agreement of renamings is preserved by lifting · Lookup returns a variable with the queried index · Lookup recovers an intrinsic variable from its index · Agreement of a typed and a numerical renaming

TheoremLookup recovers an intrinsic variable from its index#✓fully proved

For every context \(\Gamma\), type \(A\) and intrinsic variable \(x\) of type \(A\) in \(\Gamma\), looking up the de Bruijn index of \(x\) in \(\Gamma\) succeeds and returns the type \(A\) together with \(x\).

@[simp] theorem lookupVar_toNat {Base : Type u} {Γ : List (Ty Base)} {A : Ty Base}
    (x : Var Γ A) :
    lookupVar Γ x.toNat = some ⟨A, x⟩

Uses 4 · Used by 2

Statement usesSimple types · Typed de Bruijn variables of the simply typed lambda calculus · Index of a typed variable · Variable lookup

Used byElaboration inverts erasure · Erasure preserves typing

TheoremLookup returns a variable with the queried index#✓fully proved

For every context \(\Gamma\) and natural number \(n\), if looking up the de Bruijn index \(n\) in \(\Gamma\) succeeds with a type \(A\) and an intrinsic variable \(x\) of type \(A\) in \(\Gamma\), then the de Bruijn index of \(x\) is \(n\).

theorem lookupVar_result_toNat {Base : Type u} {Γ : List (Ty Base)}
    {n : Nat} {result : Sigma fun A => Var Γ A}
    (h : lookupVar Γ n = some result) : result.2.toNat = n

Uses 4 · Used by 2

Statement usesSimple types · Typed de Bruijn variables of the simply typed lambda calculus · Index of a typed variable · Variable lookup

Used byTyping is preserved by the embedding of raw STLC terms · Elaboration preserves the input syntax

DefinitionErasure of intrinsically typed terms#✓fully proved

The erasure of an intrinsically typed term in a context \(\Gamma\) is the raw term defined by recursion: a variable becomes the raw variable whose index is its position in \(\Gamma\) (counting from \(0\) at the front); an application of \(f\) to \(a\) becomes the raw application of the erasure of \(f\) to the erasure of \(a\); and a lambda with parameter type \(B\) becomes the raw lambda annotated with \(B\) whose body is the erasure of its body. Erasure thus forgets all typing information except the binder annotations.

def Tm.erase {Base : Type u} {Γ : List (Ty Base)} {A : Ty Base} :
    Tm Γ A → RawTm Base
  | .var x => .var x.toNat
  | .app f a => .app f.erase a.erase
  | .lam (A := A) body => .lam A body.erase

Uses 5 · Used by 13

Statement usesRaw lambda terms · Intrinsically typed terms of the simply typed lambda calculus · Simple types · Typed de Bruijn variables of the simply typed lambda calculus · Index of a typed variable

Used byTyping of embedded intrinsically typed STLC terms · Elaboration inverts erasure · Elaboration preserves the input syntax · Erasure preserves typing · Erasure is injective · Erasure commutes with renaming · Erasure of a weakened term · Normalization of raw terms · Raw normalization of an erased term · Raw normalization produces well-typed terms · Raw normalization is idempotent · Raw normalization reports the inferred type · Agreeing numerical renamings coincide on erased terms

AbbreviationChecked terms#✓fully proved

For a context \(\Gamma\) of simple types, a checked term in \(\Gamma\) is a pair \((A, t)\) of a simple type \(A\) and an intrinsically typed term \(t\) of type \(A\) in \(\Gamma\).

A successful elaboration returns such a pair: the inferred type together with an intrinsic term at that type.

abbrev Checked (Base : Type u) (Γ : List (Ty Base)) :=
  Sigma fun A => Tm Γ A

Uses 2 · Used by 13

Statement usesIntrinsically typed terms of the simply typed lambda calculus · Simple types

Used byElaboration of raw STLC terms · Completeness of elaboration · Elaboration inverts erasure · Elaboration preserves the input syntax · Soundness of elaboration · Erasure is injective · Declarative typing agrees with elaboration · Type inference is sound and complete · Normalization of raw terms · Raw normalization of an erased term · Raw normalization produces well-typed terms · Raw normalization is idempotent · Raw normalization reports the inferred type

DefinitionElaboration of raw STLC terms#✓fully proved

Assume equality of base types is decidable. Elaboration in a context \(\Gamma\) of simple types sends a raw term either to failure or to a checked term in \(\Gamma\) (a simple type together with an intrinsically typed term of that type in \(\Gamma\)), by recursion on the raw term. A variable with de Bruijn index \(n\) elaborates to the variable at position \(n\) of \(\Gamma\) (counting from \(0\) at the front), with the type stored there, and fails if \(\Gamma\) has at most \(n\) entries. A lambda with parameter type \(A\) and body \(b\) elaborates \(b\) in \(\Gamma\) extended by \(A\) at the front; if that gives type \(B\), it returns the lambda at type \(A \to B\), and otherwise it fails. An application of \(f\) to \(a\) elaborates \(f\) and \(a\) in \(\Gamma\), and succeeds, returning the application at type \(B\), exactly when \(f\) gets a function type \(A \to B\) and \(a\) gets type \(A\); otherwise it fails.

Cslib.Languages.LambdaCalculus.Stlc.elaborate · 16 lines

def elaborate [DecidableEq Base] (Γ : List (Ty Base)) :
    RawTm Base → Option (Checked Base Γ)
  | .var n => lookupVar Γ n
      |>.map fun ⟨A, x⟩ => ⟨A, .var x⟩
  | .lam A body => do
      let ⟨B, body'⟩ ← elaborate (A :: Γ) body
      pure ⟨A ⇒ B, .lam body'⟩
  | .app f a => do
      let ⟨F, f'⟩ ← elaborate Γ f
      match F, f' with
      | .base _, _ => none
      | A ⇒ B, f' =>
        let ⟨A', a'⟩ ← elaborate Γ a
        if h : A' = A then
          pure ⟨B, .app f' (h ▸ a')⟩
        else none

Uses 6 · Used by 13

Statement usesChecked terms · Raw lambda terms · Intrinsically typed terms of the simply typed lambda calculus · Simple types · Typed de Bruijn variables of the simply typed lambda calculus · Variable lookup

Used byCompleteness of elaboration · Elaboration inverts erasure · Elaboration preserves the input syntax · Soundness of elaboration · Erasure is injective · Declarative typing agrees with elaboration · Type inference for raw terms · Type inference is sound and complete · Normalization of raw terms · Raw normalization of an erased term · Raw normalization produces well-typed terms · Raw normalization is idempotent · Raw normalization reports the inferred type

TheoremElaboration inverts erasure#✓fully proved

Assume equality of base types is decidable. For every intrinsically typed term \(t\) of type \(A\) in context \(\Gamma\), elaborating the erasure of \(t\) in \(\Gamma\) succeeds and returns exactly the pair \((A, t)\). In other words, erasure is a section of elaboration.

@[simp] theorem elaborate_erase [DecidableEq Base] (t : Tm Γ A) :
    elaborate (Base := Base) Γ t.erase = some ⟨A, t⟩

Uses 10 · Used by 3

Statement usesChecked terms · Intrinsically typed terms of the simply typed lambda calculus · Erasure of intrinsically typed terms · Simple types · Elaboration of raw STLC terms

Proof usesRaw lambda terms · Typed de Bruijn variables of the simply typed lambda calculus · Index of a typed variable · Variable lookup · Lookup recovers an intrinsic variable from its index

Used byErasure is injective · Raw normalization of an erased term · Raw normalization is idempotent

TheoremElaboration preserves the input syntax#✓fully proved

Assume equality of base types is decidable. If elaborating a raw term \(r\) in context \(\Gamma\) succeeds with type \(A\) and intrinsically typed term \(t\), then the erasure of \(t\) is exactly \(r\).

theorem elaborate_faithful [DecidableEq Base] {raw : RawTm Base}
    {t : Tm Γ A} (h : elaborate Γ raw = some ⟨A, t⟩) :
    t.erase = raw

Uses 10

Statement usesChecked terms · Raw lambda terms · Intrinsically typed terms of the simply typed lambda calculus · Erasure of intrinsically typed terms · Simple types · Elaboration of raw STLC terms

Proof usesTyped de Bruijn variables of the simply typed lambda calculus · Index of a typed variable · Variable lookup · Lookup returns a variable with the queried index

TheoremErasure is injective#✓fully proved

For a fixed context \(\Gamma\) and type \(A\), erasure is injective on intrinsically typed terms of type \(A\) in \(\Gamma\): two such terms with the same erasure are equal.

theorem Tm.erase_injective :
    Function.Injective (@Tm.erase Base Γ A)

Uses 7

Statement usesRaw lambda terms · Intrinsically typed terms of the simply typed lambda calculus · Erasure of intrinsically typed terms · Simple types

Proof usesChecked terms · Elaboration of raw STLC terms · Elaboration inverts erasure

InductiveDeclarative typing of raw terms#✓fully proved

For a context \(\Gamma\) (a list of simple types), a raw term \(t\) and a type \(A\), the judgment \(\Gamma \vdash t : A\) is the least relation closed under three rules. A variable with de Bruijn index \(n\) has type \(A\) in \(\Gamma\) whenever looking up \(n\) in \(\Gamma\) succeeds with the type \(A\) and some intrinsic variable of type \(A\). If \(\Gamma \vdash f : A \Rightarrow B\) and \(\Gamma \vdash a : A\), then the application \(f\,a\) has type \(B\) in \(\Gamma\). If \(A :: \Gamma \vdash b : B\), where \(A :: \Gamma\) is \(\Gamma\) with \(A\) added at the front, then the abstraction \(\lambda{:}A.\,b\) with parameter type \(A\) has type \(A \Rightarrow B\) in \(\Gamma\).

inductive HasType : (Γ : List (Ty Base)) → RawTm Base → Ty Base → Prop where
  | var {Γ : List (Ty Base)} {A : Ty Base} {n : Nat} {x : Var Γ A}
      (h : lookupVar Γ n = some ⟨A, x⟩) : HasType Γ (.var n) A
  | app {Γ : List (Ty Base)} {A B : Ty Base} {f a : RawTm Base} :
      HasType Γ f (A ⇒ B) → HasType Γ a A → HasType Γ (.app f a) B
  | lam {Γ : List (Ty Base)} {A B : Ty Base} {body : RawTm Base} :
      HasType (A :: Γ) body B → HasType Γ (.lam A body) (A ⇒ B)

Uses 4 · Used by 8

Statement usesRaw lambda terms · Simple types · Typed de Bruijn variables of the simply typed lambda calculus · Variable lookup

Used byTyping is preserved by the embedding of raw STLC terms · Completeness of elaboration · Soundness of elaboration · Erasure preserves typing · Declarative typing agrees with elaboration · Type inference is sound and complete · Raw normalization produces well-typed terms · Uniqueness of types for raw terms

TheoremErasure preserves typing#✓fully proved

For every intrinsically typed term \(t\) of type \(A\) in context \(\Gamma\), the erasure of \(t\) has type \(A\) in \(\Gamma\) under the declarative typing judgment for raw terms.

theorem erase (t : Tm Γ A) : HasType Γ t.erase A

Uses 9 · Used by 2

Statement usesDeclarative typing of raw terms · Intrinsically typed terms of the simply typed lambda calculus · Erasure of intrinsically typed terms · Simple types

Proof usesRaw lambda terms · Typed de Bruijn variables of the simply typed lambda calculus · Index of a typed variable · Variable lookup · Lookup recovers an intrinsic variable from its index

Used byTyping of embedded intrinsically typed STLC terms · Raw normalization produces well-typed terms

TheoremUniqueness of types for raw terms#✓fully proved

Let \(\Gamma\) be a context of simple types and \(r\) a raw term. If \(r\) has type \(A\) in \(\Gamma\) and \(r\) has type \(B\) in \(\Gamma\) under the declarative typing judgment for raw terms, then \(A = B\).

theorem unique {raw : RawTm Base} (hA : HasType Γ raw A)
    (hB : HasType Γ raw B) : A = B

Uses 5

Statement usesDeclarative typing of raw terms · Raw lambda terms · Simple types

Proof usesTyped de Bruijn variables of the simply typed lambda calculus · Variable lookup

TheoremCompleteness of elaboration#✓fully proved

Assume equality of base types is decidable. If a raw term \(r\) has type \(A\) in context \(\Gamma\) under the declarative typing judgment, then elaborating \(r\) in \(\Gamma\) succeeds and returns the type \(A\) together with some intrinsically typed term of type \(A\) in \(\Gamma\).

theorem elaborate_complete [DecidableEq Base] {raw : RawTm Base}
    (h : HasType Γ raw A) :
    ∃ t : Tm Γ A, elaborate Γ raw = some ⟨A, t⟩

Uses 8 · Used by 2

Statement usesChecked terms · Declarative typing of raw terms · Raw lambda terms · Intrinsically typed terms of the simply typed lambda calculus · Simple types · Elaboration of raw STLC terms

Proof usesTyped de Bruijn variables of the simply typed lambda calculus · Variable lookup

Used byDeclarative typing agrees with elaboration · Type inference is sound and complete

TheoremSoundness of elaboration#✓fully proved

Assume equality of base types is decidable. If elaborating a raw term \(r\) in context \(\Gamma\) succeeds with type \(A\) (and some intrinsically typed term of type \(A\) in \(\Gamma\)), then \(r\) has type \(A\) in \(\Gamma\) under the declarative typing judgment.

theorem elaborate_sound [DecidableEq Base] {raw : RawTm Base} {t : Tm Γ A}
    (h : elaborate Γ raw = some ⟨A, t⟩) : HasType Γ raw A

Uses 8 · Used by 2

Statement usesChecked terms · Declarative typing of raw terms · Raw lambda terms · Intrinsically typed terms of the simply typed lambda calculus · Simple types · Elaboration of raw STLC terms

Proof usesTyped de Bruijn variables of the simply typed lambda calculus · Variable lookup

Used byDeclarative typing agrees with elaboration · Type inference is sound and complete

TheoremDeclarative typing agrees with elaboration#✓fully proved

Assume equality of base types is decidable. For every context \(\Gamma\), raw term \(t\) and type \(A\), the declarative typing judgment \(\Gamma \vdash t : A\) holds if and only if there is an intrinsically typed term \(u\) of type \(A\) in context \(\Gamma\) such that elaborating \(t\) in \(\Gamma\) succeeds and returns the type \(A\) together with \(u\).

theorem iff_elaborates [DecidableEq Base] {raw : RawTm Base} :
    HasType Γ raw A ↔ ∃ t : Tm Γ A, elaborate Γ raw = some ⟨A, t⟩

Uses 8

Statement usesChecked terms · Declarative typing of raw terms · Raw lambda terms · Intrinsically typed terms of the simply typed lambda calculus · Simple types · Elaboration of raw STLC terms

Proof usesCompleteness of elaboration · Soundness of elaboration

DefinitionType inference for raw terms#✓fully proved

Assume equality of base types is decidable. Given a context \(\Gamma\) and a raw term \(t\), type inference elaborates \(t\) in \(\Gamma\); if elaboration succeeds, it returns the type component of the result and forgets the intrinsically typed term, and if elaboration fails, inference fails.

def infer [DecidableEq Base] (Γ : List (Ty Base)) (raw : RawTm Base) :
    Option (Ty Base) :=
  (elaborate Γ raw).map Sigma.fst

Uses 4 · Used by 3

Statement usesRaw lambda terms · Intrinsically typed terms of the simply typed lambda calculus · Simple types · Elaboration of raw STLC terms

Used byType checking for raw STLC terms · Type inference is sound and complete · Raw normalization reports the inferred type

TheoremType inference is sound and complete#✓fully proved

Assume equality of base types is decidable. For every context \(\Gamma\), raw term \(t\) and type \(A\), type inference for \(t\) in \(\Gamma\) returns \(A\) if and only if the declarative typing judgment \(\Gamma \vdash t : A\) holds.

theorem infer_eq_some_iff [DecidableEq Base] {raw : RawTm Base} :
    infer Γ raw = some A ↔ HasType Γ raw A

Uses 9

Statement usesDeclarative typing of raw terms · Raw lambda terms · Simple types · Type inference for raw terms

Proof usesChecked terms · Completeness of elaboration · Soundness of elaboration · Intrinsically typed terms of the simply typed lambda calculus · Elaboration of raw STLC terms

DefinitionType checking for raw STLC terms#✓fully proved

Assume equality of base types is decidable. Given a context \(\Gamma\) (a list of simple types), a raw term \(r\) and a simple type \(A\), the type checker returns true exactly when type inference for \(r\) in \(\Gamma\) returns the type \(A\), and false otherwise.

def check [DecidableEq Base] (Γ : List (Ty Base))
    (raw : RawTm Base) (A : Ty Base) : Bool :=
  infer Γ raw == some A

Uses 3

Statement usesRaw lambda terms · Simple types · Type inference for raw terms

DefinitionNormalization of raw terms#✓fully proved

Let the base types have decidable equality. Given a context \(\Gamma\) of simple types and a raw term \(r\), raw normalization elaborates \(r\) in \(\Gamma\). If elaboration fails, raw normalization fails. If elaboration returns a type \(A\) and an intrinsically typed term \(t\) of type \(A\), raw normalization returns \(A\) together with the erasure to a raw term of the normal form of \(t\) computed by normalization by evaluation.

def normalizeRaw [DecidableEq Base] (Γ : List (Ty Base))
    (raw : RawTm Base) : Option (Sigma fun _ : Ty Base => RawTm Base) := do
  let ⟨A, t⟩ ← elaborate Γ raw
  pure ⟨A, (normalizeTm t).erase⟩

Uses 7 · Used by 4

Statement usesChecked terms · Raw lambda terms · Intrinsically typed terms of the simply typed lambda calculus · Erasure of intrinsically typed terms · Simple types · Elaboration of raw STLC terms · Normalization of terms

Used byRaw normalization of an erased term · Raw normalization produces well-typed terms · Raw normalization is idempotent · Raw normalization reports the inferred type

TheoremRaw normalization of an erased term#✓fully proved

Assume equality of base types is decidable. For every intrinsically typed term \(t\) of type \(A\) in context \(\Gamma\), raw normalization of the erasure of \(t\) in \(\Gamma\) succeeds and returns the type \(A\) together with the erasure of the normal form of \(t\) computed by normalization by evaluation.

@[simp] theorem normalizeRaw_erase [DecidableEq Base] (t : Tm Γ A) :
    normalizeRaw (Base := Base) Γ t.erase = some ⟨A, (normalizeTm t).erase⟩

Uses 11

Statement usesRaw lambda terms · Intrinsically typed terms of the simply typed lambda calculus · Erasure of intrinsically typed terms · Simple types · Normalization of raw terms · Normalization of terms

Proof usesChecked terms · Typed de Bruijn variables of the simply typed lambda calculus · Elaboration of raw STLC terms · Elaboration inverts erasure · Normalization by evaluation

TheoremRaw normalization reports the inferred type#✓fully proved

Let the base types have decidable equality, let \(\Gamma\) be a context of simple types and let \(r\) be a raw term. If normalizing \(r\) in \(\Gamma\) succeeds and returns a type \(A\) together with a raw term, then type inference for \(r\) in \(\Gamma\) returns \(A\).

theorem normalizeRaw_type [DecidableEq Base] {raw normalized : RawTm Base}
    (h : normalizeRaw Γ raw = some ⟨A, normalized⟩) :
    infer Γ raw = some A

Uses 11

Statement usesRaw lambda terms · Simple types · Type inference for raw terms · Normalization of raw terms

Proof usesChecked terms · Intrinsically typed terms of the simply typed lambda calculus · Erasure of intrinsically typed terms · Typed de Bruijn variables of the simply typed lambda calculus · Elaboration of raw STLC terms · Normalization by evaluation · Normalization of terms

TheoremRaw normalization produces well-typed terms#✓fully proved

Assume equality of base types is decidable. For every context \(\Gamma\) and raw term \(t\), if raw normalization of \(t\) in \(\Gamma\) succeeds with a type \(A\) and a raw term \(t'\), then the declarative typing judgment \(\Gamma \vdash t' : A\) holds.

theorem normalizeRaw_hasType [DecidableEq Base] {raw normalized : RawTm Base}
    (h : normalizeRaw Γ raw = some ⟨A, normalized⟩) :
    HasType Γ normalized A

Uses 12

Statement usesDeclarative typing of raw terms · Raw lambda terms · Simple types · Normalization of raw terms

Proof usesChecked terms · Erasure preserves typing · Intrinsically typed terms of the simply typed lambda calculus · Erasure of intrinsically typed terms · Typed de Bruijn variables of the simply typed lambda calculus · Elaboration of raw STLC terms · Normalization by evaluation · Normalization of terms

TheoremRaw normalization is idempotent#✓fully proved

Assume equality of base types is decidable. For every context \(\Gamma\) and raw term \(t\), if raw normalization of \(t\) in \(\Gamma\) succeeds with a type \(A\) and a raw term \(t'\), then raw normalization of \(t'\) in \(\Gamma\) succeeds with the same type \(A\) and the same term \(t'\).

theorem normalizeRaw_idempotent [DecidableEq Base]
    {raw normalized : RawTm Base}
    (h : normalizeRaw Γ raw = some ⟨A, normalized⟩) :
    normalizeRaw Γ normalized = some ⟨A, normalized⟩

Uses 12

Statement usesRaw lambda terms · Simple types · Normalization of raw terms

Proof usesChecked terms · Intrinsically typed terms of the simply typed lambda calculus · Erasure of intrinsically typed terms · Typed de Bruijn variables of the simply typed lambda calculus · Elaboration of raw STLC terms · Elaboration inverts erasure · Normalization by evaluation · Normal forms are fixed points of normalization · Normalization of terms

DefinitionLifting a numerical renaming#✓fully proved

Given a renaming \(\rho : \mathbb{N} \to \mathbb{N}\) of de Bruijn indices, its lift through one binder is the map \(\mathbb{N} \to \mathbb{N}\) sending \(0\) to \(0\) and \(n + 1\) to \(\rho(n) + 1\).

def liftRen (ρ : Nat → Nat) : Nat → Nat
  | 0 => 0
  | n + 1 => ρ n + 1

Used by 6

Used byErasure commutes with renaming · Agreement of renamings is preserved by lifting · Lifting commutes with composition of numerical renamings · Renaming of raw terms · Composition of renamings of raw terms · Renaming preserves the size of a raw term

DefinitionRenaming of raw terms#✓fully proved

Given a map \(\rho : \mathbb{N} \to \mathbb{N}\) on de Bruijn indices, renaming a raw term by \(\rho\) replaces each variable \(n\) by \(\rho(n)\), renames both parts of an application by \(\rho\), and renames the body of a lambda abstraction, keeping its parameter type, by the lifted map \(\rho'\) given by \(\rho'(0) = 0\) and \(\rho'(n + 1) = \rho(n) + 1\).

def rename (ρ : Nat → Nat) : RawTm Base → RawTm Base
  | .var n => .var (ρ n)
  | .app f a => RawTm.app (rename ρ f) (rename ρ a)
  | .lam A body => RawTm.lam A (rename (liftRen ρ) body)

Uses 3 · Used by 5

Statement usesRaw lambda terms · Lifting a numerical renaming · Simple types

Used byErasure commutes with renaming · Erasure of a weakened term · Composition of renamings of raw terms · Agreeing numerical renamings coincide on erased terms · Renaming preserves the size of a raw term

TheoremLifting commutes with composition of numerical renamings#✓fully proved

For maps \(\rho, \sigma : \mathbb{N} \to \mathbb{N}\), the lift of \(\sigma \circ \rho\) through one binder equals the lift of \(\sigma\) composed after the lift of \(\rho\).

theorem liftRen_comp (ρ σ : Nat → Nat) :
    liftRen (σ ∘ ρ) = liftRen σ ∘ liftRen ρ

Uses 1 · Used by 1

Statement usesLifting a numerical renaming

Used byComposition of renamings of raw terms

TheoremComposition of renamings of raw terms#✓fully proved

For all maps \(\rho, \sigma : \mathbb{N} \to \mathbb{N}\) and every raw term \(t\), renaming \(t\) by \(\rho\) and then renaming the result by \(\sigma\) gives the same raw term as renaming \(t\) by the composite \(\sigma \circ \rho\).

theorem rename_comp (ρ σ : Nat → Nat) (t : RawTm Base) :
    rename σ (rename ρ t) = rename (σ ∘ ρ) t

Uses 5

Statement usesRaw lambda terms · Renaming of raw terms

Proof usesLifting a numerical renaming · Lifting commutes with composition of numerical renamings · Simple types

TheoremRenaming preserves the size of a raw term#✓fully proved

For every map \(\rho : \mathbb{N} \to \mathbb{N}\) and every raw term \(t\), the renaming of \(t\) by \(\rho\) has the same number of syntax nodes as \(t\).

@[simp] theorem size_rename (ρ : Nat → Nat) (t : RawTm Base) :
    (rename ρ t).size = t.size

Uses 5

Statement usesRaw lambda terms · Renaming of raw terms · Size of a raw term

Proof usesLifting a numerical renaming · Simple types

TheoremShifting preserves the size of a raw term#✓fully proved

For all natural numbers \(k\) and \(c\) and every raw term \(t\), shifting \(t\) by \(k\) at cutoff \(c\) (adding \(k\) to each variable index that is at least the cutoff, which grows by one under each binder) gives a raw term with the same number of syntax nodes as \(t\).

@[simp] theorem size_shift (amount cutoff : Nat) (t : RawTm Base) :
    (t.shift amount cutoff).size = t.size

Uses 4

Statement usesRaw lambda terms · Shifting raw terms · Size of a raw term

Proof usesSimple types

DefinitionIndices occurring in a raw term#✓fully proved

The list of de Bruijn indices of a raw term, read from left to right with repetitions: a variable with index \(n\) gives \([n]\), an application gives the indices of the function followed by those of the argument, and a lambda abstraction gives the indices of its body, unshifted.

Bound occurrences are intentionally included, so this list is useful for diagnostics rather than for scoping.

def indices : RawTm Base → List Nat
  | .var n => [n]
  | .app f a => indices f ++ indices a
  | .lam _ body => indices body

Uses 2

Statement usesRaw lambda terms · Simple types

DefinitionFree indices of a raw term#✓fully proved

For a binder depth \(d\) and a raw term \(t\), the free indices of \(t\) at depth \(d\) form a list defined by recursion on \(t\): a variable with index \(n\) contributes \([n - d]\) if \(d \le n\) and the empty list otherwise; an application contributes the free indices of the function followed by those of the argument, both at depth \(d\); and a lambda abstraction contributes the free indices of its body at depth \(d + 1\).

def freeIndices : Nat → RawTm Base → List Nat
  | depth, .var n => if depth ≤ n then [n - depth] else []
  | depth, .app f a => freeIndices depth f ++ freeIndices depth a
  | depth, .lam _ body => freeIndices (depth + 1) body

Uses 2 · Used by 10

Statement usesRaw lambda terms · Simple types

Used byVariables captured by a lambda · Correctness of flat closure conversion for closed programs · Flat closure conversion of a closed term is well scoped · Correctness of flat closure conversion · Flat closure conversion preserves scoping · Converted terms are well scoped · Accessors implementing the free variables of a term · Flat accessors implement the variables of a closure body · Free variables one binder deeper · Closed raw terms

DefinitionClosed raw terms#✓fully proved

A raw term \(t\) is closed when its list of free indices at binder depth \(0\) is empty.

def Closed (t : RawTm Base) : Prop := freeIndices 0 t = []

Uses 2 · Used by 3

Statement usesRaw lambda terms · Free indices of a raw term

Used byCorrectness of flat closure conversion for closed programs · Flat closure conversion of a closed term is well scoped · Closure conversion of a closed term is well scoped

DefinitionAgreement of a typed and a numerical renaming#✓fully proved

A typed renaming \(\rho\) from context \(\Gamma\) to context \(\Delta\) agrees with a map \(r : \mathbb{N} \to \mathbb{N}\) when, for every type \(A\) and every variable \(x\) of type \(A\) in \(\Gamma\), the de Bruijn index of \(\rho(x)\) equals \(r\) applied to the de Bruijn index of \(x\).

def RenAgrees (ρ : Ren Γ Δ) (r : Nat → Nat) : Prop :=
  ∀ {A} (x : Var Γ A), (ρ x).toNat = r x.toNat

Uses 4 · Used by 4

Statement usesRenamings of simply typed contexts · Simple types · Typed de Bruijn variables of the simply typed lambda calculus · Index of a typed variable

Used byAgreement of renamings is preserved by composition · Erasure commutes with renaming · Agreement of renamings is preserved by lifting · Agreeing numerical renamings coincide on erased terms

TheoremAgreement of renamings is preserved by lifting#✓fully proved

Let \(\rho\) be a typed renaming from context \(\Gamma\) to \(\Delta\) and let \(r : \mathbb{N} \to \mathbb{N}\) be a numerical renaming that agrees with \(\rho\). Then for every type \(A\), the lift of \(\rho\) under a binder of type \(A\) agrees with the lift of \(r\) through one binder.

theorem RenAgrees.lift {ρ : Ren Γ Δ} {r : Nat → Nat} (h : RenAgrees ρ r) :
    RenAgrees (Var.lift (A := A) ρ) (RawTm.liftRen r)

Uses 7 · Used by 1

Statement usesLifting a numerical renaming · Renamings of simply typed contexts · Agreement of a typed and a numerical renaming · Simple types · Lifting a renaming under a binder

Proof usesTyped de Bruijn variables of the simply typed lambda calculus · Index of a typed variable

Used byErasure commutes with renaming

TheoremAgreement of renamings is preserved by composition#✓fully proved

Let \(\rho\) be a typed renaming from context \(\Gamma\) to \(\Delta\), let \(\sigma\) be a typed renaming from \(\Delta\) to \(\Xi\), and let \(r, s : \mathbb{N} \to \mathbb{N}\). If \(\rho\) agrees with \(r\) and \(\sigma\) agrees with \(s\), then the composite renaming that applies \(\rho\) and then \(\sigma\) agrees with \(s \circ r\).

theorem RenAgrees.comp {ρ : Ren Γ Δ} {r : Nat → Nat}
    {σ : Ren Δ Ξ} {s : Nat → Nat}
    (hρ : RenAgrees ρ r) (hσ : RenAgrees σ s) :
    RenAgrees (Var.comp ρ σ) (s ∘ r)

Uses 6

Statement usesRenamings of simply typed contexts · Agreement of a typed and a numerical renaming · Simple types · Composition of renamings of simply typed contexts

Proof usesTyped de Bruijn variables of the simply typed lambda calculus · Index of a typed variable

TheoremErasure commutes with renaming#✓fully proved

Let \(\rho\) be a typed renaming from context \(\Gamma\) to \(\Delta\) and let \(r : \mathbb{N} \to \mathbb{N}\) be a numerical renaming that agrees with \(\rho\). Then for every intrinsically typed term \(t\) of type \(A\) in context \(\Gamma\), the erasure of the renamed term \(\rho(t)\) equals the raw renaming by \(r\) (lifted at every binder) of the erasure of \(t\).

theorem Tm.erase_rename (ρ : Ren Γ Δ) (r : Nat → Nat)
    (h : RenAgrees ρ r) (t : Tm Γ A) :
    (Tm.rename ρ t).erase = RawTm.rename r t.erase

Uses 13 · Used by 2

Statement usesRaw lambda terms · Renaming of raw terms · Renamings of simply typed contexts · Agreement of a typed and a numerical renaming · Intrinsically typed terms of the simply typed lambda calculus · Erasure of intrinsically typed terms · Renaming a simply typed term · Simple types

Proof usesLifting a numerical renaming · Agreement of renamings is preserved by lifting · Typed de Bruijn variables of the simply typed lambda calculus · Lifting a renaming under a binder · Index of a typed variable

Used byErasure of a weakened term · Agreeing numerical renamings coincide on erased terms

TheoremErasure of a weakened term#✓fully proved

For every intrinsically typed term \(t\) in context \(\Gamma\) and every type \(B\), the erasure of the weakening of \(t\) to the context \(\Gamma\) extended by \(B\) equals the raw renaming by the successor map \(n \mapsto n + 1\) (lifted at every binder) of the erasure of \(t\). Thus every free index is incremented by one.

@[simp] theorem Tm.erase_weaken (t : Tm Γ A) :
    (Tm.weaken (B := B) t).erase = RawTm.rename Nat.succ t.erase

Uses 9

Statement usesRaw lambda terms · Renaming of raw terms · Intrinsically typed terms of the simply typed lambda calculus · Erasure of intrinsically typed terms · Weakening a simply typed term · Simple types

Proof usesErasure commutes with renaming · Typed de Bruijn variables of the simply typed lambda calculus · Index of a typed variable

TheoremAgreeing numerical renamings coincide on erased terms#✓fully proved

Let \(\rho\) be a type-preserving renaming of variables from context \(\Gamma\) to context \(\Delta\), and let \(r, s : \mathbb{N} \to \mathbb{N}\) both agree with \(\rho\): for every variable \(x\) of \(\Gamma\), the de Bruijn index of \(\rho(x)\) is the image of the index of \(x\) under \(r\), and also under \(s\). Then for every intrinsically typed term \(t\) of type \(A\) in context \(\Gamma\), renaming the erasure of \(t\) by \(r\) and renaming it by \(s\) give the same raw term.

theorem RawTm.rename_eq_on_erase (ρ : Ren Γ Δ) (r s : Nat → Nat)
    (hr : RenAgrees ρ r) (hs : RenAgrees ρ s) (t : Tm Γ A) :
    RawTm.rename r t.erase = RawTm.rename s t.erase

Uses 9

Statement usesRaw lambda terms · Renaming of raw terms · Renamings of simply typed contexts · Agreement of a typed and a numerical renaming · Intrinsically typed terms of the simply typed lambda calculus · Erasure of intrinsically typed terms · Simple types

Proof usesErasure commutes with renaming · Renaming a simply typed term

42 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.