TypeSystemNormalization
DefinitionThis block formalizes pure type systems with fully annotated syntax over an arbitrary sort type S. Expressions are de Bruijn variables, sorts, applications, lambda abstractions with a domain annotation, and dependent products (pi) with a domain; renaming, simultaneous substitution (with lifting under binders) and single-variable instantiation are defined structurally. A Specification consists of an axiom relation between pairs of sorts and a ternary rule relation on sorts, with no functionality assumed for either. Beta is the one-step reduction generated by contracting (lam A b) a to b instantiated at a, closed under reduction in either side of an application and in the domain or body of lam and pi; Converts is the equivalence relation generated by Beta. An expression is Normal if it has no Beta step, WeaklyNormalizing if it reduces (reflexive-transitively) to a normal form, and StronglyNormalizing if it is accessible for the converse of Beta, so no infinite reduction exists, including reductions inside type annotations. Typing judgments HasType P Γ M A, with contexts as lists of types stored newest first, are inductively generated by: the axiom rule typing sort s by sort t in the empty context whenever the axioms relate s and t; variable 0 typed by the renamed type when the context is extended by a type of some sort; weakening; the product rule giving pi A B the sort s3 when A has sort s1, B has sort s2 in the extended context and the rule relates s1, s2, s3; abstraction, requiring the product type to be well-sorted; application, with result type the instantiation of the codomain at the argument; and conversion along Converts to a well-sorted type. ValidContext is generated from the empty context by adding a type that has some sort. An expression M is Legal in a context if for some A either M has type A or A has type M. SystemWeaklyNormalizing and SystemStronglyNormalizing are defined propositions saying that, for every valid context, every legal expression is weakly, respectively strongly, normalizing; no theorem about them is established in this block.
-- Generated from openai/math @ adc7f1241b42e322a6451854ab7e4b4c146bf78a
-- Source: lean/ComparatorChallenges/TypeSystemNormalization.lean; bytes 16..4166
-- Kind: block; original declaration names and bodies preserved.
-- Source groups are independent. Target: Lean 4.33.1; see compilation.json.
import Mathlib
namespace OAI
/-!
Full annotated PTS syntax, modulo alpha-renaming via de Bruijn indices.
Contexts are stored newest-first, each declaration in its prefix context.
No functionality assumptions on axioms or product rules.
-/
namespace PureTypeSystem
universe u
inductive Expr (Sorts : Type u) : Type u
| var : Nat → Expr Sorts
| sort : Sorts → Expr Sorts
| app : Expr Sorts → Expr Sorts → Expr Sorts
| lam : Expr Sorts → Expr Sorts → Expr Sorts
| pi : Expr Sorts → Expr Sorts → Expr Sorts
deriving DecidableEq
namespace Expr
variable {S : Type u}
def liftRen (ρ : Nat → Nat) : Nat → Nat
| 0 => 0
| n + 1 => ρ n + 1
def rename (ρ : Nat → Nat) : Expr S → Expr S
| var n => var (ρ n)
| sort s => sort s
| app f a => app (rename ρ f) (rename ρ a)
| lam A b => lam (rename ρ A) (rename (liftRen ρ) b)
| pi A B => pi (rename ρ A) (rename (liftRen ρ) B)
def liftSub (σ : Nat → Expr S) : Nat → Expr S
| 0 => var 0
| n + 1 => rename Nat.succ (σ n)
def subst (σ : Nat → Expr S) : Expr S → Expr S
| var n => σ n
| sort s => sort s
| app f a => app (subst σ f) (subst σ a)
| lam A b => lam (subst σ A) (subst (liftSub σ) b)
| pi A B => pi (subst σ A) (subst (liftSub σ) B)
def single (a : Expr S) : Nat → Expr S
| 0 => a
| n + 1 => var n
def instantiate (b a : Expr S) : Expr S := subst (single a) b
end Expr
structure Specification (S : Type u) where
axioms : S → S → Prop
rule : S → S → S → Prop
inductive Beta {S : Type u} : Expr S → Expr S → Prop
| head (A b a) : Beta (.app (.lam A b) a) (b.instantiate a)
| app_left {f f' a} : Beta f f' → Beta (.app f a) (.app f' a)
| app_right {f a a'} : Beta a a' → Beta (.app f a) (.app f a')
| lam_domain {A A' b} : Beta A A' → Beta (.lam A b) (.lam A' b)
| lam_body {A b b'} : Beta b b' → Beta (.lam A b) (.lam A b')
| pi_domain {A A' B} : Beta A A' → Beta (.pi A B) (.pi A' B)
| pi_body {A B B'} : Beta B B' → Beta (.pi A B) (.pi A B')
def Converts {S : Type u} : Expr S → Expr S → Prop := Relation.EqvGen Beta
def Normal {S : Type u} (M : Expr S) : Prop := ∀ N, ¬ Beta M N
def WeaklyNormalizing {S : Type u} (M : Expr S) : Prop :=
∃ N, Relation.ReflTransGen Beta M N ∧ Normal N
/-- Accessibility for the converse of reduction: strong normalization,
including reductions in all type annotations. -/
def StronglyNormalizing {S : Type u} (M : Expr S) : Prop :=
Acc (fun N M : Expr S => Beta M N) M
inductive HasType {S : Type u} (P : Specification S) :
List (Expr S) → Expr S → Expr S → Prop
| ax {s t} : P.axioms s t → HasType P [] (.sort s) (.sort t)
| var {Γ A s} : HasType P Γ A (.sort s) →
HasType P (A :: Γ) (.var 0) (A.rename Nat.succ)
| weaken {Γ M B A s} : HasType P Γ M B → HasType P Γ A (.sort s) →
HasType P (A :: Γ) (M.rename Nat.succ) (B.rename Nat.succ)
| product {Γ A B s₁ s₂ s₃} : HasType P Γ A (.sort s₁) →
HasType P (A :: Γ) B (.sort s₂) → P.rule s₁ s₂ s₃ →
HasType P Γ (.pi A B) (.sort s₃)
| abstraction {Γ A b B s} : HasType P (A :: Γ) b B →
HasType P Γ (.pi A B) (.sort s) →
HasType P Γ (.lam A b) (.pi A B)
| application {Γ f a A B} : HasType P Γ f (.pi A B) →
HasType P Γ a A → HasType P Γ (.app f a) (B.instantiate a)
| conversion {Γ M A B s} : HasType P Γ M A → HasType P Γ B (.sort s) →
Converts A B → HasType P Γ M B
inductive ValidContext {S : Type u} (P : Specification S) : List (Expr S) → Prop
| nil : ValidContext P []
| cons {Γ A s} : ValidContext P Γ → HasType P Γ A (.sort s) →
ValidContext P (A :: Γ)
def Legal {S : Type u} (P : Specification S) (Γ : List (Expr S)) (M : Expr S) : Prop :=
∃ A, HasType P Γ M A ∨ HasType P Γ A M
def SystemWeaklyNormalizing {S : Type u} (P : Specification S) : Prop :=
∀ Γ, ValidContext P Γ → ∀ M, Legal P Γ M → WeaklyNormalizing M
def SystemStronglyNormalizing {S : Type u} (P : Specification S) : Prop :=
∀ Γ, ValidContext P Γ → ∀ M, Legal P Γ M → StronglyNormalizing M
end PureTypeSystem
end OAI
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.