Binary beta-invariant relations

7 fully proved

System F

StructureBeta-invariant binary relations on the term model#✓fully proved

A binary relation on the term model, invariant under beta conversion.

structure Rel where
  /-- The actual binary predicate. -/
  holds : Model → Model → Prop
  /-- Conversion may replace either argument independently. -/
  congr : ∀ {f f' g g'}, BetaEq f f' → BetaEq g g' →
    (holds f g ↔ holds f' g')

Uses 2 · Used by 33

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

Used byRelational interpretation of Fω types · Type-beta conversion preserves the relational interpretation · Relational interpretation of an Fω universal type · Relational interpretation of an Fω function type · Relational interpretation of an instantiated Fω type · Relational interpretation of a renamed Fω type · Relational interpretation of a substituted Fω type · Relational interpretation of a weakened Fω type · Kind algebra of beta-invariant relations · No closed Fω term inhabits \(\forall X, X\) · 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 · No closed Fω term inhabits \(\forall F, \forall X, F\,X\) · Relational interpretation of canonically embedded types · Type translation preserves the relational interpretation · 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 · Total beta-invariant relation · Universal quantification over a family of relations · Binary logical relation of a System F type · Relational interpretation of an instantiated System F type · Relational interpretation of a renamed System F type · Relational interpretation of a substituted System F type · Relational interpretation of a weakened System F type · No closed System F term inhabits \(\forall X, X\) · 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

Operations on beta-invariant relations

TheoremExtensionality of beta-invariant relations#✓fully proved

Admissible relations are determined by their binary predicates.

@[ext] theorem ext {R S : Rel}
    (h : ∀ f g, R.holds f g ↔ S.holds f g) : R = S

Uses 3

Statement usesUntyped locally closed term model · Beta-invariant binary relations on the term model

Proof usesBeta equivalence in the untyped term model

DefinitionFunction-space relation of beta-invariant relations#✓fully proved

Related functions send every related input pair to related outputs.

def arrow (A B : Rel) : Rel where
  holds f g := ∀ x y, A.holds x y → B.holds (Model.app f x) (Model.app g y)
  congr hff' hgg' := ⟨
    fun h x y hxy => (B.congr (hff'.appFun x) (hgg'.appFun y)).mp (h x y hxy),
    fun h x y hxy => (B.congr (hff'.appFun x) (hgg'.appFun y)).mpr (h x y hxy)⟩

Uses 5 · Used by 5

Statement usesBeta equivalence in the untyped term model · Beta equivalence is a congruence in function position · Untyped locally closed term model · Application in the untyped term model · Beta-invariant binary relations on the term model

Used byKind algebra of beta-invariant relations · Type translation preserves the relational interpretation · Binary logical relation of a System F type · Relational interpretation of a renamed System F type · Relational interpretation of a substituted System F type

DefinitionUniversal quantification over a family of relations#✓fully proved

Universal relatedness, over any index sort, uses impredicative Prop.

def universal {ι : Sort u} (family : ι → Rel) : Rel where
  holds f g := ∀ i, (family i).holds f g
  congr hff' hgg' := ⟨
    fun h i => ((family i).congr hff' hgg').mp (h i),
    fun h i => ((family i).congr hff' hgg').mpr (h i)⟩

Uses 3 · Used by 5

Statement usesBeta equivalence in the untyped term model · Untyped locally closed term model · Beta-invariant binary relations on the term model

Used byKind algebra of beta-invariant relations · Type translation preserves the relational interpretation · Binary logical relation of a System F type · Relational interpretation of a renamed System F type · Relational interpretation of a substituted System F type

DefinitionEmpty beta-invariant relation#✓fully proved

The empty relation is admissible and prevents vacuous universality.

def empty : Rel where
  holds _ _ := False
  congr _ _ := Iff.rfl

Uses 3 · Used by 3

Statement usesBeta equivalence in the untyped term model · Untyped locally closed term model · Beta-invariant binary relations on the term model

Used byNo closed Fω term inhabits \(\forall X, X\) · No closed Fω term inhabits \(\forall F, \forall X, F\,X\) · No closed System F term inhabits \(\forall X, X\)

DefinitionTotal beta-invariant relation#✓fully proved

The total binary relation is admissible.

def total : Rel where
  holds _ _ := True
  congr _ _ := Iff.rfl

Uses 3 · Used by 4

Statement usesBeta equivalence in the untyped term model · Untyped locally closed term model · Beta-invariant binary relations on the term model

Used byNo closed Fω term inhabits \(\forall X, X\) · Closed inhabitants of the higher-kinded identity type are identities · Higher-kinded identity inhabitants preserve admissible relations · No closed Fω term inhabits \(\forall F, \forall X, F\,X\)

DefinitionRelation of two terms beta-equal to a fixed term#✓fully proved

Both arguments belong to the fixed beta-conversion class of x.

def betaClass (x : Model) : Rel where
  holds f g := BetaEq f x ∧ BetaEq g x
  congr hff' hgg' := ⟨
    fun h => ⟨hff'.symm.trans h.1, hgg'.symm.trans h.2⟩,
    fun h => ⟨hff'.trans h.1, hgg'.trans h.2⟩⟩

Uses 5 · Used by 2

Statement usesBeta equivalence in the untyped term model · Symmetry of beta equivalence · Transitivity of beta equivalence · Untyped locally closed term model · Beta-invariant binary relations on the term model

Used byClosed inhabitants of the higher-kinded identity type are identities · Closed inhabitants of the polymorphic identity type are identities

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.