ZMod.val and numerals

Stream: Is there code for X?

[Jeremy Avigad]

Consider the following:

import Mathlib.Data.ZMod.Basic
import Mathlib.Tactic.NormNum.Prime

def BIG_PRIME := 89

example : ZMod.val (16 : ZMod BIG_PRIME) = 16 := by
  rfl

I am in a setting where I have goals with expressions like the one that appears on the LHS and I want to simplify them to the RHS with rw or simp. I don't mind rewriting rw [foo 16] or something like that if necessary, but the goals are too big to use change and there are too many of them to conveniently state each instance with a have or as a separate simp lemma.

In analogy to Fin.coe_ofNat_eq_mod, I tried this:

theorem bar (n : Nat) (h : n < BIG_PRIME) :
    ZMod.val (ofNat(n) : ZMod BIG_PRIME) = n

but Lean can't even parse the ofNat(n); the error message I get is

failed to synthesize
  OfNat (ZMod BIG_PRIME) n

although it somehow manages to do it when n is replaced by a concrete numeral like 16.

Any thoughts about how I can do this?

[Jeremy Avigad]

Sorry, I forgot to mention that I also did this:

instance : Fact (Nat.Prime BIG_PRIME) := by
 norm_num [BIG_PRIME]; exact ⟨trivial⟩

So Lean ought to be able to infer that BIG_PRIME is not 0 or 1. For example, this works:

theorem foo (n : Nat) (h : n < BIG_PRIME) :
    ZMod.val (↑(n) : ZMod BIG_PRIME) = n :=
  Nat.mod_eq_of_lt h

[Yaël Dillies]

