Scoped pure System F

18 fully proved

System F

InductiveScoped types of pure System F#✓fully proved

Pure System F types with n available type variables.

inductive Ty : Nat → Type where
  | var {n : Nat} : Fin n → Ty n
  | arr {n : Nat} : Ty n → Ty n → Ty n
  | all {n : Nat} : Ty (n + 1) → Ty n
  deriving DecidableEq, Repr

Used by 89

Used byErasure of Fω terms to System F syntax · Fω erasure commutes with term-variable renaming · Fω erasure commutes with term substitution · Fω erasure ignores type substitution · Beta conversion of a closed Fω lambda application · Translated System F terms have the same closing instances · Relational interpretation of canonically embedded types · Type translation preserves the relational interpretation · Canonical embedding of System F types into Fω · Canonical embedding preserves System F typing · Translation of System F types into Fω · Translation of System F terms into Fω · Type translation depends only on variable images · Type translation commutes with type-binder instantiation · Term translation commutes with term-variable renaming · Type translation of a source renaming · Type translation of a source substitution · Term translation of a source type substitution · Term translation simulates each weak call-by-value step · Term translation commutes with term substitution · Type translation commutes with target renaming · Type translation commutes with target substitution · Term translation commutes with target type substitution · Term translation commutes with type-binder instantiation · Term translation commutes with weakening under a type binder · Term translation preserves System F typing · Term translation preserves weak call-by-value values · Canonical forms of function-typed values · Canonical forms of universally typed values · Type preservation for a call-by-value step · Type preservation along evaluation sequences · Progress for well-typed terms without free term variables · Type safety for closed well-typed terms · One-step call-by-value evaluation · Value forms of pure System F · Binary logical relation of a System F type · Relational interpretation of an instantiated System F type · Relational interpretation of a renamed System F type · Relational interpretation of a substituted System F type · Relational interpretation of a weakened System F type · No closed System F term inhabits \(\forall X, X\) · Fundamental theorem of relational parametricity for System F · Closed typed System F terms are related to themselves · Polymorphic identity term · Polymorphic identity type · Typing of the polymorphic identity · Closed inhabitants of the polymorphic identity type are identities · Polymorphic identity inhabitants preserve admissible relations · Term variable contexts of System F · Instantiating the newest type binder of a type · Lifting a type substitution under a type binder · Lifted type substitution weakens old images · Lifted type substitution fixes the fresh variable · Type-variable renaming in System F types · Term-variable renaming in System F terms · Simultaneous type substitution in System F types · Simultaneous term substitution in System F terms · Scoped terms of pure System F · Type-variable renaming in System F terms · Type substitution in System F terms · Beta conversion of a closed System F lambda application · Closing erases System F type application · System F closing is invariant under type substitution · Type erasure under an untyped environment · Erasure with locally closed images is locally closed · Opening commutes with erasure under an environment · Erasure of a term-variable renaming · Shifting commutes with erasure under an environment · Erasure of a term substitution · Untyped erasure is invariant under type substitution · Erasure of a System F evaluation step is a beta conversion · Instantiating a term binder preserves typing · Term renaming preserves typing · Term substitution preserves typing · Instantiating a type binder preserves typing · Type renaming preserves typing · Type substitution preserves typing · Extrinsic typing of pure System F terms · Instantiating a weakened type restores it · Lifted identity type substitution is the identity · Successive type renamings fuse into their composition · Identity renaming fixes every type · Renaming after a type substitution · Successive type substitutions fuse into one substitution · Identity type substitution fixes every type · Type substitution commutes with instantiation · Lifted type substitution commutes with weakening · Substitution after a type renaming · Variable-valued substitution is a type renaming

DefinitionLifting a scoped renaming under a binder#✓fully proved

Extend a scoped renaming, preserving the newly bound variable.

def liftRen {n k : Nat} (ρ : Fin n → Fin k) :
    Fin (n + 1) → Fin (k + 1) :=
  Fin.cases 0 (fun i => (ρ i).succ)

Used by 18

