Modules

A Module T is a closed, well-typed, normal ModuleExpression of type T, together with the operations on such (application, projections, pairing) and the IsModule bridge from Lean types to ModuleTypeReps. The underlying expression calculus lives in ModuleExpression.lean (and the files it imports).

structure GaudisCrypt.Module (T : ModuleTypeRep) : Type 1

• expression : ModuleExpression
• typed : self.expression.HasType [] T
• normal : self.expression.NormalClosed

noncomputable def GaudisCrypt.ModuleExpression.toModule {T : ModuleTypeRep} (m : ModuleExpression) (h : m.HasType [] T := by moduletyping!) : Module T

Build a Module from a well-typed closed expression by normalising it.

Equations

• m.toModule h = { expression := m.reduce, typed := ⋯, normal := ⋯ }

@[implicit_reducible]

noncomputable instance GaudisCrypt.instCoeFunModuleArrForall {T U : ModuleTypeRep} : CoeFun (Module (T.arr U)) fun (x : Module (T.arr U)) => Module T → Module U

Equations

• GaudisCrypt.instCoeFunModuleArrForall = { coe := fun (f : GaudisCrypt.Module (T.arr U)) (x : GaudisCrypt.Module T) => (f.expression.app x.expression).toModule ⋯ }

noncomputable def GaudisCrypt.Module.fst' {T U : ModuleTypeRep} (m : Module (T.prod U)) : Module T

Equations

• m.fst' = m.expression.fst.toModule ⋯

noncomputable def GaudisCrypt.Module.snd' {T U : ModuleTypeRep} (m : Module (T.prod U)) : Module U

Equations

• m.snd' = m.expression.snd.toModule ⋯

noncomputable def GaudisCrypt.Module.pair' {T U : ModuleTypeRep} (m1 : Module T) (m2 : Module U) : Module (T.prod U)

Equations

• m1.pair' m2 = (m1.expression.pair m2.expression).toModule ⋯

theorem GaudisCrypt.Module.ext {T : ModuleTypeRep} {m1 m2 : Module T} (h : m1.expression = m2.expression) : m1 = m2

theorem GaudisCrypt.Module.ext_iff {T : ModuleTypeRep} {m1 m2 : Module T} : m1 = m2 ↔ m1.expression = m2.expression

@[simp]

theorem GaudisCrypt.Module.expression_fst' {T U : ModuleTypeRep} (m : Module (T.prod U)) : m.fst'.expression = m.expression.fst.reduce

@[simp]

theorem GaudisCrypt.Module.expression_snd' {T U : ModuleTypeRep} (m : Module (T.prod U)) : m.snd'.expression = m.expression.snd.reduce

@[simp]

theorem GaudisCrypt.Module.toModule_expression {T : ModuleTypeRep} (m : ModuleExpression) (h : m.HasType [] T) : (m.toModule h).expression = m.reduce

@[simp]

theorem GaudisCrypt.Module.reduce_expression {T : ModuleTypeRep} (m : Module T) : m.expression.reduce = m.expression

@[simp]

theorem GaudisCrypt.Module.substituteSimultaneously_expression {T : ModuleTypeRep} (m : Module T) (σ : ℕ → ModuleExpression) : ModuleExpression.substituteSimultaneously σ m.expression = m.expression

A module's expression is closed, so a substitution leaves it alone.

@[simp]

theorem GaudisCrypt.Module.rename_expression {T : ModuleTypeRep} (m : Module T) (ρ : ℕ → ℕ) : ModuleExpression.rename ρ m.expression = m.expression

A module's expression is closed, so a renaming leaves it alone. (This is what a substitution going under a binder does to it — liftSubst renames by Nat.succ — so normalising an application of a curried module needs this as well as Module.substituteSimultaneously_expression.)

theorem GaudisCrypt.Module.expression_pair' {T U : ModuleTypeRep} (m1 : Module T) (m2 : Module U) : (m1.pair' m2).expression = m1.expression.pair m2.expression

Pairing two modules pairs their expressions — no reduce left over, both being normal.

theorem GaudisCrypt.Module.reduce_pair_expression {T U : ModuleTypeRep} {a b : ModuleExpression} (m1 : Module T) (m2 : Module U) (ha : a.reduce = m1.expression) (hb : b.reduce = m2.expression) : (a.pair b).reduce = (m1.pair' m2).expression

Reducing a pair componentwise: if the components reduce to the expressions of the modules m1/m2, the pair reduces to the expression of their Module.pair'. Turns a reduce of a whole record into the record of the reduced components, with no detour through termination — normality of the result comes from the modules m1/m2. (Currently unused: moduleApply used to peel X.apply_simp's record with it, but now normalises both sides with reduce_simp instead.)

@[simp]

