inductive GaudisCrypt.TypedModules.ModuleTypeRep : Type 1

Possible types of modules

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

inductive GaudisCrypt.TypedModules.ModuleContext : Type 1

Module context typing: Types of a given module contexts; just a list of module types

• empty : ModuleContext
• append : ModuleContext → ModuleTypeRep → ModuleContext

inductive GaudisCrypt.TypedModules.ModuleContextIdx : ModuleContext → ModuleTypeRep → Type 1

Pointer into a module context; type safe for a given module context typing

• zero {a : ModuleTypeRep} {Γ : ModuleContext} : ModuleContextIdx (Γ.append a) a
• succ {Γ : ModuleContext} {a b : ModuleTypeRep} : ModuleContextIdx Γ a → ModuleContextIdx (Γ.append b) a

def GaudisCrypt.TypedModules.ModuleContextIdx.toNat {Γ : ModuleContext} {T : ModuleTypeRep} : ModuleContextIdx Γ T → ℕ

Equations

• GaudisCrypt.TypedModules.ModuleContextIdx.zero.toNat = 0
• n.succ.toNat = n.toNat.succ

def GaudisCrypt.TypedModules.HoleSigs.toModuleTypeRepTuple : HoleSigs → ModuleTypeRep

Note: lives in GaudisCrypt.TypedModules, not in GaudisCrypt.HoleSigs, so that it does not clash with GaudisCrypt.HoleSigs.toModuleTypeRepTuple from Language/ModuleExpressions.lean (same name, different ModuleTypeRep). Dot notation on a HoleSigs therefore does not find it; write HoleSigs.toModuleTypeRepTuple holes.

Equations

• One or more equations did not get rendered due to their size.
• GaudisCrypt.TypedModules.HoleSigs.toModuleTypeRepTuple GaudisCrypt.HoleSigs.empty = GaudisCrypt.TypedModules.ModuleTypeRep.unit

theorem GaudisCrypt.TypedModules.ModuleContextIdx.toNat_inj' {Γ : ModuleContext} {T1 T2 : ModuleTypeRep} (r1 : ModuleContextIdx Γ T1) (r2 : ModuleContextIdx Γ T2) : r1.toNat = r2.toNat → T1 = T2 ∧ r1 ≍ r2

inductive GaudisCrypt.TypedModules.ModuleExpression : ModuleContext → ModuleTypeRep → Type 1

ModuleExpression Γ T is the type of all module expressions that are well-typed in module contexts of type Γ and have type T.

• proc {Δ : ModuleContext} {sig : ProcedureSignature} : Procedure sig → ModuleExpression Δ (ModuleTypeRep.proc sig)
• procHoles {Δ : ModuleContext} {holes : HoleSigs} {sig : ProcedureSignature} : holes.NonEmpty → ProcedureWithHoles holes sig → ModuleExpression Δ ((HoleSigs.toModuleTypeRepTuple holes).arr (ModuleTypeRep.proc sig))
• var {Δ : ModuleContext} {M : ModuleTypeRep} : ModuleContextIdx Δ M → ModuleExpression Δ M
• app {Δ : ModuleContext} {A B : ModuleTypeRep} : ModuleExpression Δ (A.arr B) → ModuleExpression Δ A → ModuleExpression Δ B
• fst {Δ : ModuleContext} {A B : ModuleTypeRep} : ModuleExpression Δ (A.prod B) → ModuleExpression Δ A
• snd {Δ : ModuleContext} {A B : ModuleTypeRep} : ModuleExpression Δ (A.prod B) → ModuleExpression Δ B
• abs {B : ModuleTypeRep} {Δ : ModuleContext} {A : ModuleTypeRep} : ModuleExpression (Δ.append A) B → ModuleExpression Δ (A.arr B)
• pair {Δ : ModuleContext} {A B : ModuleTypeRep} : ModuleExpression Δ A → ModuleExpression Δ B → ModuleExpression Δ (A.prod B)
• unit {Δ : ModuleContext} : ModuleExpression Δ ModuleTypeRep.unit

def GaudisCrypt.TypedModules.IsPair {Δ : ModuleContext} {T U : ModuleTypeRep} (m : ModuleExpression Δ (T.prod U)) : Prop

Equations

• GaudisCrypt.TypedModules.IsPair (a.pair a_1) = (true = true)
• GaudisCrypt.TypedModules.IsPair m = (false = true)

@[implicit_reducible]

instance GaudisCrypt.TypedModules.instDecidableIsPair {Δ : ModuleContext} {T U : ModuleTypeRep} (m : ModuleExpression Δ (T.prod U)) : Decidable (IsPair m)

Equations

• GaudisCrypt.TypedModules.instDecidableIsPair (a.pair a_1) = isTrue ⋯
• GaudisCrypt.TypedModules.instDecidableIsPair (GaudisCrypt.TypedModules.ModuleExpression.var a) = isFalse Bool.false_ne_true
• GaudisCrypt.TypedModules.instDecidableIsPair (a.app a_1) = isFalse Bool.false_ne_true
• GaudisCrypt.TypedModules.instDecidableIsPair a.fst = isFalse Bool.false_ne_true
• GaudisCrypt.TypedModules.instDecidableIsPair a.snd = isFalse Bool.false_ne_true

def GaudisCrypt.TypedModules.IsPair.split {Δ : ModuleContext} {T U : ModuleTypeRep} {m : ModuleExpression Δ (T.prod U)} : IsPair m → ModuleExpression Δ T × ModuleExpression Δ U

Equations

• x_1.split = (m1, m2)
• x_1.split = ⋯.elim
• x_1.split = ⋯.elim
• x_1.split = ⋯.elim
• x_1.split = ⋯.elim

