The star/forall System F fragment inside pure Fω

26 fully proved

Type translation

DefinitionLifting System F type-variable images under a star binder#✓fully proved

Extend images of System F type variables under a star-kinded binder.

def liftTypes {n : Nat} {Δ : List Kind} (φ : Fin n → Ty Δ .star) :
    Fin (n + 1) → Ty (.star :: Δ) .star :=
  Fin.cases (.var .zero) (fun i => (φ i).rename KVar.succ)

Uses 4 · Used by 18

Statement usesKinded type variables of Fω · Kinds of pure Fω · Intrinsically kinded Fω type operators · Renaming of Fω type operators

Used byTranslated System F terms have the same closing instances · Type translation preserves the relational interpretation · Translation of System F types into Fω · Translation of System F terms into Fω · Type translation commutes with type-binder instantiation · Term translation commutes with term-variable renaming · Type translation of a source renaming · Type translation of a source substitution · Term translation of a source type substitution · Term translation simulates each weak call-by-value step · Term translation commutes with term substitution · Type translation commutes with target renaming · Type translation commutes with target 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

DefinitionTranslation of System F types into Fω#✓fully proved

Translate System F types with arbitrary kind-star variable images.

def Ty.fromSystemF : {n : Nat} → {Δ : List Kind} →
    (Fin n → Ty Δ .star) → SystemF.Ty n → Ty Δ .star
  | _, _, φ, .var i => φ i
  | _, _, φ, .arr A B => .arr (fromSystemF φ A) (fromSystemF φ B)
  | _, _, φ, .all B => .all (fromSystemF (liftTypes φ) B)

Uses 4 · Used by 18

Statement usesKinds of pure Fω · Intrinsically kinded Fω type operators · Lifting System F type-variable images under a star binder · Scoped types of pure System F

Used byTranslated System F terms have the same closing instances · Type translation preserves the relational interpretation · Canonical embedding of System F types into Fω · Translation of System F terms into Fω · Type translation depends only on variable images · Type translation commutes with type-binder instantiation · Term translation commutes with term-variable renaming · Type translation of a source renaming · Type translation of a source substitution · Term translation of a source type substitution · Term translation simulates each weak call-by-value step · Term translation commutes with term substitution · Type translation commutes with target renaming · Type translation commutes with target substitution · Term translation commutes with target type substitution · Term translation commutes with type-binder instantiation · Term translation preserves System F typing · Term translation preserves weak call-by-value values

Properties of the type translation

TheoremType translation depends only on variable images#✓fully proved

The translation depends only on the images of free type variables.

theorem fromSystemF_congr {φ ψ : Fin n → Ty Δ .star}
    (h : ∀ i, φ i = ψ i) (t : SystemF.Ty n) :
    fromSystemF φ t = fromSystemF ψ t

Uses 4 · Used by 5

Statement usesKinds of pure Fω · Intrinsically kinded Fω type operators · Translation of System F types into Fω · Scoped types of pure System F

Used byType translation commutes with type-binder instantiation · Type translation of a source renaming · Type translation of a source substitution · Type translation commutes with target renaming · Type translation commutes with target substitution

TheoremType translation commutes with target renaming#✓fully proved

Target kind-preserving renaming commutes with the System F translation.

theorem fromSystemF_target_rename (φ : Fin n → Ty Δ .star)
    (ρ : KRen Δ Ε) (t : SystemF.Ty n) :
    (fromSystemF φ t).rename ρ =
      fromSystemF (fun i => (φ i).rename ρ) t

Uses 12 · Used by 3

Statement usesKind-preserving renamings of type variables · Kinds of pure Fω · Intrinsically kinded Fω type operators · Translation of System F types into Fω · Renaming of Fω type operators · Scoped types of pure System F

Proof usesLifting a renaming under a type binder · Kinded type variables of Fω · Type translation depends only on variable images · Renaming of type operators depends only on variable images · Composition of kind-preserving renamings · Lifting System F type-variable images under a star binder

Used byType translation of a source substitution · Term translation of a source type substitution · Term translation preserves System F typing

TheoremType translation commutes with target substitution#✓fully proved

Target type substitution commutes with the System F translation.