theorem GaudisCrypt.Module.fst_pair' {T U : ModuleTypeRep} (m1 : Module T) (m2 : Module U) : (m1.pair' m2).fst' = m1

@[simp]

theorem GaudisCrypt.Module.snd_pair' {T U : ModuleTypeRep} (m1 : Module T) (m2 : Module U) : (m1.pair' m2).snd' = m2

theorem GaudisCrypt.Module.pair_fst_snd' {a✝ a✝¹ : ModuleTypeRep} {m : Module (a✝.prod a✝¹)} : m.fst'.pair' m.snd' = m

@[reducible, inline]

abbrev GaudisCrypt.Module.Unit : Type 1

Equations

• GaudisCrypt.Module.Unit = GaudisCrypt.Module GaudisCrypt.ModuleTypeRep.unit

noncomputable def GaudisCrypt.Module.unit : Module ModuleTypeRep.unit

Equations

• GaudisCrypt.Module.unit = GaudisCrypt.ModuleExpression.unit.toModule GaudisCrypt.Module.unit._proof_1

class GaudisCrypt.IsModule (T : Type 1) : Type 1

• moduleTypeRep : ModuleTypeRep
• isModule : T = Module (moduleTypeRep T)

@[reducible]

instance GaudisCrypt.instIsModuleModule {t : ModuleTypeRep} : IsModule (Module t)

Equations

• GaudisCrypt.instIsModuleModule = { moduleTypeRep := t, isModule := ⋯ }

def GaudisCrypt.Module.moduleTypeRep (T : Type 1) [inst : IsModule T] : ModuleTypeRep

Equations

• GaudisCrypt.Module.moduleTypeRep T = GaudisCrypt.IsModule.moduleTypeRep T

def GaudisCrypt.Module.cast (T : Type 1) [inst : IsModule T] (m : T) : Module (moduleTypeRep T)

Equations

• GaudisCrypt.Module.cast T m = ⋯ ▸ m

def GaudisCrypt.Module.cast' (T : Type 1) [inst : IsModule T] (m : Module (moduleTypeRep T)) : T

Equations

• GaudisCrypt.Module.cast' T m = ⋯ ▸ m

def GaudisCrypt.Module.Arr (M N : Type 1) [IsModule M] [IsModule N] : Type 1

Equations

• GaudisCrypt.Module.Arr M N = GaudisCrypt.Module ((GaudisCrypt.Module.moduleTypeRep M).arr (GaudisCrypt.Module.moduleTypeRep N))

@[implicit_reducible]

instance GaudisCrypt.instIsModuleArr (M N : Type 1) [IsModule M] [IsModule N] : IsModule (Module.Arr M N)

Equations

• GaudisCrypt.instIsModuleArr M N = { moduleTypeRep := (GaudisCrypt.Module.moduleTypeRep M).arr (GaudisCrypt.Module.moduleTypeRep N), isModule := ⋯ }

def GaudisCrypt.Module.Proc (sig : ProcedureSignature) : Type 1

Equations

• GaudisCrypt.Module.Proc sig = GaudisCrypt.Module (GaudisCrypt.ModuleTypeRep.proc sig)

@[implicit_reducible]

instance GaudisCrypt.instIsModuleProc {sig : ProcedureSignature} : IsModule (Module.Proc sig)

Equations

• GaudisCrypt.instIsModuleProc = { moduleTypeRep := GaudisCrypt.ModuleTypeRep.proc sig, isModule := ⋯ }

noncomputable def GaudisCrypt.Module.app' {A B : ModuleTypeRep} (m : Module (A.arr B)) (m' : Module A) : Module B

Equations

