The call-by-value erasure bridge

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

Actual CBV steps preserve beta conversion of closing instances.

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

inductive Tm : Nat → Nat → Type where
  | var {n m : Nat} : Fin m → Tm n m
  | lam {n m : Nat} : Ty n → Tm n (m + 1) → Tm n m
  | app {n m : Nat} : Tm n m → Tm n m → Tm n m
  | tabs {n m : Nat} : Tm (n + 1) m → Tm n m
  | tapp {n m : Nat} : Tm n m → Ty n → Tm n m
  deriving DecidableEq, Repr

CSLibExt/Languages/LambdaCalculus/SystemF/Syntax.lean:83

inductive Step : {n m : Nat} → Tm n m → Tm n m → Prop where
  | appFun {n m : Nat} {f f' a : Tm n m} :
      Step f f' → Step (.app f a) (.app f' a)
  | appArg {n m : Nat} {f a a' : Tm n m} :
      Value f → Step a a' → Step (.app f a) (.app f a')
  | beta {n m : Nat} {A : Ty n} {b : Tm n (m + 1)} {a : Tm n m} :
      Value a → Step (.app (.lam A b) a) (b.instantiate a)
  | tappFun {n m : Nat} {f f' : Tm n m} {A : Ty n} :
      Step f f' → Step (.tapp f A) (.tapp f' A)
  | tyBeta {n m : Nat} {b : Tm (n + 1) m} {A : Ty n} :
      Step (.tapp (.tabs b) A) (b.tySubst (Fin.cases A Ty.var))

CSLibExt/Languages/LambdaCalculus/SystemF/Semantics.lean:29

abbrev Model : Type := {t : Term Nat // t.LcAt 0}

CSLibExt/Languages/LambdaCalculus/SystemF/Model.lean:27

abbrev BetaEq (f g : Model) : Prop :=
  Relation.EqvGen Term.FullBeta f.val g.val

CSLibExt/Languages/LambdaCalculus/SystemF/Model.lean:30

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)⟩

CSLibExt/Languages/LambdaCalculus/SystemF/Erasure.lean:140

Uses 19 · Used by 1

Statement usesBeta equivalence in the untyped term model · Untyped locally closed term model · One-step call-by-value evaluation · Scoped terms of pure System F · Closing System F terms in the term model

Proof usesBeta 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 · Closing a System F application · Beta conversion of a closed System F lambda application · Closing an instantiated System F term binder · Closing erases System F type abstraction · Closing erases System F type application · System F closing is invariant under type substitution · 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 byErasure of multistep System F evaluation is a beta conversion

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

Finite CBV evaluation preserves conversion of erased instances.

theorem erasure_steps {n m : Nat} {t t' : Tm n m} (hs : Steps t t')
    (σ : Fin m → Model) : BetaEq (Tm.close σ t) (Tm.close σ t')

inductive Tm : Nat → Nat → Type where
  | var {n m : Nat} : Fin m → Tm n m
  | lam {n m : Nat} : Ty n → Tm n (m + 1) → Tm n m
  | app {n m : Nat} : Tm n m → Tm n m → Tm n m
  | tabs {n m : Nat} : Tm (n + 1) m → Tm n m
  | tapp {n m : Nat} : Tm n m → Ty n → Tm n m
  deriving DecidableEq, Repr

CSLibExt/Languages/LambdaCalculus/SystemF/Syntax.lean:83

abbrev Steps {n m : Nat} : Tm n m → Tm n m → Prop :=
  Relation.ReflTransGen Step

CSLibExt/Languages/LambdaCalculus/SystemF/Semantics.lean:42

abbrev Model : Type := {t : Term Nat // t.LcAt 0}

CSLibExt/Languages/LambdaCalculus/SystemF/Model.lean:27

abbrev BetaEq (f g : Model) : Prop :=
  Relation.EqvGen Term.FullBeta f.val g.val

CSLibExt/Languages/LambdaCalculus/SystemF/Model.lean:30

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)⟩

CSLibExt/Languages/LambdaCalculus/SystemF/Erasure.lean:140

Uses 9

Statement usesBeta equivalence in the untyped term model · Untyped locally closed term model · Multi-step call-by-value evaluation · Scoped terms of pure System F · Closing System F terms in the term model

Proof usesReflexivity of beta equivalence · Transitivity of beta equivalence · One-step call-by-value evaluation · Erasure of a System F evaluation step is a beta conversion

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.