Normalization for module expressions

Weak normalization: every well-typed module expression terminates. Split off from ModuleExpressionBasics.lean (which develops syntax, typing, reduction and normal forms without it) so that this — the other deep open fact besides confluence — stands on its own; ModuleExpression.lean collects the consequences.

The proof is Tait's reducibility (logical relations) in its Kripke form: Red T Γ m says that m is a well-typed weakly normalizing term of type T in context Γ, hereditarily so under every elimination the type allows. The function case quantifies over all renamings Γ → Γ', which is what makes the relation stable under weakening (Red.rename) — needed because the abs case of the fundamental lemma goes under a binder.

The three candidate properties are Red.weaklyNormalizing/Red.hasType (CR1), Red.of_step/Red.of_multiStep (backward closure, CR2) and Red.of_neutral (CR3, here in the sharp form "a normal neutral term is reducible", since Neutral in this development already means normal neutral). HasType.red_substituteSimultaneously is the fundamental lemma and HasType.terminating its corollary at the identity substitution.

Renaming preserves reduction and normal forms

A de Bruijn renaming touches only variables, so every syntactic notion of the reduction theory is stable under it. These are the facts the Kripke clause of Red needs.

theorem GaudisCrypt.ModuleExpression.isProcTuple_of_rename {m : ModuleExpression} {ρ : ℕ → ℕ} (h : (rename ρ m).IsProcTuple) : m.IsProcTuple

Being a procedure tuple is a property of the term's shape, not of its variables, so a renaming cannot create one.

theorem GaudisCrypt.ModuleExpression.Normal.rename {m : ModuleExpression} : m.Normal → ∀ (ρ : ℕ → ℕ), (ModuleExpression.rename ρ m).Normal

Normal forms are stable under renaming.

theorem GaudisCrypt.ModuleExpression.Neutral.rename {m : ModuleExpression} : m.Neutral → ∀ (ρ : ℕ → ℕ), (ModuleExpression.rename ρ m).Neutral

Neutral forms are stable under renaming.

theorem GaudisCrypt.ModuleExpression.ReductionStep.rename {m n : ModuleExpression} (h : m.ReductionStep n) (ρ : ℕ → ℕ) : (ModuleExpression.rename ρ m).ReductionStep (ModuleExpression.rename ρ n)

Reduction is stable under renaming.

theorem GaudisCrypt.ModuleExpression.MultiStepReduction.rename {m n : ModuleExpression} (h : m.MultiStepReduction n) (ρ : ℕ → ℕ) : (ModuleExpression.rename ρ m).MultiStepReduction (ModuleExpression.rename ρ n)

Multi-step reduction is stable under renaming.

Weak normalization

Terminating asks for a stuck reduct; the reducibility argument needs the sharper "reduces to a normal form", which is stable under renaming (a stuck term need not stay stuck under a renaming for any obvious syntactic reason, whereas a normal term visibly does). For well-typed terms the two agree — Stuck.normal — and that is how Terminating is recovered at the end.

def GaudisCrypt.ModuleExpression.WeaklyNormalizing (m : ModuleExpression) : Prop

m reduces to a normal form. Refines Terminating.

Equations

• m.WeaklyNormalizing = ∃ (n : GaudisCrypt.ModuleExpression), m.MultiStepReduction n ∧ n.Normal

theorem GaudisCrypt.ModuleExpression.Normal.weaklyNormalizing {m : ModuleExpression} (h : m.Normal) : m.WeaklyNormalizing

theorem GaudisCrypt.ModuleExpression.WeaklyNormalizing.terminating {m : ModuleExpression} (h : m.WeaklyNormalizing) : m.Terminating

