modneq notation pull request

Stream: new members

[Alfredo]

Hello there, i am not sure if i am in the right place to ask but i am planning on submitting a pretty simple PR contribution to mathlib and i will like someone with more experience to take a look : https://github.com/oxarbitrage/mathlib/pull/1 . Any feedback will be very appreciated.

[Kyle Miller]

I might suggest defining it as

notation a ` ≢ `:50 b ` [MOD `:50 n `]`:0 := ¬ (a ≡ b [MOD n])

since that way the modeq will directly be visible to rw and simp.

Or, if you do want modneq as a def of its own (for example, if you want dot notation to work for it), you can follow how neq works here and do

@[reducible] def modneq (n a b : ℕ) := ¬ (a ≡ b [MOD n])
notation a ` ≢ `:50 b ` [MOD `:50 n `]`:0 := modneq n a b

The reducible makes it so that things can see through the definition. (You shouldn't don't need @[derive decidable] when you have this attribute.)

[Kyle Miller]

In either case, I think it would be better if the a % n ≠ b % n form were some sort of "modneq_iff" lemma rather than being the definition itself since you want modneq to transparently be that it's not modeq.

[Eric Wieser]

Note also that you have not made this PR in a way that it can actually be merged; make sure to read or contribution guidelines

[Alfredo]

Note also that you have not made this PR in a way that it can actually be merged; make sure to read or contribution guidelines

I think i did, besides not having the PR pointing to the mathlib repository what do i have missing ?

[Mauricio Collares]

Your shouldn't push to a fork for CI reasons. That is, your PR source branch must be a part of leanprover-community/mathlib itself. Maintainers can grant you permission to push to non-master branches if you don't have it already.

[Alfredo]

Thank you for the suggestions Kyle, i agree with it. I made some changes so now i have it as:

@[reducible] def modneq (n a b : ℕ) := ¬ (a ≡ b [MOD n])

notation a ` ≢ `:50 b ` [MOD `:50 n `]`:0 := modneq n a b

lemma modneq.def (n a b : ℕ): a % n ≠ b % n = ¬ (a ≡ b [MOD n]) := rfl

The modneq.def is similar to https://github.com/leanprover-community/lean/blob/68455b087d87e9dc3f736da0de95807e05260460/library/init/logic.lean#L103

However, it requires a bit more effort to prove:

example : 15 ≡ 3 [MOD 12] := by norm_num [modeq]
example : 19 ≢ 6 [MOD 11] :=
begin
  rw [modneq, ←modneq.def],
  norm_num,
end

Ill keep trying but let me know how do you see it

[Alfredo]

Thank you @Mauricio Collares i think i do have permissions already, i submitted a PR a few months ago iirc

[Alfredo]

I did on my own fork because i wanted to show the idea first, if it was a bad one i didnt wanted people on mathlib wasting time reviewing it

[Alfredo]

i will push directly the next time

[Mauricio Collares]

That's fair! But I think marking your PR as a Draft has the same meaning

[Alfredo]

maybe as a draft pull request

[Alfredo]

right, agree, thanks

[Alfredo]

ill do that now

[Alfredo]

So, here it is now, thanks again @Mauricio Collares https://github.com/leanprover-community/mathlib/pull/14682

[Kyle Miller]

@Alfredo You might like to have this too:

lemma modneq_iff(n a b : ℕ) : a ≢ b [MOD n] ↔ a % n ≠ b % n := rfl

That way you can rewrite in one step.

[Alfredo]

great, with that we can do:

example : 19 ≢ 6 [MOD 11] := by norm_num [modneq_iff],

[Eric Wieser]

modneq.def looks like a weird lemma to have, we don't normally write lemmas about equality of props

[Alfredo Garcia]

removed modneq.def then changed the PR from the draft state: https://github.com/leanprover-community/mathlib/pull/14682

[Alfredo Garcia]

thank you Eric for all the help, looks great now.