theorem fromSystemF_target_subst (φ : Fin n → Ty Δ .star)
    (σ : Sub Δ Ε) (t : SystemF.Ty n) :
    (fromSystemF φ t).subst σ =
      fromSystemF (fun i => (φ i).subst σ) t

Uses 10 · Used by 2

Statement usesKinds of pure Fω · Intrinsically kinded Fω type operators · Kind-preserving simultaneous type substitutions · Translation of System F types into Fω · Simultaneous substitution of Fω type operators · Scoped types of pure System F

Proof usesType translation depends only on variable images · Lifting a type substitution under a type binder · Lifted substitution commutes with weakening · Lifting System F type-variable images under a star binder

Used byType translation commutes with type-binder instantiation · Term translation commutes with target type substitution

TheoremType translation of a source renaming#✓fully proved

Source type renaming is precomposition of the translated variable images.

theorem fromSystemF_source_rename (φ : Fin k → Ty Δ .star)
    (ρ : Fin n → Fin k) (t : SystemF.Ty n) :
    fromSystemF φ (t.rename ρ) = fromSystemF (fun i => φ (ρ i)) t

Uses 8 · Used by 3

Statement usesKinds of pure Fω · Intrinsically kinded Fω type operators · Translation of System F types into Fω · Scoped types of pure System F · Type-variable renaming in System F types

Proof usesType translation depends only on variable images · Lifting System F type-variable images under a star binder · Lifting a scoped renaming under a binder

Used byType translation of a source substitution · Term translation of a source type substitution · Term translation preserves System F typing

TheoremType translation of a source substitution#✓fully proved

Source type substitution translates to simultaneous operator images.

theorem fromSystemF_source_subst (φ : Fin k → Ty Δ .star)
    (σ : Fin n → SystemF.Ty k) (t : SystemF.Ty n) :
    fromSystemF φ (t.subst σ) =
      fromSystemF (fun i => fromSystemF φ (σ i)) t

Uses 12 · Used by 2

Statement usesKinds of pure Fω · Intrinsically kinded Fω type operators · Translation of System F types into Fω · Scoped types of pure System F · Simultaneous type substitution in System F types

Proof usesKinded type variables of Fω · Type translation depends only on variable images · Type translation of a source renaming · Type translation commutes with target renaming · Renaming of Fω type operators · Lifting System F type-variable images under a star binder · Lifting a type substitution under a type binder

Used byType translation commutes with type-binder instantiation · Term translation of a source type substitution

TheoremType translation commutes with type-binder instantiation#✓fully proved

The System F translation commutes with type-binder instantiation.

theorem fromSystemF_instantiate (φ : Fin n → Ty Δ .star)
    (B : SystemF.Ty (n + 1)) (A : SystemF.Ty n) :
    fromSystemF φ (B.instantiate A) =
      (fromSystemF (liftTypes φ) B).instantiate (fromSystemF φ A)

Uses 15 · Used by 1

Statement usesKinds of pure Fω · Intrinsically kinded Fω type operators · Translation of System F types into Fω · Instantiation of an Fω type binder · Lifting System F type-variable images under a star binder · Scoped types of pure System F · Instantiating the newest type binder of a type

Proof usesKinded type variables of Fω · Type translation depends only on variable images · Type translation of a source substitution · Type translation commutes with target substitution · Instantiating a weakened type operator leaves it unchanged · Renaming of Fω type operators · Substitution for the newest type variable · Simultaneous substitution of Fω type operators

Used byTerm translation preserves System F typing

Term translation

DefinitionTranslation of System F terms into Fω#✓fully proved

Translate all five System F term constructors, retaining type binders.

def Tm.fromSystemF : {n m : Nat} → {Δ : List Kind} →
    (Fin n → Ty Δ .star) → SystemF.Tm n m → Tm Δ m
  | _, _, _, _, .var i => .var i
  | _, _, _, φ, .lam A b => .lam (Ty.fromSystemF φ A) (fromSystemF φ b)
  | _, _, _, φ, .app f a => .app (fromSystemF φ f) (fromSystemF φ a)
  | _, _, _, φ, .tabs b => .tabs (fromSystemF (liftTypes φ) b)
  | _, _, _, φ, .tapp f A => .tapp (fromSystemF φ f) (Ty.fromSystemF φ A)

