decide_zmod: deciding ground ring identities over ZMod m by bounded residue computation

HexDecide transfers a single ZMod m multiplication to an integer multiply-then-%m (residueMulReal). A ground ring identity — one built from +, *, -, neg, ^ over concrete ZMod m numerals — is a whole expression tree. This module lifts that single-op transfer to the tree (the ReprTransferExpr.OpExpr.denote_commutes idea, for the full ring signature), and reduces mod m after every node so intermediates stay in [0, m). That bounded-residue discipline keeps the final check on the GMP Int fast path, so decide_zmod closes by kernel decide — axiom-free ([propext, Classical.choice, Quot.sound], no Lean.ofReduceBool) — where computing inside ZMod/Fin, or over unreduced ℤ, either stalls the kernel or blows the coefficients up.

Main results

• RingExpr — the ground ring-expression algebra.
• RingExpr.denoteA / denoteR — its meaning in ZMod m, and the bounded integer-residue computation (% m after every operation).
• RingExpr.denoteR_cast — the abstraction theorem (the homomorphism square lifted over the tree by induction).
• RingExpr.decide_transfer — the backward transfer a decide on the residues proves the abstract identity.
• decide_zmod — the tactic front: reifies a ZMod m equality goal into RingExpr and closes it via decide_transfer + kernel decide.

Scope and extensions

• Ground identities only: every leaf must be a ZMod m numeral. A goal with a free ZMod m variable is not decidable and is out of scope (use ring/ reduce_mod_char there).
• Exponents are literal ℕ. denoteR computes base ^ n before reducing, so a huge exponent can build a large intermediate; a binary powMod in denoteR removes that (future).
• A polynomial identity ∀ x, p x = q x reduces to coefficient equality (the seqpoly refinement, HexSeqPoly) — a separate decide_zmod_poly on top of this core.

inductive Transfer.ZModDecide.RingExpr : Type

Ground ring expressions over integer-numeral leaves.

• lit : ℤ → RingExpr
• add : RingExpr → RingExpr → RingExpr
• sub : RingExpr → RingExpr → RingExpr
• mul : RingExpr → RingExpr → RingExpr
• neg : RingExpr → RingExpr
• pow : RingExpr → ℕ → RingExpr

def Transfer.ZModDecide.instReprRingExpr.repr : RingExpr → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Transfer.ZModDecide.instReprRingExpr : Repr RingExpr

Equations

• Transfer.ZModDecide.instReprRingExpr = { reprPrec := Transfer.ZModDecide.instReprRingExpr.repr }

def Transfer.ZModDecide.RingExpr.denoteA (m : ℕ) : RingExpr → ZMod m

The abstract meaning of a RingExpr in ZMod m.

Equations

• Transfer.ZModDecide.RingExpr.denoteA m (Transfer.ZModDecide.RingExpr.lit z) = ↑z
• Transfer.ZModDecide.RingExpr.denoteA m (a.add b) = Transfer.ZModDecide.RingExpr.denoteA m a + Transfer.ZModDecide.RingExpr.denoteA m b
• Transfer.ZModDecide.RingExpr.denoteA m (a.sub b) = Transfer.ZModDecide.RingExpr.denoteA m a - Transfer.ZModDecide.RingExpr.denoteA m b
• Transfer.ZModDecide.RingExpr.denoteA m (a.mul b) = Transfer.ZModDecide.RingExpr.denoteA m a * Transfer.ZModDecide.RingExpr.denoteA m b
• Transfer.ZModDecide.RingExpr.denoteA m a.neg = -Transfer.ZModDecide.RingExpr.denoteA m a
• Transfer.ZModDecide.RingExpr.denoteA m (a.pow n) = Transfer.ZModDecide.RingExpr.denoteA m a ^ n

def Transfer.ZModDecide.RingExpr.denoteR (m : ℤ) : RingExpr → ℤ

The bounded integer-residue computation: % m after every operation, so every intermediate stays in [0, m) (bar a single pow, reduced immediately). This is what decide evaluates — Int arithmetic on the GMP fast path.

Equations

• Transfer.ZModDecide.RingExpr.denoteR m (Transfer.ZModDecide.RingExpr.lit z) = z % m
• Transfer.ZModDecide.RingExpr.denoteR m (a.add b) = (Transfer.ZModDecide.RingExpr.denoteR m a + Transfer.ZModDecide.RingExpr.denoteR m b) % m
• Transfer.ZModDecide.RingExpr.denoteR m (a.sub b) = (Transfer.ZModDecide.RingExpr.denoteR m a - Transfer.ZModDecide.RingExpr.denoteR m b) % m
• Transfer.ZModDecide.RingExpr.denoteR m (a.mul b) = Transfer.ZModDecide.RingExpr.denoteR m a * Transfer.ZModDecide.RingExpr.denoteR m b % m
• Transfer.ZModDecide.RingExpr.denoteR m a.neg = -Transfer.ZModDecide.RingExpr.denoteR m a % m
• Transfer.ZModDecide.RingExpr.denoteR m (a.pow n) = Transfer.ZModDecide.RingExpr.denoteR m a ^ n % m

theorem Transfer.ZModDecide.RingExpr.denoteR_cast (m : ℕ) [NeZero m] (e : RingExpr) : ↑(denoteR (↑m) e) = denoteA m e

The abstraction theorem. The residue computation, cast back into ZMod m, equals the abstract value: the single-op commuting square (% m invisible under Int.cast, ZMod.intCast_mod) lifted over the tree by induction.

theorem Transfer.ZModDecide.RingExpr.decide_transfer (m : ℕ) [NeZero m] (e₁ e₂ : RingExpr) (h : denoteR (↑m) e₁ = denoteR (↑m) e₂) : denoteA m e₁ = denoteA m e₂

The backward transfer. A decidable equality of the two bounded residue computations proves the abstract ZMod m identity — decide on the residues, underwritten by denoteR_cast rather than trusted.

The decide_zmod tactic

partial def Transfer.ZModDecide.reifyZMod (e : Lean.Expr) : Lean.MetaM Lean.Expr

Reify a ground ZMod m expression into a RingExpr term. Fails on any leaf that is not a numeral (e.g. a free variable), keeping the tactic total on the ground fragment it is sound for.

def Transfer.ZModDecide.tacticDecide_zmod : Lean.ParserDescr

Close a ground ring identity over ZMod m by bounded residue computation: reify both sides, then discharge via RingExpr.decide_transfer and a kernel decide on the reduced integer residues. Axiom-free (no Lean.ofReduceBool). Every leaf must be a numeral; a free ZMod m variable is rejected.

Equations

• Transfer.ZModDecide.tacticDecide_zmod = Lean.ParserDescr.node `Transfer.ZModDecide.tacticDecide_zmod 1024 (Lean.ParserDescr.nonReservedSymbol "decide_zmod" false)

Examples

Axiom audit

theorem Transfer.ZModDecide.zmod_example_audit : 7 ^ 4 + 2 * 9 - 3 = 7 ^ 4 + 2 * 9 - 3