Capture-avoiding binding laws for kinded type operators

TheoremRenaming of type operators depends only on variable images#✓fully proved

Renaming depends only on its action on kinded variables.

theorem rename_congr {ρ τ : KRen Δ Ε}
    (h : ∀ {ν} (x : KVar Δ ν), ρ x = τ x) (t : Ty Δ κ) :
    rename ρ t = rename τ t

Uses 5 · Used by 4

Statement usesKind-preserving renamings of type variables · Kinded type variables of Fω · Kinds of pure Fω · Intrinsically kinded Fω type operators · Renaming of Fω type operators

Used byIdentity renaming fixes type operators · Composition of kind-preserving renamings · Renaming after substitution of type operators · Type translation commutes with target renaming

TheoremIdentity renaming fixes type operators#✓fully proved

The identity renaming fixes every type operator.

@[simp] theorem rename_id (t : Ty Δ κ) :
    rename (fun {_} x => x) t = t

Uses 6

Statement usesKinded type variables of Fω · Kinds of pure Fω · Intrinsically kinded Fω type operators · Renaming of Fω type operators

Proof usesLifting a renaming under a type binder · Renaming of type operators depends only on variable images

TheoremComposition of kind-preserving renamings#✓fully proved

Successive kind-preserving renamings fuse, including beneath binders.

theorem rename_rename (ρ : KRen Δ Ε) (τ : KRen Ε Ζ) (t : Ty Δ κ) :
    rename τ (rename ρ t) = rename (fun {_} x => τ (ρ x)) t

Uses 7 · Used by 2

Statement usesKind-preserving renamings of type variables · Kinded type variables of Fω · Kinds of pure Fω · Intrinsically kinded Fω type operators · Renaming of Fω type operators

Proof usesLifting a renaming under a type binder · Renaming of type operators depends only on variable images

Used byRenaming after substitution of type operators · Type translation commutes with target renaming

TheoremSubstitution of type operators depends only on variable images#✓fully proved

Substitution depends only on the images of kinded variables.

theorem subst_congr {σ τ : Sub Δ Ε}
    (h : ∀ {ν} (x : KVar Δ ν), σ x = τ x) (t : Ty Δ κ) :
    subst σ t = subst τ t

Uses 5 · Used by 7

Statement usesKinded type variables of Fω · Kinds of pure Fω · Intrinsically kinded Fω type operators · Kind-preserving simultaneous type substitutions · Simultaneous substitution of Fω type operators

Used byRenaming commutes with type-binder instantiation · Renaming after substitution of type operators · Identity substitution fixes type operators · Substitution commutes with type-binder instantiation · Substitution after renaming of type operators · Composition of simultaneous type-operator substitutions · Renaming as substitution by variables

TheoremIdentity substitution fixes type operators#✓fully proved

Substituting each variable by itself fixes every type operator.

@[simp] theorem subst_id (t : Ty Δ κ) : subst Ty.var t = t

Uses 6 · Used by 1

Statement usesKinded type variables of Fω · Kinds of pure Fω · Intrinsically kinded Fω type operators · Simultaneous substitution of Fω type operators

Proof usesLifting a type substitution under a type binder · Substitution of type operators depends only on variable images

Used byInstantiating a weakened type operator leaves it unchanged

TheoremSubstitution after renaming of type operators#✓fully proved

Substitution after renaming is precomposition on the variable images.

theorem subst_rename (ρ : KRen Δ Ε) (σ : Sub Ε Ζ) (t : Ty Δ κ) :
    subst σ (rename ρ t) = subst (fun {_} x => σ (ρ x)) t

Uses 10 · Used by 4

Statement usesKind-preserving renamings of type variables · Kinded type variables of Fω · Kinds of pure Fω · Intrinsically kinded Fω type operators · Kind-preserving simultaneous type substitutions · Renaming of Fω type operators · Simultaneous substitution of Fω type operators

Proof usesLifting a renaming under a type binder · Lifting a type substitution under a type binder · Substitution of type operators depends only on variable images

Used byInstantiating a weakened type operator leaves it unchanged · Renaming commutes with type-binder instantiation · Lifted substitution commutes with weakening · Composition of simultaneous type-operator substitutions

TheoremRenaming after substitution of type operators#✓fully proved

Renaming after substitution renames each substituted type operator.

theorem rename_subst (σ : Sub Δ Ε) (ρ : KRen Ε Ζ) (t : Ty Δ κ) :
    rename ρ (subst σ t) =
      subst (fun {_} x => rename ρ (σ x)) t

Uses 12 · Used by 3

Statement usesKind-preserving renamings of type variables · Kinded type variables of Fω · Kinds of pure Fω · Intrinsically kinded Fω type operators · Kind-preserving simultaneous type substitutions · Renaming of Fω type operators · Simultaneous substitution of Fω type operators

Proof usesLifting a renaming under a type binder · Lifting a type substitution under a type binder · Renaming of type operators depends only on variable images · Composition of kind-preserving renamings · Substitution of type operators depends only on variable images

Used byRenaming commutes with type-binder instantiation · Lifted substitution commutes with weakening · Composition of simultaneous type-operator substitutions

