tactic for easy calculations in ZMod p?

Stream: Is there code for X?

[David Renshaw]

import Mathlib.Data.ZMod.Basic

lemma foo (a b : ZMod 7) (h : a + 3 * b = 0) : a = 4 * b := by
  -- is there a tactic that can avoid all of this manual rewriting?
  have h9: a + 3 * b - 3 * b = 0 - 3 * b := congrFun (congrArg HSub.hSub h) _
  rwa [add_sub_cancel, zero_sub, ←neg_mul, show ((-3):ZMod 7) = 4 by rfl] at h9

Is there a tactic that can automate this proof?

[David Renshaw]

(that code is Lean 4)

[Yaël Dillies]

What about (untested)

  rw [show (4 : zmod 7) = -3, by norm_num]
  linear_combination h

[David Renshaw]

Nice!

import Mathlib.Data.ZMod.Basic
import Mathlib.Tactic.LinearCombination

lemma lemma2 (a b : ZMod 7) (h : a + 3 * b = 0) : a = 4 * b := by
  rw [show (4 : ZMod 7) = -3 by norm_num]
  linear_combination h

[David Renshaw]

And it succeeds in context: https://github.com/dwrensha/math-puzzles-in-lean4/commit/a7526ac929ae14aaa95983f1dea4d2b0b2b17bb5
Thanks!

[Anne Baanen]

Yaël Dillies said:

What about (untested)

  rw [show (4 : zmod 7) = -3, by norm_num]
  linear_combination h

Last time I checked, norm_num doesn't have any specific support for ZMod so I believe the norm_num call is just a complicated way to write dec_trivial. I was actually looking into making a tactic that goes through an expression in characteristic p and rewrites all coefficients to be between 0 and p. My Lean4 metaprogramming skills aren't quite good enough to make it work yet though :P

[David Renshaw]

just plain rfl seems to work for me

[David Renshaw]

Makes me wonder why linear_combination needs this hint from me.

[Eric Wieser]

Well 4 = 11 and infinitely many other similar statements are also true by rfl...

[Eric Wieser]

Polyrith can solve things like this after #17142

[David Renshaw]

Well 4 = 11 and infinitely many other similar statements are also true by rfl

My (naive) reasoning is:

1. linear_combination is chaining together a bunch of ringinvocations
2. ring is stronger than ring_nf, which is "ring normal form", and "normal form" means normalizing all terms
3. (-3 : ZMod 7) should normalize to 4, (as should (11 : ZMod 7)).

[Eric Wieser]

"normal form" means "normal form in the language of rings", not "normal form in whatever ring you happen to be using"

[Eric Wieser]

Somewhat surprisingly, ring can't even solve:

lemma lemma2 (R) [Ring R] (x : R) : 1 + x + 1 = x + 2 := by ring

[Alex J. Best]

