System F erasure and closing environments

21 fully proved

System F

DefinitionShift of untyped bound indices above a cutoff#✓fully proved

Shift free bound indices in CSLib syntax, preserving indices below c.

def shiftAt (c : Nat) : Term Nat → Term Nat
  | .bvar i => .bvar (if i < c then i else i + 1)
  | .fvar x => .fvar x
  | .app f a => .app (shiftAt c f) (shiftAt c a)
  | .abs b => .abs (shiftAt (c + 1) b)

Used by 6

Used byErasure with locally closed images is locally closed · Opening commutes with erasure under an environment · Shifting commutes with erasure under an environment · Erasure of a term substitution · Lifting a raw erasure environment under a binder · Shifting leaves locally closed terms unchanged

DefinitionLifting a raw erasure environment under a binder#✓fully proved

Lift a raw erasure environment beneath one scoped term binder.

def liftRaw {m : Nat} (σ : Fin m → Term Nat) :
    Fin (m + 1) → Term Nat :=
  Fin.cases (.bvar 0) (fun i => shiftAt 0 (σ i))

Uses 1 · Used by 9

Statement usesShift of untyped bound indices above a cutoff

Used byTranslated System F terms have the same closing instances · Beta conversion of a closed System F lambda application · Type erasure under an untyped environment · Erasure with locally closed images is locally closed · Opening commutes with erasure under an environment · Erasure of a term-variable renaming · Shifting commutes with erasure under an environment · Erasure of a term substitution · Untyped erasure is invariant under type substitution

TheoremShifting leaves locally closed terms unchanged#✓fully proved

Introducing a binder does not shift an already locally closed term.

theorem shiftAt_closed (c : Nat) (t : Term Nat) (h : t.LcAt 0) :
    shiftAt c t = t

Uses 1 · Used by 2

Statement usesShift of untyped bound indices above a cutoff

Used byBeta conversion of a closed System F lambda application · Opening commutes with erasure under an environment

Type erasure and closing

DefinitionType erasure under an untyped environment#✓fully proved

Erase a scoped term under an arbitrary simultaneous untyped environment.

@[simp] def eraseWith {n m : Nat} (σ : Fin m → Term Nat) :
    Tm n m → Term Nat
  | .var i => σ i
  | .lam _ b => .abs (eraseWith (liftRaw σ) b)
  | .app f a => .app (eraseWith σ f) (eraseWith σ a)
  | .tabs b => eraseWith σ b
  | .tapp f _ => eraseWith σ f

Uses 3 · Used by 10

Statement usesScoped terms of pure System F · Scoped types of pure System F · Lifting a raw erasure environment under a binder

Used byTranslated System F terms have the same closing instances · Closing System F terms in the term model · Beta conversion of a closed System F lambda application · Type erasure of System F terms to untyped terms · Erasure with locally closed images is locally closed · Opening commutes with erasure under an environment · Erasure of a term-variable renaming · Shifting commutes with erasure under an environment · Erasure of a term substitution · Untyped erasure is invariant under type substitution

DefinitionType erasure of System F terms to untyped terms#✓fully proved

Type erasure into the existing untyped de Bruijn syntax.

def erase {n m : Nat} (t : Tm n m) : Term Nat :=
  eraseWith (fun i => .bvar i.val) t

Uses 2

Statement usesScoped terms of pure System F · Type erasure under an untyped environment

TheoremErasure with locally closed images is locally closed#✓fully proved

Erasure preserves the closure invariant of its environment images.

theorem eraseWith_lcAt {n m k : Nat} (σ : Fin m → Term Nat) (t : Tm n m)
    (hσ : ∀ i, (σ i).LcAt k) : (eraseWith σ t).LcAt k

Uses 5 · Used by 1

Statement usesScoped terms of pure System F · Type erasure under an untyped environment

Proof usesScoped types of pure System F · Lifting a raw erasure environment under a binder · Shift of untyped bound indices above a cutoff

Used byClosing System F terms in the term model

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

Close every scoped term variable with a locally closed model term.

def close {n m : Nat} (σ : Fin m → Model) (t : Tm n m) : Model :=
  ⟨eraseWith (fun i => (σ i).val) t,
    eraseWith_lcAt _ t (fun i => (σ i).property)⟩

Uses 4 · Used by 18

Statement usesUntyped locally closed term model · Scoped terms of pure System F · Type erasure under an untyped environment · Erasure with locally closed images is locally closed