def GaudisCrypt.TypedModules.IsPair.fst {Δ : ModuleContext} {T U : ModuleTypeRep} {m : ModuleExpression Δ (T.prod U)} (h : IsPair m) : ModuleExpression Δ T

Equations

• h.fst = h.split.1

def GaudisCrypt.TypedModules.IsPair.snd {Δ : ModuleContext} {T U : ModuleTypeRep} {m : ModuleExpression Δ (T.prod U)} (h : IsPair m) : ModuleExpression Δ U

Equations

• h.snd = h.split.2

def GaudisCrypt.TypedModules.IsAbs {Δ : ModuleContext} {T : ModuleTypeRep} (m : ModuleExpression Δ T) : Prop

Equations

• GaudisCrypt.TypedModules.IsAbs a.abs = (true = true)
• GaudisCrypt.TypedModules.IsAbs m = (false = true)

@[implicit_reducible]

instance GaudisCrypt.TypedModules.instDecidableIsAbs {a✝ : ModuleContext} {a✝¹ : ModuleTypeRep} {m : ModuleExpression a✝ a✝¹} : Decidable (IsAbs m)

Equations

• GaudisCrypt.TypedModules.instDecidableIsAbs = isTrue ⋯
• GaudisCrypt.TypedModules.instDecidableIsAbs = isFalse Bool.false_ne_true
• GaudisCrypt.TypedModules.instDecidableIsAbs = isFalse Bool.false_ne_true
• GaudisCrypt.TypedModules.instDecidableIsAbs = isFalse Bool.false_ne_true
• GaudisCrypt.TypedModules.instDecidableIsAbs = isFalse Bool.false_ne_true
• GaudisCrypt.TypedModules.instDecidableIsAbs = isFalse Bool.false_ne_true
• GaudisCrypt.TypedModules.instDecidableIsAbs = isFalse Bool.false_ne_true
• GaudisCrypt.TypedModules.instDecidableIsAbs = isFalse Bool.false_ne_true
• GaudisCrypt.TypedModules.instDecidableIsAbs = isFalse Bool.false_ne_true

def GaudisCrypt.TypedModules.IsAbs.body {Δ : ModuleContext} {T U : ModuleTypeRep} {m : ModuleExpression Δ (T.arr U)} : IsAbs m → ModuleExpression (Δ.append T) U

Equations

• x_1.body = body
• x_1.body = ⋯.elim
• x_1.body = ⋯.elim
• x_1.body = ⋯.elim
• x_1.body = ⋯.elim

def GaudisCrypt.TypedModules.IsProcHoles {Δ : ModuleContext} {T : ModuleTypeRep} : ModuleExpression Δ T → Prop

Equations

• GaudisCrypt.TypedModules.IsProcHoles (GaudisCrypt.TypedModules.ModuleExpression.procHoles a a_1) = True
• GaudisCrypt.TypedModules.IsProcHoles x✝ = False

@[implicit_reducible]

instance GaudisCrypt.TypedModules.instDecidableIsProcHoles {a✝ : ModuleContext} {a✝¹ : ModuleTypeRep} {m : ModuleExpression a✝ a✝¹} : Decidable (IsProcHoles m)

Equations

• GaudisCrypt.TypedModules.instDecidableIsProcHoles = isTrue trivial
• GaudisCrypt.TypedModules.instDecidableIsProcHoles = isFalse not_false
• GaudisCrypt.TypedModules.instDecidableIsProcHoles = isFalse not_false
• GaudisCrypt.TypedModules.instDecidableIsProcHoles = isFalse not_false
• GaudisCrypt.TypedModules.instDecidableIsProcHoles = isFalse not_false
• GaudisCrypt.TypedModules.instDecidableIsProcHoles = isFalse not_false
• GaudisCrypt.TypedModules.instDecidableIsProcHoles = isFalse not_false
• GaudisCrypt.TypedModules.instDecidableIsProcHoles = isFalse not_false
• GaudisCrypt.TypedModules.instDecidableIsProcHoles = isFalse not_false

def GaudisCrypt.TypedModules.IsProcTuple {Δ : ModuleContext} {T : ModuleTypeRep} : ModuleExpression Δ T → Prop

IsProcTuple m holds when m is a right-nested tuple of hole-free procedures: either .proc _, or .pair (.proc _) rest with IsProcTuple rest. These are exactly the ground arguments a procedure-with-holes can be instantiated with (the module-level analogue of STLC BasicTerms).

Equations

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

@[implicit_reducible]

instance GaudisCrypt.TypedModules.instDecidableIsProcTuple {Δ : ModuleContext} {T : ModuleTypeRep} (m : ModuleExpression Δ T) : Decidable (IsProcTuple m)

Equations

