Scoped pure Fω terms

8 fully proved

Terms and contexts

InductiveScoped pure Fω terms#✓fully proved

Pure terms at a kind telescope and a finite term-variable depth.

inductive Tm : List Kind → Nat → Type where
  | var {Δ : List Kind} {m : Nat} : Fin m → Tm Δ m
  | lam {Δ : List Kind} {m : Nat} : Ty Δ .star → Tm Δ (m + 1) → Tm Δ m
  | app {Δ : List Kind} {m : Nat} : Tm Δ m → Tm Δ m → Tm Δ m
  | tabs {Δ : List Kind} {m : Nat} {κ : Kind} : Tm (κ :: Δ) m → Tm Δ m
  | tapp {Δ : List Kind} {m : Nat} {κ : Kind} : Tm Δ m → Ty Δ κ → Tm Δ m

Uses 2 · Used by 63

Statement usesKinds of pure Fω · Intrinsically kinded Fω type operators

Used byCanonical forms for Fω values of quantified type · Canonical forms for Fω values of function type · Inversion of Fω lambda typing up to conversion · Type preservation for Fω weak call-by-value reduction · Type preservation along multistep Fω reduction · Progress for closed Fω terms · Type safety of Fω weak call-by-value reduction · Weak call-by-value reduction of Fω · Inversion of Fω type-lambda typing up to conversion · Weak call-by-value values of Fω · Erasure 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 Fω terms in the System F term model · Closing an Fω application · Beta conversion of a closed Fω lambda application · Closing an instantiated Fω term binder · Closing commutes with Fω term substitution · Closing erases type abstraction · Closing erases type application · Closing is invariant under type substitution · Closing an Fω variable · Erasure of closed Fω terms to the term model · Erasure of an Fω evaluation step is a beta conversion · Erasure of multistep Fω evaluation is a beta conversion · No closed Fω term inhabits \(\forall X, X\) · Fundamental theorem of higher-kinded parametricity for Fω · Closed typed Fω terms are related to themselves · Higher-kinded polymorphic identity term · Typing of the higher-kinded identity · Closed inhabitants of the higher-kinded identity type are identities · Higher-kinded identity inhabitants preserve admissible relations · No closed Fω term inhabits \(\forall F, \forall X, F\,X\) · Term-binder instantiation preserves Fω typing · Term renaming preserves Fω typing · Term substitution preserves Fω typing · Type-binder instantiation preserves Fω typing · Type renaming preserves Fω typing · Type substitution preserves Fω typing · Typing rules of pure Fω · Instantiation of an Fω term binder · Lifting a term substitution under a term binder · Term-variable renaming in Fω terms · Simultaneous term substitution in Fω · Type-variable renaming in Fω terms · Type substitution in Fω terms · Translated System F terms have the same closing instances · Canonical embedding of System F terms into Fω · Canonical embedding preserves multistep evaluation · 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

AbbreviationTerm contexts of pure Fω#✓fully proved

An ordered unrestricted term context of kind-star types.

abbrev Ctx (Δ : List Kind) (m : Nat) := Fin m → Ty Δ .star

Uses 2 · Used by 19

Statement usesKinds of pure Fω · Intrinsically kinded Fω type operators

Used byCanonical forms for Fω values of quantified type · Canonical forms for Fω values of function type · Inversion of Fω lambda typing up to conversion · Type preservation for Fω weak call-by-value reduction · Type preservation along multistep Fω reduction · Progress for closed Fω terms · Type safety of Fω weak call-by-value reduction · Inversion of Fω type-lambda typing up to conversion · Fundamental theorem of higher-kinded parametricity for Fω · Closed typed Fω terms are related to themselves · Typing of the higher-kinded identity · Term-binder instantiation preserves Fω typing · Term renaming preserves Fω typing · Term substitution preserves Fω typing · Type-binder instantiation preserves Fω typing · Type renaming preserves Fω typing · Type substitution preserves Fω typing · Typing rules of pure Fω · Term translation preserves System F typing

Renaming and substitution in terms

DefinitionType substitution in Fω terms#✓fully proved

Substitute kinded type variables in all annotations and type arguments.

@[simp] def tySubst {Δ Ε : List Kind} {m : Nat} (σ : Ty.Sub Δ Ε) :
    Tm Δ m → Tm Ε 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 6 · Used by 15

Statement usesKinds of pure Fω · Scoped pure Fω terms · Intrinsically kinded Fω type operators · Kind-preserving simultaneous type substitutions · Lifting a type substitution under a type binder · Simultaneous substitution of Fω type operators

Used byType preservation for Fω weak call-by-value reduction · Progress for closed Fω terms · Weak call-by-value reduction of Fω · Fω erasure commutes with term substitution · Fω erasure ignores type substitution · Closing is invariant under type substitution · Erasure of an Fω evaluation step is a beta conversion · Type-binder instantiation preserves Fω typing · Type renaming preserves Fω typing · Type substitution preserves Fω typing · Type-variable renaming in Fω terms · Term translation simulates each weak call-by-value step · Term translation commutes with target type substitution · Term translation commutes with type-binder instantiation · Term translation commutes with weakening under a type binder

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

Rename type variables without changing term variables.

def tyRename {Δ Ε : List Kind} {m : Nat} (ρ : KRen Δ Ε) (t : Tm Δ m) :
    Tm Ε m := tySubst (fun {_} x => .var (ρ x)) t

Uses 6 · Used by 5

Statement usesKind-preserving renamings of type variables · Kinded type variables of Fω · Kinds of pure Fω · Scoped pure Fω terms · Type substitution in Fω terms · Intrinsically kinded Fω type operators

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

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

Rename term variables, lifting only beneath term lambdas.

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

Uses 4 · Used by 4

Statement usesKinds of pure Fω · Scoped pure Fω terms · Intrinsically kinded Fω type operators · Lifting a scoped renaming under a binder

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

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

Lift a term substitution beneath one term binder.

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

Uses 3 · Used by 4

Statement usesKinds of pure Fω · Scoped pure Fω terms · Term-variable renaming in Fω terms

Used byFω erasure commutes with term substitution · Term substitution preserves Fω typing · Simultaneous term substitution in Fω · Term translation commutes with term substitution

DefinitionSimultaneous term substitution in Fω#✓fully proved

Term substitution avoids capture in both namespaces.

@[simp] def subst {Δ : List Kind} {m k : Nat} (σ : Fin m → Tm Δ k) :
    Tm Δ m → Tm Δ 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 KVar.succ (σ i)) b)
  | .tapp f A => .tapp (subst σ f) A

Uses 6 · Used by 6

Statement usesKinded type variables of Fω · Kinds of pure Fω · Scoped pure Fω terms · Lifting a term substitution under a term binder · Type-variable renaming in Fω terms · Intrinsically kinded Fω type operators

Used byFω erasure commutes with term substitution · Closing commutes with Fω term substitution · Term substitution preserves Fω typing · Instantiation of an Fω term binder · Term translation commutes with term-binder instantiation · Term translation commutes with term substitution

DefinitionInstantiation of an Fω term binder#✓fully proved

Discharge the newest term binder.

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

Uses 3 · Used by 9

Statement usesKinds of pure Fω · Scoped pure Fω terms · Simultaneous term substitution in Fω

Used byType preservation for Fω weak call-by-value reduction · Progress for closed Fω terms · Weak call-by-value reduction of Fω · Fω erasure commutes with term-binder instantiation · Closing an instantiated Fω term binder · Erasure of an Fω evaluation step is a beta conversion · Term-binder instantiation preserves Fω typing · Term translation commutes with term-binder instantiation · Term translation simulates each weak call-by-value step

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.