System F embedding agreement with the single term/relation model

TheoremTranslated System F terms have the same closing instances#✓fully proved

Translated System F terms have exactly the same model closing instances.

theorem Tm.close_fromSystemF {n m : Nat} {Δ : List Kind}
    (φ : Fin n → Ty Δ .star) (σ : Fin m → SystemF.Model) (t : SystemF.Tm n m) :
    close σ (fromSystemF φ t) = SystemF.Tm.close σ t

Uses 14 · Used by 1

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

Proof usesScoped pure Fω terms · Erasure of Fω terms to System F syntax · Translation of System F types into Fω · Lifting System F type-variable images under a star binder · Type erasure under an untyped environment · Scoped types of pure System F · Lifting a raw erasure environment under a binder

Used byCanonical embedding preserves closing instances

TheoremCanonical embedding preserves closing instances#✓fully proved

Canonical embedding preserves arbitrary model closing instances exactly.

theorem Tm.close_embed {n m : Nat} (σ : Fin m → SystemF.Model)
    (t : SystemF.Tm n m) : close σ (Tm.embed t) = SystemF.Tm.close σ t

Uses 10 · Used by 1

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

Proof usesKinded type variables of Fω · Star-kinded variable of an all-star telescope · Translated System F terms have the same closing instances · Intrinsically kinded Fω type operators

Used byCanonical embedding preserves model erasure

TheoremCanonical embedding preserves model erasure#✓fully proved

A System F term and its Fω embedding have identical model erasures.

theorem Tm.eraseModel_embed {n : Nat} (t : SystemF.Tm n 0) :
    eraseModel (Tm.embed t) = SystemF.Tm.eraseModel t

Uses 7

Statement usesKinds of pure Fω · Canonical embedding of System F terms into Fω · Erasure of closed Fω terms to the term model · Untyped locally closed term model · Scoped terms of pure System F · Erasure of closed System F terms to the term model

Proof usesCanonical embedding preserves closing instances

TheoremType translation preserves the relational interpretation#✓fully proved

The star/forall translation preserves the same binary type interpretation.

theorem Ty.interpret_fromSystemF {n : Nat} {Δ : List Kind}
    (φ : Fin n → Ty Δ .star) (ρ : KEnv SystemF.Rel Δ) (A : SystemF.Ty n) :
    (fromSystemF φ A).interpret ρ =
      A.interpret (fun i => (φ i).interpret ρ)

Uses 14 · Used by 1

Statement usesKinded semantic environment · Kinds of pure Fω · Semantic interpretation of kinds · Intrinsically kinded Fω type operators · Translation of System F types into Fω · Relational interpretation of Fω types · Beta-invariant binary relations on the term model · Scoped types of pure System F · Binary logical relation of a System F type

Proof usesExtension of a kinded semantic environment · Relational interpretation of a weakened Fω type · Lifting System F type-variable images under a star binder · Function-space relation of beta-invariant relations · Universal quantification over a family of relations

Used byRelational interpretation of canonically embedded types

TheoremRelational interpretation of canonically embedded types#✓fully proved

Canonical embedding interprets each source variable by its matching kinded lookup.

theorem Ty.interpret_embed {n : Nat} (A : SystemF.Ty n)
    (ρ : KEnv SystemF.Rel (List.replicate n .star)) :
    (Ty.embed A).interpret ρ = A.interpret (fun i => ρ (KVar.ofFin i))

Uses 12

Statement usesKinded semantic environment · Star-kinded variable of an all-star telescope · Kinds of pure Fω · Semantic interpretation of kinds · Canonical embedding of System F types into Fω · Relational interpretation of Fω types · Beta-invariant binary relations on the term model · Scoped types of pure System F · Binary logical relation of a System F type

Proof usesKinded type variables of Fω · Intrinsically kinded Fω type operators · Type translation preserves the relational interpretation

5 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.