Pure Fω typing with proved type-beta conversion

7 fully proved

Typing rules

InductiveTyping rules of pure Fω#✓fully proved

The five pure term rules and the type-beta conversion rule of Fω.

Cslib.Languages.LambdaCalculus.FOmega.Typing · 20 lines

inductive Typing : {Δ : List Kind} → {m : Nat} →
    Ctx Δ m → Tm Δ m → Ty Δ .star → Prop where
  | var {Δ : List Kind} {m : Nat} {Γ : Ctx Δ m} (i : Fin m) :
      Typing Γ (.var i) (Γ i)
  | lam {Δ : List Kind} {m : Nat} {Γ : Ctx Δ m}
      {A B : Ty Δ .star} {b : Tm Δ (m + 1)} :
      Typing (Fin.cases A Γ) b B → Typing Γ (.lam A b) (.arr A B)
  | app {Δ : List Kind} {m : Nat} {Γ : Ctx Δ m}
      {A B : Ty Δ .star} {f a : Tm Δ m} :
      Typing Γ f (.arr A B) → Typing Γ a A → Typing Γ (.app f a) B
  | tabs {Δ : List Kind} {m : Nat} {κ : Kind} {Γ : Ctx Δ m}
      {b : Tm (κ :: Δ) m} {C : Ty (κ :: Δ) .star} :
      Typing (fun i => (Γ i).rename KVar.succ) b C →
      Typing Γ (.tabs b) (.all C)
  | tapp {Δ : List Kind} {m : Nat} {κ : Kind} {Γ : Ctx Δ m}
      {f : Tm Δ m} {A : Ty Δ κ} {C : Ty (κ :: Δ) .star} :
      Typing Γ f (.all C) → Typing Γ (.tapp f A) (C.instantiate A)
  | conv {Δ : List Kind} {m : Nat} {Γ : Ctx Δ m}
      {t : Tm Δ m} {A B : Ty Δ .star} :
      Typing Γ t A → Ty.Conv A B → Typing Γ t B

Uses 8 · Used by 23

Statement usesTerm contexts of pure Fω · Kinded type variables of Fω · Kinds of pure Fω · Scoped pure Fω terms · Intrinsically kinded Fω type operators · Type-beta conversion in Fω · Instantiation of an Fω type binder · Renaming of 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 · No closed Fω term inhabits \(\forall X, X\) · Fundamental theorem of higher-kinded parametricity for Fω · Closed typed Fω terms are related to themselves · 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 · Canonical embedding preserves System F typing · Term translation preserves System F typing

Typing

TheoremType substitution preserves Fω typing#✓fully proved

Kind-correct type substitution preserves typing in arbitrary contexts.

theorem tySubst {Ε : List Kind} (h : Typing Γ t A) (σ : Ty.Sub Δ Ε) :
    Typing (fun i => (Γ i).subst σ) (t.tySubst σ) (A.subst σ)

Uses 16 · Used by 2

Statement usesTerm contexts of pure Fω · Kinds of pure Fω · Scoped pure Fω terms · Type substitution in Fω terms · Intrinsically kinded Fω type operators · Kind-preserving simultaneous type substitutions · Simultaneous substitution of Fω type operators · Typing rules of pure Fω

Proof usesKinded type variables of Fω · Type-beta conversion in Fω · Type-beta conversion is stable under substitution · Instantiation of an Fω type binder · Lifting a type substitution under a type binder · Renaming of Fω type operators · Substitution commutes with type-binder instantiation · Lifted substitution commutes with weakening

Used byType-binder instantiation preserves Fω typing · Type renaming preserves Fω typing

TheoremType renaming preserves Fω typing#✓fully proved

Kind-preserving type renaming preserves typing.

theorem tyRename {Ε : List Kind} (h : Typing Γ t A) (ρ : KRen Δ Ε) :
    Typing (fun i => (Γ i).rename ρ) (t.tyRename ρ) (A.rename ρ)

Uses 13 · Used by 1

