Erasure adapter to the existing System F scoped syntax

DefinitionErasure of Fω terms to System F syntax#✓fully proved

Erase types using the already banked System F scoped term carrier.

def eraseSyntax : {Δ : List Kind} → {m : Nat} → Tm Δ m → SystemF.Tm 0 m
  | _, _, .var i => .var i
  | _, _, .lam _ b => .lam (.all (.var 0)) (eraseSyntax b)
  | _, _, .app f a => .app (eraseSyntax f) (eraseSyntax a)
  | _, _, .tabs b => eraseSyntax b
  | _, _, .tapp f _ => eraseSyntax f

Uses 5 · Used by 10

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

Used byFω erasure commutes with term-binder instantiation · Fω erasure commutes with term-variable renaming · Fω erasure commutes with term substitution · Fω erasure ignores type substitution · Closing Fω terms in the System F term model · Beta conversion of a closed Fω lambda application · Closing an instantiated Fω term binder · Closing commutes with Fω term substitution · Closing is invariant under type substitution · Translated System F terms have the same closing instances

TheoremFω erasure ignores type substitution#✓fully proved

Erasure ignores all kind-correct type substitutions.

@[simp] theorem eraseSyntax_tySubst (σ : Ty.Sub Δ Ε) (t : Tm Δ m) :
    eraseSyntax (tySubst σ t) = eraseSyntax t

Uses 10 · Used by 2

Statement usesKinds of pure Fω · Scoped pure Fω terms · Erasure of Fω terms to System F syntax · Type substitution in Fω terms · Kind-preserving simultaneous type substitutions · Scoped terms of pure System F

Proof usesIntrinsically kinded Fω type operators · Lifting a type substitution under a type binder · Simultaneous substitution of Fω type operators · Scoped types of pure System F

Used byFω erasure commutes with term substitution · Closing is invariant under type substitution

TheoremFω erasure commutes with term-variable renaming#✓fully proved

Erasure commutes with scoped term-variable renaming.

@[simp] theorem eraseSyntax_rename (ρ : Fin m → Fin k) (t : Tm Δ m) :
    eraseSyntax (rename ρ t) = SystemF.Tm.rename ρ (eraseSyntax t)

Uses 9 · Used by 1

Statement usesKinds of pure Fω · Scoped pure Fω terms · Erasure of Fω terms to System F syntax · Term-variable renaming in Fω terms · Scoped terms of pure System F · Term-variable renaming in System F terms

Proof usesIntrinsically kinded Fω type operators · Scoped types of pure System F · Lifting a scoped renaming under a binder

Used byFω erasure commutes with term substitution

TheoremFω erasure commutes with term substitution#✓fully proved

Erasure commutes with simultaneous substitution of scoped terms.

@[simp] theorem eraseSyntax_subst (σ : Fin m → Tm Δ k) (t : Tm Δ m) :
    eraseSyntax (subst σ t) =
      SystemF.Tm.subst (fun i => eraseSyntax (σ i)) (eraseSyntax t)

Uses 15 · Used by 2

Statement usesKinds of pure Fω · Scoped pure Fω terms · Erasure of Fω terms to System F syntax · Simultaneous term substitution in Fω · Scoped terms of pure System F · Simultaneous term substitution in System F terms

Proof usesKinded type variables of Fω · Fω erasure commutes with term-variable renaming · Fω erasure ignores type substitution · Lifting a term substitution under a term binder · Type substitution in Fω terms · Intrinsically kinded Fω type operators · Lifting a term substitution under a term lambda · Term-variable renaming in System F terms · Scoped types of pure System F

Used byFω erasure commutes with term-binder instantiation · Closing commutes with Fω term substitution

TheoremFω erasure commutes with term-binder instantiation#✓fully proved

Erasure commutes with discharging a term binder.

@[simp] theorem eraseSyntax_instantiate (b : Tm Δ (m + 1)) (a : Tm Δ m) :
    eraseSyntax (instantiate b a) =
      SystemF.Tm.instantiate (eraseSyntax b) (eraseSyntax a)

Uses 8 · Used by 1

Statement usesKinds of pure Fω · Scoped pure Fω terms · Erasure of Fω terms to System F syntax · Instantiation of an Fω term binder · Scoped terms of pure System F · Instantiating the newest term binder of a term

Proof usesFω erasure commutes with term substitution · Simultaneous term substitution in System F terms

Used byClosing an instantiated Fω term binder

5 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.