Conversion-aware weak call-by-value safety for pure Fω

InductiveWeak call-by-value values of Fω#✓fully proved

Weak-CBV values: neither form of lambda evaluates beneath its binder.

inductive Value : {Δ : List Kind} → {m : Nat} → Tm Δ m → Prop where
  | lam {Δ : List Kind} {m : Nat} (A : Ty Δ .star) (b : Tm Δ (m + 1)) :
      Value (.lam A b)
  | tabs {Δ : List Kind} {m : Nat} {κ : Kind} (b : Tm (κ :: Δ) m) :
      Value (.tabs b)

Uses 3 · Used by 9

Statement usesKinds of pure Fω · Scoped pure Fω terms · Intrinsically kinded Fω type operators

Used byCanonical forms for Fω values of quantified type · Canonical forms for Fω values of function type · Type preservation for Fω weak call-by-value reduction · Progress for closed Fω terms · Type safety of Fω weak call-by-value reduction · Weak call-by-value reduction of Fω · Erasure of an Fω evaluation step is a beta conversion · Term translation simulates each weak call-by-value step · Term translation preserves weak call-by-value values

InductiveWeak call-by-value reduction of Fω#✓fully proved

Ordinary left-to-right weak call-by-value reduction.

inductive Step : {Δ : List Kind} → {m : Nat} → Tm Δ m → Tm Δ m → Prop where
  | beta {Δ : List Kind} {m : Nat} {A : Ty Δ .star}
      {b : Tm Δ (m + 1)} {a : Tm Δ m} :
      Value a → Step (.app (.lam A b) a) (b.instantiate a)
  | tybeta {Δ : List Kind} {m : Nat} {κ : Kind}
      (b : Tm (κ :: Δ) m) (a : Ty Δ κ) :
      Step (.tapp (.tabs b) a) (b.tySubst (Ty.single a))
  | appFun {Δ : List Kind} {m : Nat} {f f' a : Tm Δ m} :
      Step f f' → Step (.app f a) (.app f' a)
  | appArg {Δ : List Kind} {m : Nat} {f a a' : Tm Δ m} :
      Value f → Step a a' → Step (.app f a) (.app f a')
  | tapp {Δ : List Kind} {m : Nat} {κ : Kind}
      {f f' : Tm Δ m} {a : Ty Δ κ} :
      Step f f' → Step (.tapp f a) (.tapp f' a)

Uses 7 · Used by 9

Statement usesKinds of pure Fω · Scoped pure Fω terms · Instantiation of an Fω term binder · Type substitution in Fω terms · Intrinsically kinded Fω type operators · Substitution for the newest type variable · Weak call-by-value values of Fω

Used byType preservation for Fω weak call-by-value reduction · Type preservation along multistep Fω reduction · Progress for closed Fω terms · Type safety of Fω weak call-by-value reduction · Erasure of an Fω evaluation step is a beta conversion · Erasure of multistep Fω evaluation is a beta conversion · Canonical embedding preserves single evaluation steps · Canonical embedding preserves multistep evaluation · Term translation simulates each weak call-by-value step

TheoremInversion of Fω lambda typing up to conversion#✓fully proved

Lambda typing inversion retains the annotation and a proved conversion.

theorem Typing.lam_inv {A T : Ty Δ .star} {b : Tm Δ (m + 1)}
    (h : Typing Γ (.lam A b) T) :
    ∃ B, Typing (Fin.cases A Γ) b B ∧ Ty.Conv (.arr A B) T

Uses 9 · Used by 2

Statement usesTerm contexts of pure Fω · Kinds of pure Fω · Scoped pure Fω terms · Intrinsically kinded Fω type operators · Type-beta conversion in Fω · Typing rules of pure Fω

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

Used byCanonical forms for Fω values of quantified type · Type preservation for Fω weak call-by-value reduction

TheoremInversion of Fω type-lambda typing up to conversion#✓fully proved

Type-lambda inversion retains its binder kind and body conversion.

theorem Typing.tabs_inv {κ : Kind} {T : Ty Δ .star}
    {b : Tm (κ :: Δ) m} (h : Typing Γ (.tabs b) T) :
    ∃ B : Ty (κ :: Δ) .star,
      Typing (fun i => (Γ i).rename KVar.succ) b B ∧
        Ty.Conv (.all B) T

Uses 9 · Used by 3

Statement usesTerm contexts of pure Fω · Kinded type variables of Fω · Kinds of pure Fω · Scoped pure Fω terms · Intrinsically kinded Fω type operators · Type-beta conversion in Fω · Renaming of Fω type operators · Typing rules of pure Fω

Proof usesInstantiation of an Fω type binder

Used byCanonical forms for Fω values of quantified type · Canonical forms for Fω values of function type · Type preservation for Fω weak call-by-value reduction

TheoremType preservation for Fω weak call-by-value reduction#✓fully proved

Weak-CBV reduction preserves typing in unrestricted open contexts.

