Impredicative binary interpretation of System F types

DefinitionBinary logical relation of a System F type#✓fully proved

The impredicative binary logical relation denoted by a System F type.

@[simp] def interpret {n : Nat} : Ty n → (Fin n → Rel) → Rel
  | .var i, ρ => ρ i
  | .arr A B, ρ => Rel.arrow (interpret A ρ) (interpret B ρ)
  | .all B, ρ => Rel.universal (fun R : Rel => interpret B (Fin.cases R ρ))

Uses 4 · Used by 9

Statement usesBeta-invariant binary relations on the term model · Function-space relation of beta-invariant relations · Universal quantification over a family of relations · Scoped types of pure System F

Used byRelational interpretation of canonically embedded types · Type translation preserves the relational interpretation · 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 · 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

TheoremRelational interpretation of a renamed System F type#✓fully proved

Interpreting a renamed type precomposes the relation environment.

theorem interpret_rename {n k : Nat} (η : Fin n → Fin k) (A : Ty n)
    (ρ : Fin k → Rel) :
    interpret (rename η A) ρ = interpret A (ρ ∘ η)

Uses 7 · Used by 2

Statement usesBeta-invariant binary relations on the term model · Scoped types of pure System F · Binary logical relation of a System F type · Type-variable renaming in System F types

Proof usesFunction-space relation of beta-invariant relations · Universal quantification over a family of relations · Lifting a scoped renaming under a binder

Used byRelational interpretation of a substituted System F type · Relational interpretation of a weakened System F type

TheoremRelational interpretation of a substituted System F type#✓fully proved

Type substitution is interpreted by substituting arbitrary relations.

theorem interpret_subst {n k : Nat} (σ : Fin n → Ty k) (A : Ty n)
    (ρ : Fin k → Rel) :
    interpret (subst σ A) ρ = interpret A (fun i => interpret (σ i) ρ)

Uses 8 · Used by 1

Statement usesBeta-invariant binary relations on the term model · Scoped types of pure System F · Binary logical relation of a System F type · Simultaneous type substitution in System F types

Proof usesFunction-space relation of beta-invariant relations · Universal quantification over a family of relations · Relational interpretation of a renamed System F type · Lifting a type substitution under a type binder

Used byRelational interpretation of an instantiated System F type

TheoremRelational interpretation of an instantiated System F type#✓fully proved

Universal instantiation inserts the argument's whole logical relation.

theorem interpret_instantiate {n : Nat} (B : Ty (n + 1)) (A : Ty n)
    (ρ : Fin n → Rel) :
    interpret (instantiate B A) ρ =
      interpret B (Fin.cases (interpret A ρ) ρ)

Uses 6 · Used by 1

Statement usesBeta-invariant binary relations on the term model · Scoped types of pure System F · Instantiating the newest type binder of a type · Binary logical relation of a System F type

Proof usesRelational interpretation of a substituted System F type · Simultaneous type substitution in System F types

Used byFundamental theorem of relational parametricity for System F

TheoremRelational interpretation of a weakened System F type#✓fully proved

Weakening a type does not make it depend on the new arbitrary relation.

@[simp] theorem interpret_weaken {n : Nat} (A : Ty n) (ρ : Fin n → Rel)
    (R : Rel) : interpret (rename Fin.succ A) (Fin.cases R ρ) =
      interpret A ρ

Uses 5 · Used by 1

Statement usesBeta-invariant binary relations on the term model · Scoped types of pure System F · Binary logical relation of a System F type · Type-variable renaming in System F types

Proof usesRelational interpretation of a renamed System F type

Used byFundamental theorem of relational parametricity for System F

5 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.