Uses 7 · Used by 13

Statement usesKinds of pure Fω · Scoped pure Fω terms · Intrinsically kinded Fω type operators · Translation of System F types into Fω · Lifting System F type-variable images under a star binder · Scoped terms of pure System F · Scoped types of pure System F

Used byTranslated System F terms have the same closing instances · Canonical embedding 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

TheoremTerm translation preserves System F typing#✓fully proved

Every System F typing derivation is preserved by the star translation.

theorem Tm.fromSystemF_typing {n m : Nat} {Δ : List Kind}
    {Γ : SystemF.Ctx n m} {t : SystemF.Tm n m} {A : SystemF.Ty n}
    (h : SystemF.Typing Γ t A) (φ : Fin n → Ty Δ .star) :
    Typing (fun i => Ty.fromSystemF φ (Γ i)) (fromSystemF φ t)
      (Ty.fromSystemF φ A)

Uses 20 · Used by 1

Statement usesKinds of pure Fω · Translation of System F terms into Fω · Intrinsically kinded Fω type operators · Translation of System F types into Fω · Typing rules of pure Fω · Term variable contexts of System F · Scoped terms of pure System F · Scoped types of pure System F · Extrinsic typing of pure System F terms

Proof usesTerm contexts of pure Fω · Kinded type variables of Fω · Scoped pure Fω terms · Type translation commutes with type-binder instantiation · Type translation of a source renaming · Type translation commutes with target renaming · Instantiation of an Fω type binder · Renaming of Fω type operators · Lifting System F type-variable images under a star binder · Instantiating the newest type binder of a type · Type-variable renaming in System F types

Used byCanonical embedding preserves System F typing

DefinitionStar-kinded variable of an all-star telescope#✓fully proved

The corresponding star-kinded variable in an n-star telescope.

def KVar.ofFin : {n : Nat} → Fin n → KVar (List.replicate n .star) .star
  | 0, i => nomatch i
  | _n + 1, i => Fin.cases .zero (fun j => .succ (ofFin j)) i

Uses 2 · Used by 6

Statement usesKinded type variables of Fω · Kinds of pure Fω

Used byCanonical embedding preserves closing instances · Relational interpretation of canonically embedded types · Canonical embedding of System F types into Fω · Canonical embedding of System F terms into Fω · Canonical embedding preserves single evaluation steps · Canonical embedding preserves System F typing

DefinitionCanonical embedding of System F types into Fω#✓fully proved

The canonical variable-for-variable embedding of System F types.

def Ty.embed {n : Nat} (t : SystemF.Ty n) : Ty (List.replicate n .star) .star :=
  fromSystemF (fun i => .var (KVar.ofFin i)) t

Uses 6 · Used by 2

Statement usesKinded type variables of Fω · Star-kinded variable of an all-star telescope · Kinds of pure Fω · Intrinsically kinded Fω type operators · Translation of System F types into Fω · Scoped types of pure System F

Used byRelational interpretation of canonically embedded types · Canonical embedding preserves System F typing

DefinitionCanonical embedding of System F terms into Fω#✓fully proved

The canonical scoped embedding of System F terms into pure Fω.

def Tm.embed {n m : Nat} (t : SystemF.Tm n m) : Tm (List.replicate n .star) m :=
  fromSystemF (fun i => .var (KVar.ofFin i)) t

Uses 7 · Used by 5

Statement usesKinded type variables of Fω · Star-kinded variable of an all-star telescope · Kinds of pure Fω · Scoped pure Fω terms · Translation of System F terms into Fω · Intrinsically kinded Fω type operators · Scoped terms of pure System F

Used byCanonical embedding preserves closing instances · Canonical embedding preserves model erasure · Canonical embedding preserves single evaluation steps · Canonical embedding preserves multistep evaluation · Canonical embedding preserves System F typing

TheoremCanonical embedding preserves System F typing#✓fully proved

Canonical embedding preserves every System F typing derivation.

