Fω closing instances in the single existing term model

DefinitionClosing Fω terms in the System F term model#✓fully proved

Close scoped Fω variables in exactly the existing System F term model.

def close (σ : Fin m → SystemF.Model) (t : Tm Δ m) : SystemF.Model :=
  SystemF.Tm.close σ (eraseSyntax t)

Uses 5 · Used by 14

Statement usesKinds of pure Fω · Scoped pure Fω terms · Erasure of Fω terms to System F syntax · Untyped locally closed term model · Closing System F terms in the term model

Used byClosing 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 · Fundamental theorem of higher-kinded parametricity for Fω · Canonical embedding preserves closing instances · Translated System F terms have the same closing instances

DefinitionErasure of closed Fω terms to the term model#✓fully proved

Erase a closed-term Fω expression, with an arbitrary type telescope.

def eraseModel (t : Tm Δ 0) : SystemF.Model := close Fin.elim0 t

Uses 4 · Used by 4

Statement usesKinds of pure Fω · Scoped pure Fω terms · Closing Fω terms in the System F term model · Untyped locally closed term model

Used byClosed typed Fω terms are related to themselves · Closed inhabitants of the higher-kinded identity type are identities · Higher-kinded identity inhabitants preserve admissible relations · Canonical embedding preserves model erasure

TheoremClosing an Fω variable#✓fully proved

Closing a variable returns its actual model environment image.

@[simp] theorem close_var (σ : Fin m → SystemF.Model) (i : Fin m) :
    close σ (.var i : Tm Δ m) = σ i

Uses 4

Statement usesKinds of pure Fω · Scoped pure Fω terms · Closing Fω terms in the System F term model · Untyped locally closed term model

TheoremClosing an Fω application#✓fully proved

Closing preserves the existing model application constructor.

@[simp] theorem close_app (σ : Fin m → SystemF.Model) (f a : Tm Δ m) :
    close σ (.app f a) = SystemF.Model.app (close σ f) (close σ a)

Uses 5 · Used by 1

Statement usesKinds of pure Fω · Scoped pure Fω terms · Closing Fω terms in the System F term model · Untyped locally closed term model · Application in the untyped term model

Used byErasure of an Fω evaluation step is a beta conversion

TheoremClosing erases type abstraction#✓fully proved

Type abstraction adds no binder to an erased closing instance.

@[simp] theorem close_tabs {κ : Kind} (σ : Fin m → SystemF.Model)
    (b : Tm (κ :: Δ) m) : close σ (.tabs b) = close σ b

Uses 4 · Used by 1

Statement usesKinds of pure Fω · Scoped pure Fω terms · Closing Fω terms in the System F term model · Untyped locally closed term model

Used byErasure of an Fω evaluation step is a beta conversion

TheoremClosing erases type application#✓fully proved

Type application adds no application to an erased closing instance.

@[simp] theorem close_tapp {κ : Kind} (σ : Fin m → SystemF.Model)
    (f : Tm Δ m) (A : Ty Δ κ) : close σ (.tapp f A) = close σ f

Uses 5 · Used by 1

Statement usesKinds of pure Fω · Scoped pure Fω terms · Closing Fω terms in the System F term model · Intrinsically kinded Fω type operators · Untyped locally closed term model

Used byErasure of an Fω evaluation step is a beta conversion

TheoremClosing is invariant under type substitution#✓fully proved

Any kind-correct type substitution leaves closing instances unchanged.

@[simp] theorem close_tySubst (σ : Ty.Sub Δ Ε) (η : Fin m → SystemF.Model)
    (t : Tm Δ m) : close η (tySubst σ t) = close η t

Uses 10 · Used by 1

Statement usesKinds of pure Fω · Scoped pure Fω terms · Closing Fω terms in the System F term model · Type substitution in Fω terms · Kind-preserving simultaneous type substitutions · Untyped locally closed term model

Proof usesErasure of Fω terms to System F syntax · Fω erasure ignores type substitution · Scoped terms of pure System F · Closing System F terms in the term model

Used byErasure of an Fω evaluation step is a beta conversion

TheoremBeta conversion of a closed Fω lambda application#✓fully proved

Applying an erased Fω lambda beta-converts to its extended body instance.

theorem close_beta (σ : Fin m → SystemF.Model) (A : Ty Δ .star)
    (b : Tm Δ (m + 1)) (a : SystemF.Model) :
    SystemF.BetaEq (SystemF.Model.app (close σ (.lam A b)) a)
      (close (Fin.cases a σ) b)

Uses 10 · Used by 2

Statement usesKinds of pure Fω · Scoped pure Fω terms · Closing Fω terms in the System F term model · Intrinsically kinded Fω type operators · Beta equivalence in the untyped term model · Untyped locally closed term model · Application in the untyped term model

Proof usesErasure of Fω terms to System F syntax · Beta conversion of a closed System F lambda application · Scoped types of pure System F

Used byErasure of an Fω evaluation step is a beta conversion · Fundamental theorem of higher-kinded parametricity for Fω

TheoremClosing commutes with Fω term substitution#✓fully proved

Closing composes actual Fω term substitutions with model environments.

theorem close_subst (σ : Fin m → Tm Δ k) (η : Fin k → SystemF.Model)
    (t : Tm Δ m) :
    close η (subst σ t) = close (fun i => close η (σ i)) t

Uses 11

Statement usesKinds of pure Fω · Scoped pure Fω terms · Closing Fω terms in the System F term model · Simultaneous term substitution in Fω · Untyped locally closed term model

Proof usesErasure of Fω terms to System F syntax · Fω erasure commutes with term substitution · Scoped terms of pure System F · Closing System F terms in the term model · Closing commutes with System F term substitution · Simultaneous term substitution in System F terms

TheoremClosing an instantiated Fω term binder#✓fully proved

Actual term-binder discharge extends the same model closing environment.

theorem close_instantiate (η : Fin m → SystemF.Model)
    (b : Tm Δ (m + 1)) (a : Tm Δ m) :
    close η (instantiate b a) = close (Fin.cases (close η a) η) b

Uses 11 · Used by 1

Statement usesKinds of pure Fω · Scoped pure Fω terms · Closing Fω terms in the System F term model · Instantiation of an Fω term binder · Untyped locally closed term model

Proof usesErasure of Fω terms to System F syntax · Fω erasure commutes with term-binder instantiation · Scoped terms of pure System F · Closing System F terms in the term model · Closing an instantiated System F term binder · Instantiating the newest term binder of a term

Used byErasure of an Fω evaluation step is a beta conversion

10 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.