Z / q.Z

Stream: mathlib4

[Son Ho]

@Jonathan Protzenko and I are trying to formalize operations which involve the finite group Z / q.Z (where q is prime). What is the most convenient way of defining Z / q.Z? More specifically, should we work with ZMod, or with something like Z / Ideal.span q (following what I see in https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/ZMod/Quotient.html )?

[Eric Wieser]

ZMod q is the canonical spelling

[Jonathan Protzenko]

thanks, we're browsing the documentation for this file and looking for the power function, how do we go about finding this one?

[Eric Rodriguez]

Just write x ^ n as usual.

[Adam Topaz]

Are you looking for computationally efficient exponentiation? E.g. for RSA? If so, then I don’t think we have this yet.

[Adam Topaz]

For proof of concept purposes (I.e. if the numbers don’t get too large, or if you’re proving things with q and the exponent being arbitrary), then using ^ will work just fine.

[Son Ho]

No, we're not looking for efficient computations. But as you guessed, we're trying to verify a crypto primitive (the Kyber NTT).
As of now, I have the issue that I don't manage to reduce terms when doing proofs.

More specifically : in Kyber we use q = 3329, which gives us that zeta = 17 is a root of 1 (more specifically: zeta ^ 256 = 1).
I want to prove that below, but I'm not sure how to proceed in the proof. In particular, I would expect that simp manages to simplify terms, but it doesn't happen :

import Lean
import Mathlib.Data.ZMod.Algebra

open ZMod

def q := 3329
def Zq := ZMod q

instance commRing : CommRing Zq := ZMod.commRing q
instance commSemiRing : CommSemiring Zq := commRing.toCommSemiring
instance semiRing : Semiring Zq := commRing.toSemiring

def one : Zq := ⟨ 1, by simp ⟩
def zeta : Zq := ⟨ 17, by simp ⟩

theorem zeta_256_is_one : Pow.pow zeta 256 = one := by
  simp [Pow.pow, zeta, one]
  -- Stuck here

Do you know how I should proceed?

[Adam Topaz]

Does by decide work?

[Son Ho]

I tried it but it also fails. I also don't manage to reduce something like zeta * zeta.

[Adam Topaz]

by rfl works :)

[Adam Topaz]

although rfl fails (max recursion depth yada yada yada)

[Son Ho]

Oh wow, thanks!

[Son Ho]

But I'm still a bit puzzled: if I have in my goal a subterm zeta * zeta and I want to reduce it to 289 (without introducing a subgoal specifically for this). How could I do it? :)

[Jonathan Protzenko]

The context is that we would find it nice if we could "clean up" a term by simplifying away things that compute... hope this helps!

[Adam Topaz]

Son Ho said:

But I'm still a bit puzzled: if I have in my goal a subterm zeta * zeta and I want to reduce it to 289 (without introducing a subgoal specifically for this). How could I do it? :)

This would be rfl as well.

[Adam Topaz]

Or norm_num

[Adam Topaz]

example : zeta * zeta = 289 := rfl
example : zeta * zeta = 289 := show 17 * 17 = 289 by norm_num

[Son Ho]

But it doesn't simplify subterms, it only applies to proofs of equality, right?
Let's say my goal is : P (zeta * zeta) for some predicate P, and I want to simplify it to P 289.

[Adam Topaz]

example (P : Zq → Prop) (h : P 289) : P (zeta * zeta) := by
  rwa [show zeta * zeta = 289 from rfl]

example (P : Zq → Prop) (h : P 289) : P (zeta * zeta) := by
  rwa [show zeta * zeta = 289 from show 17 * 17 = 289 by norm_num]

example (P : Zq → Prop) (h : P 289) : P (zeta * zeta) := h

[Adam Topaz]

when your numbers get big, I suppose the norm_num approach would be the way to go.

[Adam Topaz]

but in this case, everything can be done with rfl essentially.

[Son Ho]

Perfect, thanks!

[Adam Topaz]

No problem! Good luck with your project.