theorem GaudisCrypt.ModuleExpression.WeaklyNormalizing.head {m m' : ModuleExpression} (hstep : m.ReductionStep m') (h : m'.WeaklyNormalizing) : m.WeaklyNormalizing

Weak normalization is closed under expansion by a single step.

theorem GaudisCrypt.ModuleExpression.WeaklyNormalizing.of_multiStep {m m' : ModuleExpression} (hred : m.MultiStepReduction m') (h : m'.WeaklyNormalizing) : m.WeaklyNormalizing

Weak normalization is closed under expansion along a multi-step reduction.

theorem GaudisCrypt.ModuleExpression.WeaklyNormalizing.rename {m : ModuleExpression} (h : m.WeaklyNormalizing) (ρ : ℕ → ℕ) : (ModuleExpression.rename ρ m).WeaklyNormalizing

theorem GaudisCrypt.ModuleExpression.WeaklyNormalizing.abs {b : ModuleExpression} (h : b.WeaklyNormalizing) : b.abs.WeaklyNormalizing

theorem GaudisCrypt.ModuleExpression.WeaklyNormalizing.pair {a b : ModuleExpression} (ha : a.WeaklyNormalizing) (hb : b.WeaklyNormalizing) : (a.pair b).WeaklyNormalizing

Renamings compose

theorem GaudisCrypt.ModuleExpression.HasType.isRenaming_id {Γ : ModuleContext} : IsRenaming Γ Γ id

theorem GaudisCrypt.ModuleExpression.HasType.IsRenaming.comp {Δ Γ Ξ : ModuleContext} {ρ ρ' : ℕ → ℕ} (h : IsRenaming Δ Γ ρ) (h' : IsRenaming Γ Ξ ρ') : IsRenaming Δ Ξ (ρ' ∘ ρ)

The reducibility relation

def GaudisCrypt.ModuleExpression.Red : ModuleTypeRep → ModuleContext → ModuleExpression → Prop

Tait's reducibility candidates, Kripke-style. Red T Γ m says: m has type T in Γ and is weakly normalizing, and hereditarily so under the eliminations T allows — projections at a product type, and application to a reducible argument (in any context reachable from Γ by a renaming) at a function type.

Equations

• One or more equations did not get rendered due to their size.

theorem GaudisCrypt.ModuleExpression.Red.hasType {T : ModuleTypeRep} {Γ : ModuleContext} {m : ModuleExpression} (h : Red T Γ m) : m.HasType Γ T

CR1, typing half.

theorem GaudisCrypt.ModuleExpression.Red.weaklyNormalizing {T : ModuleTypeRep} {Γ : ModuleContext} {m : ModuleExpression} (h : Red T Γ m) : m.WeaklyNormalizing

CR1, normalization half.

theorem GaudisCrypt.ModuleExpression.Red.of_step {T : ModuleTypeRep} {Γ : ModuleContext} {m m' : ModuleExpression} : m.HasType Γ T → m.ReductionStep m' → Red T Γ m' → Red T Γ m

CR2: reducibility is closed under expansion by a single step.

theorem GaudisCrypt.ModuleExpression.Red.of_multiStep {T : ModuleTypeRep} {Γ : ModuleContext} {m m' : ModuleExpression} (hred : m.MultiStepReduction m') (h : Red T Γ m') : m.HasType Γ T → Red T Γ m

CR2 along a multi-step reduction.

theorem GaudisCrypt.ModuleExpression.Red.of_neutral {T : ModuleTypeRep} {Γ : ModuleContext} {m : ModuleExpression} : m.Neutral → m.HasType Γ T → Red T Γ m

CR3: a well-typed normal neutral term is reducible. (Neutral already implies Normal in this development, so no reasoning about the term's reducts is needed.)

theorem GaudisCrypt.ModuleExpression.Red.rename {T : ModuleTypeRep} {Γ Γ' : ModuleContext} {m : ModuleExpression} {ρ : ℕ → ℕ} : Red T Γ m → HasType.IsRenaming Γ Γ' ρ → Red T Γ' (ModuleExpression.rename ρ m)

Reducibility is stable under weakening (any renaming of the context).

The fundamental lemma

def GaudisCrypt.ModuleExpression.RedSubst (Δ Γ : ModuleContext) (σ : ℕ → ModuleExpression) : Prop

A substitution all of whose values are reducible at the type their index carries.

Equations

• GaudisCrypt.ModuleExpression.RedSubst Δ Γ σ = ∀ {n : ℕ} (h : n < List.length Δ), GaudisCrypt.ModuleExpression.Red Δ[n] Γ (σ n)

theorem GaudisCrypt.ModuleExpression.RedSubst.isSubst {Δ Γ : ModuleContext} {σ : ℕ → ModuleExpression} (h : RedSubst Δ Γ σ) : HasType.IsSubst Δ Γ σ

theorem GaudisCrypt.ModuleExpression.RedSubst.lift {Δ Γ : ModuleContext} {A : ModuleTypeRep} {σ : ℕ → ModuleExpression} (h : RedSubst Δ Γ σ) : RedSubst (A :: Δ) (A :: Γ) (liftSubst σ)

Lifting a reducible substitution under a binder keeps it reducible.

theorem GaudisCrypt.ModuleExpression.HasType.red_substituteSimultaneously {m : ModuleExpression} {Δ : ModuleContext} {T : ModuleTypeRep} (h : m.HasType Δ T) {Γ : ModuleContext} {σ : ℕ → ModuleExpression} : RedSubst Δ Γ σ → Red T Γ (ModuleExpression.substituteSimultaneously σ m)

The fundamental lemma of the reducibility argument: a well-typed term is reducible under every reducible substitution.

Weak normalization

theorem GaudisCrypt.ModuleExpression.HasType.terminating {m : ModuleExpression} {Δ : ModuleContext} {T : ModuleTypeRep} (h : m.HasType Δ T) : m.Terminating

Weak normalization: every well-typed module expression reduces to a normal form, hence terminates. Instantiate the fundamental lemma at the identity substitution, which is reducible because a variable is a normal neutral term.