Thats probably as ring is designed for CommRings, so its probably silently falling back to not doing very much at all (maybe it even thinks it's working on the nats inside the ofnat notation).

[Alex J. Best]

It would certainly be nice to normalize to some normal form for rings of some fixed explicitly given characteristic in addition, but we don't have a tactic that does that yet, @Anne Baanen was working on something like this in lean 3 I believe. EDIT: oops I see Anne already mentioned this above :wink:

[Anne Baanen]

I am working on this in Lean 4 right as we speak!

[Eric Wieser]

Alex J. Best said:

Thats probably as ring is designed for CommRings

This gets me every time...

[Eric Wieser]

Can we call it comm_ring_nf to make that clear?

[Ruben Van de Velde]

crnf?

[Eric Wieser]

I don't think we need to make it short since no one ever types ring_nf anyway

[Eric Wieser]

I'm pretty sure every use of it exists because Try this generated it when someone typed ring

[Jireh Loreaux]

my brain really wants "crnf" to mean "carriage return / newline feed" :laughing:

[Heather Macbeth]

To return to the original problem, you don't need to state some fact like (4 : zmod 7) = -3 that's particularly relevant to the problem. You can just write out whatever the defining features of your ring are and then include them in your linear_combination calculation.

lemma lemma2 (a b : ZMod 7) (h : a + 3 * b = 0) : a = 4 * b := by
  have h2 : (7:ZMod 7) = 0 := rfl
  linear_combination h - b * h2

[Heather Macbeth]

See also the discussion for $\mathbb{C}$ at
https://hrmacbeth.github.io/computations_in_lean/02_Using_Polyrith.html#isometries-of-the-complex-plane

[Anne Baanen]

My tactic is now PR'd as #5376!

[Yury G. Kudryashov]

In Coq (note: I don't know the details), tactics like ring and field allow type-specific plugins for things like IsNumeral and "is n = m?"

[Yury G. Kudryashov]

I guess, mathlib uses norm_num for this and only deals rational constants.

[Yury G. Kudryashov]

Is it possible to write a norm_num plugins that knows about CharP?

[Yury G. Kudryashov]

Disclaimer: I know nothing about internals of norm_num.

[Mario Carneiro]

depends on what you mean, what is triggering the plugin to be called?

[Yury G. Kudryashov]

E.g., ring wants to know whether 2 = 5 or not

[Yury G. Kudryashov]

Or ring never wants this, it wants to normalize the coefficient?

[Mario Carneiro]

that's right

[Yury G. Kudryashov]

Can we have some normalize operation with plugins, then? (Part of) #5376 can be one of them.

[Mario Carneiro]

most likely this can't be done with plugins, you would need to change parts of the core

[Mario Carneiro]

I think that has the same issue, what induces the plugin to be called? Why is it not calling all plugins on every number all the time?

[Mario Carneiro]

there needs to be some kind of trigger which isn't always true

[Yury G. Kudryashov]

Can it call all plugins on the final result of the computation in Rat? Or will it be too slow?

[Yury G. Kudryashov]

(e.g., since failing an instance search for CharP can be slow)

[Mario Carneiro]

how final is final? Anything that is happening inside ring is called a ton of times

[Mario Carneiro]

note that in lean 3 there was a separate tactic norm_fin that handled this reasoning

[Anne Baanen]

Yury G. Kudryashov said:

In Coq (note: I don't know the details), tactics like ring and field allow type-specific plugins for things like IsNumeral and "is n = m?"

This is one of the reasons I implemented reduce_mod_char, Assia was somewhat shocked that this functionality wasn't available in our ring :)

[Anne Baanen]

If I recall correctly, in Coq the user specifies which coefficients to use in a call to ring. Based on some quick Lean 3 experiments, it should be possible in our implementation to define a record with info on how to recognize/add/subtract/multiply coefficients, and a zero-test. If the user writes ring, we put the ℚ version of this record, if the user writes ring zmod 5 we use zmod 5, etc.

[Anne Baanen]

reduce_mod_char is more like norm_fin in that it looks at the type to figure out the characteristic, rather than using typeclass inference. Unlike norm_fin, reduce_mod_char also supports polynomials over zmod n, etc.

[Eric Rodriguez]

Is it easy to write override this in case it can't be figured out, e.g. reduce_mod_char p will use inference to find the right instance?

[Anne Baanen]

The problem isn't so much figuring out the characteristic of a single expression, as it is figuring out which subexpressions are eligible for rewriting. I suppose we could a heuristic to drill down to the "interesting" expressions (e.g. if we see $a = $b, try $a and $b) and then try rewriting any of their subexpressions with the same type. But that seems quite fragile: what if we want to show Polynomial.natDegree ((3 * X^3 : (ZMod 3)[X]) = 0?

[Eric Rodriguez]

I'm suggesting a mixed approach - the approach you suggest usually, but if you are given an explicit p, then assume all expressions containing any sort of numeral could be subject to this and look at typeclass search.

[Eric Rodriguez]

Because as I see it, this approach doesn't work if you're working over K [char_p p K]

[Johan Commelin]

It was discussed to make p an outparam of CharP. That would help here, right?

[Anne Baanen]

Johan Commelin said:

It was discussed to make p an outparam of CharP. That would help here, right?

I certainly expect it would not hurt, although Lean 4 is slightly more willing to find instances when there are still metavariables in the goal.

[Alex J. Best]

@Anne Baanen does reduce_mod_char normalize rational expressions too btw?

[Anne Baanen]

There is no special handling for those, beyond using norm_num's machinery to parse expressions. Could you give an example of something you'd like the tactic to handle?

[Alex J. Best]

E.g. to turn (1 : Zmod 2)/ 3 into 1 (or more interestingly for larger numbers of course!
Maybe that one already works actually. But (1 : Zmod 5)/ 2 into 3 would be non-trivial

[Anne Baanen]

That's indeed along the same lines as I was thinking, thanks for confirming! I couldn't actually figure out how to make (1 : Zmod 5)/ 2 elaborate correctly, there is no HDiv instance and adding a Fact (Prime 5) hypothesis didn't seem to help...

[Johan Commelin]

But that should yield a field instance, shouldn't it?

[Johan Commelin]

Sounds like a bug

[Johan Commelin]

import Mathlib.Data.ZMod.Basic
import Mathlib.Tactic.FieldSimp

example (p : ℕ) [Fact p.Prime] : Field (ZMod p) := inferInstance

example [Fact (Nat.Prime 5)] : (1 : ZMod 5) / 2 = 3 := by
  have : (2 : ZMod 5) ≠ 0 := ne_of_beq_false rfl
  field_simp
  rfl

[Johan Commelin]

Probably Prime was not elaborating to Nat.Prime in your example

[Anne Baanen]

I indeed forgot Nat.Prime != Prime :sweat_smile:

[Anne Baanen]

(Now that docs#Nat.Prime is defined in terms of the ring structure, would it be worth removing it altogether to avoid this kind of confusion?)

[Johan Commelin]

But it is defined to be Irreducible, right?

[Anne Baanen]

Oh yeah... I suppose that matches more closely with the standard notion of "only divisible by 1 and itself". Looks like one year ago the plan was to get rid of Nat.Prime altogether: https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.2312709.20-.20redefine.20nat.2Eprime.20as.20prime