Reducing mod n

Stream: mathlib4

[Michael Stoll]

What is the mathlib4 analogue of apply_fun (coe : ℕ → zmod n) at h ?

[Michael Stoll]

It seems that apply_fun (fun (z : ℕ) ↦ (z : ZMod n)) at hworks... Is this the idiomatic way of doing this?

[Kyle Miller]

You could probably do apply_fun (· : ZMod n) at h, which should mean the same thing but is shorter.

[Michael Stoll]

Follow-up question: I'm having difficulties getting 8 : ZMod 8 simplified to zero.

import Mathlib
lemma ex (x m : ℕ) (h : x ^ 2 = 8 * m) : (x : ZMod 8) ^ 2 = 0 := by
  apply_fun (fun (z : ℕ) ↦ (z : ZMod 8)) at h
  norm_num at h -- leaves `↑x ^ 2 = 8 * ↑m` with `8 : ZMod 8`
  -- simp at h -- `simp made no progress`
  rw [(rfl : (8 : ZMod 8) = 0)] at h -- does nothing
  -- how do I change `8 : ZMod 8` to `0`?
  convert h -- this works, but is too involved for my taste
  exact? -- Try this: `exact Eq.symm (mul_eq_zero_of_left rfl ↑m)`

IIRC, norm_numdid that in mathlib3...
(and the try this gives an error, because the pasted code stumbles over the coercion...)

[Michael Stoll]

Kyle Miller said:

You could probably do apply_fun (· : ZMod n) at h, which should mean the same thing but is shorter.

This gives an error (in my use case, n = 8):

type mismatch
  fun x => x
has type
  ?m.109937 → ?m.109937 : Sort ?u.109936
but is expected to have type
  ZMod 8 : Type

[Yaël Dillies]

You can always replace coe by (\u).

[Adam Topaz]

Here's how I would do it:

import Mathlib

lemma ex (x m : ℕ) (h : x ^ 2 = 8 * m) : (x : ZMod 8) ^ 2 = 0 := by
  norm_num at h
  norm_cast
  simp [h]

[Adam Topaz]

oh wait that's not complete.

[Adam Topaz]

anyway, instead of the rw, you can use change as follows:

import Mathlib

lemma ex (x m : ℕ) (h : x ^ 2 = 8 * m) : (x : ZMod 8) ^ 2 = 0 := by
  apply_fun (fun e => (e : ZMod 8)) at h
  norm_num at h -- leaves `↑x ^ 2 = 8 * ↑m` with `8 : ZMod 8`
  change _ = 0 * _ at h
  simpa using h

[Michael Stoll]

Yeah, but my point is that this shouldn't be necessary!

[Adam Topaz]

This works for me:

import Mathlib

lemma ex (x m : ℕ) (h : x ^ 2 = 8 * m) : (x : ZMod 8) ^ 2 = 0 := by
  apply_fun (fun e => (e : ZMod 8)) at h
  norm_num at h -- leaves `↑x ^ 2 = 8 * ↑m` with `8 : ZMod 8`
  rw [show (8 : ZMod 8) = 0 by rfl] at h
  simpa using h

[Adam Topaz]

You can also replace the lambda with Nat.cast if that's preferable:

lemma ex (x m : ℕ) (h : x ^ 2 = 8 * m) : (x : ZMod 8) ^ 2 = 0 := by
  apply_fun (Nat.cast : ℕ → ZMod 8) at h
  norm_num at h -- leaves `↑x ^ 2 = 8 * ↑m` with `8 : ZMod 8`
  rw [show (8 : ZMod 8) = 0 by rfl] at h
  simpa using h

[Michael Stoll]

why does rw [show (8 : ZMod 8) = 0 by rfl] at h work, but rw [(rfl : (8 : ZMod 8) = 0)] at h doesn't?

[Adam Topaz]

I'm not sure.

[Kyle Miller]

show inserts a type hint, type ascriptions don't

[Adam Topaz]

right. You can see this by comparing e1 and e2 in the following:

lemma ex (x m : ℕ) (h : x ^ 2 = 8 * m) : (x : ZMod 8) ^ 2 = 0 := by
  apply_fun (Nat.cast : ℕ → ZMod 8) at h
  norm_num at h -- leaves `↑x ^ 2 = 8 * ↑m` with `8 : ZMod 8`
  have e1 := (rfl : (8 : ZMod 8) = 0)
  have e2 : (8 : ZMod 8) = 0 := rfl
  rw [show (8 : ZMod 8) = 0 by rfl] at h
  simpa using h

[Michael Stoll]