Used byFω erasure commutes with term-variable renaming · Term renaming preserves Fω typing · Term-variable renaming in Fω terms · Term translation commutes with term-variable renaming · Type translation of a source renaming · Relational interpretation of a renamed System F type · Lifted renaming shifts each renamed old variable · Lifted renaming fixes the newly bound variable · Type-variable renaming in System F types · Term-variable renaming in System F terms · Erasure of a term-variable renaming · Term renaming preserves typing · Lifting preserves composition of renamings · Lifted identity renaming is the identity · Successive type renamings fuse into their composition · Identity renaming fixes every type · Renaming after a type substitution · Substitution after a type renaming

TheoremLifted renaming fixes the newly bound variable#✓fully proved

The new variable is unaffected by a lifted renaming.

@[simp] theorem liftRen_zero {n k : Nat} (ρ : Fin n → Fin k) :
    liftRen ρ 0 = 0

Uses 1

Statement usesLifting a scoped renaming under a binder

TheoremLifted renaming shifts each renamed old variable#✓fully proved

A lifted renaming shifts every renamed old variable.

@[simp] theorem liftRen_succ {n k : Nat} (ρ : Fin n → Fin k)
    (i : Fin n) : liftRen ρ i.succ = (ρ i).succ

Uses 1

Statement usesLifting a scoped renaming under a binder

Type renaming and substitution

DefinitionType-variable renaming in System F types#✓fully proved

Capture-avoiding renaming of type variables.

@[simp] def rename {n k : Nat} (ρ : Fin n → Fin k) : Ty n → Ty k
  | .var i => .var (ρ i)
  | .arr A B => .arr (rename ρ A) (rename ρ B)
  | .all B => .all (rename (liftRen ρ) B)

Uses 2 · Used by 26

Statement usesScoped types of pure System F · Lifting a scoped renaming under a binder

Used byType translation of a source renaming · Term translation preserves System F typing · Canonical forms of function-typed values · Canonical forms of universally typed values · Type preservation for a call-by-value step · Progress for well-typed terms without free term variables · Relational interpretation of a renamed System F type · Relational interpretation of a weakened System F type · Fundamental theorem of relational parametricity for System F · Typing of the polymorphic identity · Lifting a type substitution under a type binder · Lifted type substitution weakens old images · Term renaming preserves typing · Term substitution preserves typing · Instantiating a type binder preserves typing · Type renaming preserves typing · Type substitution preserves typing · Extrinsic typing of pure System F terms · Instantiating a weakened type restores it · Successive type renamings fuse into their composition · Identity renaming fixes every type · Renaming after a type substitution · Type substitution commutes with instantiation · Lifted type substitution commutes with weakening · Substitution after a type renaming · Variable-valued substitution is a type renaming

DefinitionLifting a type substitution under a type binder#✓fully proved

Lift a type substitution under one type binder.

def liftSub {n k : Nat} (σ : Fin n → Ty k) : Fin (n + 1) → Ty (k + 1) :=
  Fin.cases (.var 0) (fun i => rename Fin.succ (σ i))

Uses 2 · Used by 16

Statement usesScoped types of pure System F · Type-variable renaming in System F types

Used byType translation of a source substitution · Term translation of a source type substitution · Relational interpretation of a substituted System F type · Lifted type substitution weakens old images · Lifted type substitution fixes the fresh variable · Simultaneous type substitution in System F types · Type substitution in System F terms · Untyped erasure is invariant under type substitution · Type substitution preserves typing · Lifted identity type substitution is the identity · Renaming after a type substitution · Successive type substitutions fuse into one substitution · Identity type substitution fixes every type · Type substitution commutes with instantiation · Lifted type substitution commutes with weakening · Substitution after a type renaming

DefinitionSimultaneous type substitution in System F types#✓fully proved

Simultaneous, capture-avoiding type substitution.

@[simp] def subst {n k : Nat} (σ : Fin n → Ty k) : Ty n → Ty k
  | .var i => σ i
  | .arr A B => .arr (subst σ A) (subst σ B)
  | .all B => .all (subst (liftSub σ) B)