theorem Tm.embed_typing {n m : Nat} {Γ : SystemF.Ctx n m}
    {t : SystemF.Tm n m} {A : SystemF.Ty n} (h : SystemF.Typing Γ t A) :
    Typing (fun i => Ty.embed (Γ i)) (Tm.embed t) (Ty.embed A)

Uses 12

Statement usesKinds of pure Fω · Canonical embedding of System F terms into Fω · Canonical embedding of System F types into Fω · Typing rules of pure Fω · Term variable contexts of System F · Scoped terms of pure System F · Scoped types of pure System F · Extrinsic typing of pure System F terms

Proof usesKinded type variables of Fω · Star-kinded variable of an all-star telescope · Term translation preserves System F typing · Intrinsically kinded Fω type operators

TheoremTerm translation depends only on type-variable images#✓fully proved

Term translation depends only on the images of its free type variables.

theorem Tm.fromSystemF_congr {n m : Nat} {Δ : List Kind}
    {φ ψ : Fin n → Ty Δ .star} (h : ∀ i, φ i = ψ i) (t : SystemF.Tm n m) :
    fromSystemF φ t = fromSystemF ψ t

Uses 5 · Used by 3

Statement usesKinds of pure Fω · Scoped pure Fω terms · Translation of System F terms into Fω · Intrinsically kinded Fω type operators · Scoped terms of pure System F

Used byTerm translation of a source type substitution · Term translation commutes with target type substitution · Term translation commutes with type-binder instantiation

TheoremTerm translation commutes with target type substitution#✓fully proved

Operator substitution commutes with translating System F terms.

theorem Tm.fromSystemF_target_tySubst {n m : Nat} {Δ Ε : List Kind}
    (φ : Fin n → Ty Δ .star) (σ : Ty.Sub Δ Ε) (t : SystemF.Tm n m) :
    (fromSystemF φ t).tySubst σ =
      fromSystemF (fun i => (φ i).subst σ) t

Uses 15 · Used by 2

Statement usesKinds of pure Fω · Scoped pure Fω terms · Translation of System F terms into Fω · Type substitution in Fω terms · Intrinsically kinded Fω type operators · Kind-preserving simultaneous type substitutions · Simultaneous substitution of Fω type operators · Scoped terms of pure System F

Proof usesTerm translation depends only on type-variable images · Translation of System F types into Fω · Type translation commutes with target substitution · Lifting a type substitution under a type binder · Lifted substitution commutes with weakening · Lifting System F type-variable images under a star binder · Scoped types of pure System F

Used byTerm translation commutes with type-binder instantiation · Term translation commutes with weakening under a type binder

TheoremTerm translation of a source type substitution#✓fully proved

Source type substitution commutes with the pure-term translation.

theorem Tm.fromSystemF_source_tySubst {n k m : Nat} {Δ : List Kind}
    (φ : Fin k → Ty Δ .star) (σ : Fin n → SystemF.Ty k)
    (t : SystemF.Tm n m) :
    fromSystemF φ (t.tySubst σ) =
      fromSystemF (fun i => Ty.fromSystemF φ (σ i)) t

Uses 17 · Used by 2

Statement usesKinds of pure Fω · Scoped pure Fω terms · Translation of System F terms into Fω · Intrinsically kinded Fω type operators · Translation of System F types into Fω · Scoped terms of pure System F · Type substitution in System F terms · Scoped types of pure System F

Proof usesKinded type variables of Fω · Term translation depends only on type-variable images · Type translation of a source renaming · Type translation of a source substitution · Type translation commutes with target renaming · Renaming of Fω type operators · Lifting System F type-variable images under a star binder · Lifting a type substitution under a type binder · Simultaneous type substitution in System F types

Used byTerm translation commutes with type-binder instantiation · Term translation commutes with weakening under a type binder

TheoremTerm translation commutes with weakening under a type binder#✓fully proved

Weakening beneath a type binder agrees in both calculus presentations.

theorem Tm.fromSystemF_tyRename_succ {n m : Nat} {Δ : List Kind}
    (φ : Fin n → Ty Δ .star) (t : SystemF.Tm n m) :
    fromSystemF (liftTypes φ) (t.tyRename Fin.succ) =
      (fromSystemF φ t).tyRename KVar.succ

Uses 16 · Used by 1