Used byClosing Fω terms in the System F term model · Closing an instantiated Fω term binder · Closing commutes with Fω term substitution · Closing is invariant under type substitution · Canonical embedding preserves closing instances · Translated System F terms have the same closing instances · Fundamental theorem of relational parametricity for System F · Closing a System F application · Beta conversion of a closed System F lambda application · Closing an instantiated System F term binder · Closing commutes with System F term substitution · Closing erases System F type abstraction · Closing erases System F type application · System F closing is invariant under type substitution · Closing a System F variable · Erasure of closed System F terms to the term model · Erasure of a System F evaluation step is a beta conversion · Erasure of multistep System F evaluation is a beta conversion

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

Erase a term with no free term variables into the existing term model.

def eraseModel {n : Nat} (t : Tm n 0) : Model := close Fin.elim0 t

Uses 3 · Used by 4

Statement usesUntyped locally closed term model · Scoped terms of pure System F · Closing System F terms in the term model

Used byCanonical embedding preserves model erasure · Closed typed System F terms are related to themselves · Closed inhabitants of the polymorphic identity type are identities · Polymorphic identity inhabitants preserve admissible relations

TheoremOpening commutes with erasure under an environment#✓fully proved

Opening an erased instance opens exactly its raw environment images.

theorem eraseWith_openRec {n m : Nat} (u : Term Nat) (hu : u.LcAt 0)
    (k : Nat) (σ : Fin m → Term Nat) (t : Tm n m) :
    Term.openRec k u (eraseWith σ t) =
      eraseWith (fun i => Term.openRec k u (σ i)) t

Uses 6 · Used by 1

Statement usesScoped terms of pure System F · Type erasure under an untyped environment

Proof usesScoped types of pure System F · Lifting a raw erasure environment under a binder · Shift of untyped bound indices above a cutoff · Shifting leaves locally closed terms unchanged

Used byBeta conversion of a closed System F lambda application

TheoremUntyped erasure is invariant under type substitution#✓fully proved

Type substitution changes no part of the erased untyped term.

theorem eraseWith_tySubst {n k m : Nat} (σ : Fin n → Ty k)
    (η : Fin m → Term Nat) (t : Tm n m) :
    eraseWith η (tySubst σ t) = eraseWith η t

Uses 7 · Used by 2

Statement usesScoped terms of pure System F · Type erasure under an untyped environment · Type substitution in System F terms · Scoped types of pure System F

Proof usesLifting a type substitution under a type binder · Simultaneous type substitution in System F types · Lifting a raw erasure environment under a binder

Used bySystem F closing is invariant under type substitution · Erasure of a term substitution

TheoremClosing a System F variable#✓fully proved

Closing a variable returns exactly its environment image.

@[simp] theorem close_var {n m : Nat} (σ : Fin m → Model) (i : Fin m) :
    close σ (.var i : Tm n m) = σ i

Uses 3

Statement usesUntyped locally closed term model · Scoped terms of pure System F · Closing System F terms in the term model

TheoremClosing a System F application#✓fully proved

Closing commutes with the upstream model's application.

@[simp] theorem close_app {n m : Nat} (σ : Fin m → Model) (f a : Tm n m) :
    close σ (.app f a) = Model.app (close σ f) (close σ a)

Uses 4 · Used by 1

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

Used byErasure of a System F evaluation step is a beta conversion

TheoremClosing erases System F type abstraction#✓fully proved

A type lambda contributes no untyped binder.

@[simp] theorem close_tabs {n m : Nat} (σ : Fin m → Model)
    (b : Tm (n + 1) m) : close σ (.tabs b) = close σ b

Uses 3 · Used by 1

Statement usesUntyped locally closed term model · Scoped terms of pure System F · Closing System F terms in the term model

Used byErasure of a System F evaluation step is a beta conversion

TheoremClosing erases System F type application#✓fully proved

A type argument contributes no untyped application.

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

Uses 4 · Used by 1

Statement usesUntyped locally closed term model · Scoped terms of pure System F · Closing System F terms in the term model · Scoped types of pure System F

Used byErasure of a System F evaluation step is a beta conversion

TheoremSystem F closing is invariant under type substitution#✓fully proved

Closing is independent of every type substitution.

@[simp] theorem close_tySubst {n k m : Nat} (σ : Fin n → Ty k)
    (η : Fin m → Model) (t : Tm n m) :
    close η (tySubst σ t) = close η t

Uses 6 · Used by 1