Statement usesTerm contexts of pure Fω · Kind-preserving renamings of type variables · Kinds of pure Fω · Scoped pure Fω terms · Type-variable renaming in Fω terms · Intrinsically kinded Fω type operators · Renaming of Fω type operators · Typing rules of pure Fω

Proof usesKinded type variables of Fω · Type substitution in Fω terms · Simultaneous substitution of Fω type operators · Renaming as substitution by variables · Type substitution preserves Fω typing

Used byTerm substitution preserves Fω typing

TheoremTerm renaming preserves Fω typing#✓fully proved

A context-respecting term-variable renaming preserves the result type.

theorem rename {k : Nat} {Ξ : Ctx Δ k} (h : Typing Γ t A)
    (ρ : Fin m → Fin k) (hρ : ∀ i, Ξ (ρ i) = Γ i) :
    Typing Ξ (t.rename ρ) A

Uses 11 · Used by 1

Statement usesTerm contexts of pure Fω · Kinds of pure Fω · Scoped pure Fω terms · Term-variable renaming in Fω terms · Intrinsically kinded Fω type operators · Typing rules of pure Fω

Proof usesKinded type variables of Fω · Type-beta conversion in Fω · Instantiation of an Fω type binder · Renaming of Fω type operators · Lifting a scoped renaming under a binder

Used byTerm substitution preserves Fω typing

TheoremTerm substitution preserves Fω typing#✓fully proved

Arbitrary correctly typed term substitution preserves typing.

theorem subst {k : Nat} {Ξ : Ctx Δ k} (h : Typing Γ t A)
    (σ : Fin m → Tm Δ k) (hσ : ∀ i, Typing Ξ (σ i) (Γ i)) :
    Typing Ξ (t.subst σ) A

Uses 14 · Used by 1

Statement usesTerm contexts of pure Fω · Kinds of pure Fω · Scoped pure Fω terms · Simultaneous term substitution in Fω · Intrinsically kinded Fω type operators · Typing rules of pure Fω

Proof usesKinded type variables of Fω · Lifting a term substitution under a term binder · Type-variable renaming in Fω terms · Type-beta conversion in Fω · Instantiation of an Fω type binder · Renaming of Fω type operators · Term renaming preserves Fω typing · Type renaming preserves Fω typing

Used byTerm-binder instantiation preserves Fω typing

TheoremTerm-binder instantiation preserves Fω typing#✓fully proved

Discharging a typed term binder retains the body result type.

theorem instantiate {B : Ty Δ .star} {b : Tm Δ (m + 1)} {a : Tm Δ m}
    (hb : Typing (Fin.cases A Γ) b B) (ha : Typing Γ a A) :
    Typing Γ (b.instantiate a) B

Uses 7 · Used by 1

Statement usesTerm contexts of pure Fω · Kinds of pure Fω · Scoped pure Fω terms · Instantiation of an Fω term binder · Intrinsically kinded Fω type operators · Typing rules of pure Fω

Proof usesTerm substitution preserves Fω typing

Used byType preservation for Fω weak call-by-value reduction

TheoremType-binder instantiation preserves Fω typing#✓fully proved

Discharging a type binder substitutes its result and restores context.

theorem tyInstantiate {κ : Kind} {b : Tm (κ :: Δ) m}
    {C : Ty (κ :: Δ) .star}
    (hb : Typing (fun i => (Γ i).rename KVar.succ) b C) (a : Ty Δ κ) :
    Typing Γ (b.tySubst (Ty.single a)) (C.instantiate a)

Uses 13 · Used by 1

Statement usesTerm contexts of pure Fω · Kinded type variables of Fω · Kinds of pure Fω · Scoped pure Fω terms · Type substitution in Fω terms · Intrinsically kinded Fω type operators · Instantiation of an Fω type binder · Renaming of Fω type operators · Substitution for the newest type variable · Typing rules of pure Fω

Proof usesInstantiating a weakened type operator leaves it unchanged · Simultaneous substitution of Fω type operators · Type substitution preserves Fω typing

Used byType preservation for Fω weak call-by-value reduction

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.