rw in ZMOD

Stream: general

[Adam Kurkiewicz]

Is there a way to make rw work in ZMOD (or in MOD for that matter).

Specifically, something like this would be a huge quality-of-life-improvement when doing elementary number theory with lots of modular arithmetic:

import Mathlib.Tactic

variable (a : ℤ) (x : ℤ) (y : ℤ) (m₁ : ℤ)

variable (lemma_1 : a ^ 2 ≡ -3 [ZMOD m₁])

variable (lemma_2 : a ^ 2 * x ^ 2 ≡ y ^ 2 [ZMOD m₁])

lemma lemma_3 : (-3) * x ^ 2 ≡ y ^ 2 [ZMOD m₁] := by
  rw [lemma_1] at lemma_2
  exact lemma_2

[Kevin Buzzard]

rw only works with equalities. If a=7 and I'm allowed to rewrite to change a to b because it's congruent to a mod 37 then you'd get the false statement b=7.

[Kevin Buzzard]

But two numbers are congruent mod n iff they're equal when reduced mod n so if you don't use the MOD language and switch to the % n language then the rewrite will work.

[Adam Kurkiewicz]

It doesn't have to be literally rewrite. I was wondering if there is a similar tactic to rewrite that would work here. Heather implemented something like this for inqualities (I think it was called rel in her book). And this kind of "replacement" would be valid mod m1. The point is that a ^ 2 is equal to (-3 + k * m1). So whatever we do with it downstream (multiply, add, substract, etc...), k * m1 is essentially zero, so we can just replace a^2 with -3. Note that lemma_3 is also ZMOD m1

[Adam Kurkiewicz]

No?

[Kevin Buzzard]

Yes I could imagine a bespoke tactic which did this. If Heather didn't write it then maybe we don't have it.

[Edward van de Meent]

it all works if you use ZMod n... and i imagine that if the statement you want is about divisibility, you could cast back...

[Edward van de Meent]

i don't know how good that api is, though

[Kevin Buzzard]

Yes that's a much better idea than my lifting suggestion because it works far more generally

[Damiano Testa]

This also works, but requires writing the intermediate step:

lemma lemma_3 : (-3) * x ^ 2 ≡ y ^ 2 [ZMOD m₁] := by
  trans a ^ 2 * x ^ 2
  · exact? says exact Int.ModEq.mul (id (Int.ModEq.symm lemma_1)) rfl
  · exact? says exact lemma_2

[Adam Kurkiewicz]

Oh, this trans and exact? magic is very nice, thank you!

[Adam Kurkiewicz]

As I'm doing number theory IMO questions for Compfiles there is a ton of modular arithmetic and a nice API to work with would go a long way. The magic suggested by @Damiano Testa should allow to quickly solve very simple goals like this without having to write too much repetitive invocations to Int.ModEq.mul, etc...

[Edward van de Meent]

you may also be interested in the calc tactic for reasoning about intermediate steps of transitive properties

[Adam Kurkiewicz]

Yup, I've used calc, it's nice

[Kim Morrison]

Isn't the answer here to use ZMod n, and us all to try to forget _ ≡ _ [ZMOD _] ever existed? (Maybe even try to stop using it?)

[Heather Macbeth]

Actually the tactic rel (or gcongr) works just fine here. That is, gcongr-for-modular-arithmetic doesn't have a name, it's just called gcongr :)

import Mathlib.Tactic

variable (a : ℤ) (x : ℤ) (y : ℤ) (m₁ : ℤ)

variable (lemma_1 : a ^ 2 ≡ -3 [ZMOD m₁])

variable (lemma_2 : a ^ 2 * x ^ 2 ≡ y ^ 2 [ZMOD m₁])

lemma lemma_3 : (-3) * x ^ 2 ≡ y ^ 2 [ZMOD m₁] := by
  calc (-3) * x ^ 2 ≡ a ^ 2 * x ^ 2 [ZMOD m₁] := by rel [lemma_1]
    _ ≡ y ^ 2 [ZMOD m₁]:= by rel [lemma_2]