Uses 2 · Used by 18

Statement usesScoped types of pure System F · Lifting a type substitution under a type binder

Used byType translation of a source substitution · Term translation of a source type substitution · Relational interpretation of an instantiated System F type · Relational interpretation of a substituted System F type · Instantiating the newest type binder of a type · Type substitution in System F terms · Untyped erasure is invariant under type substitution · Instantiating a type binder preserves typing · Type renaming preserves typing · Type substitution preserves typing · Instantiating a weakened type restores it · Renaming after a type substitution · Successive type substitutions fuse into one substitution · Identity type substitution fixes every type · Type substitution commutes with instantiation · Lifted type substitution commutes with weakening · Substitution after a type renaming · Variable-valued substitution is a type renaming

DefinitionInstantiating the newest type binder of a type#✓fully proved

Discharge the newest type binder by an arbitrary type.

def instantiate {n : Nat} (B : Ty (n + 1)) (A : Ty n) : Ty n :=
  subst (Fin.cases A Ty.var) B

Uses 2 · Used by 15

Statement usesScoped types of pure System F · Simultaneous type substitution in System F types

Used byType translation commutes with type-binder instantiation · Term translation preserves System F typing · Canonical forms of function-typed values · Canonical forms of universally typed values · Type preservation for a call-by-value step · Progress for well-typed terms without free term variables · Relational interpretation of an instantiated System F type · Fundamental theorem of relational parametricity for System F · Term renaming preserves typing · Term substitution preserves typing · Instantiating a type binder preserves typing · Type substitution preserves typing · Extrinsic typing of pure System F terms · Instantiating a weakened type restores it · Type substitution commutes with instantiation

TheoremLifted type substitution fixes the fresh variable#✓fully proved

The fresh type variable is fixed by a lifted substitution.

@[simp] theorem liftSub_zero {n k : Nat} (σ : Fin n → Ty k) :
    liftSub σ 0 = .var 0

Uses 2

Statement usesScoped types of pure System F · Lifting a type substitution under a type binder

TheoremLifted type substitution weakens old images#✓fully proved

Old type-substitution images are weakened under a binder.

@[simp] theorem liftSub_succ {n k : Nat} (σ : Fin n → Ty k)
    (i : Fin n) : liftSub σ i.succ = rename Fin.succ (σ i)

Uses 3

Statement usesScoped types of pure System F · Lifting a type substitution under a type binder · Type-variable renaming in System F types

System F

InductiveScoped terms of pure System F#✓fully proved

Pure terms with n type variables and m term variables.

inductive Tm : Nat → Nat → Type where
  | var {n m : Nat} : Fin m → Tm n m
  | lam {n m : Nat} : Ty n → Tm n (m + 1) → Tm n m
  | app {n m : Nat} : Tm n m → Tm n m → Tm n m
  | tabs {n m : Nat} : Tm (n + 1) m → Tm n m
  | tapp {n m : Nat} : Tm n m → Ty n → Tm n m
  deriving DecidableEq, Repr

Uses 1 · Used by 76

Statement usesScoped types of pure System F

