Type-beta confluence and conversion inversion

InductiveParallel type-beta reduction in Fω#✓fully proved

Parallel type-beta reduction, retaining the context and kind indices.

inductive Par : {Δ : List Kind} → {κ : Kind} → Ty Δ κ → Ty Δ κ → Prop where
  | var {Δ : List Kind} {κ : Kind} (x : KVar Δ κ) : Par (.var x) (.var x)
  | lam {Δ : List Kind} {κ μ : Kind} {b c : Ty (κ :: Δ) μ} :
      Par b c → Par (.lam b) (.lam c)
  | app {Δ : List Kind} {κ μ : Kind}
      {f g : Ty Δ (.arrow κ μ)} {a b : Ty Δ κ} :
      Par f g → Par a b → Par (.app f a) (.app g b)
  | arr {Δ : List Kind} {a a' b b' : Ty Δ .star} :
      Par a a' → Par b b' → Par (.arr a b) (.arr a' b')
  | all {Δ : List Kind} {κ : Kind} {b c : Ty (κ :: Δ) .star} :
      Par b c → Par (.all b) (.all c)
  | beta {Δ : List Kind} {κ μ : Kind}
      {b c : Ty (κ :: Δ) μ} {a a' : Ty Δ κ} :
      Par b c → Par a a' → Par (.app (.lam b) a) (instantiate c a')

Uses 4 · Used by 17

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

Used byMultistep type-beta reduction under a universal quantifier · Reducts of quantified types are quantified types · Multistep type-beta reduction in type applications · Multistep type-beta reduction in function types · Reducts of function types are function types · Parallel type-beta reduction implies conversion · Multistep type-beta reduction implies conversion · Parallel type-beta reduction is stable under instantiation · Church–Rosser property of type-beta conversion · Multistep type-beta reduction under an operator abstraction · Confluence of parallel type-beta reduction · Diamond property of parallel type-beta reduction · Multistep parallel type-beta reduction · Reflexivity of parallel type-beta reduction · Parallel type-beta reduction is stable under renaming · Parallel type-beta reduction is stable under substitution · Parallel reducts reduce to the complete development

TheoremReflexivity of parallel type-beta reduction#✓fully proved

Parallel reduction is reflexive on every kinded operator.

theorem Par.refl (a : Ty Δ κ) : Par a a

Uses 4 · Used by 3

Statement usesKinds of pure Fω · Intrinsically kinded Fω type operators · Parallel type-beta reduction in Fω

Proof usesKinded type variables of Fω

Used byMultistep type-beta reduction in type applications · Multistep type-beta reduction in function types · Church–Rosser property of type-beta conversion

TheoremParallel type-beta reduction is stable under renaming#✓fully proved

Parallel beta reduction is stable under kinded renaming.

theorem Par.rename (h : Par a b) (ρ : KRen Δ Ε) :
    Par (Ty.rename ρ a) (Ty.rename ρ b)

Uses 9 · Used by 1

Statement usesKind-preserving renamings of type variables · Kinds of pure Fω · Intrinsically kinded Fω type operators · Parallel type-beta reduction in Fω · Renaming of Fω type operators

Proof usesLifting a renaming under a type binder · Kinded type variables of Fω · Instantiation of an Fω type binder · Renaming commutes with type-binder instantiation

Used byParallel type-beta reduction is stable under substitution

TheoremParallel type-beta reduction is stable under substitution#✓fully proved

Parallel reduction respects simultaneous substitution on both sides.

theorem Par.subst (h : Par a b) {σ τ : Sub Δ Ε}
    (hσ : ∀ {ν} (x : KVar Δ ν), Par (σ x) (τ x)) :
    Par (Ty.subst σ a) (Ty.subst τ b)

Uses 10 · Used by 1

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

Proof usesParallel type-beta reduction is stable under renaming · Instantiation of an Fω type binder · Lifting a type substitution under a type binder · Substitution commutes with type-binder instantiation

Used byParallel type-beta reduction is stable under instantiation