• One or more equations did not get rendered due to their size.
• GaudisCrypt.TypedModules.instDecidableIsProcTuple GaudisCrypt.TypedModules.ModuleExpression.unit = isTrue trivial
• GaudisCrypt.TypedModules.instDecidableIsProcTuple (GaudisCrypt.TypedModules.ModuleExpression.unit.pair rest) = isFalse GaudisCrypt.TypedModules.instDecidableIsProcTuple._proof_1
• GaudisCrypt.TypedModules.instDecidableIsProcTuple ((GaudisCrypt.TypedModules.ModuleExpression.var a_2).pair rest) = isFalse ⋯
• GaudisCrypt.TypedModules.instDecidableIsProcTuple ((a_2.app a_3).pair rest) = isFalse ⋯
• GaudisCrypt.TypedModules.instDecidableIsProcTuple (a_2.fst.pair rest) = isFalse ⋯
• GaudisCrypt.TypedModules.instDecidableIsProcTuple (a_2.snd.pair rest) = isFalse ⋯
• GaudisCrypt.TypedModules.instDecidableIsProcTuple (a_2.abs.pair rest) = isFalse GaudisCrypt.TypedModules.instDecidableIsProcTuple._proof_1
• GaudisCrypt.TypedModules.instDecidableIsProcTuple ((a_2.pair a_3).pair rest) = isFalse GaudisCrypt.TypedModules.instDecidableIsProcTuple._proof_1
• GaudisCrypt.TypedModules.instDecidableIsProcTuple ((GaudisCrypt.TypedModules.ModuleExpression.procHoles a_2 a_3).pair rest) = isFalse GaudisCrypt.TypedModules.instDecidableIsProcTuple._proof_1
• GaudisCrypt.TypedModules.instDecidableIsProcTuple (GaudisCrypt.TypedModules.ModuleExpression.proc a) = isFalse not_false
• GaudisCrypt.TypedModules.instDecidableIsProcTuple (GaudisCrypt.TypedModules.ModuleExpression.var a) = isFalse not_false
• GaudisCrypt.TypedModules.instDecidableIsProcTuple (a.app a_1) = isFalse not_false
• GaudisCrypt.TypedModules.instDecidableIsProcTuple a.fst = isFalse not_false
• GaudisCrypt.TypedModules.instDecidableIsProcTuple a.snd = isFalse not_false
• GaudisCrypt.TypedModules.instDecidableIsProcTuple a.abs = isFalse not_false
• GaudisCrypt.TypedModules.instDecidableIsProcTuple (GaudisCrypt.TypedModules.ModuleExpression.procHoles a a_1) = isFalse not_false

def GaudisCrypt.TypedModules.IsProcArgType : ModuleTypeRep → Prop

A type that can be the argument type of a procedure-with-holes: a right-nested tuple of procedure types.

Equations

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

theorem GaudisCrypt.TypedModules.IsProcHoles.isProcArgType {Δ : ModuleContext} {A B : ModuleTypeRep} {f : ModuleExpression Δ (A.arr B)} (h : IsProcHoles f) : IsProcArgType A

