Type-substitution algebra for impredicative System F

13 fully proved

System F

TheoremLifted identity renaming is the identity#✓fully proved

Lifting the identity renaming gives the identity.

@[simp] theorem liftRen_id {n : Nat} :
    liftRen (id : Fin n → Fin n) = id

Uses 1 · Used by 1

Statement usesLifting a scoped renaming under a binder

Used byIdentity renaming fixes every type

TheoremLifting preserves composition of renamings#✓fully proved

Lifting preserves composition of renamings.

theorem liftRen_comp {n k l : Nat} (ρ : Fin n → Fin k)
    (η : Fin k → Fin l) :
    liftRen (η ∘ ρ) = liftRen η ∘ liftRen ρ

Uses 1 · Used by 1

Statement usesLifting a scoped renaming under a binder

Used bySuccessive type renamings fuse into their composition

Renaming and substitution laws

TheoremIdentity renaming fixes every type#✓fully proved

Type renaming by the identity does not change a type.

@[simp] theorem rename_id {n : Nat} (A : Ty n) : rename id A = A

Uses 4

Statement usesScoped types of pure System F · Type-variable renaming in System F types

Proof usesLifting a scoped renaming under a binder · Lifted identity renaming is the identity

TheoremSuccessive type renamings fuse into their composition#✓fully proved

Two type renamings fuse into their composition.

theorem rename_comp {n k l : Nat} (ρ : Fin n → Fin k)
    (η : Fin k → Fin l) (A : Ty n) :
    rename η (rename ρ A) = rename (η ∘ ρ) A

Uses 4 · Used by 1

Statement usesScoped types of pure System F · Type-variable renaming in System F types

Proof usesLifting a scoped renaming under a binder · Lifting preserves composition of renamings

Used byRenaming after a type substitution

TheoremSubstitution after a type renaming#✓fully proved

Substitution after renaming composes the variable environments.

theorem subst_rename {n k l : Nat} (ρ : Fin n → Fin k)
    (σ : Fin k → Ty l) (A : Ty n) :
    subst σ (rename ρ A) = subst (σ ∘ ρ) A

Uses 5 · Used by 4

Statement usesScoped types of pure System F · Type-variable renaming in System F types · Simultaneous type substitution in System F types

Proof usesLifting a type substitution under a type binder · Lifting a scoped renaming under a binder

Used byInstantiating a weakened type restores it · Type substitution commutes with instantiation · Lifted type substitution commutes with weakening · Variable-valued substitution is a type renaming

TheoremRenaming after a type substitution#✓fully proved

Renaming after substitution renames each substituted image.

theorem rename_subst {n k l : Nat} (σ : Fin n → Ty k)
    (ρ : Fin k → Fin l) (A : Ty n) :
    rename ρ (subst σ A) = subst (fun i => rename ρ (σ i)) A

Uses 6 · Used by 1

Statement usesScoped types of pure System F · Type-variable renaming in System F types · Simultaneous type substitution in System F types

Proof usesLifting a type substitution under a type binder · Successive type renamings fuse into their composition · Lifting a scoped renaming under a binder

Used byLifted type substitution commutes with weakening

TheoremLifted identity type substitution is the identity#✓fully proved

Lifting the variable substitution gives the variable substitution.

@[simp] theorem liftSub_var {n : Nat} :
    liftSub (var : Fin n → Ty n) = var

Uses 2 · Used by 1

Statement usesScoped types of pure System F · Lifting a type substitution under a type binder

Used byIdentity type substitution fixes every type

TheoremIdentity type substitution fixes every type#✓fully proved

Substitution of each type variable by itself is the identity.

@[simp] theorem subst_id {n : Nat} (A : Ty n) : subst var A = A

Uses 4 · Used by 3

Statement usesScoped types of pure System F · Simultaneous type substitution in System F types

Proof usesLifting a type substitution under a type binder · Lifted identity type substitution is the identity

Used byInstantiating a weakened type restores it · Type substitution commutes with instantiation · Variable-valued substitution is a type renaming

TheoremVariable-valued substitution is a type renaming#✓fully proved

A variable-valued substitution is the corresponding type renaming.

@[simp] theorem subst_var_rename {n k : Nat} (ρ : Fin n → Fin k)
    (A : Ty n) : subst (fun i => var (ρ i)) A = rename ρ A

Uses 5 · Used by 1

Statement usesScoped types of pure System F · Type-variable renaming in System F types · Simultaneous type substitution in System F types

Proof usesIdentity type substitution fixes every type · Substitution after a type renaming

Used byType renaming preserves typing

TheoremLifted type substitution commutes with weakening#✓fully proved

Lifted type substitution commutes with weakening an old type.

theorem subst_lift_rename {n k : Nat} (σ : Fin n → Ty k) (A : Ty n) :
    subst (liftSub σ) (rename Fin.succ A) =
      rename Fin.succ (subst σ A)

Uses 6 · Used by 2

Statement usesScoped types of pure System F · Lifting a type substitution under a type binder · Type-variable renaming in System F types · Simultaneous type substitution in System F types

Proof usesRenaming after a type substitution · Substitution after a type renaming

Used byType substitution preserves typing · Successive type substitutions fuse into one substitution

TheoremSuccessive type substitutions fuse into one substitution#✓fully proved

Two simultaneous type substitutions fuse by substituting each image.

theorem subst_comp {n k l : Nat} (σ : Fin n → Ty k)
    (τ : Fin k → Ty l) (A : Ty n) :
    subst τ (subst σ A) = subst (fun i => subst τ (σ i)) A

Uses 4 · Used by 1

Statement usesScoped types of pure System F · Simultaneous type substitution in System F types

Proof usesLifting a type substitution under a type binder · Lifted type substitution commutes with weakening

Used byType substitution commutes with instantiation

TheoremType substitution commutes with instantiation#✓fully proved

Type substitution commutes with discharging a type binder.

theorem subst_instantiate {n k : Nat} (σ : Fin n → Ty k)
    (B : Ty (n + 1)) (A : Ty n) :
    subst σ (instantiate B A) =
      instantiate (subst (liftSub σ) B) (subst σ A)

Uses 8 · Used by 1

Statement usesScoped types of pure System F · Instantiating the newest type binder of a type · Lifting a type substitution under a type binder · Simultaneous type substitution in System F types

Proof usesType-variable renaming in System F types · Successive type substitutions fuse into one substitution · Identity type substitution fixes every type · Substitution after a type renaming

Used byType substitution preserves typing

TheoremInstantiating a weakened type restores it#✓fully proved

Instantiating a freshly weakened type restores the original type.

@[simp] theorem instantiate_rename {n : Nat} (B A : Ty n) :
    instantiate (rename Fin.succ B) A = B

Uses 6 · Used by 1

Statement usesScoped types of pure System F · Instantiating the newest type binder of a type · Type-variable renaming in System F types

Proof usesSimultaneous type substitution in System F types · Identity type substitution fixes every type · Substitution after a type renaming

Used byInstantiating a type binder preserves typing

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.