Statement usesKinded type variables of Fω · Kinds of pure Fω · Scoped pure Fω terms · Translation of System F terms into Fω · Type-variable renaming in Fω terms · Intrinsically kinded Fω type operators · Lifting System F type-variable images under a star binder · Scoped terms of pure System F · Type-variable renaming in System F terms

Proof usesTerm translation of a source type substitution · Term translation commutes with target type substitution · Type substitution in Fω terms · Renaming of Fω type operators · Simultaneous substitution of Fω type operators · Renaming as substitution by variables · Scoped types of pure System F

Used byTerm translation commutes with term substitution

TheoremTerm translation commutes with term-variable renaming#✓fully proved

Term-variable renaming commutes with the System F translation.

theorem Tm.fromSystemF_rename {n m k : Nat} {Δ : List Kind}
    (φ : Fin n → Ty Δ .star) (ρ : Fin m → Fin k) (t : SystemF.Tm n m) :
    fromSystemF φ (t.rename ρ) = (fromSystemF φ t).rename ρ

Uses 11 · Used by 1

Statement usesKinds of pure Fω · Scoped pure Fω terms · Translation of System F terms into Fω · Term-variable renaming in Fω terms · Intrinsically kinded Fω type operators · Scoped terms of pure System F · Term-variable renaming in System F terms

Proof usesTranslation of System F types into Fω · Lifting System F type-variable images under a star binder · Scoped types of pure System F · Lifting a scoped renaming under a binder

Used byTerm translation commutes with term substitution

TheoremTerm translation commutes with term substitution#✓fully proved

Simultaneous term substitution commutes with the System F translation.

theorem Tm.fromSystemF_subst {n m k : Nat} {Δ : List Kind}
    (φ : Fin n → Ty Δ .star) (σ : Fin m → SystemF.Tm n k)
    (t : SystemF.Tm n m) :
    fromSystemF φ (t.subst σ) =
      (fromSystemF φ t).subst (fun i => fromSystemF φ (σ i))

Uses 17 · Used by 1

Statement usesKinds of pure Fω · Scoped pure Fω terms · Translation of System F terms into Fω · Simultaneous term substitution in Fω · Intrinsically kinded Fω type operators · Scoped terms of pure System F · Simultaneous term substitution in System F terms

Proof usesKinded type variables of Fω · Term translation commutes with term-variable renaming · Term translation commutes with weakening under a type binder · Lifting a term substitution under a term binder · Type-variable renaming in Fω terms · Translation of System F types into Fω · Lifting System F type-variable images under a star binder · Lifting a term substitution under a term lambda · Type-variable renaming in System F terms · Scoped types of pure System F

Used byTerm translation commutes with term-binder instantiation

TheoremTerm translation commutes with term-binder instantiation#✓fully proved

Term-binder instantiation commutes with the System F translation.

theorem Tm.fromSystemF_instantiate {n m : Nat} {Δ : List Kind}
    (φ : Fin n → Ty Δ .star) (b : SystemF.Tm n (m + 1))
    (a : SystemF.Tm n m) :
    fromSystemF φ (b.instantiate a) =
      (fromSystemF φ b).instantiate (fromSystemF φ a)

Uses 9 · Used by 1

Statement usesKinds of pure Fω · Scoped pure Fω terms · Translation of System F terms into Fω · Instantiation of an Fω term binder · Intrinsically kinded Fω type operators · Scoped terms of pure System F · Instantiating the newest term binder of a term

Proof usesTerm translation commutes with term substitution · Simultaneous term substitution in Fω

Used byTerm translation simulates each weak call-by-value step

TheoremTerm translation commutes with type-binder instantiation#✓fully proved

Type-binder discharge agrees for translated System F terms.

theorem Tm.fromSystemF_tyInstantiate {n m : Nat} {Δ : List Kind}
    (φ : Fin n → Ty Δ .star) (b : SystemF.Tm (n + 1) m)
    (A : SystemF.Ty n) :
    fromSystemF φ (b.tySubst (Fin.cases A SystemF.Ty.var)) =
      (fromSystemF (liftTypes φ) b).tySubst (Ty.single (Ty.fromSystemF φ A))