Used byErasure of Fω terms to System F syntax · Fω erasure commutes with term-binder instantiation · Fω erasure commutes with term-variable renaming · Fω erasure commutes with term substitution · Fω erasure ignores type substitution · Closing an instantiated Fω term binder · Closing commutes with Fω term substitution · Closing is invariant under type substitution · Canonical embedding preserves closing instances · Translated System F terms have the same closing instances · Canonical embedding preserves model erasure · Canonical embedding of System F terms into Fω · Canonical embedding preserves single evaluation steps · Canonical embedding preserves multistep evaluation · Canonical embedding preserves System F typing · Translation of System F terms into Fω · Term translation depends only on type-variable images · Term translation commutes with term-binder instantiation · Term translation commutes with term-variable renaming · Term translation of a source type substitution · Term translation simulates each weak call-by-value step · Term translation commutes with term substitution · Term translation commutes with target type substitution · Term translation commutes with type-binder instantiation · Term translation commutes with weakening under a type binder · Term translation preserves System F typing · Term translation preserves weak call-by-value values · Canonical forms of function-typed values · Canonical forms of universally typed values · Type preservation for a call-by-value step · Type preservation along evaluation sequences · Progress for well-typed terms without free term variables · Type safety for closed well-typed terms · One-step call-by-value evaluation · Multi-step call-by-value evaluation · Value forms of pure System F · No closed System F term inhabits \(\forall X, X\) · Fundamental theorem of relational parametricity for System F · Closed typed System F terms are related to themselves · Polymorphic identity term · Typing of the polymorphic identity · Closed inhabitants of the polymorphic identity type are identities · Polymorphic identity inhabitants preserve admissible relations · Instantiating the newest term binder of a term · Lifting a term substitution under a term lambda · Term-variable renaming in System F terms · Simultaneous term substitution in System F terms · Type-variable renaming in System F terms · Type substitution in System F terms · Closing System F terms in the term model · Closing a System F application · Beta conversion of a closed System F lambda application · Closing an instantiated System F term binder · Closing commutes with System F term substitution · Closing erases System F type abstraction · Closing erases System F type application · System F closing is invariant under type substitution · Closing a System F variable · Type erasure of System F terms to untyped terms · Erasure of closed System F terms to the term model · Type erasure under an untyped environment · Erasure with locally closed images is locally closed · Opening commutes with erasure under an environment · Erasure of a term-variable renaming · Shifting commutes with erasure under an environment · Erasure of a term substitution · Untyped erasure is invariant under type substitution · Erasure of a System F evaluation step is a beta conversion · Erasure of multistep System F evaluation is a beta conversion · Instantiating a term binder preserves typing · Term renaming preserves typing · Term substitution preserves typing · Instantiating a type binder preserves typing · Type renaming preserves typing · Type substitution preserves typing · Extrinsic typing of pure System F terms

AbbreviationTerm variable contexts of System F#✓fully proved

An ordered, unrestricted term context over n type variables.

abbrev Ctx (n m : Nat) := Fin m → Ty n

Uses 1 · Used by 18

Statement usesScoped types of pure System F

Used byCanonical embedding preserves System F typing · Term translation preserves System F typing · Canonical forms of function-typed values · Canonical forms of universally typed values · Type preservation for a call-by-value step · Type preservation along evaluation sequences · Progress for well-typed terms without free term variables · Type safety for closed well-typed terms · Fundamental theorem of relational parametricity for System F · Closed typed System F terms are related to themselves · Typing of the polymorphic identity · Instantiating a term binder preserves typing · Term renaming preserves typing · Term substitution preserves typing · Instantiating a type binder preserves typing · Type renaming preserves typing · Type substitution preserves typing · Extrinsic typing of pure System F terms

Term renaming and substitution

DefinitionType substitution in System F terms#✓fully proved

Substitute type variables in annotations, arguments, and type binders.

@[simp] def tySubst {n k m : Nat} (σ : Fin n → Ty k) : Tm n m → Tm k m
  | .var i => .var i
  | .lam A b => .lam (A.subst σ) (tySubst σ b)
  | .app f a => .app (tySubst σ f) (tySubst σ a)
  | .tabs b => .tabs (tySubst (Ty.liftSub σ) b)
  | .tapp f A => .tapp (tySubst σ f) (A.subst σ)

Uses 4 · Used by 14

Statement usesScoped terms of pure System F · Scoped types of pure System F · Lifting a type substitution under a type binder · Simultaneous type substitution in System F types

Used byTerm translation of a source type substitution · Term translation simulates each weak call-by-value step · Term translation commutes with type-binder instantiation · Type preservation for a call-by-value step · Progress for well-typed terms without free term variables · One-step call-by-value evaluation · Type-variable renaming in System F terms · System F closing is invariant under type substitution · Erasure of a term substitution · Untyped erasure is invariant under type substitution · Erasure of a System F evaluation step is a beta conversion · Instantiating a type binder preserves typing · Type renaming preserves typing · Type substitution preserves typing

