The existing untyped beta-conversion term model

10 fully proved

System F

AbbreviationUntyped locally closed term model#✓fully proved

Locally closed terms in the pinned CSLib untyped calculus.

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

Used by 53

Used byClosing Fω terms in the System F term model · Closing an Fω application · Beta conversion of a closed Fω lambda application · Closing an instantiated Fω term binder · Closing commutes with Fω term substitution · Closing erases type abstraction · Closing erases type application · Closing is invariant under type substitution · Closing an Fω variable · Erasure of closed Fω terms to the term model · Erasure of an Fω evaluation step is a beta conversion · Erasure of multistep Fω evaluation is a beta conversion · Relational interpretation of an Fω universal type · Relational interpretation of an Fω function type · Fundamental theorem of higher-kinded parametricity for Fω · Closed typed Fω terms are related to themselves · Closed inhabitants of the higher-kinded identity type are identities · Higher-kinded identity inhabitants preserve admissible relations · Canonical embedding preserves closing instances · Translated System F terms have the same closing instances · Canonical embedding preserves model erasure · Function-space relation of beta-invariant relations · Relation of two terms beta-equal to a fixed term · Empty beta-invariant relation · Extensionality of beta-invariant relations · Beta-invariant binary relations on the term model · Total beta-invariant relation · Universal quantification over a family of relations · Fundamental theorem of relational parametricity for System F · Closed typed System F terms are related to themselves · Closed inhabitants of the polymorphic identity type are identities · Polymorphic identity inhabitants preserve admissible relations · Closing System F terms in the term model · 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 · Application in the untyped term model · Beta equivalence is a congruence in argument position · Beta equivalence is a congruence in function position · Symbolic atoms of the untyped term model · Beta equivalence in the untyped term model · Model terms are locally closed · Reflexivity of beta equivalence · Symmetry of beta equivalence · Transitivity of beta equivalence

AbbreviationBeta equivalence in the untyped term model#✓fully proved

Equivalence closure of the existing full-beta reduction.

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

Uses 1 · Used by 22

Statement usesUntyped locally closed term model

Used byBeta conversion of a closed Fω lambda application · Erasure of an Fω evaluation step is a beta conversion · Erasure of multistep Fω evaluation is a beta conversion · Fundamental theorem of higher-kinded parametricity for Fω · Closed inhabitants of the higher-kinded identity type are identities · Function-space relation of beta-invariant relations · Relation of two terms beta-equal to a fixed term · Empty beta-invariant relation · Extensionality of beta-invariant relations · Beta-invariant binary relations on the term model · Total beta-invariant relation · Universal quantification over a family of relations · Fundamental theorem of relational parametricity for System F · Closed inhabitants of the polymorphic identity type are identities · Beta conversion of a closed System F lambda application · Erasure of a System F evaluation step is a beta conversion · Erasure of multistep System F evaluation is a beta conversion · Beta equivalence is a congruence in argument position · Beta equivalence is a congruence in function position · Reflexivity of beta equivalence · Symmetry of beta equivalence · Transitivity of beta equivalence

Model

DefinitionApplication in the untyped term model#✓fully proved

Application in the existing untyped term model preserves local closure.

def app (f a : Model) : Model :=
  ⟨.app f.val a.val, by
    simpa only [Term.LcAt, Bool.and_eq_true] using
      And.intro f.property a.property⟩

Uses 1 · Used by 16

Statement usesUntyped locally closed term model

Used byClosing an Fω application · Beta conversion of a closed Fω lambda application · Erasure of an Fω evaluation step is a beta conversion · Relational interpretation of an Fω function type · Fundamental theorem of higher-kinded parametricity for Fω · Closed inhabitants of the higher-kinded identity type are identities · Higher-kinded identity inhabitants preserve admissible relations · Function-space relation of beta-invariant relations · Fundamental theorem of relational parametricity for System F · Closed inhabitants of the polymorphic identity type are identities · Polymorphic identity inhabitants preserve admissible relations · Closing a System F application · Beta conversion of a closed System F lambda application · Erasure of a System F evaluation step is a beta conversion · Beta equivalence is a congruence in argument position · Beta equivalence is a congruence in function position

TheoremModel terms are locally closed#✓fully proved

The Boolean carrier invariant implies CSLib's cofinite local closure.

theorem lc (t : Model) : t.val.LC

Uses 1 · Used by 3

Statement usesUntyped locally closed term model

Used byBeta conversion of a closed System F lambda application · Beta equivalence is a congruence in argument position · Beta equivalence is a congruence in function position

DefinitionSymbolic atoms of the untyped term model#✓fully proved

A symbolic atom is locally closed; it is not a new System F constant.

def atom (i : Nat) : Model := ⟨.fvar i, rfl⟩

Uses 1

Statement usesUntyped locally closed term model

Beta Eq

TheoremReflexivity of beta equivalence#✓fully proved

Upstream beta equivalence is reflexive.

@[refl] theorem refl (f : Model) : BetaEq f f

Uses 2 · Used by 6

Statement usesBeta equivalence in the untyped term model · Untyped locally closed term model

Used byErasure of an Fω evaluation step is a beta conversion · Erasure of multistep Fω evaluation is a beta conversion · Closed inhabitants of the higher-kinded identity type are identities · Closed inhabitants of the polymorphic identity type are identities · Erasure of a System F evaluation step is a beta conversion · Erasure of multistep System F evaluation is a beta conversion

TheoremSymmetry of beta equivalence#✓fully proved

Upstream beta equivalence is symmetric.

@[symm] theorem symm {f g : Model} (h : BetaEq f g) : BetaEq g f

Uses 2 · Used by 1

Statement usesBeta equivalence in the untyped term model · Untyped locally closed term model

Used byRelation of two terms beta-equal to a fixed term

TheoremTransitivity of beta equivalence#✓fully proved

Upstream beta equivalence is transitive.

@[trans] theorem trans {f g h : Model} (hfg : BetaEq f g)
    (hgh : BetaEq g h) : BetaEq f h

Uses 2 · Used by 3

Statement usesBeta equivalence in the untyped term model · Untyped locally closed term model

Used byErasure of multistep Fω evaluation is a beta conversion · Relation of two terms beta-equal to a fixed term · Erasure of multistep System F evaluation is a beta conversion

TheoremBeta equivalence is a congruence in function position#✓fully proved

Application preserves beta equivalence in its function position.

theorem appFun {f g : Model} (h : BetaEq f g) (a : Model) :
    BetaEq (Model.app f a) (Model.app g a)

Uses 4 · Used by 3

Statement usesBeta equivalence in the untyped term model · Untyped locally closed term model · Application in the untyped term model

Proof usesModel terms are locally closed

Used byErasure of an Fω evaluation step is a beta conversion · Function-space relation of beta-invariant relations · Erasure of a System F evaluation step is a beta conversion

TheoremBeta equivalence is a congruence in argument position#✓fully proved

Application preserves beta equivalence in its argument position.

theorem appArg (f : Model) {a b : Model} (h : BetaEq a b) :
    BetaEq (Model.app f a) (Model.app f b)

Uses 4 · Used by 2

Statement usesBeta equivalence in the untyped term model · Untyped locally closed term model · Application in the untyped term model

Proof usesModel terms are locally closed

Used byErasure of an Fω evaluation step is a beta conversion · 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.