theorem Typing.preservation {A : Ty Δ .star} {t t' : Tm Δ m}
    (h : Typing Γ t A) (hs : Step t t') : Typing Γ t' A

Uses 21 · Used by 1

Statement usesTerm contexts of pure Fω · Kinds of pure Fω · Weak call-by-value reduction of Fω · Scoped pure Fω terms · Intrinsically kinded Fω type operators · Typing rules of pure Fω

Proof usesKinded type variables of Fω · Instantiation of an Fω term binder · Type substitution in Fω terms · Type-beta conversion in Fω · Injectivity of quantified types up to conversion · Injectivity of function types up to conversion · Type-beta conversion is stable under substitution · Instantiation of an Fω type binder · Renaming of Fω type operators · Substitution for the newest type variable · Term-binder instantiation preserves Fω typing · Inversion of Fω lambda typing up to conversion · Inversion of Fω type-lambda typing up to conversion · Type-binder instantiation preserves Fω typing · Weak call-by-value values of Fω

Used byType preservation along multistep Fω reduction

TheoremCanonical forms for Fω values of function type#✓fully proved

A value typed at an arrow, despite conversion, is a term lambda.

theorem Value.arrow {A B : Ty Δ .star} {t : Tm Δ m}
    (hv : Value t) (h : Typing Γ t (.arr A B)) :
    ∃ C b, t = .lam C b

Uses 11 · Used by 1

Statement usesTerm contexts of pure Fω · Kinds of pure Fω · Scoped pure Fω terms · Intrinsically kinded Fω type operators · Typing rules of pure Fω · Weak call-by-value values of Fω

Proof usesKinded type variables of Fω · Type-beta conversion in Fω · Function types are not convertible to quantified types · Renaming of Fω type operators · Inversion of Fω type-lambda typing up to conversion

Used byProgress for closed Fω terms

TheoremCanonical forms for Fω values of quantified type#✓fully proved

A value at a quantified type is a type lambda of the same binder kind.

theorem Value.all {κ : Kind} {C : Ty (κ :: Δ) .star} {t : Tm Δ m}
    (hv : Value t) (h : Typing Γ t (.all C)) :
    ∃ b : Tm (κ :: Δ) m, t = .tabs b

Uses 13 · Used by 1

Statement usesTerm contexts of pure Fω · Kinds of pure Fω · Scoped pure Fω terms · Intrinsically kinded Fω type operators · Typing rules of pure Fω · Weak call-by-value values of Fω

Proof usesKinded type variables of Fω · Type-beta conversion in Fω · Conversion preserves the kind of a universal binder · Function types are not convertible to quantified types · Renaming of Fω type operators · Inversion of Fω lambda typing up to conversion · Inversion of Fω type-lambda typing up to conversion

Used byProgress for closed Fω terms

TheoremProgress for closed Fω terms#✓fully proved

Closed-term progress, allowing an arbitrary open kinded-type telescope.

theorem Typing.progress {Γ : Ctx Δ 0} {A : Ty Δ .star} {t : Tm Δ 0}
    (h : Typing Γ t A) : Value t ∨ ∃ t', Step t t'

Uses 16 · Used by 1

Statement usesTerm contexts of pure Fω · Kinds of pure Fω · Weak call-by-value reduction of Fω · Scoped pure Fω terms · Intrinsically kinded Fω type operators · Typing rules of pure Fω · Weak call-by-value values of Fω

Proof usesKinded type variables of Fω · Instantiation of an Fω term binder · Type substitution in Fω terms · Type-beta conversion in Fω · Instantiation of an Fω type binder · Renaming of Fω type operators · Substitution for the newest type variable · Canonical forms for Fω values of quantified type · Canonical forms for Fω values of function type

Used byType safety of Fω weak call-by-value reduction

TheoremType preservation along multistep Fω reduction#✓fully proved

Every finite weak-CBV reduction sequence preserves typing.

theorem Typing.preservation_steps {A : Ty Δ .star} {t t' : Tm Δ m}
    (h : Typing Γ t A) (hs : Relation.ReflTransGen Step t t') :
    Typing Γ t' A

Uses 7 · Used by 1

Statement usesTerm contexts of pure Fω · Kinds of pure Fω · Weak call-by-value reduction of Fω · Scoped pure Fω terms · Intrinsically kinded Fω type operators · Typing rules of pure Fω

Proof usesType preservation for Fω weak call-by-value reduction

Used byType safety of Fω weak call-by-value reduction

TheoremType safety of Fω weak call-by-value reduction#✓fully proved

No reachable closed well-typed term is stuck, with type variables allowed.

theorem Typing.safety {Γ : Ctx Δ 0} {A : Ty Δ .star} {t t' : Tm Δ 0}
    (h : Typing Γ t A) (hs : Relation.ReflTransGen Step t t') :
    Value t' ∨ ∃ u, Step t' u

Uses 9

Statement usesTerm contexts of pure Fω · Kinds of pure Fω · Weak call-by-value reduction of Fω · Scoped pure Fω terms · Intrinsically kinded Fω type operators · Typing rules of pure Fω · Weak call-by-value values of Fω

Proof usesType preservation along multistep Fω reduction · Progress for closed Fω terms

10 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.