Uses 19 · Used by 1

Statement usesKinds of pure Fω · Scoped pure Fω terms · Translation of System F terms into Fω · Type substitution in Fω terms · Intrinsically kinded Fω type operators · Translation of System F types into Fω · Substitution for the newest type variable · Lifting System F type-variable images under a star binder · Scoped terms of pure System F · Type substitution in System F terms · Scoped types of pure System F

Proof usesKinded type variables of Fω · Term translation depends only on type-variable images · Term translation of a source type substitution · Term translation commutes with target type substitution · Instantiation of an Fω type binder · Instantiating a weakened type operator leaves it unchanged · Renaming of Fω type operators · Simultaneous substitution of Fω type operators

Used byTerm translation simulates each weak call-by-value step

TheoremTerm translation preserves weak call-by-value values#✓fully proved

The System F translation preserves both weak-CBV value forms.

theorem Tm.fromSystemF_value {n m : Nat} {Δ : List Kind}
    (φ : Fin n → Ty Δ .star) {t : SystemF.Tm n m} (h : SystemF.Value t) :
    Value (fromSystemF φ t)

Uses 10 · Used by 1

Statement usesKinds of pure Fω · Translation of System F terms into Fω · Intrinsically kinded Fω type operators · Weak call-by-value values of Fω · Scoped terms of pure System F · Value forms of pure System F

Proof usesScoped pure Fω terms · Translation of System F types into Fω · Lifting System F type-variable images under a star binder · Scoped types of pure System F

Used byTerm translation simulates each weak call-by-value step

TheoremTerm translation simulates each weak call-by-value step#✓fully proved

Every System F weak-CBV step is simulated by one Fω weak-CBV step.

theorem Tm.fromSystemF_step {n m : Nat} {Δ : List Kind}
    (φ : Fin n → Ty Δ .star) {t t' : SystemF.Tm n m}
    (h : SystemF.Step t t') : Step (fromSystemF φ t) (fromSystemF φ t')

Uses 20 · Used by 1

Statement usesKinds of pure Fω · Weak call-by-value reduction of Fω · Translation of System F terms into Fω · Intrinsically kinded Fω type operators · One-step call-by-value evaluation · Scoped terms of pure System F

Proof usesScoped pure Fω terms · Term translation commutes with term-binder instantiation · Term translation commutes with type-binder instantiation · Term translation preserves weak call-by-value values · Instantiation of an Fω term binder · Type substitution in Fω terms · Translation of System F types into Fω · Substitution for the newest type variable · Weak call-by-value values of Fω · Lifting System F type-variable images under a star binder · Instantiating the newest term binder of a term · Type substitution in System F terms · Scoped types of pure System F · Value forms of pure System F

Used byCanonical embedding preserves single evaluation steps

TheoremCanonical embedding preserves single evaluation steps#✓fully proved

The canonical embedding preserves individual System F evaluation steps.

theorem Tm.embed_step {n m : Nat} {t t' : SystemF.Tm n m}
    (h : SystemF.Step t t') : Step (Tm.embed t) (Tm.embed t')

Uses 9 · Used by 1

Statement usesKinds of pure Fω · Weak call-by-value reduction of Fω · Canonical embedding of System F terms into Fω · One-step call-by-value evaluation · Scoped terms of pure System F

Proof usesKinded type variables of Fω · Star-kinded variable of an all-star telescope · Term translation simulates each weak call-by-value step · Intrinsically kinded Fω type operators

Used byCanonical embedding preserves multistep evaluation

TheoremCanonical embedding preserves multistep evaluation#✓fully proved

The canonical embedding preserves finite System F evaluation sequences.

theorem Tm.embed_steps {n m : Nat} {t t' : SystemF.Tm n m}
    (h : SystemF.Steps t t') :
    Relation.ReflTransGen Step (Tm.embed t) (Tm.embed t')

Uses 8

Statement usesKinds of pure Fω · Weak call-by-value reduction of Fω · Scoped pure Fω terms · Canonical embedding of System F terms into Fω · Multi-step call-by-value evaluation · Scoped terms of pure System F

Proof usesCanonical embedding preserves single evaluation steps · One-step call-by-value evaluation

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.