TheoremParallel type-beta reduction is stable under instantiation#✓fully proved

Parallel reduction respects discharging a binder and reducing its image.

theorem Par.instantiate {b c : Ty (μ :: Δ) κ} {a a' : Ty Δ μ}
    (hb : Par b c) (ha : Par a a') :
    Par (Ty.instantiate b a) (Ty.instantiate c a')

Uses 7 · Used by 1

Statement usesKinds of pure Fω · Intrinsically kinded Fω type operators · Parallel type-beta reduction in Fω · Instantiation of an Fω type binder

Proof usesKinded type variables of Fω · Parallel type-beta reduction is stable under substitution · Substitution for the newest type variable

Used byParallel reducts reduce to the complete development

DefinitionComplete development of type-beta redexes#✓fully proved

Contract all originally present type-beta redexes recursively.

def develop : {Δ : List Kind} → {κ : Kind} → Ty Δ κ → Ty Δ κ
  | _, _, .var x => .var x
  | _, _, .lam b => .lam (develop b)
  | _, _, .app (.lam b) a => instantiate (develop b) (develop a)
  | _, _, .app f a => .app (develop f) (develop a)
  | _, _, .arr a b => .arr (develop a) (develop b)
  | _, _, .all b => .all (develop b)

Uses 4 · Used by 2

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

Used byDiamond property of parallel type-beta reduction · Parallel reducts reduce to the complete development

TheoremParallel reducts reduce to the complete development#✓fully proved

Every parallel reduct reduces to the original complete development.

theorem Par.to_develop (h : Par a b) : Par b (develop a)

Uses 7 · Used by 1

Statement usesKinds of pure Fω · Intrinsically kinded Fω type operators · Parallel type-beta reduction in Fω · Complete development of type-beta redexes

Proof usesKinded type variables of Fω · Parallel type-beta reduction is stable under instantiation · Instantiation of an Fω type binder

Used byDiamond property of parallel type-beta reduction

TheoremDiamond property of parallel type-beta reduction#✓fully proved

Parallel beta reduction has the diamond property at each kind.

theorem par_diamond : Relation.Diamond (Par (Δ := Δ) (κ := κ))

Uses 5 · Used by 1

Statement usesKinds of pure Fω · Intrinsically kinded Fω type operators · Parallel type-beta reduction in Fω

Proof usesParallel reducts reduce to the complete development · Complete development of type-beta redexes

Used byConfluence of parallel type-beta reduction

TheoremConfluence of parallel type-beta reduction#✓fully proved

Parallel type-beta reduction is confluent; no termination premise.

theorem par_confluent : Relation.Confluent (Par (Δ := Δ) (κ := κ))

Uses 4 · Used by 1

Statement usesKinds of pure Fω · Intrinsically kinded Fω type operators · Parallel type-beta reduction in Fω

Proof usesDiamond property of parallel type-beta reduction

Used byChurch–Rosser property of type-beta conversion

AbbreviationMultistep parallel type-beta reduction#✓fully proved

Finitely many parallel beta reductions, including zero reductions.

abbrev Red (a b : Ty Δ κ) := Relation.ReflTransGen Par a b

Uses 3 · Used by 12

Statement usesKinds of pure Fω · Intrinsically kinded Fω type operators · Parallel type-beta reduction in Fω

Used byMultistep type-beta reduction under a universal quantifier · Injectivity of quantified types up to conversion · Reducts of quantified types are quantified types · Conversion preserves the kind of a universal binder · Multistep type-beta reduction in type applications · Multistep type-beta reduction in function types · Injectivity of function types up to conversion · Reducts of function types are function types · Multistep type-beta reduction implies conversion · Type-beta conversion is joinability by a common reduct · Church–Rosser property of type-beta conversion · Multistep type-beta reduction under an operator abstraction

TheoremMultistep type-beta reduction under an operator abstraction#✓fully proved

Multiple parallel reductions are stable under an operator binder.

theorem Red.lam {b c : Ty (μ :: Δ) κ} (h : Red b c) :
    Red (.lam b) (.lam c)

Uses 4 · Used by 1

Statement usesKinds of pure Fω · Intrinsically kinded Fω type operators · Multistep parallel type-beta reduction

Proof usesParallel type-beta reduction in Fω

Used byChurch–Rosser property of type-beta conversion

TheoremMultistep type-beta reduction under a universal quantifier#✓fully proved

Multiple parallel reductions are stable under a universal binder.

theorem Red.all {b c : Ty (μ :: Δ) .star} (h : Red b c) :
    Red (.all b) (.all c)

Uses 4 · Used by 1

Statement usesKinds of pure Fω · Intrinsically kinded Fω type operators · Multistep parallel type-beta reduction

Proof usesParallel type-beta reduction in Fω

Used byChurch–Rosser property of type-beta conversion

TheoremMultistep type-beta reduction in type applications#✓fully proved

Multiple reductions are congruent in both type-application arguments.

theorem Red.app {f g : Ty Δ (.arrow μ κ)} {a b : Ty Δ μ}
    (hf : Red f g) (ha : Red a b) : Red (.app f a) (.app g b)

Uses 5 · Used by 1

Statement usesKinds of pure Fω · Intrinsically kinded Fω type operators · Multistep parallel type-beta reduction

Proof usesParallel type-beta reduction in Fω · Reflexivity of parallel type-beta reduction

Used byChurch–Rosser property of type-beta conversion

TheoremMultistep type-beta reduction in function types#✓fully proved

Multiple reductions are congruent in both term-function type arguments.

theorem Red.arr {a a' b b' : Ty Δ .star}
    (ha : Red a a') (hb : Red b b') : Red (.arr a b) (.arr a' b')

Uses 5 · Used by 1

Statement usesKinds of pure Fω · Intrinsically kinded Fω type operators · Multistep parallel type-beta reduction

Proof usesParallel type-beta reduction in Fω · Reflexivity of parallel type-beta reduction

Used byChurch–Rosser property of type-beta conversion

TheoremChurch–Rosser property of type-beta conversion#✓fully proved

Conversion entails a common parallel-beta reduct (Church-Rosser).

theorem Conv.join (h : Conv a b) : ∃ c, Red a c ∧ Red b c

Uses 12 · Used by 4

Statement usesKinds of pure Fω · Intrinsically kinded Fω type operators · Type-beta conversion in Fω · Multistep parallel type-beta reduction

Proof usesParallel type-beta reduction in Fω · Reflexivity of parallel type-beta reduction · Multistep type-beta reduction under a universal quantifier · Multistep type-beta reduction in type applications · Multistep type-beta reduction in function types · Multistep type-beta reduction under an operator abstraction · Instantiation of an Fω type binder · Confluence of parallel type-beta reduction

Used byInjectivity of quantified types up to conversion · Conversion preserves the kind of a universal binder · Injectivity of function types up to conversion · Type-beta conversion is joinability by a common reduct

TheoremParallel type-beta reduction implies conversion#✓fully proved

Every parallel-beta reduction is a proved conversion.

theorem Par.conv (h : Par a b) : Conv a b

Uses 6 · Used by 1

Statement usesKinds of pure Fω · Intrinsically kinded Fω type operators · Type-beta conversion in Fω · Parallel type-beta reduction in Fω

Proof usesKinded type variables of Fω · Instantiation of an Fω type binder

Used byMultistep type-beta reduction implies conversion

TheoremMultistep type-beta reduction implies conversion#✓fully proved

Finitely many parallel-beta reductions are a proved conversion.

theorem Red.conv (h : Red a b) : Conv a b

Uses 6 · Used by 3

Statement usesKinds of pure Fω · Intrinsically kinded Fω type operators · Type-beta conversion in Fω · Multistep parallel type-beta reduction

Proof usesParallel type-beta reduction in Fω · Parallel type-beta reduction implies conversion

Used byInjectivity of quantified types up to conversion · Injectivity of function types up to conversion · Type-beta conversion is joinability by a common reduct

TheoremType-beta conversion is joinability by a common reduct#✓fully proved

Conversion is exactly common-reduct joinability, not semantic equality.

theorem conv_iff_join : Conv a b ↔ ∃ c, Red a c ∧ Red b c

Uses 6

Statement usesKinds of pure Fω · Intrinsically kinded Fω type operators · Type-beta conversion in Fω · Multistep parallel type-beta reduction

Proof usesChurch–Rosser property of type-beta conversion · Multistep type-beta reduction implies conversion

TheoremReducts of function types are function types#✓fully proved

Reduction of a term-function type keeps its outer constructor.

theorem Red.arr_inv {a b c : Ty Δ .star} (h : Red (.arr a b) c) :
    ∃ a' b', c = .arr a' b' ∧ Red a a' ∧ Red b b'

Uses 6 · Used by 1

Statement usesKinds of pure Fω · Intrinsically kinded Fω type operators · Multistep parallel type-beta reduction

Proof usesKinded type variables of Fω · Parallel type-beta reduction in Fω · Instantiation of an Fω type binder

Used byInjectivity of function types up to conversion

TheoremReducts of quantified types are quantified types#✓fully proved

Reduction of a quantified type keeps its binder kind and outer shape.

theorem Red.all_inv {body : Ty (μ :: Δ) .star} {c : Ty Δ .star}
    (h : Red (.all body) c) :
    ∃ body' : Ty (μ :: Δ) .star, c = .all body' ∧ Red body body'

Uses 6 · Used by 2

Statement usesKinds of pure Fω · Intrinsically kinded Fω type operators · Multistep parallel type-beta reduction

Proof usesKinded type variables of Fω · Parallel type-beta reduction in Fω · Instantiation of an Fω type binder

Used byInjectivity of quantified types up to conversion · Conversion preserves the kind of a universal binder

TheoremInjectivity of function types up to conversion#✓fully proved

Convertible term-function types have convertible domains and codomains.

theorem Conv.arr_inj {a a' b b' : Ty Δ .star}
    (h : Conv (.arr a b) (.arr a' b')) : Conv a a' ∧ Conv b b'

Uses 8 · Used by 1

Statement usesKinds of pure Fω · Intrinsically kinded Fω type operators · Type-beta conversion in Fω

Proof usesKinded type variables of Fω · Church–Rosser property of type-beta conversion · Multistep parallel type-beta reduction · Reducts of function types are function types · Multistep type-beta reduction implies conversion

Used byType preservation for Fω weak call-by-value reduction

TheoremConversion preserves the kind of a universal binder#✓fully proved

Conversion cannot change the kind of a universal binder.

theorem Conv.all_kind {ν : Kind} {body : Ty (μ :: Δ) .star}
    {body' : Ty (ν :: Δ) .star} (h : Conv (.all body) (.all body')) :
    μ = ν

Uses 7 · Used by 1

Statement usesKinds of pure Fω · Intrinsically kinded Fω type operators · Type-beta conversion in Fω

Proof usesKinded type variables of Fω · Church–Rosser property of type-beta conversion · Multistep parallel type-beta reduction · Reducts of quantified types are quantified types

Used byCanonical forms for Fω values of quantified type

TheoremInjectivity of quantified types up to conversion#✓fully proved

Convertible quantified types at the same kind have convertible bodies.

theorem Conv.all_inj {body body' : Ty (μ :: Δ) .star}
    (h : Conv (.all body) (.all body')) : Conv body body'

Uses 8 · Used by 1

Statement usesKinds of pure Fω · Intrinsically kinded Fω type operators · Type-beta conversion in Fω

Proof usesKinded type variables of Fω · Church–Rosser property of type-beta conversion · Multistep parallel type-beta reduction · Reducts of quantified types are quantified types · Multistep type-beta reduction implies conversion

Used byType preservation for Fω weak call-by-value reduction

23 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.