Module expressions, basics

The raw calculus underlying modules: ModuleTypeRep (the types), the untyped syntax tree ModuleExpression with extrinsic typing (ModuleExpression.HasType), de Bruijn renaming/substitution with the σ-calculus laws they satisfy, call-by-value reduction with its normal forms, and the deciding tactics moduletyping and normalmodule.

This is the part of the development that depends neither on confluence (ModuleExpressionConfluence.lean) nor on normalization (ModuleExpressionNormalization.lean); their consequences — the reduce theory and the reduce_simp tactic — live in ModuleExpression.lean, which is what downstream modules import.

Modules.lean builds Module T — a closed, well-typed, normal expression — on top of that.

inductive GaudisCrypt.ModuleTypeRep : Type 1

Possible types of modules.

• proc : ProcedureSignature → ModuleTypeRep
• prod : ModuleTypeRep → ModuleTypeRep → ModuleTypeRep
• arr : ModuleTypeRep → ModuleTypeRep → ModuleTypeRep
• unit : ModuleTypeRep

@[reducible, inline]

abbrev GaudisCrypt.ModuleContext : Type 1

Equations

• GaudisCrypt.ModuleContext = List GaudisCrypt.ModuleTypeRep

def GaudisCrypt.HoleSigs.toModuleTypeRepTuple : HoleSigs → ModuleTypeRep