(did you mean to post this in #Is there code for X??)

[Notification Bot]

3 messages were moved here from #general > Is there code for X by Jeremy Avigad.

[Jeremy Avigad]

@Yaël Dillies Yes, sorry -- I just moved them.

[Yaël Dillies]

Jeremy Avigad said:

In analogy to Fin.coe_ofNat_eq_mod, I tried this:

theorem bar (n : Nat) (h : n < BIG_PRIME) :
    ZMod.val (ofNat(n) : ZMod BIG_PRIME) = n

but Lean can't even parse the ofNat(n); the error message I get is

failed to synthesize
  OfNat (ZMod BIG_PRIME) n

although it somehow manages to do it when n is replaced by a concrete numeral like 16.

Any thoughts about how I can do this?

Numerals fall into three categories:

• 0
• 1
• big

Therefore to handle all numerals you need to write three lemmas:

• ZMod.val 0 = 0
• ZMod.val 1 = 1
• ∀ n < BIG_PRIME, n.AtLeastTwo → ZMod.val ofNat(n) = n

Of course, you should also write a lemma in terms of Nat.cast, and this lemma can then be used to prove the other three lemmas

[Yaël Dillies]

A possibly better answer is that this sounds like a job for a (d)simproc, akin to docs#Fin.isValue

[Yaël Dillies]

Yaël Dillies said:

Therefore to handle all numerals you need to write three lemmas: [...]

I must say that docs#Fin.coe_ofNat_eq_mod looks like an exception to what I just claimed, but that's because Fin has a custom OfNat instance that covers all numerals at once: docs#Fin.instOfNat. If you ask me, this instance looks a bit odd since it forces 0 : Fin n and 1 : Fin n instances to be defeq to ⟨0 % n, _⟩ and ⟨1 % n, _⟩ instead of the more natural ⟨0, _⟩ and ⟨1, _⟩.

[Jeremy Avigad]

Your solution doesn't work.

theorem foo' : ∀ n < BIG_PRIME, n.AtLeastTwo → ZMod.val (n := BIG_PRIME) n = n := fun _ h _ => Nat.mod_eq_of_lt h

is the same as my theorem foo. It is stated in terms of a cast from Nat to ZMod BIG_PRIME, not numerals. You can't use it to rewrite ZMod.val (n := BIG_PRIME) 16.

[Antoine Chambert-Loir]

Trial and error gave me this, but I don't understand what I wrote.

theorem junk (n : ℕ) (h : n < BIG_PRIME) :
    ZMod.val (@OfNat.ofNat (ZMod BIG_PRIME) n
      (OfNat.mk (n : ZMod BIG_PRIME)) : ZMod BIG_PRIME) = n :=
  Nat.mod_eq_of_lt h

example : ZMod.val (16 : ZMod BIG_PRIME) = 16 := by
  rw [junk]
  norm_num [BIG_PRIME]
  exact Nat.lt_of_sub_eq_succ rfl

[Jeremy Avigad]

Aha! That's great. I should have thought of manually forcing Lean to synthesize the instance. Thanks! I should even be able to make junk do the calculation with (h : n < BIG_PRIME := by simp [BIG_PRIME]).

[Antoine Chambert-Loir]

and this works as well:

theorem gen_junk (p : ℕ) (n : ℕ) (h : n < p) :
    ZMod.val (@OfNat.ofNat (ZMod p) n
      (OfNat.mk (n : ZMod p)) : ZMod p) = n := by
  simp only [ZMod.val_natCast]
  rw [Nat.mod_eq, if_neg]
  simp only [not_and, not_le]
  exact fun _ => h

[Yaël Dillies]

Jeremy Avigad said:

theorem foo' {n : ℕ : ∀ n < BIG_PRIME, n.AtLeastTwo → ZMod.val (n := BIG_PRIME) n = n := fun _ h _ => Nat.mod_eq_of_lt h

is the same as my theorem foo. It is stated in terms of a cast from Nat to ZMod BIG_PRIME, not numerals.

That's because you used n instead of ofNat(n):

import Mathlib.Data.ZMod.Basic
import Mathlib.Tactic.NormNum

def BIG_PRIME := 89

theorem ZMod.val_ofNat {n : ℕ} [n.AtLeastTwo] (hn : n < BIG_PRIME) :
    ZMod.val (n := BIG_PRIME) ofNat(n) = ofNat(n) := Nat.mod_eq_of_lt hn

example : ZMod.val (16 : ZMod BIG_PRIME) = 16 := by
  rw [ZMod.val_ofNat]
  norm_num [BIG_PRIME]

[Yaël Dillies]

Sorry, I realise that was a typo in my original message. Fixed

[Edward van de Meent]

what is hn : BIG_PRIME supposed to mean?

[Edward van de Meent]

btw, presumably you want ofNat(n) in the type of foo'

[Yaël Dillies]

Fixed

[Yaël Dillies]

Argh, I got confused between Jeremy's snippet and mine when copying from gitpod

[Yaël Dillies]

Fixed for good this time

[Edward van de Meent]

btw, you can change foo to drop the lt assumption, presuming norm_num does some reduction later:

theorem foo'' {n : ℕ} [n.AtLeastTwo] :
    ZMod.val (n := BIG_PRIME) ofNat(n) = ofNat(n) % BIG_PRIME := rfl

example : ZMod.val (16 : ZMod BIG_PRIME) = 16 := by
  rw [foo'']
  norm_num [BIG_PRIME]
  -- exact Nat.lt_of_sub_eq_succ rfl -- no longer necessary

[Yaël Dillies]

You're outdated compared to my snippet :wink:

[Antoine Chambert-Loir]

I think I understand why that worked. OfNat.ofNat has the following form:

{α : Type u} → (x : ℕ) → [self : OfNat α x] → α

so one needs to produce the instance. (For a natural number, there is docs#instOfNatNat.)

The following gives it, but, again, I don't know what I'm doing:

instance instOfNatZMod (p n : Nat) : OfNat (ZMod p) n := by
  exact ⟨n⟩

theorem junk' (p : ℕ) (n : ℕ) (h : n < p) :
    ZMod.val (OfNat.ofNat n : ZMod p) = n := by
  simp only [OfNat.ofNat, ZMod.val_natCast]
  rw [Nat.mod_eq, if_neg]
  simp only [not_and, not_le]
  exact fun _ => h

example : ZMod.val (16 : ZMod BIG_PRIME) = 16 := by
  apply junk'
  simp [BIG_PRIME]

[Edward van de Meent]

also of interest maybe: docs#ZMod.val_natCast

[Yaël Dillies]

You really shouldn't be writing any more OfNat instance, as these are very prone to causing diamonds

[Yaël Dillies]

Here is the mathlib-approved version of everything I've said so far:

import Mathlib.Data.ZMod.Basic
import Mathlib.Tactic.NormNum

lemma ZMod.val_ofNat (n a : ℕ) [a.AtLeastTwo] :
    ZMod.val (n := n) ofNat(a) = ofNat(a) % n := ZMod.val_natCast _

lemma ZMod.val_ofNat_of_lt {n a : ℕ} [a.AtLeastTwo] (han : a < n) :
    ZMod.val (n := n) ofNat(a) = ofNat(a) := ZMod.val_natCast_of_lt han

def BIG_PRIME := 89

example : ZMod.val (16 : ZMod BIG_PRIME) = 16 := by
  rw [ZMod.val_ofNat]; norm_num [BIG_PRIME]

[Edward van de Meent]

for completeness, we also have:

example : ZMod.val (16 : ZMod BIG_PRIME) = 16 := by
  apply ZMod.val_ofNat_of_lt; norm_num [BIG_PRIME]

(assuming yaël's snippet)

[Jeremy Avigad]

This solves all my problems. Thanks!

[Yaël Dillies]

I've opened #23441 for the two lemmas

[Edward van de Meent]

CI complains about an error in Mathlib.NumberTheory.LegendreSymbol.AddCharacter

[Yaël Dillies]

Just fixed it now

[Antoine Chambert-Loir]

Additional question: What does the syntax ofNat(n) means? — with parentheses and no space?

[Ruben Van de Velde]

It means OfNat.ofNat n

[Edward van de Meent]

i think it does a tiny bit more than just that though? I seem to recall it adds something which makes stuff like simp ignore the OfNat.ofNat or something? something to do with no_index

[Edward van de Meent]

looking at the thread mentioned at the docs of ofNat(.), it seems to explain that simp won't match on something like 3 if the simp lemma mentions a plain OfNat.ofNat. It is verified experimentally that indeed using ofNat(.) instead on both sides of such simp lemmas improves simp behaviour

[Edward van de Meent]

#mathlib4 > writing lemmas about `ofNat` @ 💬 <- this thread