Missing zmod lemma?

Stream: new members

[Michael Stoll]

Not sure if this is the right stream for this question... (I'm still thinking of myself as a new member, though).
We have (in data.zmod.basic) the following

 theorem zmod.int_coe_eq_int_coe_iff (a b : ℤ) (c : ℕ) : ↑a = ↑b ↔ a ≡ b [ZMOD ↑c]
 theorem zmod.int_coe_eq_int_coe_iff' (a b : ℤ) (c : ℕ) : ↑a = ↑b ↔ a % ↑c = b % ↑c
 theorem zmod.int_coe_zmod_eq_zero_iff_dvd (a : ℤ) (b : ℕ) : ↑a = 0 ↔ ↑b ∣ a

but I cannot seem to find

theorem zmod.int_coe_eq_int_coe_iff_dvd_sub (a b : ℤ) (c : ℕ) : ↑a = ↑b ↔ ↑c ∣ a-b

(which would be useful to have). Is there a reason why this is missing?

[Michael Stoll]

(Also, the naming of the results is not completely consistent; the last one has an additional _zmod...)

[Alex J. Best]

This is an ok place for the question, but #general or #Is there code for X? would also be ok for it.
I don't think there is any particular reason it is missing, most likely nobody needed precisely that lemma (or they just rewrote with docs#sub_eq_zero and used one of the ones you mentioned instead). Seems like a useful enough lemma to add to mathlib. Removing the zmod would also be welcome I'm sure

[Michael Stoll]

So how does this work? Do I wait and hope that somebody adds it eventually, or can/should I do it myself? In the latter case, I'll need some help, since I have never used github so far.
But probably this would be a good opportunity to learn how to do it, since I'll most likely want to add stuff to mathlib at some point.

[Michael Stoll]

I'm not sure about removing the _zmod, though, since I'd be afraid this could break code that uses the present name.

[Alex J. Best]

You can do it, this would be a nice first PR to mathlib I think, to get used to the workflow.
We have some instructions at https://leanprover-community.github.io/contribute/index.html, but the upshot is you can ask here for push access to the mathlib git repository (and give your github username). Then you push your updates to a branch of the leanprover-community/mathlib repo (using git) and create a PR for that branch (using the github website).

As for breaking existing code, we have continuous integration tools that will check that all of mathlib still builds with your changes, so that is fine (some things may need fixing as part of the PR but any breakage will be discovered). As for external projects there is potential for breakage when they update, but we try and smooth that by having tools to let people know about breaking changes, rather than by not making breaking changes, mathlib has very little in the way of backwards compatibility guarentees.

[Michael Stoll]

OK, thanks for the pointer! I'll have a look at how this works (but maybe not today...).

[Eric Wieser]

Does this lemma exist if you apply one of the first two lemmas you mention first?

[Eric Wieser]

maybe docs#int.dvd_sub?

[Eric Wieser]

a ≡ b [ZMOD c] ↔ c ∣ a-b

Is probably the lemma I would expect to have

[Yaël Dillies]

docs#int.modeq_iff_dvd

[Michael Stoll]

I think all these equivalences should be available.

[Eric Wieser]

Aren't you effectively stating that every lemma with a ≡ b [ZMOD c] on the LHS should have an analogous lemma about zmod?

[Michael Stoll]

Why not? The zmod version seems more useful to me, since zmod n is a finite ring (which allows for example the use of dec_trivial to prove statements [as I recently learned]).

[Michael Stoll]

Another question: How do I get

@[simp]
lemma zmod.coe_self_eq_zero (a : ℕ) : (a : zmod a) = 0 := by rw zmod.nat_coe_zmod_eq_zero_iff_dvd

to apply to (say) (2 : zmod 2)? The problem seems to be that 2 : zmod 2 is not the same as (2 : nat) : zmod 2.

[Kyle Miller]

Michael Stoll said:

(which allows for example the use of dec_trivial to prove statements [as I recently learned]).

In principle, dec_trivial can prove things about ZMOD too, and it might just be a matter of missing decidable instances.

[Michael Stoll]

Well, I guess it is good to have flexibility, so have both!

[Kevin Buzzard]

Michael Stoll said:

Another question: How do I get

@[simp]
lemma zmod.coe_self_eq_zero (a : ℕ) : (a : zmod a) = 0 := by rw zmod.nat_coe_zmod_eq_zero_iff_dvd

to apply to (say) (2 : zmod 2)? The problem seems to be that 2 : zmod 2 is not the same as (2 : nat) : zmod 2.

Yeah, good question. For numerals the way people usually do things is to prove results for bit0 and bit1. You can set_option pp.numerals false to see what Lean actually sees.

[Michael Stoll]

This kind of stumbling block is something I have repeatedly hurt my feet on. It would be nice if there were some kind of automatic coercion of numerals...

[Kevin Buzzard]

I think in Lean 4 they completely overhauled numerals.

[Kyle Miller]

Do tactic#norm_num or tactic#norm_cast work for you to normalize the numerals?

[Michael Stoll]

Instead of simp, I can do rw [(by norm_cast : (2 : zmod 2) = ((2 : ℕ) : zmod 2)), zmod.coe_self_eq_zero]. But I would rather want to have simp do that automatically.

[Kyle Miller]

Kevin Buzzard said:

I think in Lean 4 they completely overhauled numerals.

I'm probably misunderstanding it, but the mental model I have was that all numerals will be in "(2 : nat) : zmod 2" form

[Michael Stoll]

In that case, it should work, but it doesn't.

[Kevin Buzzard]

it should work in Lean 4 -- we're all using Lean 3

[Kyle Miller]

Regarding zmod.coe_self_eq_zero, I think that sort of lemma is more under the purview of norm_num. It can't normalize 2 : zmod 2 yet, but it's a matter of creating a norm_num tactic using code from norm_fin.

Here's a hack though:

meta def by_norm_cast : tactic unit := `[norm_cast]

lemma zmod.coe_self_eq_zero (a : ℕ) (a' : zmod a) (h : a' = a . by_norm_cast) :
  a' = 0 :=
begin
  change a' = a at h,
  rw [h, zmod.nat_coe_zmod_eq_zero_iff_dvd],
end

example : (2 : fin 2) = 0 :=
begin
  rw zmod.coe_self_eq_zero 2 2,
end

[Michael Stoll]

Would this work as a simp lemma?

[Kevin Buzzard]

(deleted)

[Michael Stoll]

Coming back to the original topic, I would like to add this lemma (and change the names of two by removing "_zmod") to see how the process works. Can someone give me permission to push a branch? I'm MichaelStollBayreuth on Github. Thanks!

[Bryan Gin-ge Chen]

Michael Stoll said:

Coming back to the original topic, I would like to add this lemma (and change the names of two by removing "_zmod") to see how the process works. Can someone give me permission to push a branch? I'm MichaelStollBayreuth on Github. Thanks!

Invite sent! https://github.com/leanprover-community/mathlib/invitations

[Michael Stoll]

Thanks!

[Michael Stoll]

The PR is #12944. It is just the lemma with a one-line proof (after a suggestion by @Eric Wieser ).

[Eric Wieser]

Looks like 3 lines to me ;). You could use by rw ... instead of begin rw ... end next time to save two lines

[Michael Stoll]

Actually, it adds four lines...
What is the recommended style here, use begin ... end or by ... if it is a one-line proof?

[Eric Rodriguez]

by ... for one-liners, not for twopliners