Proved type-beta conversion for pure Fω

InductiveType-beta conversion in Fω#✓fully proved

Type-beta conversion at a fixed context and kind.

Cslib.Languages.LambdaCalculus.FOmega.Ty.Conv · 18 lines

inductive Conv : {Δ : List Kind} → {κ : Kind} → Ty Δ κ → Ty Δ κ → Prop where
  | refl {Δ : List Kind} {κ : Kind} (a : Ty Δ κ) : Conv a a
  | symm {Δ : List Kind} {κ : Kind} {a b : Ty Δ κ} :
      Conv a b → Conv b a
  | trans {Δ : List Kind} {κ : Kind} {a b c : Ty Δ κ} :
      Conv a b → Conv b c → Conv a c
  | beta {Δ : List Kind} {κ μ : Kind}
      (b : Ty (κ :: Δ) μ) (a : Ty Δ κ) :
      Conv (.app (.lam b) a) (instantiate b a)
  | lam {Δ : List Kind} {κ μ : Kind} {b c : Ty (κ :: Δ) μ} :
      Conv b c → Conv (.lam b) (.lam c)
  | app {Δ : List Kind} {κ μ : Kind}
      {f g : Ty Δ (.arrow κ μ)} {a b : Ty Δ κ} :
      Conv f g → Conv a b → Conv (.app f a) (.app g b)
  | arr {Δ : List Kind} {a a' b b' : Ty Δ .star} :
      Conv a a' → Conv b b' → Conv (.arr a b) (.arr a' b')
  | all {Δ : List Kind} {κ : Kind} {b c : Ty (κ :: Δ) .star} :
      Conv b c → Conv (.all b) (.all c)

Uses 3 · Used by 24

Statement usesKinds of pure Fω · Intrinsically kinded Fω type operators · Instantiation of an Fω type binder

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 · Progress for closed Fω terms · Inversion of Fω type-lambda typing up to conversion · Type-beta conversion preserves the relational interpretation · Fundamental theorem of higher-kinded parametricity for Fω · Function types are not convertible to quantified types · Type-beta conversion is stable under renaming · Soundness of type-beta conversion in kind algebras · Type-beta conversion is stable under substitution · Pointwise convertible substitutions give convertible results · Term renaming preserves Fω typing · Term substitution preserves Fω typing · Type substitution preserves Fω typing · Typing rules of pure Fω · Injectivity of quantified types up to conversion · Conversion preserves the kind of a universal binder · Injectivity of function types up to conversion · Parallel type-beta reduction implies conversion · Multistep type-beta reduction implies conversion · Type-beta conversion is joinability by a common reduct · Church–Rosser property of type-beta conversion

TheoremSoundness of type-beta conversion in kind algebras#✓fully proved

Every type-beta conversion is sound in every semantic kind algebra.

theorem Conv.sound {α : Type*} (h : Conv a b) (M : KindAlgebra α)
    (η : KEnv α Δ) : eval M η a = eval M η b

Uses 10 · Used by 2

Statement usesKinded semantic environment · Kinds of pure Fω · Semantic interpretation of kinds · Kind algebra of arrow and universal type constructors · Intrinsically kinded Fω type operators · Type-beta conversion in Fω · Semantic evaluation of kinded type operators

Proof usesExtension of a kinded semantic environment · Evaluation of an instantiated type operator · Instantiation of an Fω type binder

Used byType-beta conversion preserves the relational interpretation · Function types are not convertible to quantified types

TheoremType-beta conversion is stable under renaming#✓fully proved

Kind-preserving renaming respects proved type-beta conversion.

theorem Conv.rename (h : Conv a b) (ρ : KRen Δ Ε) :
    Conv (Ty.rename ρ a) (Ty.rename ρ b)

Uses 8 · Used by 1

Statement usesKind-preserving renamings of type variables · Kinds of pure Fω · Intrinsically kinded Fω type operators · Type-beta conversion in Fω · Renaming of Fω type operators

Proof usesLifting a renaming under a type binder · Instantiation of an Fω type binder · Renaming commutes with type-binder instantiation

Used byPointwise convertible substitutions give convertible results

TheoremType-beta conversion is stable under substitution#✓fully proved

Kind-preserving substitution respects proved type-beta conversion.

theorem Conv.subst (h : Conv a b) (σ : Sub Δ Ε) :
    Conv (Ty.subst σ a) (Ty.subst σ b)

Uses 8 · Used by 2

Statement usesKinds of pure Fω · Intrinsically kinded Fω type operators · Type-beta conversion in Fω · Kind-preserving simultaneous type substitutions · Simultaneous substitution of Fω type operators

Proof usesInstantiation of an Fω type binder · Lifting a type substitution under a type binder · Substitution commutes with type-binder instantiation

Used byType preservation for Fω weak call-by-value reduction · Type substitution preserves Fω typing

TheoremPointwise convertible substitutions give convertible results#✓fully proved

Pointwise convertible substitution images give convertible results.

theorem Conv.subst_congr {σ τ : Sub Δ Ε}
    (h : ∀ {ν} (x : KVar Δ ν), Conv (σ x) (τ x)) (t : Ty Δ κ) :
    Conv (Ty.subst σ t) (Ty.subst τ t)

Uses 8

Statement usesKinded type variables of Fω · Kinds of pure Fω · Intrinsically kinded Fω type operators · Type-beta conversion in Fω · Kind-preserving simultaneous type substitutions · Simultaneous substitution of Fω type operators

Proof usesType-beta conversion is stable under renaming · Lifting a type substitution under a type binder

TheoremFunction types are not convertible to quantified types#✓fully proved

Term-function arrows cannot convert to quantified types, at any kind.

theorem not_conv_arr_all {a b : Ty Δ .star} {body : Ty (μ :: Δ) .star} :
    ¬ Conv (.arr a b) (.all body)

Uses 8 · Used by 2

Statement usesKinds of pure Fω · Intrinsically kinded Fω type operators · Type-beta conversion in Fω

Proof usesKinded type variables of Fω · Semantic interpretation of kinds · Kind algebra of arrow and universal type constructors · Soundness of type-beta conversion in kind algebras · Semantic evaluation of kinded type operators

Used byCanonical forms for Fω values of quantified type · Canonical forms for Fω values of function type

6 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.