TheoremComposition of simultaneous type-operator substitutions#✓fully proved

Capture-avoiding simultaneous substitutions compose.

theorem subst_subst (σ : Sub Δ Ε) (τ : Sub Ε Ζ) (t : Ty Δ κ) :
    subst τ (subst σ t) =
      subst (fun {_} x => subst τ (σ x)) t

Uses 10 · Used by 1

Statement usesKinded type variables of Fω · Kinds of pure Fω · Intrinsically kinded Fω type operators · Kind-preserving simultaneous type substitutions · Simultaneous substitution of Fω type operators

Proof usesLifting a type substitution under a type binder · Renaming of Fω type operators · Renaming after substitution of type operators · Substitution of type operators depends only on variable images · Substitution after renaming of type operators

Used bySubstitution commutes with type-binder instantiation

TheoremInstantiating a weakened type operator leaves it unchanged#✓fully proved

Discharging a fresh binder leaves a weakened operator unchanged.

@[simp] theorem instantiate_rename_succ (t : Ty Δ κ) (a : Ty Δ μ) :
    instantiate (rename KVar.succ t) a = t

Uses 9 · Used by 4

Statement usesKinded type variables of Fω · Kinds of pure Fω · Intrinsically kinded Fω type operators · Instantiation of an Fω type binder · Renaming of Fω type operators

Proof usesSubstitution for the newest type variable · Simultaneous substitution of Fω type operators · Identity substitution fixes type operators · Substitution after renaming of type operators

Used bySubstitution commutes with type-binder instantiation · Type-binder instantiation preserves Fω typing · Type translation commutes with type-binder instantiation · Term translation commutes with type-binder instantiation

TheoremSubstitution commutes with type-binder instantiation#✓fully proved

Simultaneous substitution commutes with discharging a type binder.

theorem subst_instantiate (σ : Sub Δ Ε)
    (b : Ty (μ :: Δ) κ) (a : Ty Δ μ) :
    subst σ (instantiate b a) =
      instantiate (subst (liftSub σ) b) (subst σ a)

Uses 12 · Used by 3

Statement usesKinds of pure Fω · Intrinsically kinded Fω type operators · Kind-preserving simultaneous type substitutions · Instantiation of an Fω type binder · Lifting a type substitution under a type binder · Simultaneous substitution of Fω type operators

Proof usesKinded type variables of Fω · Instantiating a weakened type operator leaves it unchanged · Renaming of Fω type operators · Substitution for the newest type variable · Substitution of type operators depends only on variable images · Composition of simultaneous type-operator substitutions

Used byType-beta conversion is stable under substitution · Type substitution preserves Fω typing · Parallel type-beta reduction is stable under substitution

TheoremRenaming commutes with type-binder instantiation#✓fully proved

Renaming commutes with discharging a type binder.

theorem rename_instantiate (ρ : KRen Δ Ε)
    (b : Ty (μ :: Δ) κ) (a : Ty Δ μ) :
    rename ρ (instantiate b a) =
      instantiate (rename (KRen.lift ρ) b) (rename ρ a)

Uses 12 · Used by 2

Statement usesKind-preserving renamings of type variables · Lifting a renaming under a type binder · Kinds of pure Fω · Intrinsically kinded Fω type operators · Instantiation of an Fω type binder · Renaming of Fω type operators

Proof usesKinded type variables of Fω · Renaming after substitution of type operators · Substitution for the newest type variable · Simultaneous substitution of Fω type operators · Substitution of type operators depends only on variable images · Substitution after renaming of type operators

Used byType-beta conversion is stable under renaming · Parallel type-beta reduction is stable under renaming

TheoremRenaming as substitution by variables#✓fully proved

Renaming is substitution by the corresponding variable constructors.

theorem subst_var_rename (ρ : KRen Δ Ε) (t : Ty Δ κ) :
    subst (fun {_} x => .var (ρ x)) t = rename ρ t

Uses 9 · Used by 2

Statement usesKind-preserving renamings of type variables · Kinded type variables of Fω · Kinds of pure Fω · Intrinsically kinded Fω type operators · Renaming of Fω type operators · Simultaneous substitution of Fω type operators

Proof usesLifting a renaming under a type binder · Lifting a type substitution under a type binder · Substitution of type operators depends only on variable images

Used byType renaming preserves Fω typing · Term translation commutes with weakening under a type binder

TheoremLifted substitution commutes with weakening#✓fully proved

Lifted type substitution commutes with weakening past the new binder.

theorem subst_lift_rename (σ : Sub Δ Ε) (t : Ty Δ κ) :
    subst (liftSub (μ := μ) σ) (rename KVar.succ t) =
      rename KVar.succ (subst σ t)

Uses 9 · Used by 3

Statement usesKinded type variables of Fω · Kinds of pure Fω · Intrinsically kinded Fω type operators · Kind-preserving simultaneous type substitutions · Lifting a type substitution under a type binder · Renaming of Fω type operators · Simultaneous substitution of Fω type operators

Proof usesRenaming after substitution of type operators · Substitution after renaming of type operators

Used byType substitution preserves Fω typing · Type translation commutes with target substitution · Term translation commutes with target type substitution

13 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.