Statement usesUntyped locally closed term model · Scoped terms of pure System F · Closing System F terms in the term model · Type substitution in System F terms · Scoped types of pure System F

Proof usesUntyped erasure is invariant under type substitution

Used byErasure of a System F evaluation step is a beta conversion

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

An erased lambda application beta-converts to its extended body instance.

theorem close_beta {n m : Nat} (σ : Fin m → Model) (A : Ty n)
    (b : Tm n (m + 1)) (a : Model) :
    BetaEq (Model.app (close σ (.lam A b)) a) (close (Fin.cases a σ) b)

Uses 11 · Used by 3

Statement usesBeta equivalence in the untyped term model · Untyped locally closed term model · Application in the untyped term model · Scoped terms of pure System F · Closing System F terms in the term model · Scoped types of pure System F

Proof usesModel terms are locally closed · Type erasure under an untyped environment · Opening commutes with erasure under an environment · Lifting a raw erasure environment under a binder · Shifting leaves locally closed terms unchanged

Used byBeta conversion of a closed Fω lambda application · Fundamental theorem of relational parametricity for System F · Erasure of a System F evaluation step is a beta conversion

TheoremShifting commutes with erasure under an environment#✓fully proved

Shifting an erased instance shifts exactly its raw environment images.

theorem eraseWith_shift {n m : Nat} (c : Nat) (σ : Fin m → Term Nat)
    (t : Tm n m) : shiftAt c (eraseWith σ t) =
      eraseWith (fun i => shiftAt c (σ i)) t

Uses 5 · Used by 1

Statement usesScoped terms of pure System F · Type erasure under an untyped environment · Shift of untyped bound indices above a cutoff

Proof usesScoped types of pure System F · Lifting a raw erasure environment under a binder

Used byErasure of a term substitution

TheoremErasure of a term-variable renaming#✓fully proved

Erasing a term-variable renaming precomposes the raw environment.

theorem eraseWith_rename {n m k : Nat} (η : Fin m → Fin k)
    (σ : Fin k → Term Nat) (t : Tm n m) :
    eraseWith σ (rename η t) = eraseWith (σ ∘ η) t

Uses 6 · Used by 1

Statement usesScoped terms of pure System F · Type erasure under an untyped environment · Term-variable renaming in System F terms

Proof usesScoped types of pure System F · Lifting a raw erasure environment under a binder · Lifting a scoped renaming under a binder

Used byErasure of a term substitution

TheoremErasure of a term substitution#✓fully proved

Actual term substitution erases by composing raw environments.

theorem eraseWith_subst {n m k : Nat} (σ : Fin m → Tm n k)
    (η : Fin k → Term Nat) (t : Tm n m) :
    eraseWith η (subst σ t) =
      eraseWith (fun i => eraseWith η (σ i)) t

Uses 12 · Used by 1

Statement usesScoped terms of pure System F · Type erasure under an untyped environment · Simultaneous term substitution in System F terms

Proof usesErasure of a term-variable renaming · Shifting commutes with erasure under an environment · Untyped erasure is invariant under type substitution · Lifting a term substitution under a term lambda · Term-variable renaming in System F terms · Type substitution in System F terms · Scoped types of pure System F · Lifting a raw erasure environment under a binder · Shift of untyped bound indices above a cutoff

Used byClosing commutes with System F term substitution

TheoremClosing commutes with System F term substitution#✓fully proved

Closing an actual substitution composes its model-valued environments.

theorem close_subst {n m k : Nat} (σ : Fin m → Tm n k)
    (η : Fin k → Model) (t : Tm n m) :
    close η (subst σ t) = close (fun i => close η (σ i)) t

Uses 5 · Used by 2

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

Proof usesErasure of a term substitution

Used byClosing commutes with Fω term substitution · Closing an instantiated System F term binder

TheoremClosing an instantiated System F term binder#✓fully proved

Actual binder discharge agrees with extending the closing environment.

theorem close_instantiate {n m : Nat} (η : Fin m → Model)
    (b : Tm n (m + 1)) (a : Tm n m) :
    close η (instantiate b a) = close (Fin.cases (close η a) η) b

Uses 6 · Used by 2

Statement usesUntyped locally closed term model · Scoped terms of pure System F · Closing System F terms in the term model · Instantiating the newest term binder of a term

Proof usesClosing commutes with System F term substitution · Simultaneous term substitution in System F terms

Used byClosing an instantiated Fω term binder · Erasure of a System F evaluation step is a beta conversion

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.