[Adam Kurkiewicz]

And how can I lift into Zmod n? I've tried dsimp[Int.ModEq], and what I'm getting is statements with %s.

Specifically, I was thinking that the tactic reduce_mod_char should be able to destroy a goal like 6 * c + 5 ≡ 2 [ZMOD 3], but it makes no progress.

[Ruben Van de Velde]

import Mathlib

example (c : ℕ) : 6 * (c : ZMod 3) + 5 = 2 := by
  reduce_mod_char

[Adam Kurkiewicz]

Oh that's great to hear @Heather Macbeth

[Ruben Van de Velde]

Ugh:

import Mathlib

example (c : ℕ) : 6 * (c : ZMod 3) + 5 = 2 := by
  reduce_mod_char

example (c : ℤ) : 6 * c + 5 ≡ 2 [ZMOD 3] := by
  have zmod : 6 * (c : ZMod 3) + 5 = 2 := by
    reduce_mod_char
  have : (3 : ℤ) = (3 : ℕ) := by rw [Nat.cast_ofNat]
  rw [this, ← ZMod.intCast_eq_intCast_iff, Int.cast_ofNat, ← zmod]
  norm_cast

[Adam Kurkiewicz]

Thanks Ruben, let me try this

[Edward van de Meent]

example : (3 : ℤ) = (3 : ℕ) := by
  norm_num

[Adam Kurkiewicz]

That's a MWE of what I'm trying to do btw:

import Mathlib.Tactic

variable (y : ℤ) (x : ℤ)
variable (Hs : 3 * x ^ 2 + y ^ 2 = 6 * c + 5)

example : y ^ 2 ≡ 2 [ZMOD 3] := by
  calc  y ^ 2 ≡ 3 * x ^ 2 + y ^ 2 [ZMOD 3] := by sorry
        _ ≡ 6 * c + 5 [ZMOD 3] := by rw[Hs]
        _ ≡ 2 [ZMOD 3] := by
          reduce_mod_char

(I think I can adapt your solution)

[Adam Kurkiewicz]

This does work, thank you!

import Mathlib.Tactic

variable (y : ℤ) (x : ℤ)
variable (Hs : 3 * x ^ 2 + y ^ 2 = 6 * c + 5)

example : y ^ 2 ≡ 2 [ZMOD 3] := by
  calc  y ^ 2 ≡ 3 * x ^ 2 + y ^ 2 [ZMOD 3] := by sorry
        _ ≡ 6 * c + 5 [ZMOD 3] := by rw[Hs]
        _ ≡ 2 [ZMOD 3] := by
          have zmod : 6 * (c : ZMod 3) + 5 = 2 := by
            reduce_mod_char
          have : (3 : ℤ) = (3 : ℕ) := by rw [Nat.cast_ofNat]
          rw[this]
          rw[← ZMod.intCast_eq_intCast_iff]
          rw[Int.cast_ofNat]
          rw[← zmod]
          norm_cast

So @Kim Morrison , because it's so hard to switch between _ ≡ _ [ZMOD _] and Zmod n it's best to stick to the latter as it's got more advanced support, e.g. the reduce_mod_char tactic?

And then Zmod n is basically a ring like ℤ and a lot of the ring-based tactics will just work there, with the occasional need to lift things from ℤ to Zmod n?

[Adam Kurkiewicz]

Is there a mod_cases tactic in Zmod n? I'm struggling to find one, and when I use by_cases, I end up with the last case where n ≠ 1, ..., n, which is hard to despatch with.

[Edward van de Meent]

fin_cases is the tactic you're looking for

[Edward van de Meent]

this works for any type with a Fintype instance, i think

[Adam Kurkiewicz]