lemma ex4 : (8 : ZMod 8) = 0 := by simp only -- works

lemma ex5 (m : ℕ) : (8 : ZMod 8) * m = 0 * m := by simp only -- does not work

[Michael Stoll]

(I'm on vacation, but it's a rainy day, and so I thought I'd get started seriously in Lean4. Somehow, it feels quite a bit like when I started using Lean(3) quite some time ago... :thinking: )

[Jireh Loreaux]

There's #5376, but it has a merge conflict and probably needs more review.

[Alex J. Best]

Michael Stoll said:

lemma ex4 : (8 : ZMod 8) = 0 := by simp only -- works

lemma ex5 (m : ℕ) : (8 : ZMod 8) * m = 0 * m := by simp only -- does not work

The first simp only is probably giving up and trying decide or rfl, whereas the second isn't.

[Adam Topaz]

@Alex J. Best note that rfl also solves the second one...

[Adam Topaz]

Why isn't simp giving up in the same way in ex5?

[Adam Topaz]

Well, I guess decide won't work for the second one, so maybe that's it.

[Alex J. Best]

Indeed its doing decide:

lemma ex4 : (8 : ZMod 8) = 0 := by simp (config := {decide:=false}) only -- now they both don't work, success!
lemma ex5 (m : ℕ) : (8 : ZMod 8) * m = 0 * m := by simp only -- does not work

[Alex J. Best]

Michael Stoll said:

(I'm on vacation, but it's a rainy day, and so I thought I'd get started seriously in Lean4. Somehow, it feels quite a bit like when I started using Lean(3) quite some time ago... :thinking: )

One reason why this probably feels the case is that you are trying things involving numerals. Numerals changed completely between lean 3 and lean 4, so we (mathlib) are still in the dark ages regarding them (or maybe the middle ages), the port of mathlib is done but a lot more adjustments need to take place to make things work how we want. This can take the form of tactics, or useful lemmas. For example here is a nice lemma that will make simp do what you want

@[simp]
lemma tada {n : Nat} [Nat.AtLeastTwo n] {R : Type _} [NonAssocSemiring R] [CharP R n] : (OfNat.ofNat n : R) = 0 :=
  CharP.cast_eq_zero R n

[Michael Stoll]

OK; maybe somebody should PR this (under an appropriate name...)?
But I would think this is something norm_num should also be doing. More precisely, I think it would be good if norm_numwould replace any numeral n in a ring of (non-zero) characteristic m by (the value of) n % m. @Mario Carneiro ?

[Jireh Loreaux]

I'll again mention that #5376 exists.

[Michael Stoll]

Maybe this can be included in what norm_num does? That would seem to be the most convenient way.
(But keep reduce_mod_char as a separate tactic.)

[Michael Stoll]

Alex J. Best said:

Michael Stoll said:

(I'm on vacation, but it's a rainy day, and so I thought I'd get started seriously in Lean4. Somehow, it feels quite a bit like when I started using Lean(3) quite some time ago... :thinking: )

One reason why this probably feels the case is that you are trying things involving numerals. Numerals changed completely between lean 3 and lean 4, so we (mathlib) are still in the dark ages regarding them (or maybe the middle ages), the port of mathlib is done but a lot more adjustments need to take place to make things work how we want. This can take the form of tactics, or useful lemmas. For example here is a nice lemma that will make simp do what you want

@[simp]
lemma tada {n : Nat} [Nat.AtLeastTwo n] {R : Type _} [NonAssocSemiring R] [CharP R n] : (OfNat.ofNat n : R) = 0 :=
  CharP.cast_eq_zero R n

When I replace tada in the simp only with its definition (for the concrete case) CharP.cast_eq_zero (ZMod 8) 8, it does not work. Why is this? (Same with just CharP.cast_eq_zero (ZMod 8) or CharP.cast_eq_zero.)

[Alex J. Best]

I agree this should probably be part of norm num eventually, it just doesn't yet for reasons of not enough time being invested in making it work! (Note that norm num didn't yet do this in lean 3 either, but many of us have hoped for better mod n tactics for some time).
Simp works up to syntactic equality so one shouldn't expect in general that you can replace a simp lemma by its definition and have it work the same, if some definitional equality is involved (in this case the definitional equality is between a numeral and the explicit cast of the same numeral from the naturals to the ring)

[Michael Stoll]

In the lean3 version of the prof I was translating to lean4, norm_num was sufficient to get rid of 8 : zmod 8 in the expression (but I don't know enough of how norm_num works internally to have an idea of what precisely causes the difference in behaviout).