Module expressions

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

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

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
• (holes.append sig).toModuleTypeRepTuple = (GaudisCrypt.ModuleTypeRep.proc sig).prod holes.toModuleTypeRepTuple

inductive GaudisCrypt.ModuleExpression [ProgramSpec] : Type (max 1 u_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 [ProgramSpec] {sig : ProcedureSignature} : Procedure sig → ModuleExpression
• procHoles [ProgramSpec] {holes : HoleSigs} {sig : ProcedureSignature} : holes.NonEmpty → ProcedureWithHoles holes sig → ModuleExpression
• var [ProgramSpec] : ℕ → ModuleExpression
• app [ProgramSpec] : ModuleExpression → ModuleExpression → ModuleExpression
• fst [ProgramSpec] : ModuleExpression → ModuleExpression
• snd [ProgramSpec] : ModuleExpression → ModuleExpression
• abs [ProgramSpec] : ModuleExpression → ModuleExpression
• pair [ProgramSpec] : ModuleExpression → ModuleExpression → ModuleExpression
• unit [ProgramSpec] : ModuleExpression

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

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

theorem GaudisCrypt.ModuleExpression.HasType.procHoles_inv [ProgramSpec] {Δ : 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 [ProgramSpec] {Δ : ModuleContext} {T : ModuleTypeRep} {n : ℕ} (h : (ModuleExpression.var n).HasType Δ T) : ∃ (hn : n < List.length Δ), Δ[n] = T

theorem GaudisCrypt.ModuleExpression.HasType.app_inv [ProgramSpec] {Δ : 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 [ProgramSpec] {Δ : ModuleContext} {A : ModuleTypeRep} {m : ModuleExpression} (h : m.fst.HasType Δ A) : ∃ (B : ModuleTypeRep), m.HasType Δ (A.prod B)

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

theorem GaudisCrypt.ModuleExpression.HasType.abs_inv [ProgramSpec] {Δ : 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 [ProgramSpec] {Δ : 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 [ProgramSpec] {Δ : 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 [ProgramSpec] (ρ : ℕ → ℕ) : 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 [ProgramSpec] (σ : ℕ → 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 [ProgramSpec] (σ : ℕ → 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 [ProgramSpec] (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 [ProgramSpec] (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

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 [ProgramSpec] {holes : HoleSigs} : holes.Instantiation → ModuleExpression

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

Equations

• One or more equations did not get rendered due to their size.
• x_2.toModuleExpr = GaudisCrypt.ModuleExpression.unit

inductive GaudisCrypt.ModuleExpression.ReductionStep [ProgramSpec] : ModuleExpression → ModuleExpression → Prop

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

• beta [ProgramSpec] {body arg : ModuleExpression} : (body.abs.app arg).ReductionStep (body.substitute arg)
• appL [ProgramSpec] {f f' arg : ModuleExpression} : f.ReductionStep f' → (f.app arg).ReductionStep (f'.app arg)
• appR [ProgramSpec] {f arg arg' : ModuleExpression} : arg.ReductionStep arg' → (f.app arg).ReductionStep (f.app arg')
• lam [ProgramSpec] {body body' : ModuleExpression} : body.ReductionStep body' → body.abs.ReductionStep body'.abs
• pairL [ProgramSpec] {a a' b : ModuleExpression} : a.ReductionStep a' → (a.pair b).ReductionStep (a'.pair b)
• pairR [ProgramSpec] {a b b' : ModuleExpression} : b.ReductionStep b' → (a.pair b).ReductionStep (a.pair b')
• fstPair [ProgramSpec] {a b : ModuleExpression} : (a.pair b).fst.ReductionStep a
• fst [ProgramSpec] {e e' : ModuleExpression} : e.ReductionStep e' → e.fst.ReductionStep e'.fst
• sndPair [ProgramSpec] {a b : ModuleExpression} : (a.pair b).snd.ReductionStep b
• snd [ProgramSpec] {e e' : ModuleExpression} : e.ReductionStep e' → e.snd.ReductionStep e'.snd
• delta [ProgramSpec] {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 fun {sig : ProcedureSignature} => inst))

def GaudisCrypt.ModuleExpression.MultiStepReduction [ProgramSpec] : ModuleExpression → ModuleExpression → Prop

Equations

• GaudisCrypt.ModuleExpression.MultiStepReduction = Rewriting.Star 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 [ProgramSpec] {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 [ProgramSpec] (Δ Γ : 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 [ProgramSpec] {Δ Γ : 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 [ProgramSpec] {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 [ProgramSpec] {Δ : 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 [ProgramSpec] {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 [ProgramSpec] {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 [ProgramSpec] {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 [ProgramSpec] : 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 [ProgramSpec] (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 [ProgramSpec] : ModuleExpression → Prop

Beta-normal form: no redex anywhere.

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

inductive GaudisCrypt.ModuleExpression.Neutral [ProgramSpec] : 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 [ProgramSpec] {n : ℕ} : (ModuleExpression.var n).Neutral
• app [ProgramSpec] {f arg : ModuleExpression} : f.Neutral → arg.Normal → (f.app arg).Neutral
• appProcHoles [ProgramSpec] {holes : HoleSigs} {sig : ProcedureSignature} {arg : ModuleExpression} {p : ProcedureWithHoles holes sig} (ne : holes.NonEmpty) : arg.Normal → ¬arg.IsProcTuple → ((procHoles ne p).app arg).Neutral
• fst [ProgramSpec] {e : ModuleExpression} : e.Neutral → e.fst.Neutral
• snd [ProgramSpec] {e : ModuleExpression} : e.Neutral → e.snd.Neutral

@[implicit_reducible]

instance GaudisCrypt.ModuleExpression.instDecidableNormal [ProgramSpec] (m : ModuleExpression) : Decidable m.Normal

Equations

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

@[implicit_reducible]

instance GaudisCrypt.ModuleExpression.instDecidableNeutral [ProgramSpec] (m : ModuleExpression) : Decidable m.Neutral

Equations

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

inductive GaudisCrypt.ModuleExpression.NormalClosed [ProgramSpec] : 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 [ProgramSpec] {sig : ProcedureSignature} {p : Procedure sig} : (ModuleExpression.proc p).NormalClosed
• procHoles [ProgramSpec] {holes : HoleSigs} {sig : ProcedureSignature} {ne : holes.NonEmpty} {p : ProcedureWithHoles holes sig} : (ModuleExpression.procHoles ne p).NormalClosed
• abs [ProgramSpec] {body : ModuleExpression} : body.Normal → body.abs.NormalClosed
• pair [ProgramSpec] {a b : ModuleExpression} : a.NormalClosed → b.NormalClosed → (a.pair b).NormalClosed
• unit [ProgramSpec] : ModuleExpression.unit.NormalClosed

Embedding into Metatheory.STLCext

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

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

theorem GaudisCrypt.ModuleExpression.HasType.preservation_multi [ProgramSpec] {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 [ProgramSpec] (m : ModuleExpression) : Prop

Equations

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

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

def GaudisCrypt.ModuleExpression.Terminating [ProgramSpec] (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 [ProgramSpec] {m : ModuleExpression} (h : m.Stuck) : m.Terminating

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

theorem GaudisCrypt.ModuleExpression.multiStepReduction_confluence [ProgramSpec] {m n1 n2 : ModuleExpression} : m.MultiStepReduction n1 → m.MultiStepReduction n2 → n1.Stuck → n2.Stuck → n1 = n2

def GaudisCrypt.ModuleExpression.convertible [ProgramSpec] : 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 [ProgramSpec] (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 [ProgramSpec] {m : ModuleExpression} (ht : m.Terminating) : m.reduce.Stuck

theorem GaudisCrypt.ModuleExpression.multiStepReduction_terminating [ProgramSpec] {m n : ModuleExpression} (h : m.MultiStepReduction n) : m.Terminating ↔ n.Terminating

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

@[simp]

theorem GaudisCrypt.ModuleExpression.reduce_of_stuck [ProgramSpec] {m : ModuleExpression} (h : m.Stuck) : m.reduce = m

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

Multi-step reduction refines convertibility.

theorem GaudisCrypt.ModuleExpression.convertible_terminating [ProgramSpec] {m n : ModuleExpression} (h : m.convertible n) : m.Terminating ↔ n.Terminating

Termination is invariant along equireducibility: each ReductionStep preserves it via multiStepReduction_terminating, and refl/symm/trans closure is immediate.

theorem GaudisCrypt.ModuleExpression.convertible_reduce [ProgramSpec] {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_terminating [ProgramSpec] {m : ModuleExpression} : m.Terminating ↔ m.reduce.Terminating

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

theorem GaudisCrypt.ModuleExpression.reduce_hasType [ProgramSpec] {m : ModuleExpression} {Δ : ModuleContext} {T : ModuleTypeRep} (h : m.HasType Δ T) : m.reduce.HasType Δ T

Reduction preserves typing.

theorem GaudisCrypt.ModuleExpression.progress [ProgramSpec] {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 [ProgramSpec] {Δ : ModuleContext} {T : ModuleTypeRep} {m : ModuleExpression} (h : m.Stuck) (hty : m.HasType Δ T) : m.Normal

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

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

theorem GaudisCrypt.ModuleExpression.reduce_normal [ProgramSpec] {Δ : ModuleContext} {T : ModuleTypeRep} {m : ModuleExpression} (h : m.HasType Δ T) : m.reduce.Normal

The reduct of a well-typed closed term is closed-normal.

theorem GaudisCrypt.ModuleExpression.reduce_normalClosed [ProgramSpec] {m : ModuleExpression} {T : ModuleTypeRep} (h : m.HasType [] T) : m.reduce.NormalClosed

The reduct of a well-typed closed term is closed-normal.

theorem GaudisCrypt.ModuleExpression.reduce_idempotent [ProgramSpec] (m : ModuleExpression) : m.reduce.reduce = m.reduce

@[simp]

theorem GaudisCrypt.ModuleExpression.reduce_of_normal [ProgramSpec] {m : ModuleExpression} (h : m.Normal) : m.reduce = m

A normal term is its own reduct (normal terms are stuck).

@[simp]

theorem GaudisCrypt.ModuleExpression.reduce_proc [ProgramSpec] {sig : ProcedureSignature} (p : Procedure sig) : (proc p).reduce = proc p

theorem GaudisCrypt.ModuleExpression.confluence [ProgramSpec] {m m1 m2 : ModuleExpression} (h1 : m.MultiStepReduction m1) (h2 : m.MultiStepReduction m2) : m1.reduce = m2.reduce

theorem GaudisCrypt.ModuleExpression.reduce_step [ProgramSpec] {m n : ModuleExpression} (h : m.ReductionStep n) : m.reduce = n.reduce

theorem GaudisCrypt.ModuleExpression.reduce_convertible [ProgramSpec] {m n : ModuleExpression} : m.convertible n → m.reduce = n.reduce

theorem GaudisCrypt.ModuleExpression.reduce_multiStepReduction [ProgramSpec] {m n : ModuleExpression} (h : m.MultiStepReduction n) : m.reduce = n.reduce

theorem GaudisCrypt.ModuleExpression.reduce_convertible_iff [ProgramSpec] {m n : ModuleExpression} : m.convertible n ↔ m.reduce = n.reduce

theorem GaudisCrypt.ModuleExpression.reduce_beta [ProgramSpec] (body arg : ModuleExpression) : (body.abs.app arg).reduce = (body.substitute arg).reduce

Misc

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

A well-typed closed term is never neutral.

theorem GaudisCrypt.ModuleExpression.multiStepReduction_app_cong [ProgramSpec] {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_fst_cong [ProgramSpec] {e e' : ModuleExpression} (h : e.MultiStepReduction e') : e.fst.MultiStepReduction e'.fst

fst is a congruence for multi-step reduction.

theorem GaudisCrypt.ModuleExpression.multiStepReduction_pair_cong [ProgramSpec] {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 [ProgramSpec] {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.reduce_pair_terminating [ProgramSpec] {m1 m2 : ModuleExpression} (h1 : m1.Terminating) (h2 : m2.Terminating) : (m1.pair m2).reduce = m1.reduce.pair m2.reduce

Remaining reduce specification lemmas

@[simp]

theorem GaudisCrypt.ModuleExpression.reduce_fst [ProgramSpec] (m m' : ModuleExpression) : (m.pair m').fst.reduce = m.reduce

@[simp]

theorem GaudisCrypt.ModuleExpression.reduce_snd [ProgramSpec] (m m' : ModuleExpression) : (m.pair m').snd.reduce = m'.reduce

theorem GaudisCrypt.ModuleExpression.reduce_fst_cong [ProgramSpec] (m m' : ModuleExpression) : m.reduce = m'.reduce → m.fst.reduce = m'.fst.reduce

theorem GaudisCrypt.ModuleExpression.reduce_snd_cong [ProgramSpec] (m m' : ModuleExpression) : m.reduce = m'.reduce → m.snd.reduce = m'.snd.reduce

theorem GaudisCrypt.ModuleExpression.reduce_pair_cong [ProgramSpec] {a a' b b' : ModuleExpression} (ha : a.reduce = a') (hb : b.reduce = b') : (a.pair b).reduce = (a'.pair b').reduce

Congruence form for .pair: combines two independently-computed simplifications reduce a = a' / reduce b = b' (however they were obtained — a'/b' need not themselves be fully reduced) into one for the surrounding .pair. Proved directly via convertible: pairL/pairR lift convertible_reduce through .pair on each side, and reduce_convertible_iff turns the resulting convertible witness back into a reduce equation.

theorem GaudisCrypt.ModuleExpression.reduce_app_cong [ProgramSpec] {a a' b b' : ModuleExpression} (ha : a.reduce = a') (hb : b.reduce = b') : (a.app b).reduce = (a'.app b').reduce

Congruence form for .app, matching reduce_pair_cong.

One-sided congruences. reduce_pair_cong/reduce_app_cong replace both components, so simplifying only one of them means proving reduce b = b' for the other by rfl, i.e. putting reduce b there — a reduce around a component that had none. These leave the other component exactly as it is. (The hypothesis reduce a = a' already forces a' to be reduce a, hence reduce a' = a' by idempotence, which is what makes the untouched side go through.)

theorem GaudisCrypt.ModuleExpression.reduce_pair_cong_left [ProgramSpec] {a a' b : ModuleExpression} (ha : a.reduce = a') : (a.pair b).reduce = (a'.pair b).reduce

theorem GaudisCrypt.ModuleExpression.reduce_pair_cong_right [ProgramSpec] {a b b' : ModuleExpression} (hb : b.reduce = b') : (a.pair b).reduce = (a.pair b').reduce

theorem GaudisCrypt.ModuleExpression.reduce_app_cong_left [ProgramSpec] {a a' b : ModuleExpression} (ha : a.reduce = a') : (a.app b).reduce = (a'.app b).reduce

theorem GaudisCrypt.ModuleExpression.reduce_app_cong_right [ProgramSpec] {a b b' : ModuleExpression} (hb : b.reduce = b') : (a.app b).reduce = (a.app b').reduce

theorem GaudisCrypt.ModuleExpression.reduce_abs_cong [ProgramSpec] {a a' : ModuleExpression} (ha : a.reduce = a') : a.abs.reduce = a'.abs.reduce

Congruence form for .abs, matching reduce_pair_cong/reduce_app_cong.

Stripping an inner reduce

reduce only cares about its argument up to convertibility, so a subterm that is already a reduce can be replaced by what it reduces (reduce_idempotent on both sides of the matching _cong lemma). This is what makes the .reduces that toModule leaves behind disappear when a composite expression is reduced — the module_apply tactic (GaudisCrypt/Language/Syntax2.lean) uses all six of them to bring the two sides of an X.apply_simp goal into the same shape.

theorem GaudisCrypt.ModuleExpression.reduce_app_left [ProgramSpec] (f x : ModuleExpression) : (f.reduce.app x).reduce = (f.app x).reduce

theorem GaudisCrypt.ModuleExpression.reduce_app_right [ProgramSpec] (f x : ModuleExpression) : (f.app x.reduce).reduce = (f.app x).reduce

theorem GaudisCrypt.ModuleExpression.reduce_pair_left [ProgramSpec] (a b : ModuleExpression) : (a.reduce.pair b).reduce = (a.pair b).reduce

theorem GaudisCrypt.ModuleExpression.reduce_pair_right [ProgramSpec] (a b : ModuleExpression) : (a.pair b.reduce).reduce = (a.pair b).reduce

theorem GaudisCrypt.ModuleExpression.reduce_fst_inner [ProgramSpec] (m : ModuleExpression) : m.reduce.fst.reduce = m.fst.reduce

theorem GaudisCrypt.ModuleExpression.reduce_snd_inner [ProgramSpec] (m : ModuleExpression) : m.reduce.snd.reduce = m.snd.reduce

theorem GaudisCrypt.ModuleExpression.pair_type_is_pair [ProgramSpec] {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.tacticNormalmoduleStep : Lean.ParserDescr

One step of normalmodule's core script, factored out so normalmodule can require it to fire at least once (see below) while still repeating it leniently afterwards.

Equations

• GaudisCrypt.tacticNormalmoduleStep = Lean.ParserDescr.node `GaudisCrypt.tacticNormalmoduleStep 1024 (Lean.ParserDescr.nonReservedSymbol "normalmoduleStep" false)

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)

reduce_simp

def GaudisCrypt.tacticReduce_simp_head : Lean.ParserDescr

Equations

• GaudisCrypt.tacticReduce_simp_head = Lean.ParserDescr.node `GaudisCrypt.tacticReduce_simp_head 1024 (Lean.ParserDescr.nonReservedSymbol "reduce_simp_head" false)

def GaudisCrypt.tacticReduce_simp : Lean.ParserDescr

Fully normalize reduce m subterms — one reduction step at a time via reduce_simp_head, then the reduce collapsed via reduce_of_normal (see reduceSimpProcImpl) — repeatedly, including inside freshly-exposed nested reduces (handled by simp's own subterm traversal, not by this tactic). Lenient per subterm — whatever it can't reduce is left as it is — but, like simp, it fails when that is every subterm and the goal comes back unchanged. Closes the goal outright if it simplifies all the way to True.

substitute and friends are in the simp set because reduce_beta's result is reduce (body.substitute arg), with substitute a structurally recursive def that no reduce_simp_head branch matches on: unfolding it is what turns that result back into a constructor tree the next step can work on.

Equations

• GaudisCrypt.tacticReduce_simp = Lean.ParserDescr.node `GaudisCrypt.tacticReduce_simp 1024 (Lean.ParserDescr.nonReservedSymbol "reduce_simp" false)