Fω weak-CBV erasure into the existing full-beta term model

TheoremErasure of an Fω evaluation step is a beta conversion#✓fully proved

Every actual Fω CBV step preserves beta conversion of arbitrary closing instances.

theorem erasure_step {Δ : List Kind} {m : Nat} {t t' : Tm Δ m}
    (hs : Step t t') (σ : Fin m → SystemF.Model) :
    SystemF.BetaEq (Tm.close σ t) (Tm.close σ t')

Uses 21 · Used by 1

Statement usesKinds of pure Fω · Weak call-by-value reduction of Fω · Scoped pure Fω terms · Closing Fω terms in the System F term model · Beta equivalence in the untyped term model · Untyped locally closed term model

Proof usesClosing an Fω application · Beta conversion of a closed Fω lambda application · Closing an instantiated Fω term binder · Closing erases type abstraction · Closing erases type application · Closing is invariant under type substitution · Instantiation of an Fω term binder · Type substitution in Fω terms · Intrinsically kinded Fω type operators · Substitution for the newest type variable · Weak call-by-value values of Fω · Beta equivalence is a congruence in argument position · Beta equivalence is a congruence in function position · Reflexivity of beta equivalence · Application in the untyped term model

Used byErasure of multistep Fω evaluation is a beta conversion

TheoremErasure of multistep Fω evaluation is a beta conversion#✓fully proved

Finite Fω evaluation preserves beta conversion of the closing instances.

theorem erasure_steps {Δ : List Kind} {m : Nat} {t t' : Tm Δ m}
    (hs : Relation.ReflTransGen Step t t') (σ : Fin m → SystemF.Model) :
    SystemF.BetaEq (Tm.close σ t) (Tm.close σ t')

Uses 9

Statement usesKinds of pure Fω · Weak call-by-value reduction of Fω · Scoped pure Fω terms · Closing Fω terms in the System F term model · Beta equivalence in the untyped term model · Untyped locally closed term model

Proof usesErasure of an Fω evaluation step is a beta conversion · Reflexivity of beta equivalence · Transitivity of beta equivalence

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.