Thank you! I also just realised that I can do match ... with. Excellent. This is so much easier than _ \== _ [ZMOD _]

[Adam Kurkiewicz]

This is the quality of life improvement I was talking about in the beginning of the post. Compare the two approaches:

That's a simple lemma with _ ≡ _ [ZMOD 4]:

lemma square_mod_4 {x : ℤ} : x ^ 2 ≡ 1 [ZMOD 4] ∨ x ^ 2 ≡ 0 [ZMOD 4] := by
  rw[show x ^ 2 = x * x by ring]
  mod_cases x_mod_4 : x % 4
  · right

    rw[show (0 : ℤ) = 0 * 0 by rfl]
    apply Int.ModEq.mul
    exact x_mod_4
    exact x_mod_4
  · left
    rw[show (1 : ℤ) = 1 * 1 by rfl]
    apply Int.ModEq.mul
    exact x_mod_4
    exact x_mod_4
  · right
    calc  x * x ≡ 2 * 2 [ZMOD 4] := by
                  apply Int.ModEq.mul
                  exact x_mod_4
                  exact x_mod_4
          _ ≡ 0 [ZMOD 4]:= by rfl
  · left
    calc  x * x ≡ 3 * 3 [ZMOD 4] := by
                  apply Int.ModEq.mul
                  exact x_mod_4
                  exact x_mod_4
          _ ≡ 1 [ZMOD 4]:= by rfl

and that's the same lemma with Zmod n:

lemma square_mod_4_zmod {x : ZMod 4} : x ^ 2 = 1 ∨ x ^ 2 = 0 := by
  match x with
  | 0 =>
  right
  ring
  | 1 =>
  left
  ring
  | 2 =>
  right
  ring_nf
  rfl
  | 3 =>
  left
  ring_nf
  rfl

[Adam Kurkiewicz]

Much less cognitive overload! Thanks all!

[Edward van de Meent]

lemma square_mod_4_zmod' {x : ZMod 4} : x ^ 2 = 1 ∨ x ^ 2 = 0 := by
  fin_cases x <;> decide

[Edward van de Meent]

once you tell lean "look at all the cases" you can afterwards just tell it to "just calculate the truth value", because in each case there are no free variables anymore, and equality of ZMod n is decidable

[Michael Stoll]

lemma square_mod_4_zmod' : ∀ {x : ZMod 4}, x ^ 2 = 1 ∨ x ^ 2 = 0 := by
  decide

[Edward van de Meent]

oh, oops :upside_down:

[Adam Kurkiewicz]

Oh nice

[Michael Stoll]

Note that I moved x from left of to right of the colon.

[Adam Kurkiewicz]

What's this syntax? <;>

[Michael Stoll]

(Otherwise, one needs to intro first; decide does not like free variables...)

[Michael Stoll]

Adam Kurkiewicz said:

What's this syntax? <;>

It means "apply the next tactic to all goals".

[Edward van de Meent]

all resulting goals, i think,no?

[Michael Stoll]

(But the recommended style is to have only one goal in focus before applying the first tactic, so in practice it usually makes no difference.)

[Kim Morrison]

Would someone be interested in trying to either lessen the use of ZMOD in Mathlib? or at least write some docs warning people off it?

[Damiano Testa]

Would this be in scope for the linter at #13999?

[Heather Macbeth]

In my opinion, there shouldn't be a fixed rule against Int.ModEq in mathlib, at least in leaf files. Even if the core of mathlib is written at a very high level of sophistication, we should support users at a variety of abstraction levels.

[Kim Morrison]

Yes, I think it's much too early for a linter.

[Damiano Testa]

Sure, however note that the linter is intended as a "beginner friendly" linter: for instance, it flags Nat.sub and explains its pathology.

It is certainly intended to be an explicitly opt-in linter, taking a "did you really mean to say ...?" attitude.

[Damiano Testa]

E.g., I am wondering whether the [Mul F] [Field F] could be flagged by the linter.