• m.app' m' = (m.expression.app m'.expression).toModule ⋯

noncomputable def GaudisCrypt.Module.app {M N : Type 1} [iM : IsModule M] [iN : IsModule N] (m : Arr M N) (m' : M) : N

Equations

• GaudisCrypt.Module.app m m' = ⋯ ▸ (⋯ ▸ m).app' (⋯ ▸ m')

theorem GaudisCrypt.Module.cast_app {M N : Type 1} [IsModule M] [IsModule N] (a : Arr M N) (b : M) : cast N (app a b) = (cast (Arr M N) a).app' (cast M b)

def GaudisCrypt.Parser.Attr.module_accessor : Lean.ParserDescr

Simp set collecting the field accessors moduletype emits (X.f : X → Tᵢ, a chain of Module.fst'/Module.snd').

A goal about a field of an abstract module — S : CommitmentScheme a parameter, not a literal record — can only make progress by unfolding the accessor, and a tactic cannot know the accessor's name. This set is how procApply reaches them.

Equations

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

def GaudisCrypt.Parser.Attr.module_accessor_proc : Lean.ParserDescr

Simplification procedure

Equations

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

structure GaudisCrypt.ModuleTypeUtilities (M T : Type 1) [IsModule M] [IsModule T] (acc : M → T) : Type 1

What is derivable about a field accessor acc : M → T of a module type, bundled into one declaration.

The moduletype command emits one of these per field, as X.f.utilities, rather than a separate declaration per fact — the facts are reached as X.f.utilities.accessorModule and so on. It is a structure and not a class: there is nothing to synthesise, the command hands the value over by name.

• proj : ModuleExpression → ModuleExpression

  The projection acc implements, as it acts on ModuleExpressions (fun e => e.snd.fst, …).

• accessorModule : Module.Arr M T

  The accessor as a module of its own: a projection is a module morphism.

• apply_simp (m : M) : Module.app self.accessorModule m = acc m

  …and applying that module is the accessor.

• expression_eq (m : M) : (Module.cast T (acc m)).expression = (self.proj (Module.cast M m).expression).reduce

  The accessor at the level of expressions: it is proj, reduced. The .reduce is not removable — Module.expression is always a reduct, and proj m.expression need not be normal.

def GaudisCrypt.Module.Prod (M N : Type 1) [IsModule M] [IsModule N] : Type 1

Equations

• GaudisCrypt.Module.Prod M N = GaudisCrypt.Module ((GaudisCrypt.Module.moduleTypeRep M).prod (GaudisCrypt.Module.moduleTypeRep N))

@[implicit_reducible]

instance GaudisCrypt.instIsModuleProd (M N : Type 1) [IsModule M] [IsModule N] : IsModule (Module.Prod M N)

Equations

• GaudisCrypt.instIsModuleProd M N = { moduleTypeRep := (GaudisCrypt.Module.moduleTypeRep M).prod (GaudisCrypt.Module.moduleTypeRep N), isModule := ⋯ }

noncomputable def GaudisCrypt.Module.fst {M N : Type 1} [iM : IsModule M] [iN : IsModule N] (m : Prod M N) : M

Equations

• GaudisCrypt.Module.fst m = ⋯ ▸ (⋯ ▸ m).fst'

noncomputable def GaudisCrypt.Module.snd {M N : Type 1} [iM : IsModule M] [iN : IsModule N] (m : Prod M N) : N

Equations

• GaudisCrypt.Module.snd m = ⋯ ▸ (⋯ ▸ m).snd'

noncomputable def GaudisCrypt.Module.pair {M N : Type 1} [iM : IsModule M] [iN : IsModule N] (m1 : M) (m2 : N) : Prod M N

Equations

• GaudisCrypt.Module.pair m1 m2 = ⋯ ▸ (⋯ ▸ m1).pair' (⋯ ▸ m2)

@[simp]

theorem GaudisCrypt.Module.fst_pair {M N : Type 1} [IsModule M] [IsModule N] (m1 : M) (m2 : N) : fst (pair m1 m2) = m1

@[simp]

theorem GaudisCrypt.Module.snd_pair {M N : Type 1} [IsModule M] [IsModule N] (m1 : M) (m2 : N) : snd (pair m1 m2) = m2

theorem GaudisCrypt.Module.pair_fst_snd {M N : Type 1} [IsModule M] [IsModule N] (m : Prod M N) : pair (fst m) (snd m) = m

noncomputable def GaudisCrypt.Module.proc {sig : ProcedureSignature} (p : Procedure sig) : Proc sig

Equations

• GaudisCrypt.Module.proc p = (GaudisCrypt.ModuleExpression.proc p).toModule ⋯

theorem GaudisCrypt.proc_type_is_proc {sig : ProcedureSignature} {m : ModuleExpression} (ht : m.HasType [] (ModuleTypeRep.proc sig)) (h : m.NormalClosed) : ∃ (p : Procedure sig), m = ModuleExpression.proc p

Canonical forms at procedure type: a closed normal expression of type .proc sig is literally a .proc p node.

noncomputable def GaudisCrypt.Module.Proc.procedure {sig : ProcedureSignature} (m : Proc sig) : Procedure sig

The procedure of a proc-typed module — the inverse of Module.proc. (Classical.choose only escapes the Prop-to-data restriction; the witness is unique — see Module.procedure_spec and Module.procedure_proc/Module.procedure_proc'.)

Equations

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

theorem GaudisCrypt.Module.procedure_spec {sig : ProcedureSignature} (m : Proc sig) : m.expression = ModuleExpression.proc m.procedure

Module.procedure is characterized by its defining equation (the witness of proc_type_is_proc is unique by constructor injectivity).

@[simp]

theorem GaudisCrypt.Module.procedure_proc {sig : ProcedureSignature} (p : Procedure sig) : Proc.procedure ((ModuleExpression.proc p).toModule ⋯) = p

Round-trip: wrapping a procedure as a module and extracting recovers it.

@[simp]

theorem GaudisCrypt.Module.procedure_proc' {sig : ProcedureSignature} (p : Procedure sig) : (proc p).procedure = p

Module.procedure_proc with Module.proc folded — the form the generated apply_simp lemmas actually produce. The unfolded statement above is filed under a discrimination key mentioning ModuleExpression.toModule, so it never fires against a Module.proc on its own and every caller had to unfold Module.proc alongside it. Both are @[simp], so whichever form a goal is in, one of them matches.

theorem GaudisCrypt.Module.typed_weaken {T : ModuleTypeRep} (m : Module T) (Δ : ModuleContext) : m.expression.HasType Δ T

A module's expression is well-typed in any context, not just the empty one — it is closed. This is what lets moduletyping type an expression built from already-formed modules (whose leaves are m.expression rather than a HasType constructor).

noncomputable def GaudisCrypt.Module.const {T U : Type 1} [IsModule T] [iu : IsModule U] (m : U) : Arr T U

Equations

• GaudisCrypt.Module.const m = (⋯ ▸ m).expression.abs.toModule ⋯

noncomputable def GaudisCrypt.Module.procWithHoles {holes : HoleSigs} {sig : ProcedureSignature} (p : ProcedureWithHoles holes sig) : Arr (Module holes.toModuleTypeRepTuple) (Proc sig)

Equations

• GaudisCrypt.Module.procWithHoles p_2 = GaudisCrypt.Module.const (GaudisCrypt.Module.proc p_2)
• GaudisCrypt.Module.procWithHoles p_2 = (GaudisCrypt.ModuleExpression.procHoles True.intro p_2).toModule ⋯

Applying a procedure-with-holes to its callees

The δ-rule ReductionStep.delta fires only on a literal tuple of .proc nodes (HoleSigs.Instantiation.toModuleExpr). What one has in practice is a tuple of arbitrary module expressions — the callees, as they were written — which merely reduce to such a tuple, each of them to the .proc of a Module.procedure. reduce_pair_of bridges the two, peeling the tuple component by component, and reduce_app_procWithHoles then takes the δ-step. Together they are what procApply (GaudisCrypt/Language/Syntax2.lean) runs on the X.<f>.apply_simp goals the module command emits.

@[simp]

theorem GaudisCrypt.HoleSigs.Instantiation.toModuleExpr_nil : toModuleExpr PUnit.unit = ModuleExpression.unit

@[simp]

theorem GaudisCrypt.HoleSigs.Instantiation.toModuleExpr_single {sig : ProcedureSignature} (p : Procedure sig) : toModuleExpr p = (ModuleExpression.proc p).pair ModuleExpression.unit

@[simp]

theorem GaudisCrypt.HoleSigs.Instantiation.toModuleExpr_cons {holes : HoleSigs} {sig sig' : ProcedureSignature} (inst : (cons sig' holes).Instantiation) (p : Procedure sig) : toModuleExpr (p, inst) = (ModuleExpression.proc p).pair inst.toModuleExpr

theorem GaudisCrypt.HoleSigs.Instantiation.toModuleExpr_normal {holes : HoleSigs} (inst : holes.Instantiation) : inst.toModuleExpr.Normal

A tuple of procedures is normal: it is built from .proc nodes and .unit alone.

theorem GaudisCrypt.Module.reduce_pair_of {c rest e₁ e₂ : ModuleExpression} (h₁ : e₁.Normal) (h₂ : e₂.Normal) (hc : c.reduce = e₁) (hrest : rest.reduce = e₂) : (c.pair rest).reduce = e₁.pair e₂

Peeling one component of the callee tuple, at the level of ModuleExpression alone.

Stating this at the level of expressions, rather than with the instantiation still folded up, is what makes it usable: in procApply the goal carries a written-out instantiation, so HoleSigs.Instantiation.toModuleExpr computes and the right-hand side is an ordinary expression pair. A lemma phrased in terms of Instantiation could not be applied there at all — Instantiation (.cons sig holes) does not reduce while holes is a metavariable, and the elaborator will not solve holes from a sibling argument first.

hc is discharged by moduleCallee, hrest by the next round of this same lemma.

theorem GaudisCrypt.Module.reduce_app_procWithHoles {holes : HoleSigs} {sig : ProcedureSignature} (p : ProcedureWithHoles holes sig) (T : ModuleExpression) (inst : holes.Instantiation) (h : T.reduce = inst.toModuleExpr) : ((procWithHoles p).expression.app T).reduce = ModuleExpression.proc (p.instantiate inst)

The δ-step, on an argument that only reduces to a tuple of procedures: applying Module.procWithHoles p to it is the procedure p with its holes instantiated. With no holes at all Module.procWithHoles p is the constant function Module.proc p, and instantiating changes nothing (ProcedureWithHoles.instantiate_empty) — so the statement covers that case too.