Module expressions

Everything about ModuleExpression.reduce that rests on confluence (ModuleExpressionConfluence.lean) or on normalization (ModuleExpressionNormalization.lean): reduce is idempotent, agrees on convertible terms, computes a normal form of a well-typed term, and is a congruence for every constructor — plus the reduce_simp tactic built out of those lemmas.

ModuleExpressionBasics.lean holds the part of the development that needs neither: the syntax tree, typing, substitution, reduction, normal forms and the moduletyping/normalmodule tactics. This file is the one downstream modules import.

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

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

@[simp]

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

theorem GaudisCrypt.ModuleExpression.convertible_terminating {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.reduce_terminating {m : ModuleExpression} : m.Terminating ↔ m.reduce.Terminating

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

Reduction preserves typing.

theorem GaudisCrypt.ModuleExpression.reduce_normal {Δ : 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 {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 (m : ModuleExpression) : m.reduce.reduce = m.reduce

@[simp]

theorem GaudisCrypt.ModuleExpression.reduce_of_normal {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 {sig : ProcedureSignature} (p : Procedure sig) : (proc p).reduce = proc p

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

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

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

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

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

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

theorem GaudisCrypt.ModuleExpression.reduce_pair_terminating {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 (m m' : ModuleExpression) : (m.pair m').fst.reduce = m.reduce

@[simp]

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

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

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

theorem GaudisCrypt.ModuleExpression.reduce_pair_cong {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 {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 {a a' b : ModuleExpression} (ha : a.reduce = a') : (a.pair b).reduce = (a'.pair b).reduce

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

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

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

theorem GaudisCrypt.ModuleExpression.reduce_abs_cong {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 moduleApply 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 (f x : ModuleExpression) : (f.reduce.app x).reduce = (f.app x).reduce

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

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

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

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

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

Tactics

reduce_simp

partial def GaudisCrypt.reduceSimpHead : Lean.Elab.Tactic.TacticM Unit

reduceSimpHead takes a goal of the form reduce M = reduce ?m or reduce M = ?m and solves it by instantiating the rhs as reduce M' where M' is the result of applying a single reduction step.

Rules of the form reduce X = reduce Y or reduce X = Y or convertible X Y or MultiStepReduction X Y or Step X Y in the context are also used as reduction steps.

It fails when no step applies. In particular a term that is already normal is not its business: it never uses reduce_of_normal, so it neither succeeds without reducing nor leaves a reduce around a component it did not touch. Collapsing the reduce of a normal term is the second rule of reduceSimpProcImpl instead.

A plain TacticM function, not a syntax/macro_rules pair, so it adds nothing to the tactic grammar. The head-step alternatives stay a first | … quotation run via evalTactic; the congruence rules — the only recursive part — are tried in order by hand, each followed by a recursive call, with backtracking between them. Invoke it from a proof with run_tac.

def GaudisCrypt.reduceSimp : Lean.Elab.Tactic.TacticM Unit

Fully normalize reduce m subterms — one reduction step at a time via reduceSimpHead, 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 reduceSimpHead branch matches on: unfolding it is what turns that result back into a constructor tree the next step can work on.

The tactic keyword reduce_simp is this function; it stays a keyword because proofs are written with it by hand. Tactics that want it as a step call reduceSimp directly rather than going back through the grammar.

Equations

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

def GaudisCrypt.tacticReduce_simp : Lean.ParserDescr

Fully normalize reduce m subterms — one reduction step at a time via reduceSimpHead, 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 reduceSimpHead branch matches on: unfolding it is what turns that result back into a constructor tree the next step can work on.

The tactic keyword reduce_simp is this function; it stays a keyword because proofs are written with it by hand. Tactics that want it as a step call reduceSimp directly rather than going back through the grammar.

Equations

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