def GaudisCrypt.TypedModules.IsProcHoles.destruct {Γ : ModuleContext} {T : ModuleTypeRep} {m : ModuleExpression Γ T} (h : IsProcHoles m) : (holes : HoleSigs) × (sig : ProcedureSignature) × { proc : ProcedureWithHoles holes sig // T = (HoleSigs.toModuleTypeRepTuple holes).arr (ModuleTypeRep.proc sig) }

Equations

• h_2.destruct = ⟨holes, ⟨sigs, ⟨p, ⋯⟩⟩⟩

inductive GaudisCrypt.TypedModules.Normal {Δ : ModuleContext} {T : ModuleTypeRep} : ModuleExpression Δ T → Prop

Beta-normal form: no beta-redex anywhere in the term.

• neutral {Δ : ModuleContext} {T : ModuleTypeRep} {e : ModuleExpression Δ T} : Neutral e → Normal e
• abs {Δ : ModuleContext} {A B : ModuleTypeRep} {body : ModuleExpression (Δ.append A) B} : Normal body → Normal body.abs
• pair {Δ : ModuleContext} {A B : ModuleTypeRep} {a : ModuleExpression Δ A} {b : ModuleExpression Δ B} : Normal a → Normal b → Normal (a.pair b)
• proc {Δ : ModuleContext} {x✝ : ProcedureSignature} {p : Procedure x✝} : Normal (ModuleExpression.proc p)
• procHoles {Δ : ModuleContext} {holes : HoleSigs} {sig : ProcedureSignature} {ne : holes.NonEmpty} {p : ProcedureWithHoles holes sig} : Normal (ModuleExpression.procHoles ne p)
• unit {Δ : ModuleContext} : Normal ModuleExpression.unit

inductive GaudisCrypt.TypedModules.Neutral {Δ : ModuleContext} {T : ModuleTypeRep} : ModuleExpression Δ T → Prop

Neutral form: no outermost redex. Either the head is a variable, or it is a procedure-with-holes applied to a normal argument that is not a proc-tuple (so the δ-rule cannot fire) — both are stuck. Neutral f in app rules out app (abs ..) ... Neutral e in fst/snd rules out fst (pair ..) / snd (pair ..).

• var {Δ : ModuleContext} {T : ModuleTypeRep} {r : ModuleContextIdx Δ T} : Neutral (ModuleExpression.var r)
• app {Δ : ModuleContext} {A B : ModuleTypeRep} {f : ModuleExpression Δ (A.arr B)} {arg : ModuleExpression Δ A} : Neutral f → Normal arg → Neutral (f.app arg)
• appProcHoles {Δ : ModuleContext} {A B : ModuleTypeRep} {f : ModuleExpression Δ (A.arr B)} {arg : ModuleExpression Δ A} : IsProcHoles f → Normal arg → ¬IsProcTuple arg → Neutral (f.app arg)
• fst {Δ : ModuleContext} {T x✝ : ModuleTypeRep} {e : ModuleExpression Δ (T.prod x✝)} : Neutral e → Neutral e.fst
• snd {Δ : ModuleContext} {T x✝ : ModuleTypeRep} {e : ModuleExpression Δ (x✝.prod T)} : Neutral e → Neutral e.snd

@[implicit_reducible]

instance GaudisCrypt.TypedModules.instDecidableNormal {Γ : ModuleContext} {A : ModuleTypeRep} (m : ModuleExpression Γ A) : Decidable (Normal m)

Equations

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

@[implicit_reducible]

instance GaudisCrypt.TypedModules.instDecidableNeutral {Γ : ModuleContext} {A : ModuleTypeRep} (m : ModuleExpression Γ A) : Decidable (Neutral m)

Equations

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

inductive GaudisCrypt.TypedModules.NormalClosed {T : ModuleTypeRep} : ModuleExpression ModuleContext.empty T → Prop

Beta-normal form for closed terms (empty context). Neutral terms cannot occur (they would require a variable in the empty context), so this has fewer cases than Normal. The abs body is in a one-variable context and therefore still uses the general Normal.

• proc {x✝ : ProcedureSignature} {p : Procedure x✝} : NormalClosed (ModuleExpression.proc p)
• procHoles {x✝ : HoleSigs} {n : x✝.NonEmpty} {x✝¹ : ProcedureSignature} {p : ProcedureWithHoles x✝ x✝¹} : NormalClosed (ModuleExpression.procHoles n p)
• abs {A B : ModuleTypeRep} {body : ModuleExpression (ModuleContext.empty.append A) B} : Normal body → NormalClosed body.abs
• pair {A B : ModuleTypeRep} {a : ModuleExpression ModuleContext.empty A} {b : ModuleExpression ModuleContext.empty B} : NormalClosed a → NormalClosed b → NormalClosed (a.pair b)
• unit : NormalClosed ModuleExpression.unit

theorem GaudisCrypt.TypedModules.empty_context_not_neutral {T : ModuleTypeRep} {m : ModuleExpression ModuleContext.empty T} : ¬Neutral m

theorem GaudisCrypt.TypedModules.Normal.normalClosed {T : ModuleTypeRep} {m : ModuleExpression ModuleContext.empty T} : Normal m → NormalClosed m

theorem GaudisCrypt.TypedModules.NormalClosed.normal {T : ModuleTypeRep} {m : ModuleExpression ModuleContext.empty T} : NormalClosed m → Normal m

def GaudisCrypt.TypedModules.liftRenaming {Δ Γ : ModuleContext} {A : ModuleTypeRep} (ρ : {T : ModuleTypeRep} → ModuleContextIdx Δ T → ModuleContextIdx Γ T) {T : ModuleTypeRep} : ModuleContextIdx (Δ.append A) T → ModuleContextIdx (Γ.append A) T

Extends a renaming ρ : ModuleContextIdx Δ → ModuleContextIdx Γ to work under one binder of type A. The bound variable .zero maps to itself; outer variables .succ r are renamed by ρ and re-wrapped with .succ. This is the typed analogue of incrementing the cutoff c in Pierce's shift operation.

Equations

• GaudisCrypt.TypedModules.liftRenaming ρ GaudisCrypt.TypedModules.ModuleContextIdx.zero = GaudisCrypt.TypedModules.ModuleContextIdx.zero
• GaudisCrypt.TypedModules.liftRenaming ρ r.succ = (ρ r).succ

def GaudisCrypt.TypedModules.ModuleExpression.rename {Δ Γ : ModuleContext} {T : ModuleTypeRep} (ρ : {T : ModuleTypeRep} → ModuleContextIdx Δ T → ModuleContextIdx Γ T) : ModuleExpression Δ T → ModuleExpression Γ T

Applies a renaming ρ : ModuleContextIdx Δ → ModuleContextIdx Γ to every variable in a term, producing a term over context Γ. Goes under binders by lifting ρ with liftRename. This is the typed analogue of Pierce's shift ↑_c^d, where ρ encodes both the cutoff c and the displacement d.

Equations

• One or more equations did not get rendered due to their size.
• GaudisCrypt.TypedModules.ModuleExpression.rename ρ GaudisCrypt.TypedModules.ModuleExpression.unit = GaudisCrypt.TypedModules.ModuleExpression.unit
• GaudisCrypt.TypedModules.ModuleExpression.rename ρ (GaudisCrypt.TypedModules.ModuleExpression.proc p) = GaudisCrypt.TypedModules.ModuleExpression.proc p
• GaudisCrypt.TypedModules.ModuleExpression.rename ρ (GaudisCrypt.TypedModules.ModuleExpression.procHoles ne p) = GaudisCrypt.TypedModules.ModuleExpression.procHoles ne p
• GaudisCrypt.TypedModules.ModuleExpression.rename ρ (GaudisCrypt.TypedModules.ModuleExpression.var r) = GaudisCrypt.TypedModules.ModuleExpression.var (ρ r)
• GaudisCrypt.TypedModules.ModuleExpression.rename ρ e.fst = (GaudisCrypt.TypedModules.ModuleExpression.rename (fun {T : GaudisCrypt.TypedModules.ModuleTypeRep} => ρ) e).fst
• GaudisCrypt.TypedModules.ModuleExpression.rename ρ e.snd = (GaudisCrypt.TypedModules.ModuleExpression.rename (fun {T : GaudisCrypt.TypedModules.ModuleTypeRep} => ρ) e).snd

def GaudisCrypt.TypedModules.liftSubstitution {Δ Γ : ModuleContext} {A : ModuleTypeRep} (σ : {T : ModuleTypeRep} → ModuleContextIdx Δ T → ModuleExpression Γ T) {T : ModuleTypeRep} : ModuleContextIdx (Δ.append A) T → ModuleExpression (Γ.append A) T

Extends a simultaneous substitution σ : ModuleContextIdx Δ → ModuleExpression Γ to work under one binder of type A, yielding a substitution ModuleContextIdx (Δ,A) → ModuleExpression (Γ,A). The bound variable .zero maps to the fresh variable .var .zero; outer variables .succ r are substituted by σ r and then weakened into the extended context Γ,A by renaming with .succ.

Equations

• One or more equations did not get rendered due to their size.
• GaudisCrypt.TypedModules.liftSubstitution σ GaudisCrypt.TypedModules.ModuleContextIdx.zero = GaudisCrypt.TypedModules.ModuleExpression.var GaudisCrypt.TypedModules.ModuleContextIdx.zero

def GaudisCrypt.TypedModules.substituteSimultaneously {Δ Γ : ModuleContext} {T : ModuleTypeRep} (σ : {T : ModuleTypeRep} → ModuleContextIdx Δ T → ModuleExpression Γ T) : ModuleExpression Δ T → ModuleExpression Γ T

Applies a simultaneous substitution σ : ModuleContextIdx Δ → ModuleExpression Γ to every variable in a term, producing a term over context Γ. Goes under binders by lifting σ with liftSubst.

Equations

• One or more equations did not get rendered due to their size.
• GaudisCrypt.TypedModules.substituteSimultaneously σ GaudisCrypt.TypedModules.ModuleExpression.unit = GaudisCrypt.TypedModules.ModuleExpression.unit
• GaudisCrypt.TypedModules.substituteSimultaneously σ (GaudisCrypt.TypedModules.ModuleExpression.proc p) = GaudisCrypt.TypedModules.ModuleExpression.proc p
• GaudisCrypt.TypedModules.substituteSimultaneously σ (GaudisCrypt.TypedModules.ModuleExpression.procHoles ne p) = GaudisCrypt.TypedModules.ModuleExpression.procHoles ne p
• GaudisCrypt.TypedModules.substituteSimultaneously σ (GaudisCrypt.TypedModules.ModuleExpression.var r) = σ r
• GaudisCrypt.TypedModules.substituteSimultaneously σ e.fst = (GaudisCrypt.TypedModules.substituteSimultaneously (fun {T : GaudisCrypt.TypedModules.ModuleTypeRep} => σ) e).fst
• GaudisCrypt.TypedModules.substituteSimultaneously σ e.snd = (GaudisCrypt.TypedModules.substituteSimultaneously (fun {T : GaudisCrypt.TypedModules.ModuleTypeRep} => σ) e).snd

def GaudisCrypt.TypedModules.variableSubstitution {Δ : ModuleContext} {u : ModuleTypeRep} (arg : ModuleExpression Δ u) {T : ModuleTypeRep} : ModuleContextIdx (Δ.append u) T → ModuleExpression Δ T

The single-variable substitution map used as the σ argument to substSimultaneous: de Bruijn index 0 (the outermost bound variable) maps to arg; any other index k+1 maps back to the variable at index k.

Equations

• GaudisCrypt.TypedModules.variableSubstitution arg GaudisCrypt.TypedModules.ModuleContextIdx.zero = arg
• GaudisCrypt.TypedModules.variableSubstitution arg r.succ = GaudisCrypt.TypedModules.ModuleExpression.var r

def GaudisCrypt.TypedModules.substitute {t : ModuleTypeRep} {Δ : ModuleContext} {u : ModuleTypeRep} (body : ModuleExpression (Δ.append u) t) (arg : ModuleExpression Δ u) : ModuleExpression Δ t

Single-variable de Bruijn substitution: replaces de Bruijn index 0 in body with arg. Implemented via substSimultaneous with the point substitution substVar arg.

Equations

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

def GaudisCrypt.TypedModules.HoleSigs.Instantiation.toModuleTuple {Δ : ModuleContext} {holes : HoleSigs} : holes.Instantiation → ModuleExpression Δ (toModuleTypeRepTuple holes)

Convert a HoleSigs.Instantiation into the corresponding module-expression tuple.

Like HoleSigs.toModuleTypeRepTuple, this lives in GaudisCrypt.TypedModules rather than in GaudisCrypt.HoleSigs, so dot notation on an Instantiation does not find it.

Equations

• One or more equations did not get rendered due to their size.
• GaudisCrypt.TypedModules.HoleSigs.Instantiation.toModuleTuple x_2 = GaudisCrypt.TypedModules.ModuleExpression.unit
• GaudisCrypt.TypedModules.HoleSigs.Instantiation.toModuleTuple inst = (GaudisCrypt.TypedModules.ModuleExpression.proc inst).pair GaudisCrypt.TypedModules.ModuleExpression.unit

inductive GaudisCrypt.TypedModules.ReductionStep {Δ : ModuleContext} {T : ModuleTypeRep} : ModuleExpression Δ T → ModuleExpression Δ T → Prop

Non-deterministic single-step reduction: all possible one-step reductions.

• beta {Δ : ModuleContext} {A T : ModuleTypeRep} {body : ModuleExpression (Δ.append A) T} {arg : ModuleExpression Δ A} : ReductionStep (body.abs.app arg) (substitute body arg)
• appL {Δ : ModuleContext} {A T : ModuleTypeRep} {f f' : ModuleExpression Δ (A.arr T)} {arg : ModuleExpression Δ A} : ReductionStep f f' → ReductionStep (f.app arg) (f'.app arg)
• appR {Δ : ModuleContext} {A T : ModuleTypeRep} {f : ModuleExpression Δ (A.arr T)} {arg arg' : ModuleExpression Δ A} : ReductionStep arg arg' → ReductionStep (f.app arg) (f.app arg')
• lam {Δ : ModuleContext} {A B : ModuleTypeRep} {body body' : ModuleExpression (Δ.append A) B} : ReductionStep body body' → ReductionStep body.abs body'.abs
• pairL {Δ : ModuleContext} {A B : ModuleTypeRep} {a a' : ModuleExpression Δ A} {b : ModuleExpression Δ B} : ReductionStep a a' → ReductionStep (a.pair b) (a'.pair b)
• pairR {Δ : ModuleContext} {A B : ModuleTypeRep} {a : ModuleExpression Δ A} {b b' : ModuleExpression Δ B} : ReductionStep b b' → ReductionStep (a.pair b) (a.pair b')
• fstPair {Δ : ModuleContext} {A B : ModuleTypeRep} {a : ModuleExpression Δ A} {b : ModuleExpression Δ B} : ReductionStep (a.pair b).fst a
• fst {Δ : ModuleContext} {A T : ModuleTypeRep} {e e' : ModuleExpression Δ (A.prod T)} : ReductionStep e e' → ReductionStep e.fst e'.fst
• sndPair {Δ : ModuleContext} {A B : ModuleTypeRep} {a : ModuleExpression Δ A} {b : ModuleExpression Δ B} : ReductionStep (a.pair b).snd b
• snd {Δ : ModuleContext} {A T : ModuleTypeRep} {e e' : ModuleExpression Δ (A.prod T)} : ReductionStep e e' → ReductionStep e.snd e'.snd
• delta {Δ : ModuleContext} {holes : HoleSigs} {sigs : ProcedureSignature} {ne : holes.NonEmpty} {proc : ProcedureWithHoles holes sigs} (instantiation : holes.Instantiation) : ReductionStep ((ModuleExpression.procHoles ne proc).app (HoleSigs.Instantiation.toModuleTuple instantiation)) (ModuleExpression.proc (proc.instantiate instantiation))

  δ-reduction: a procedure-with-holes applied to a ground proc-tuple argument is instantiated, producing the closed procedure substituteProcedure proc args.

def GaudisCrypt.TypedModules.MultiStepReduction {Γ : ModuleContext} {T : ModuleTypeRep} : ModuleExpression Γ T → ModuleExpression Γ T → Prop

Equations

• GaudisCrypt.TypedModules.MultiStepReduction = Rewriting.Star GaudisCrypt.TypedModules.ReductionStep

theorem GaudisCrypt.TypedModules.multiStepReduction_app {Γ : ModuleContext} {T U : ModuleTypeRep} {m1 m1' : ModuleExpression Γ (T.arr U)} {m2 m2' : ModuleExpression Γ T} (h1 : MultiStepReduction m1 m1') (h2 : MultiStepReduction m2 m2') : MultiStepReduction (m1.app m2) (m1'.app m2')

theorem GaudisCrypt.TypedModules.multiStepReduction_fst {Γ : ModuleContext} {A B : ModuleTypeRep} {e e' : ModuleExpression Γ (A.prod B)} (h : MultiStepReduction e e') : MultiStepReduction e.fst e'.fst

theorem GaudisCrypt.TypedModules.multiStepReduction_pair {Γ : ModuleContext} {A B : ModuleTypeRep} {a a' : ModuleExpression Γ A} {b b' : ModuleExpression Γ B} (h1 : MultiStepReduction a a') (h2 : MultiStepReduction b b') : MultiStepReduction (a.pair b) (a'.pair b')

def GaudisCrypt.TypedModules.procTupleLookup {Δ : ModuleContext} {holes : HoleSigs} (m : ModuleExpression Δ (HoleSigs.toModuleTypeRepTuple holes)) : IsProcTuple m → holes.Instantiation

Inverse of HoleSigs.Instantiation.toModuleTuple: extract a Procedure for each hole index from a ModuleExpression that is a right-nested tuple of procedures (IsProcTuple).

Equations

• One or more equations did not get rendered due to their size.
• GaudisCrypt.TypedModules.procTupleLookup x_3 x_4 = PUnit.unit

theorem GaudisCrypt.TypedModules.procTupleLookup_toModuleTuple {Δ : ModuleContext} {holes : HoleSigs} (m : ModuleExpression Δ (HoleSigs.toModuleTypeRepTuple holes)) (h : IsProcTuple m) : HoleSigs.Instantiation.toModuleTuple (procTupleLookup m h) = m

Round-trip: converting a proc-tuple back to an instantiation and then to a tuple recovers the original expression.

def GaudisCrypt.TypedModules.cbvReductionStep {Δ : ModuleContext} {t : ModuleTypeRep} (m : ModuleExpression Δ t) (nn : ¬Normal m) : ModuleExpression Δ t

Equations

• One or more equations did not get rendered due to their size.
• GaudisCrypt.TypedModules.cbvReductionStep (GaudisCrypt.TypedModules.ModuleExpression.proc p) nn_2 = absurd ⋯ nn_2
• GaudisCrypt.TypedModules.cbvReductionStep (GaudisCrypt.TypedModules.ModuleExpression.procHoles a p) nn_2 = absurd ⋯ nn_2
• GaudisCrypt.TypedModules.cbvReductionStep body.abs nn_2 = (GaudisCrypt.TypedModules.cbvReductionStep body ⋯).abs
• GaudisCrypt.TypedModules.cbvReductionStep (GaudisCrypt.TypedModules.ModuleExpression.var n) nn_2 = absurd ⋯ nn_2
• GaudisCrypt.TypedModules.cbvReductionStep GaudisCrypt.TypedModules.ModuleExpression.unit nn_2 = absurd ⋯ nn_2

theorem GaudisCrypt.TypedModules.cbvReductionStep_is_reductionStep {Γ : ModuleContext} {T : ModuleTypeRep} (m : ModuleExpression Γ T) (nn : ¬Normal m) : ReductionStep m (cbvReductionStep m nn)

def GaudisCrypt.TypedModules.ModuleExpression.erasedEqual {Γ : ModuleContext} {T : ModuleTypeRep} {Γ' : ModuleContext} {T' : ModuleTypeRep} (m : ModuleExpression Γ T) (m' : ModuleExpression Γ' T') : Prop

Equations

• (GaudisCrypt.TypedModules.ModuleExpression.proc p).erasedEqual (GaudisCrypt.TypedModules.ModuleExpression.proc p') = (sig = sig' ∧ p ≍ p')
• (GaudisCrypt.TypedModules.ModuleExpression.procHoles a p).erasedEqual (GaudisCrypt.TypedModules.ModuleExpression.procHoles a_1 p') = (holes = holes' ∧ sig = sig' ∧ p ≍ p')
• (GaudisCrypt.TypedModules.ModuleExpression.var r).erasedEqual (GaudisCrypt.TypedModules.ModuleExpression.var r') = (r.toNat = r'.toNat)
• (f.app a).erasedEqual (f'.app a') = (f.erasedEqual f' ∧ a.erasedEqual a')
• e.fst.erasedEqual e'.fst = e.erasedEqual e'
• e.snd.erasedEqual e'.snd = e.erasedEqual e'
• (a.pair b).erasedEqual (a'.pair b') = (a.erasedEqual a' ∧ b.erasedEqual b')
• body.abs.erasedEqual body'.abs = body.erasedEqual body'
• GaudisCrypt.TypedModules.ModuleExpression.unit.erasedEqual GaudisCrypt.TypedModules.ModuleExpression.unit = True
• m.erasedEqual m' = False

theorem GaudisCrypt.TypedModules.ModuleExpression.erasedEqual_refl {Γ : ModuleContext} {T : ModuleTypeRep} (m : ModuleExpression Γ T) : m.erasedEqual m

theorem GaudisCrypt.TypedModules.ModuleExpression.erasedEqual_pair_right {Γ : ModuleContext} {T U U' : ModuleTypeRep} (a : ModuleExpression Γ T) {b : ModuleExpression Γ U} {b' : ModuleExpression Γ U'} (h : b.erasedEqual b') : (a.pair b).erasedEqual (a.pair b')

theorem GaudisCrypt.TypedModules.ModuleExpression.erasedEqual_pair_left {Γ : ModuleContext} {T T' U : ModuleTypeRep} {a : ModuleExpression Γ T} {a' : ModuleExpression Γ T'} (b : ModuleExpression Γ U) (h : a.erasedEqual a') : (a.pair b).erasedEqual (a'.pair b)

theorem GaudisCrypt.TypedModules.ModuleExpression.erasedEqual_normal_neutral_eq {Γ : ModuleContext} {T1 T2 : ModuleTypeRep} (m : ModuleExpression Γ T1) (m' : ModuleExpression Γ T2) (h : m.erasedEqual m') : (Normal m → T1 = T2 → m ≍ m') ∧ (Neutral m → T1 = T2 ∧ m ≍ m')

theorem GaudisCrypt.TypedModules.ModuleExpression.erasedEqual_normal_eq {Γ : ModuleContext} {T : ModuleTypeRep} {n1 n2 : ModuleExpression Γ T} (hn1 : Normal n1) (h : n1.erasedEqual n2) : n1 = n2

theorem GaudisCrypt.TypedModules.ModuleExpression.erasedEqual_neutral_eq {Γ : ModuleContext} {T1 T2 : ModuleTypeRep} {e1 : ModuleExpression Γ T1} {e2 : ModuleExpression Γ T2} (hne1 : Neutral e1) (h : e1.erasedEqual e2) : T1 = T2 ∧ e1 ≍ e2

theorem GaudisCrypt.TypedModules.toModuleTuple_isProcTuple {Δ : ModuleContext} {holes : HoleSigs} (inst : holes.Instantiation) : IsProcTuple (HoleSigs.Instantiation.toModuleTuple inst)

toModuleTuple inst always satisfies IsProcTuple.

@[irreducible]

def GaudisCrypt.TypedModules.reduce {Γ : ModuleContext} {T : ModuleTypeRep} (m : ModuleExpression Γ T) : ModuleExpression Γ T

Equations

• GaudisCrypt.TypedModules.reduce m = if h : GaudisCrypt.TypedModules.Normal m then m else GaudisCrypt.TypedModules.reduce (GaudisCrypt.TypedModules.cbvReductionStep m h)

theorem GaudisCrypt.TypedModules.multiStepReduction_reduce {Γ : ModuleContext} {T : ModuleTypeRep} {m : ModuleExpression Γ T} : MultiStepReduction m (reduce m)

theorem GaudisCrypt.TypedModules.reduce_normal {Δ : ModuleContext} {t : ModuleTypeRep} (m : ModuleExpression Δ t) : Normal (reduce m)

theorem GaudisCrypt.TypedModules.reduce_normalClosed {t : ModuleTypeRep} (m : ModuleExpression ModuleContext.empty t) : NormalClosed (reduce m)

@[simp]

theorem GaudisCrypt.TypedModules.reduce_fst_pair {Γ : ModuleContext} {T U : ModuleTypeRep} (m1 : ModuleExpression Γ T) (m2 : ModuleExpression Γ U) : reduce (m1.pair m2).fst = reduce m1

@[simp]

theorem GaudisCrypt.TypedModules.reduce_fst {Γ : ModuleContext} {T T' : ModuleTypeRep} (m : ModuleExpression Γ T) (m' : ModuleExpression Γ T') : reduce (m.pair m').fst = reduce m

@[simp]

theorem GaudisCrypt.TypedModules.reduce_snd {Γ : ModuleContext} {T T' : ModuleTypeRep} (m : ModuleExpression Γ T) (m' : ModuleExpression Γ T') : reduce (m.pair m').snd = reduce m'

@[simp]

theorem GaudisCrypt.TypedModules.reduce_idempotent {Γ : ModuleContext} {T : ModuleTypeRep} (m : ModuleExpression Γ T) : reduce (reduce m) = reduce m

@[simp]

theorem GaudisCrypt.TypedModules.reduce_beta {U : ModuleTypeRep} {Γ : ModuleContext} {T : ModuleTypeRep} (body : ModuleExpression (Γ.append T) U) (arg : ModuleExpression Γ T) : reduce (body.abs.app arg) = reduce (substitute body arg)

theorem GaudisCrypt.TypedModules.confluence {Γ : ModuleContext} {T : ModuleTypeRep} {m m1 m2 : ModuleExpression Γ T} (h1 : MultiStepReduction m m1) (h2 : MultiStepReduction m m2) : reduce m1 = reduce m2

theorem GaudisCrypt.TypedModules.reduce_app {Γ : ModuleContext} {T U : ModuleTypeRep} (m : ModuleExpression Γ (T.arr U)) (m' : ModuleExpression Γ T) : reduce (m.app m') = reduce ((reduce m).app (reduce m'))

theorem GaudisCrypt.TypedModules.reduce_fst_cong {Γ : ModuleContext} {T U : ModuleTypeRep} (m m' : ModuleExpression Γ (T.prod U)) : reduce m = reduce m' → reduce m.fst = reduce m'.fst

theorem GaudisCrypt.TypedModules.reduce_pair {Γ : ModuleContext} {T U : ModuleTypeRep} (m1 : ModuleExpression Γ T) (m2 : ModuleExpression Γ U) : reduce (m1.pair m2) = (reduce m1).pair (reduce m2)

theorem GaudisCrypt.TypedModules.pair_type_is_pair {t1 t2 : ModuleTypeRep} {m : ModuleExpression ModuleContext.empty (t1.prod t2)} : NormalClosed m → ∃ (m1 : ModuleExpression ModuleContext.empty t1) (m2 : ModuleExpression ModuleContext.empty t2), m = m1.pair m2

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

• expression : ModuleExpression ModuleContext.empty T
• normal : NormalClosed self.expression

def GaudisCrypt.TypedModules.ModuleExpression.toModule {T : ModuleTypeRep} (m : ModuleExpression ModuleContext.empty T) : Module T

Equations

• m.toModule = { expression := GaudisCrypt.TypedModules.reduce m, normal := ⋯ }

@[implicit_reducible]

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

Equations

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

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

Equations

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

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

Equations

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

def GaudisCrypt.TypedModules.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.TypedModules.Module.ext {T : ModuleTypeRep} {m1 m2 : Module T} (h : m1.expression = m2.expression) : m1 = m2

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

@[simp]

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

@[simp]

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

@[simp]

theorem GaudisCrypt.TypedModules.Module.toModule_expression {T : ModuleTypeRep} (m : ModuleExpression ModuleContext.empty T) : m.toModule.expression = reduce m

@[simp]

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

@[simp]

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

@[simp]

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

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

@[reducible, inline]

abbrev GaudisCrypt.TypedModules.Module.Unit : Type 1

Equations

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

def GaudisCrypt.TypedModules.Module.unit : Module ModuleTypeRep.unit

Equations

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

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

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

@[reducible]

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

@[implicit_reducible]

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

Equations

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

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

Equations

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

@[implicit_reducible]

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

Equations

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

def GaudisCrypt.TypedModules.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

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

Equations

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

theorem GaudisCrypt.TypedModules.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.TypedModules.Module.Prod (M N : Type 1) [IsModule M] [IsModule N] : Type 1

Equations

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

@[implicit_reducible]

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

@[simp]

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

@[simp]

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

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

axiom GaudisCrypt.TypedModules.sig : ProcedureSignature

def GaudisCrypt.TypedModules.TestModule : Type 1

Equations

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

noncomputable def GaudisCrypt.TypedModules.TestModule.main (m : TestModule) : Module (ModuleTypeRep.proc sig)

Equations

• m.main = GaudisCrypt.TypedModules.Module.fst' m

noncomputable def GaudisCrypt.TypedModules.TestModule.aux (m : TestModule) : Module (ModuleTypeRep.proc sig)

Equations

• m.aux = GaudisCrypt.TypedModules.Module.snd' m

structure GaudisCrypt.TypedModules.TestModuleStruct : Type 1

• main : Module (ModuleTypeRep.proc sig)
• aux : Module (ModuleTypeRep.proc sig)

noncomputable def GaudisCrypt.TypedModules.TestModuleStruct.destruct (str : TestModuleStruct) : TestModule

Equations

• str.destruct = str.main.pair' str.aux

noncomputable def GaudisCrypt.TypedModules.TestModule.mk (str : TestModuleStruct) : TestModule

Equations

• GaudisCrypt.TypedModules.TestModule.mk str = str.main.pair' str.aux

axiom GaudisCrypt.TypedModules.testMain : Module (ModuleTypeRep.proc sig)

axiom GaudisCrypt.TypedModules.testAux : Module (ModuleTypeRep.proc sig)

noncomputable def GaudisCrypt.TypedModules.myMod : TestModule

Equations

• GaudisCrypt.TypedModules.myMod = GaudisCrypt.TypedModules.TestModule.mk { main := GaudisCrypt.TypedModules.testMain, aux := GaudisCrypt.TypedModules.testAux }

theorem GaudisCrypt.TypedModules.test : myMod.main = testMain