The right-nested product type of a hole signature (native UM copy of the TypedModules definition; namespace-scoped under GaudisCrypt to avoid clashing with TypedModules's while both coexist).

Equations

• GaudisCrypt.HoleSigs.empty.toModuleTypeRepTuple = GaudisCrypt.ModuleTypeRep.unit
• (GaudisCrypt.HoleSigs.cons sig holes).toModuleTypeRepTuple = (GaudisCrypt.ModuleTypeRep.proc sig).prod holes.toModuleTypeRepTuple

inductive GaudisCrypt.ModuleExpression : Type 1

Untyped module expressions: the raw syntax tree of the module calculus, with no context/type indices. Well-typedness is captured extrinsically by the predicate ModuleExpression.HasType. Variables are de Bruijn indices (Nat); abs carries no domain annotation (the domain is recovered by HasType).

• proc {sig : ProcedureSignature} : Procedure sig → ModuleExpression
• procHoles {holes : HoleSigs} {sig : ProcedureSignature} : holes.NonEmpty → ProcedureWithHoles holes sig → ModuleExpression
• var : ℕ → ModuleExpression
• app : ModuleExpression → ModuleExpression → ModuleExpression
• fst : ModuleExpression → ModuleExpression
• snd : ModuleExpression → ModuleExpression
• abs : ModuleExpression → ModuleExpression
• pair : ModuleExpression → ModuleExpression → ModuleExpression
• unit : ModuleExpression

inductive GaudisCrypt.ModuleExpression.HasType : ModuleExpression → ModuleContext → ModuleTypeRep → Prop

ModuleExpression.HasType m Δ T holds when the untyped expression m is well-typed in module context Δ with type T. This is the extrinsic counterpart of the indices of TypedModules.ModuleExpression: every TypedModules.ModuleExpression Δ T erases (via TypedModules.ModuleExpression.erase) to an m with HasType m Δ T, and conversely.

• proc {Δ : ModuleContext} {sig : ProcedureSignature} (p : Procedure sig) : (ModuleExpression.proc p).HasType Δ (ModuleTypeRep.proc sig)
• procHoles {Δ : ModuleContext} {holes : HoleSigs} {sig : ProcedureSignature} (ne : holes.NonEmpty) (p : ProcedureWithHoles holes sig) : (ModuleExpression.procHoles ne p).HasType Δ (holes.toModuleTypeRepTuple.arr (ModuleTypeRep.proc sig))
• var {Δ : ModuleContext} (n : ℕ) (h : n < List.length Δ) : (ModuleExpression.var n).HasType Δ Δ[n]
• app {Δ : ModuleContext} {A B : ModuleTypeRep} {m n : ModuleExpression} : m.HasType Δ (A.arr B) → n.HasType Δ A → (m.app n).HasType Δ B
• fst {Δ : ModuleContext} {A B : ModuleTypeRep} {m : ModuleExpression} : m.HasType Δ (A.prod B) → m.fst.HasType Δ A
• snd {Δ : ModuleContext} {A B : ModuleTypeRep} {m : ModuleExpression} : m.HasType Δ (A.prod B) → m.snd.HasType Δ B
• abs {Δ : List ModuleTypeRep} {A B : ModuleTypeRep} {m : ModuleExpression} : m.HasType (A :: Δ) B → m.abs.HasType Δ (A.arr B)
• pair {Δ : ModuleContext} {A B : ModuleTypeRep} {m n : ModuleExpression} : m.HasType Δ A → n.HasType Δ B → (m.pair n).HasType Δ (A.prod B)
• unit {Δ : ModuleContext} : ModuleExpression.unit.HasType Δ ModuleTypeRep.unit

theorem GaudisCrypt.ModuleExpression.HasType.proc_inv {Δ : ModuleContext} {T : ModuleTypeRep} {sig : ProcedureSignature} {p : Procedure sig} (h : (ModuleExpression.proc p).HasType Δ T) : T = ModuleTypeRep.proc sig

theorem GaudisCrypt.ModuleExpression.HasType.procHoles_inv {Δ : ModuleContext} {T : ModuleTypeRep} {holes : HoleSigs} {sig : ProcedureSignature} {ne : holes.NonEmpty} {p : ProcedureWithHoles holes sig} (h : (ModuleExpression.procHoles ne p).HasType Δ T) : T = holes.toModuleTypeRepTuple.arr (ModuleTypeRep.proc sig)

theorem GaudisCrypt.ModuleExpression.HasType.var_inv {Δ : ModuleContext} {T : ModuleTypeRep} {n : ℕ} (h : (ModuleExpression.var n).HasType Δ T) : ∃ (hn : n < List.length Δ), Δ[n] = T

theorem GaudisCrypt.ModuleExpression.HasType.app_inv {Δ : ModuleContext} {B : ModuleTypeRep} {m n : ModuleExpression} (h : (m.app n).HasType Δ B) : ∃ (A : ModuleTypeRep), m.HasType Δ (A.arr B) ∧ n.HasType Δ A

theorem GaudisCrypt.ModuleExpression.HasType.fst_inv {Δ : ModuleContext} {A : ModuleTypeRep} {m : ModuleExpression} (h : m.fst.HasType Δ A) : ∃ (B : ModuleTypeRep), m.HasType Δ (A.prod B)

theorem GaudisCrypt.ModuleExpression.HasType.snd_inv {Δ : ModuleContext} {B : ModuleTypeRep} {m : ModuleExpression} (h : m.snd.HasType Δ B) : ∃ (A : ModuleTypeRep), m.HasType Δ (A.prod B)

theorem GaudisCrypt.ModuleExpression.HasType.abs_inv {Δ : ModuleContext} {T : ModuleTypeRep} {m : ModuleExpression} (h : m.abs.HasType Δ T) : ∃ (A : ModuleTypeRep) (B : ModuleTypeRep), T = A.arr B ∧ m.HasType (A :: Δ) B

theorem GaudisCrypt.ModuleExpression.HasType.pair_inv {Δ : ModuleContext} {T : ModuleTypeRep} {m n : ModuleExpression} (h : (m.pair n).HasType Δ T) : ∃ (A : ModuleTypeRep) (B : ModuleTypeRep), T = A.prod B ∧ m.HasType Δ A ∧ n.HasType Δ B

theorem GaudisCrypt.ModuleExpression.HasType.unit_inv {Δ : ModuleContext} {T : ModuleTypeRep} (h : ModuleExpression.unit.HasType Δ T) : T = ModuleTypeRep.unit

De Bruijn renaming and substitution on the untyped tree

The untyped analogues of TypedModules.ModuleExpression.rename/substitute: since there are no type indices, a renaming is a plain Nat → Nat and a substitution a Nat → ModuleExpression. These are permanent. Their agreement with the intrinsic versions under erase is recorded by the transitional erase_rename/erase_substitute* lemmas below.

def GaudisCrypt.ModuleExpression.liftRen (ρ : ℕ → ℕ) : ℕ → ℕ

Lift a de Bruijn renaming under one binder: index 0 is fixed, n+1 ↦ ρ n + 1. Untyped analogue of liftRenaming.

Equations

• GaudisCrypt.ModuleExpression.liftRen ρ 0 = 0
• GaudisCrypt.ModuleExpression.liftRen ρ n.succ = ρ n + 1

def GaudisCrypt.ModuleExpression.rename (ρ : ℕ → ℕ) : ModuleExpression → ModuleExpression

Apply a de Bruijn renaming to every variable, going under binders with liftRen. Untyped analogue of TypedModules.ModuleExpression.rename.

Equations

• GaudisCrypt.ModuleExpression.rename ρ (GaudisCrypt.ModuleExpression.proc p) = GaudisCrypt.ModuleExpression.proc p
• GaudisCrypt.ModuleExpression.rename ρ (GaudisCrypt.ModuleExpression.procHoles ne p) = GaudisCrypt.ModuleExpression.procHoles ne p
• GaudisCrypt.ModuleExpression.rename ρ (GaudisCrypt.ModuleExpression.var n) = GaudisCrypt.ModuleExpression.var (ρ n)
• GaudisCrypt.ModuleExpression.rename ρ (f.app a) = (GaudisCrypt.ModuleExpression.rename ρ f).app (GaudisCrypt.ModuleExpression.rename ρ a)
• GaudisCrypt.ModuleExpression.rename ρ e.fst = (GaudisCrypt.ModuleExpression.rename ρ e).fst
• GaudisCrypt.ModuleExpression.rename ρ e.snd = (GaudisCrypt.ModuleExpression.rename ρ e).snd
• GaudisCrypt.ModuleExpression.rename ρ body.abs = (GaudisCrypt.ModuleExpression.rename (GaudisCrypt.ModuleExpression.liftRen ρ) body).abs
• GaudisCrypt.ModuleExpression.rename ρ (a.pair b) = (GaudisCrypt.ModuleExpression.rename ρ a).pair (GaudisCrypt.ModuleExpression.rename ρ b)
• GaudisCrypt.ModuleExpression.rename ρ GaudisCrypt.ModuleExpression.unit = GaudisCrypt.ModuleExpression.unit

def GaudisCrypt.ModuleExpression.liftSubst (σ : ℕ → ModuleExpression) : ℕ → ModuleExpression

Lift a substitution under one binder: index 0 ↦ var 0; n+1 ↦ the weakening of σ n. Untyped analogue of liftSubstitution.

Equations

• GaudisCrypt.ModuleExpression.liftSubst σ 0 = GaudisCrypt.ModuleExpression.var 0
• GaudisCrypt.ModuleExpression.liftSubst σ n.succ = GaudisCrypt.ModuleExpression.rename Nat.succ (σ n)

def GaudisCrypt.ModuleExpression.substituteSimultaneously (σ : ℕ → ModuleExpression) : ModuleExpression → ModuleExpression

Apply a simultaneous substitution to every variable, going under binders with liftSubst. Untyped analogue of substituteSimultaneously.

Equations

• GaudisCrypt.ModuleExpression.substituteSimultaneously σ (GaudisCrypt.ModuleExpression.proc p) = GaudisCrypt.ModuleExpression.proc p
• GaudisCrypt.ModuleExpression.substituteSimultaneously σ (GaudisCrypt.ModuleExpression.procHoles ne p) = GaudisCrypt.ModuleExpression.procHoles ne p
• GaudisCrypt.ModuleExpression.substituteSimultaneously σ (GaudisCrypt.ModuleExpression.var n) = σ n
• GaudisCrypt.ModuleExpression.substituteSimultaneously σ (f.app a) = (GaudisCrypt.ModuleExpression.substituteSimultaneously σ f).app (GaudisCrypt.ModuleExpression.substituteSimultaneously σ a)
• GaudisCrypt.ModuleExpression.substituteSimultaneously σ e.fst = (GaudisCrypt.ModuleExpression.substituteSimultaneously σ e).fst
• GaudisCrypt.ModuleExpression.substituteSimultaneously σ e.snd = (GaudisCrypt.ModuleExpression.substituteSimultaneously σ e).snd
• GaudisCrypt.ModuleExpression.substituteSimultaneously σ body.abs = (GaudisCrypt.ModuleExpression.substituteSimultaneously (GaudisCrypt.ModuleExpression.liftSubst σ) body).abs
• GaudisCrypt.ModuleExpression.substituteSimultaneously σ (a.pair b) = (GaudisCrypt.ModuleExpression.substituteSimultaneously σ a).pair (GaudisCrypt.ModuleExpression.substituteSimultaneously σ b)
• GaudisCrypt.ModuleExpression.substituteSimultaneously σ GaudisCrypt.ModuleExpression.unit = GaudisCrypt.ModuleExpression.unit

def GaudisCrypt.ModuleExpression.variableSubstitution (arg : ModuleExpression) : ℕ → ModuleExpression

Single-variable substitution map: 0 ↦ arg, n+1 ↦ var n. Untyped analogue of variableSubstitution.

Equations

• arg.variableSubstitution 0 = arg
• arg.variableSubstitution n.succ = GaudisCrypt.ModuleExpression.var n

def GaudisCrypt.ModuleExpression.substitute (body arg : ModuleExpression) : ModuleExpression

Single-variable de Bruijn substitution: replace index 0 in body by arg.

Equations

• body.substitute arg = GaudisCrypt.ModuleExpression.substituteSimultaneously arg.variableSubstitution body

The de Bruijn σ-calculus laws

rename and substituteSimultaneously compose in the four standard ways. Both the confluence and the normalization proof need them to push a renaming or a substitution through a β-contractum.

theorem GaudisCrypt.ModuleExpression.liftRen_comp (ρ ρ' : ℕ → ℕ) : liftRen ρ' ∘ liftRen ρ = liftRen (ρ' ∘ ρ)

theorem GaudisCrypt.ModuleExpression.rename_rename (ρ ρ' : ℕ → ℕ) (m : ModuleExpression) : rename ρ' (rename ρ m) = rename (ρ' ∘ ρ) m

theorem GaudisCrypt.ModuleExpression.liftSubst_comp_liftRen (σ : ℕ → ModuleExpression) (ρ : ℕ → ℕ) : liftSubst σ ∘ liftRen ρ = liftSubst (σ ∘ ρ)

theorem GaudisCrypt.ModuleExpression.substituteSimultaneously_rename (ρ : ℕ → ℕ) (σ : ℕ → ModuleExpression) (m : ModuleExpression) : substituteSimultaneously σ (rename ρ m) = substituteSimultaneously (σ ∘ ρ) m

Substituting into a renamed term is substituting along the composite.

theorem GaudisCrypt.ModuleExpression.liftSubst_rename (σ : ℕ → ModuleExpression) (ρ : ℕ → ℕ) : (liftSubst fun (k : ℕ) => rename ρ (σ k)) = fun (n : ℕ) => rename (liftRen ρ) (liftSubst σ n)

theorem GaudisCrypt.ModuleExpression.rename_substituteSimultaneously (ρ : ℕ → ℕ) (σ : ℕ → ModuleExpression) (m : ModuleExpression) : rename ρ (substituteSimultaneously σ m) = substituteSimultaneously (fun (n : ℕ) => rename ρ (σ n)) m

Renaming a substituted term is substituting along the renamed substitution.

theorem GaudisCrypt.ModuleExpression.liftSubst_substituteSimultaneously (σ τ : ℕ → ModuleExpression) : (liftSubst fun (k : ℕ) => substituteSimultaneously τ (σ k)) = fun (n : ℕ) => substituteSimultaneously (liftSubst τ) (liftSubst σ n)

theorem GaudisCrypt.ModuleExpression.substituteSimultaneously_substituteSimultaneously (σ τ : ℕ → ModuleExpression) (m : ModuleExpression) : substituteSimultaneously τ (substituteSimultaneously σ m) = substituteSimultaneously (fun (n : ℕ) => substituteSimultaneously τ (σ n)) m

Two substitutions in a row are one substitution along the composite.

theorem GaudisCrypt.ModuleExpression.substituteSimultaneously_var (m : ModuleExpression) : substituteSimultaneously (fun (n : ℕ) => var n) m = m

theorem GaudisCrypt.ModuleExpression.rename_id (m : ModuleExpression) : rename id m = m

The identity renaming acts trivially, on any expression (no typing hypothesis needed — contrast HasType.rename_eq_self).

theorem GaudisCrypt.ModuleExpression.rename_substitute (ρ : ℕ → ℕ) (body arg : ModuleExpression) : rename ρ (body.substitute arg) = (rename (liftRen ρ) body).substitute (rename ρ arg)

Renaming commutes with β-substitution.

theorem GaudisCrypt.ModuleExpression.substituteSimultaneously_substitute (σ : ℕ → ModuleExpression) (body arg : ModuleExpression) : substituteSimultaneously σ (body.substitute arg) = (substituteSimultaneously (liftSubst σ) body).substitute (substituteSimultaneously σ arg)

A simultaneous substitution commutes with β-substitution.

theorem GaudisCrypt.ModuleExpression.substitute_substituteSimultaneously_liftSubst (σ : ℕ → ModuleExpression) (body arg : ModuleExpression) : (substituteSimultaneously (liftSubst σ) body).substitute arg = substituteSimultaneously (fun (n : ℕ) => Nat.rec arg (fun (k : ℕ) (x : ModuleExpression) => σ k) n) body

β-substituting into a lifted simultaneous substitution is one simultaneous substitution: index 0 goes to arg, index n+1 to σ n.

Reduction on the untyped tree, and type preservation

ReductionStep mirrors the intrinsic one but on raw syntax; the payoff is HasType.preservation — what intrinsic typing gave for free must now be proved. All permanent.

def GaudisCrypt.HoleSigs.Instantiation.toModuleExpr {holes : HoleSigs} : holes.Instantiation → ModuleExpression

The untyped tuple of procedures corresponding to an instantiation (untyped analogue of HoleSigs.Instantiation.toModuleTuple).

Equations

• x_2.toModuleExpr = GaudisCrypt.ModuleExpression.unit
• inst.toModuleExpr = (GaudisCrypt.ModuleExpression.proc inst).pair GaudisCrypt.ModuleExpression.unit
• inst.toModuleExpr = (GaudisCrypt.ModuleExpression.proc inst.1).pair inst.2.toModuleExpr

theorem GaudisCrypt.HoleSigs.Instantiation.toModuleExpr_rename {holes : HoleSigs} (inst : holes.Instantiation) (ρ : ℕ → ℕ) : ModuleExpression.rename ρ inst.toModuleExpr = inst.toModuleExpr

inst.toModuleExpr is closed, so renaming leaves it alone.

theorem GaudisCrypt.HoleSigs.Instantiation.toModuleExpr_substituteSimultaneously {holes : HoleSigs} (inst : holes.Instantiation) (σ : ℕ → ModuleExpression) : ModuleExpression.substituteSimultaneously σ inst.toModuleExpr = inst.toModuleExpr

inst.toModuleExpr is closed, so substitution leaves it alone.

inductive GaudisCrypt.ModuleExpression.ReductionStep : ModuleExpression → ModuleExpression → Prop

Non-deterministic single-step reduction on untyped module expressions.

• beta {body arg : ModuleExpression} : (body.abs.app arg).ReductionStep (body.substitute arg)
• appL {f f' arg : ModuleExpression} : f.ReductionStep f' → (f.app arg).ReductionStep (f'.app arg)
• appR {f arg arg' : ModuleExpression} : arg.ReductionStep arg' → (f.app arg).ReductionStep (f.app arg')
• lam {body body' : ModuleExpression} : body.ReductionStep body' → body.abs.ReductionStep body'.abs
• pairL {a a' b : ModuleExpression} : a.ReductionStep a' → (a.pair b).ReductionStep (a'.pair b)
• pairR {a b b' : ModuleExpression} : b.ReductionStep b' → (a.pair b).ReductionStep (a.pair b')
• fstPair {a b : ModuleExpression} : (a.pair b).fst.ReductionStep a
• fst {e e' : ModuleExpression} : e.ReductionStep e' → e.fst.ReductionStep e'.fst
• sndPair {a b : ModuleExpression} : (a.pair b).snd.ReductionStep b
• snd {e e' : ModuleExpression} : e.ReductionStep e' → e.snd.ReductionStep e'.snd
• delta {holes : HoleSigs} {sigs : ProcedureSignature} (ne : holes.NonEmpty) (proc : ProcedureWithHoles holes sigs) (inst : holes.Instantiation) : ((procHoles ne proc).app inst.toModuleExpr).ReductionStep (ModuleExpression.proc (proc.instantiate inst))

def GaudisCrypt.ModuleExpression.MultiStepReduction : ModuleExpression → ModuleExpression → Prop

Transitive-reflexive closure of ReductionStep.

Equations

• GaudisCrypt.ModuleExpression.MultiStepReduction = Relation.ReflTransGen GaudisCrypt.ModuleExpression.ReductionStep

def GaudisCrypt.ModuleExpression.HasType.IsRenaming (Δ Γ : ModuleContext) (ρ : ℕ → ℕ) : Prop

A de Bruijn renaming ρ maps context Δ into Γ if every Δ-index has a Γ-index of the same type sitting at the renamed position.

Equations

• GaudisCrypt.ModuleExpression.HasType.IsRenaming Δ Γ ρ = ∀ {n : ℕ} (h : n < List.length Δ), ∃ (h' : ρ n < List.length Γ), Γ[ρ n] = Δ[n]

theorem GaudisCrypt.ModuleExpression.HasType.isRenaming_succ {Γ : ModuleContext} {A : ModuleTypeRep} : IsRenaming Γ (A :: Γ) Nat.succ

Weakening: prepending a binder is the renaming Nat.succ.

theorem GaudisCrypt.ModuleExpression.HasType.IsRenaming.lift {Δ Γ : ModuleContext} {A : ModuleTypeRep} {ρ : ℕ → ℕ} (h : IsRenaming Δ Γ ρ) : IsRenaming (A :: Δ) (A :: Γ) (liftRen ρ)

A context renaming lifts under one binder to liftRen ρ.

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

Renaming preserves typing along a context renaming.

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

A substitution σ maps Δ into Γ if it sends every Δ-index to a Γ-typed term.

Equations

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

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

A well-typed substitution lifts under one binder to liftSubst σ.

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

Simultaneous substitution preserves typing along a well-typed substitution.

theorem GaudisCrypt.ModuleExpression.HasType.substitute {Δ : List ModuleTypeRep} {u t : ModuleTypeRep} {body arg : ModuleExpression} (hb : body.HasType (u :: Δ) t) (ha : arg.HasType Δ u) : (body.substitute arg).HasType Δ t

Single-variable substitution preserves typing (the β-substitution lemma).

theorem GaudisCrypt.ModuleExpression.HasType.substituteSimultaneously_eq_self {m : ModuleExpression} {Δ : ModuleContext} {T : ModuleTypeRep} (h : m.HasType Δ T) {σ : ℕ → ModuleExpression} : (∀ n < List.length Δ, σ n = ModuleExpression.var n) → ModuleExpression.substituteSimultaneously σ m = m

A term only mentions the variables its context declares, so a substitution that is the identity on those leaves it alone — whatever it does to the indices beyond Δ. For a closed term (Δ = []) the hypothesis is vacuous: Module.substituteSimultaneously_expression.

theorem GaudisCrypt.ModuleExpression.HasType.rename_eq_self {m : ModuleExpression} {Δ : ModuleContext} {T : ModuleTypeRep} (h : m.HasType Δ T) {ρ : ℕ → ℕ} : (∀ n < List.length Δ, ρ n = n) → ModuleExpression.rename ρ m = m

The same for a renaming: a term only mentions the variables its context declares, so a renaming that is the identity on those leaves it alone. For a closed term (Δ = []) the hypothesis is vacuous: Module.rename_expression.

theorem GaudisCrypt.ModuleExpression.HasType.preservation {m m' : ModuleExpression} (hstep : m.ReductionStep m') {Δ : ModuleContext} {T : ModuleTypeRep} : m.HasType Δ T → m'.HasType Δ T

Type preservation (subject reduction): reduction preserves the typing judgment. This is the extrinsic replacement for what the intrinsic TypedModules.ModuleExpression guaranteed by construction.

def GaudisCrypt.IsProcArgType : ModuleTypeRep → Prop

Equations

• GaudisCrypt.IsProcArgType GaudisCrypt.ModuleTypeRep.unit = True
• GaudisCrypt.IsProcArgType ((GaudisCrypt.ModuleTypeRep.proc a).prod rest) = GaudisCrypt.IsProcArgType rest
• GaudisCrypt.IsProcArgType x✝ = False

Normal forms on the untyped tree

Untyped analogues of IsProcHoles/IsProcTuple/Normal/Neutral/NormalClosed. Permanent; mirror the intrinsic versions structurally.

def GaudisCrypt.ModuleExpression.IsProcTuple : ModuleExpression → Prop

m is a right-nested tuple of hole-free procedures (.unit, or .pair (.proc _) rest with IsProcTuple rest) — the ground arguments a procedure-with-holes accepts.

Equations

• GaudisCrypt.ModuleExpression.unit.IsProcTuple = True
• ((GaudisCrypt.ModuleExpression.proc a).pair rest).IsProcTuple = rest.IsProcTuple
• x✝.IsProcTuple = False

@[implicit_reducible]

instance GaudisCrypt.ModuleExpression.instDecidableIsProcTuple (m : ModuleExpression) : Decidable m.IsProcTuple

Equations

• GaudisCrypt.ModuleExpression.unit.instDecidableIsProcTuple = isTrue trivial
• ((GaudisCrypt.ModuleExpression.proc a_2).pair rest).instDecidableIsProcTuple = match rest.instDecidableIsProcTuple with | isTrue h => isTrue h | isFalse h => isFalse h
• (GaudisCrypt.ModuleExpression.unit.pair rest).instDecidableIsProcTuple = isFalse GaudisCrypt.ModuleExpression.instDecidableIsProcTuple._proof_1
• ((GaudisCrypt.ModuleExpression.var a_2).pair rest).instDecidableIsProcTuple = isFalse GaudisCrypt.ModuleExpression.instDecidableIsProcTuple._proof_1
• ((a_2.app a_3).pair rest).instDecidableIsProcTuple = isFalse GaudisCrypt.ModuleExpression.instDecidableIsProcTuple._proof_1
• (a_2.fst.pair rest).instDecidableIsProcTuple = isFalse GaudisCrypt.ModuleExpression.instDecidableIsProcTuple._proof_1
• (a_2.snd.pair rest).instDecidableIsProcTuple = isFalse GaudisCrypt.ModuleExpression.instDecidableIsProcTuple._proof_1
• (a_2.abs.pair rest).instDecidableIsProcTuple = isFalse GaudisCrypt.ModuleExpression.instDecidableIsProcTuple._proof_1
• ((a_2.pair a_3).pair rest).instDecidableIsProcTuple = isFalse GaudisCrypt.ModuleExpression.instDecidableIsProcTuple._proof_1
• ((GaudisCrypt.ModuleExpression.procHoles a_2 a_3).pair rest).instDecidableIsProcTuple = isFalse GaudisCrypt.ModuleExpression.instDecidableIsProcTuple._proof_1
• (GaudisCrypt.ModuleExpression.proc a).instDecidableIsProcTuple = isFalse GaudisCrypt.ModuleExpression.instDecidableIsProcTuple._proof_1
• (GaudisCrypt.ModuleExpression.var a).instDecidableIsProcTuple = isFalse GaudisCrypt.ModuleExpression.instDecidableIsProcTuple._proof_1
• (a.app a_1).instDecidableIsProcTuple = isFalse GaudisCrypt.ModuleExpression.instDecidableIsProcTuple._proof_1
• a.fst.instDecidableIsProcTuple = isFalse GaudisCrypt.ModuleExpression.instDecidableIsProcTuple._proof_1
• a.snd.instDecidableIsProcTuple = isFalse GaudisCrypt.ModuleExpression.instDecidableIsProcTuple._proof_1
• a.abs.instDecidableIsProcTuple = isFalse GaudisCrypt.ModuleExpression.instDecidableIsProcTuple._proof_1
• (GaudisCrypt.ModuleExpression.procHoles a a_1).instDecidableIsProcTuple = isFalse GaudisCrypt.ModuleExpression.instDecidableIsProcTuple._proof_1

inductive GaudisCrypt.ModuleExpression.Normal : ModuleExpression → Prop

Beta-normal form: no redex anywhere.

• neutral {e : ModuleExpression} : e.Neutral → e.Normal
• abs {body : ModuleExpression} : body.Normal → body.abs.Normal
• pair {a b : ModuleExpression} : a.Normal → b.Normal → (a.pair b).Normal
• proc {sig : ProcedureSignature} {p : Procedure sig} : (ModuleExpression.proc p).Normal
• procHoles {holes : HoleSigs} {sig : ProcedureSignature} {ne : holes.NonEmpty} {p : ProcedureWithHoles holes sig} : (ModuleExpression.procHoles ne p).Normal
• unit : ModuleExpression.unit.Normal

inductive GaudisCrypt.ModuleExpression.Neutral : ModuleExpression → Prop

Neutral form: no outermost redex — the head is a variable, or a procedure-with-holes applied to a normal non-proc-tuple (so the δ-rule is stuck).

• var {n : ℕ} : (ModuleExpression.var n).Neutral
• app {f arg : ModuleExpression} : f.Neutral → arg.Normal → (f.app arg).Neutral
• appProcHoles {holes : HoleSigs} {sig : ProcedureSignature} {arg : ModuleExpression} {p : ProcedureWithHoles holes sig} (ne : holes.NonEmpty) : arg.Normal → ¬arg.IsProcTuple → ((procHoles ne p).app arg).Neutral
• fst {e : ModuleExpression} : e.Neutral → e.fst.Neutral
• snd {e : ModuleExpression} : e.Neutral → e.snd.Neutral

@[implicit_reducible]

instance GaudisCrypt.ModuleExpression.instDecidableNormal (m : ModuleExpression) : Decidable m.Normal

Equations

• m.instDecidableNormal = (GaudisCrypt.ModuleExpression.decidableNormalNeutral✝ m).1

@[implicit_reducible]

instance GaudisCrypt.ModuleExpression.instDecidableNeutral (m : ModuleExpression) : Decidable m.Neutral

Equations

• m.instDecidableNeutral = (GaudisCrypt.ModuleExpression.decidableNormalNeutral✝ m).2

inductive GaudisCrypt.ModuleExpression.NormalClosed : ModuleExpression → Prop

Normal form of a closed term. Neutral terms cannot occur closed (they need a free variable), so there are fewer cases than Normal; the abs body is still general Normal (it lives under one binder).

• proc {sig : ProcedureSignature} {p : Procedure sig} : (ModuleExpression.proc p).NormalClosed
• procHoles {holes : HoleSigs} {sig : ProcedureSignature} {ne : holes.NonEmpty} {p : ProcedureWithHoles holes sig} : (ModuleExpression.procHoles ne p).NormalClosed
• abs {body : ModuleExpression} : body.Normal → body.abs.NormalClosed
• pair {a b : ModuleExpression} : a.NormalClosed → b.NormalClosed → (a.pair b).NormalClosed
• unit : ModuleExpression.unit.NormalClosed

Shape predicates for call-by-value reduction (untyped analogues)

theorem GaudisCrypt.ModuleExpression.NormalClosed.normal {m : ModuleExpression} (h : m.NormalClosed) : m.Normal

theorem GaudisCrypt.ModuleExpression.HasType.preservation_multi {m m' : ModuleExpression} {Δ : ModuleContext} {T : ModuleTypeRep} (hm : m.HasType Δ T) (h : m.MultiStepReduction m') : m'.HasType Δ T

Typing is preserved along multi-step reduction.

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

Equations

• m.Stuck = ¬∃ (n : GaudisCrypt.ModuleExpression), m.ReductionStep n

theorem GaudisCrypt.ModuleExpression.ReductionStep.not_normal {m n : ModuleExpression} (h : m.ReductionStep n) : ¬m.Normal

Whatever reduces has a redex, so it is not normal. Every case is closed by inverting the Normal/Neutral derivation: a redex head (.abs, .pair under .fst/.snd, a .procHoles applied to a proc-tuple) is never neutral, and the congruence cases contradict the induction hypothesis on the reducing subterm.

theorem GaudisCrypt.ModuleExpression.Normal.stuck {m : ModuleExpression} (h : m.Normal) : m.Stuck

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

m terminates: it multi-step reduces to some normal form.

Equations

• m.Terminating = ∃ (n : GaudisCrypt.ModuleExpression), n.Stuck ∧ m.MultiStepReduction n

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

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

def GaudisCrypt.ModuleExpression.convertible : ModuleExpression → ModuleExpression → Prop

Convertibility: the equivalence relation generated by ReductionStep, i.e. its reflexive, symmetric, transitive closure.

Equations

• GaudisCrypt.ModuleExpression.convertible = Relation.EqvGen GaudisCrypt.ModuleExpression.ReductionStep

noncomputable def GaudisCrypt.ModuleExpression.reduce (m : ModuleExpression) : ModuleExpression

β-normal form: a chosen normal form reachable from m when it terminates, else unit.

Equations

• m.reduce = if h : m.Terminating then Exists.choose h else Set.Nonempty.some ⋯

theorem GaudisCrypt.ModuleExpression.reduce_stuck {m : ModuleExpression} (ht : m.Terminating) : m.reduce.Stuck

theorem GaudisCrypt.ModuleExpression.multiStepReduction_reduce {m : ModuleExpression} (h : m.Terminating) : m.MultiStepReduction m.reduce

theorem GaudisCrypt.ModuleExpression.convertible_of_multiStep {a b : ModuleExpression} (h : a.MultiStepReduction b) : a.convertible b

Multi-step reduction refines convertibility.

theorem GaudisCrypt.ModuleExpression.convertible_reduce {m : ModuleExpression} : m.convertible m.reduce

reduce m is always convertible to m (a reduct if terminating, a class rep otherwise).

theorem GaudisCrypt.ModuleExpression.reduce_eq_of_convertible_not_term {m n : ModuleExpression} (h : m.convertible n) (hm : ¬m.Terminating) (hn : ¬n.Terminating) : m.reduce = n.reduce

reduce is constant on a convertible class of non-terminating expressions. (Not private: ModuleExpression.lean needs it for reduce_idempotent/confluence.)

theorem GaudisCrypt.ModuleExpression.exists_toModuleExpr {holes : HoleSigs} {Δ : ModuleContext} {a : ModuleExpression} : a.HasType Δ holes.toModuleTypeRepTuple → a.IsProcTuple → ∃ (inst : holes.Instantiation), a = inst.toModuleExpr

A well-typed proc-tuple is the module-expression image of some instantiation (the existence content of procTupleLookup/procTupleLookup_toModuleTuple, but as a Prop).

theorem GaudisCrypt.ModuleExpression.progress {m : ModuleExpression} {Δ : ModuleContext} {T : ModuleTypeRep} : m.HasType Δ T → ¬m.Normal → ∃ (n : ModuleExpression), m.ReductionStep n

Progress for well-typed (possibly open) terms: a non-normal well-typed term reduces.

theorem GaudisCrypt.ModuleExpression.Stuck.normal {Δ : ModuleContext} {T : ModuleTypeRep} {m : ModuleExpression} (h : m.Stuck) (hty : m.HasType Δ T) : m.Normal

theorem GaudisCrypt.ModuleExpression.Normal.normalClosed {m : ModuleExpression} {T : ModuleTypeRep} (_h : m.Normal) (_hty : m.HasType [] T) : m.NormalClosed

A normal well-typed closed term is closed-normal.

Misc

theorem GaudisCrypt.ModuleExpression.hasType_empty_context_not_neutral {m : ModuleExpression} {T : ModuleTypeRep} (h : m.HasType [] T) : ¬m.Neutral

A well-typed closed term is never neutral.

theorem GaudisCrypt.ModuleExpression.multiStepReduction_app_cong {m1 m1' m2 m2' : ModuleExpression} (h1 : m1.MultiStepReduction m1') (h2 : m2.MultiStepReduction m2') : (m1.app m2).MultiStepReduction (m1'.app m2')

app is a congruence for multi-step reduction.

theorem GaudisCrypt.ModuleExpression.multiStepReduction_abs_cong {b b' : ModuleExpression} (h : b.MultiStepReduction b') : b.abs.MultiStepReduction b'.abs

abs is a congruence for multi-step reduction.

theorem GaudisCrypt.ModuleExpression.multiStepReduction_fst_cong {e e' : ModuleExpression} (h : e.MultiStepReduction e') : e.fst.MultiStepReduction e'.fst

fst is a congruence for multi-step reduction.

theorem GaudisCrypt.ModuleExpression.multiStepReduction_snd_cong {e e' : ModuleExpression} (h : e.MultiStepReduction e') : e.snd.MultiStepReduction e'.snd

snd is a congruence for multi-step reduction.

theorem GaudisCrypt.ModuleExpression.multiStepReduction_pair_cong {a a' b b' : ModuleExpression} (h1 : a.MultiStepReduction a') (h2 : b.MultiStepReduction b') : (a.pair b).MultiStepReduction (a'.pair b')

pair is a congruence for multi-step reduction.

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

A pair of stuck expressions is stuck: pair can only step via pairL/pairR.

theorem GaudisCrypt.ModuleExpression.pair_type_is_pair {m : ModuleExpression} {t1 t2 : ModuleTypeRep} (hty : m.HasType [] (t1.prod t2)) (h : m.NormalClosed) : ∃ (m1 : ModuleExpression) (m2 : ModuleExpression), m = m1.pair m2

A well-typed closed normal term of product type is a pair.

Tactics

moduletyping

def GaudisCrypt.tacticModuletyping : Lean.ParserDescr

Syntax-directed closer for ModuleExpression.HasType m Δ T: peels off the HasType constructor matching m's head, leaves whatever it cannot close (e.g. an unprovable .var bound) as an open goal. See moduletyping! for a variant that fails loudly instead.

Equations

• GaudisCrypt.tacticModuletyping = Lean.ParserDescr.node `GaudisCrypt.tacticModuletyping 1024 (Lean.ParserDescr.nonReservedSymbol "moduletyping" false)

def GaudisCrypt.tacticModuletyping! : Lean.ParserDescr

moduletyping, but fails loudly instead of leaving unclosed goals open. Not fail-fast: it still runs the core script to completion (closing everything it can) before reporting, one "Cannot show ‹original goal›: ‹reason›" line per leftover goal, with the reason coming from describeStuckModuleTypingGoal.

Equations

• GaudisCrypt.tacticModuletyping! = Lean.ParserDescr.node `GaudisCrypt.tacticModuletyping! 1024 (Lean.ParserDescr.nonReservedSymbol "moduletyping!" false)

normalmodule

def GaudisCrypt.tacticNormalmodule : Lean.ParserDescr

Syntax-directed closer for Normal m / Neutral m: peels the constructor matching m's head, disambiguating .app's two constructors by checking whether the function side is a literal .procHoles node, and leaves whatever it cannot close open. Fails outright if it cannot make even one step of progress (e.g. Neutral (.pair _ _), which no constructor can ever produce) rather than silently no-op'ing. See normalmodule! for a variant that fails loudly with a diagnosed reason on every unclosed goal, not just a wholly-stuck one.

Equations

• GaudisCrypt.tacticNormalmodule = Lean.ParserDescr.node `GaudisCrypt.tacticNormalmodule 1024 (Lean.ParserDescr.nonReservedSymbol "normalmodule" false)

def GaudisCrypt.tacticNormalmodule! : Lean.ParserDescr

normalmodule, but fails loudly instead of leaving unclosed goals open. Not fail-fast: it still runs the core script to completion (closing everything it can) before reporting, one "Cannot show ‹original goal›: ‹reason›" line per leftover goal, with the reason coming from describeStuckNormalModuleGoal.

Equations

• GaudisCrypt.tacticNormalmodule! = Lean.ParserDescr.node `GaudisCrypt.tacticNormalmodule! 1024 (Lean.ParserDescr.nonReservedSymbol "normalmodule!" false)