DefinitionTerm-variable renaming in System F terms#✓fully proved

Rename term variables, lifting only at term binders.

@[simp] def rename {n m k : Nat} (ρ : Fin m → Fin k) : Tm n m → Tm n k
  | .var i => .var (ρ i)
  | .lam A b => .lam A (rename (liftRen ρ) b)
  | .app f a => .app (rename ρ f) (rename ρ a)
  | .tabs b => .tabs (rename ρ b)
  | .tapp f A => .tapp (rename ρ f) A

Uses 3 · Used by 7

Statement usesScoped terms of pure System F · Scoped types of pure System F · Lifting a scoped renaming under a binder

Used byFω erasure commutes with term-variable renaming · Fω erasure commutes with term substitution · Term translation commutes with term-variable renaming · Lifting a term substitution under a term lambda · Erasure of a term-variable renaming · Erasure of a term substitution · Term renaming preserves typing

DefinitionType-variable renaming in System F terms#✓fully proved

Rename type variables without changing term variables.

def tyRename {n k m : Nat} (ρ : Fin n → Fin k) (t : Tm n m) : Tm k m :=
  tySubst (fun i => .var (ρ i)) t

Uses 3 · Used by 5

Statement usesScoped terms of pure System F · Type substitution in System F terms · Scoped types of pure System F

Used byTerm translation commutes with term substitution · Term translation commutes with weakening under a type binder · Simultaneous term substitution in System F terms · Term substitution preserves typing · Type renaming preserves typing

DefinitionLifting a term substitution under a term lambda#✓fully proved

Lift a simultaneous term substitution beneath a term lambda.

def liftSub {n m k : Nat} (σ : Fin m → Tm n k) :
    Fin (m + 1) → Tm n (k + 1) :=
  Fin.cases (.var 0) (fun i => rename Fin.succ (σ i))

Uses 2 · Used by 5

Statement usesScoped terms of pure System F · Term-variable renaming in System F terms

Used byFω erasure commutes with term substitution · Term translation commutes with term substitution · Simultaneous term substitution in System F terms · Erasure of a term substitution · Term substitution preserves typing

DefinitionSimultaneous term substitution in System F terms#✓fully proved

Simultaneous term substitution, avoiding both sorts of capture.

@[simp] def subst {n m k : Nat} (σ : Fin m → Tm n k) : Tm n m → Tm n k
  | .var i => σ i
  | .lam A b => .lam A (subst (liftSub σ) b)
  | .app f a => .app (subst σ f) (subst σ a)
  | .tabs b => .tabs (subst (fun i => tyRename Fin.succ (σ i)) b)
  | .tapp f A => .tapp (subst σ f) A

Uses 4 · Used by 9

Statement usesScoped terms of pure System F · Lifting a term substitution under a term lambda · Type-variable renaming in System F terms · Scoped types of pure System F

Used byFω erasure commutes with term-binder instantiation · Fω erasure commutes with term substitution · Closing commutes with Fω term substitution · Term translation commutes with term substitution · Instantiating the newest term binder of a term · Closing an instantiated System F term binder · Closing commutes with System F term substitution · Erasure of a term substitution · Term substitution preserves typing

DefinitionInstantiating the newest term binder of a term#✓fully proved

Replace the newest term variable and discharge its binder.

def instantiate {n m : Nat} (b : Tm n (m + 1)) (a : Tm n m) : Tm n m :=
  subst (Fin.cases a Tm.var) b

Uses 2 · Used by 10

Statement usesScoped terms of pure System F · Simultaneous term substitution in System F terms

Used byFω erasure commutes with term-binder instantiation · Closing an instantiated Fω term binder · Term translation commutes with term-binder instantiation · Term translation simulates each weak call-by-value step · Type preservation for a call-by-value step · Progress for well-typed terms without free term variables · One-step call-by-value evaluation · Closing an instantiated System F term binder · Erasure of a System F evaluation step is a beta conversion · Instantiating a term binder preserves typing

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.