[Adam Kurkiewicz]

And what's the best way to shift from ZMod n into divisibility? For example in the _ ≡ _ [ZMOD n] world we had Int.modEq_zero_iff_dvd

[llllvvuu]

docs#ZMod.intCast_zmod_eq_zero_iff_dvd
docs#ZMod.intCast_eq_intCast_iff_dvd_sub

[Adam Kurkiewicz]

Oh I see, thank you!

[Eric Wieser]

I think @Yaël Dillies was hoping (with low priority) to eliminate Int.ModEq in favor of docs#AddCommGroup.ModEq ?

[Yaël Dillies]

Yes, but since then we have decided that Int should be a foundational type, so I've somewhat retropedalled on the idea

[Chris Hughes]

In Lean3, simp could be configured to work with any equivalence relation, provided it had appropriate congruence lemmas. This was pretty rarely used though.

[Eric Wieser]

Yaël Dillies said:

Yes, but since then we have decided that Int should be a foundational type, so I've somewhat retropedalled on the idea

I think the definition of ModEq is pretty dependency free; you don't need anything apart from Exists and -/+

[Yaël Dillies]

Sure but it's not "Batteries-foundational", is it?

[Eric Wieser]

I don't see why not. Batteries can still specialize all the theorems to Int and Nat, but sharing a definition with Nat / every other additive monoid feels the same as sharing the definition of NatCast

[Yaël Dillies]

Okay then sure

[Ralf Stephan]

Kim Morrison said:

Would someone be interested in trying to either lessen the use of ZMOD in Mathlib? or at least write some docs warning people off it?

What is now on my list:

• remove all dependencies on ModEq in ZMod/Basic (a dozen proofs use ModEq lemmas for convenience)
• split off the interface from ZMod to ModEq into a new file Data/Zmod/ModEq

This is exercise for me to get to know this part of Mathlib. Starting with: #15446, please have a look.

[Ralf Stephan]

These are all easy changes: #15462, #15469, #15471. This is not so easy: #15463.

[Eric Wieser]

It's not immediately clear to me that any of those are a net positive

[Eric Wieser]

Certainly the last one just makes the proof harder to read

[Ralf Stephan]

So, reducing dependencies is not priority?

[Jovan Gerbscheid]

Generalized rewriting is something that I think would be beneficial to have. There was a discussion about rewriting with inequalities a while ago, and I'm not sure what the status if of #8167. Before that, I had already made a proof of concept generalized rewriting tactic, but it turned out that two other people had done it independently as well. In my version you could rewrite with any preorder that you register for rewriting. This means things like ≤ and ⊆, but also _ ≡ _ [ZMOD _], or even the divisibility relation.

[Heather Macbeth]

#8167 took a while to get reviewed, and by the time it did get reviewed, I think the author had put it on the back burner (which is understandable). But someone should adopt it (with that author's permission) and get it into Mathlib -- many people are anxiously awaiting it!

[Heather Macbeth]

Jovan Gerbscheid said:

In my version you could rewrite with any preorder that you register for rewriting. This means things like ≤ and ⊆, but also _ ≡ _ [ZMOD _], or even the divisibility relation.

#8167 has this feature too (and in fact the relation doesn't even need to be a preorder).

[Heather Macbeth]

FWIW, @Mario Carneiro did the first review pass back in December last year, and if I remember correctly he felt that the basic structure of that PR is sound. (It piggy-backs on gcongr, which is good for code deduplication.)

[Kim Morrison]

Do we have someone who is planning on fixing this to use a discrimination tree? I wouldn't object to merging as is, if that is on someone's plausible TODO list, but I'm skeptical otherwise.

[Heather Macbeth]

@Kim Morrison Are you asking about the conversation here?:
https://github.com/leanprover-community/mathlib4/pull/8167#discussion_r1422292721

[Kim Morrison]

@Heather Macbeth yes, thanks for the link.