# Zulip Chat Archive

## Stream: maths

### Topic: quickest way to kill "trivial mod N"?

#### Kevin Buzzard (Apr 15 2020 at 17:07):

If $x,y\in\mathbb{Z}$ and $x^2-2y^2=10003$ then, because squares are 0 or 1 mod 4 and the RHS is 3 mod 4, we see that we must have $x^2\equiv y^2\equiv1$ mod 4 and hence both $x$ and $y$ are 1 or 3 mod 4. I want the proof of this to go "check all 16 cases mod 4; oh look, 12 of them don't work". I've been using `interval_cases`

to get break down to cases like `x % 4 = 2`

and `y % 4 = 1`

but then it's a bore showing that $x^2-2y^2$ is 2 mod 4. I really want to drop straight into $\mathbb{Z}/4\mathbb{Z}$ and do all the arithmetic in there. Ideally in general I'd say "consider this equation mod N" (for some small N) and then end up with d<=N^2 goals corresponding to all the possibilities of x and y mod N which satisfy the equation mod N. Is there a painless way of doing this without having to repeatedly apply `int.modeq.modeq_mul`

etc?

#### Mario Carneiro (Apr 15 2020 at 17:28):

It seems like you should be able to apply `coe : int -> zmod 4`

and then `simp`

it down to the leaves

#### Mario Carneiro (Apr 15 2020 at 17:29):

although you will have to do something extra to get `10003`

to simplify to `3`

#### Kevin Buzzard (Apr 15 2020 at 17:29):

oh the number doesn't have to be big, I just wanted to stop people trying to come up with other methods.

#### Kenny Lau (Apr 15 2020 at 17:30):

thank the lord that these are not natural numbers

#### Kevin Buzzard (Apr 15 2020 at 17:30):

example (x y : ℤ) (h : x^2+2*y^2+x=123) : false := begin set x4 : zmod 4 := x, set y4 : zmod 4 := y, have h4 : x4^2+2*y4^2+x=123, sorry, sorry end

How do I get h4?

#### Mario Carneiro (Apr 15 2020 at 17:31):

it's not so much about the fact that they are big numbers but rather that we expect numerals to be reduced mod the base while simp only pushes the coe down

#### Kevin Buzzard (Apr 15 2020 at 17:31):

I think Q1 is how to prove h4 from h, and Q2 is how to do the case split on the fintype.

#### Mario Carneiro (Apr 15 2020 at 17:33):

I think `simpa using congr_arg (coe : int -> zmod 4) h`

#### Mario Carneiro (Apr 15 2020 at 17:34):

for q2, you might be able to use dec_trivial

#### Mario Carneiro (Apr 15 2020 at 17:34):

if you revert `x4`

and `y4`

#### Johan Commelin (Apr 15 2020 at 17:34):

Why is that not `exact_mod_cast h`

?

#### Mario Carneiro (Apr 15 2020 at 17:35):

it probably is that too

#### Mario Carneiro (Apr 15 2020 at 17:35):

well, you still have to use `congr_arg`

(or `apply_fun`

) on `h`

#### Kenny Lau (Apr 15 2020 at 17:39):

import data.zmod.basic universe u example (x y : ℤ) (H : x^2 - 2*y^2 = 10003) : false := begin apply_fun (coe : ℤ → zmod 4) at H, rw ← zmod.cast_mod_int 4 10003 at H, have h1 : (10003 % ((4:ℕ+):ℕ) : ℤ) = 3, norm_num, rw h1 at H, clear h1, push_cast at H, generalize_hyp : (x : zmod 4) = x4 at H, generalize_hyp : (y : zmod 4) = y4 at H, clear x y, /- revert x4 y4, exact dec_trivial -- why doesn't this work -/ fin_cases x4; fin_cases y4; exact absurd H dec_trivial -- why doesn't this work end

#### Kenny Lau (Apr 15 2020 at 17:39):

where are my decidable equalities on zmod 4

#### Alex J. Best (Apr 15 2020 at 17:40):

example (x y : ℤ) (h : x^2 - 2*y^2 = 10003) : (((x : zmod 4) = 1) ∨ ((x : zmod 4) = 3)) ∧ (((y : zmod 4) = 1) ∨ ((y : zmod 4) = 3)) := begin replace h := congr_arg (coe : ℤ → zmod 4) h, push_cast at h, revert h, generalize : (↑x : zmod 4) = X, generalize : (↑y : zmod 4) = Y, revert X Y, exact dec_trivial, end

#### Kenny Lau (Apr 15 2020 at 17:40):

oh, I misread the question

#### Mario Carneiro (Apr 15 2020 at 17:44):

I feel like there should be a way to combine `generalize`

and `revert`

in Alex's proof

#### Kenny Lau (Apr 15 2020 at 17:45):

import data.zmod.basic universe u example (x y : ℤ) (H : x^2 - 2*y^2 = 10003) : (x%4=1 ∨ x%4=3) ∧ (y%4=1 ∨ y%4=3) := begin apply_fun (coe : ℤ → zmod 4) at H, rw ← zmod.cast_mod_int 4 10003 at H, have h1 : (10003 % ((4:ℕ+):ℕ) : ℤ) = 3, norm_num, rw h1 at H, clear h1, change (x≡1[ZMOD((4:ℕ+):ℕ)] ∨ x≡3[ZMOD((4:ℕ+):ℕ)]) ∧ (y≡1[ZMOD((4:ℕ+):ℕ)] ∨ y≡3[ZMOD((4:ℕ+):ℕ)]), iterate 4 { rw ← zmod.eq_iff_modeq_int }, push_cast at H, revert H, generalize : (x : zmod 4) = x4, generalize : (y : zmod 4) = y4, clear x y, revert x4 y4, exact dec_trivial end

#### Johan Commelin (Apr 15 2020 at 17:54):

Isn't `(x%4=1 ∨ x%4=3) ∧ (y%4=1 ∨ y%4=3)`

a very complicated way of saying `x%2 = 1`

and `y%2 = 1`

?

#### Kenny Lau (Apr 15 2020 at 17:55):

oh right

#### Reid Barton (Apr 15 2020 at 17:56):

Yes but somehow it's an extra ingredient that x^2 mod 4 only depends on x mod 2.

#### Kenny Lau (Apr 15 2020 at 18:02):

it looks like there is not much communication between different `zmod n`

s

#### Johan Commelin (Apr 15 2020 at 18:03):

Sounds like a good starter project

#### Kenny Lau (Apr 15 2020 at 18:18):

theorem zmod_communication {m n : ℕ+} (h : m ∣ n) (x : ℤ) : (zmod.cast (x : zmod n) : zmod m) = x := let ⟨k, hk⟩ := h in suffices ((((x:zmod n).val:ℕ):ℤ) : zmod m) = x, by rwa [← coe_coe] at this, by rw [zmod.coe_val_cast_int, zmod.eq_iff_modeq_int]; exact int.mod_mod_of_dvd _ ⟨k, by exact_mod_cast hk⟩

#### Kenny Lau (Apr 15 2020 at 18:21):

import data.zmod.basic universe u theorem zmod_communication {m n : ℕ+} (h : m ∣ n) (x : ℤ) : (zmod.cast (x : zmod n) : zmod m) = x := let ⟨k, hk⟩ := h in suffices ((((x:zmod n).val:ℕ):ℤ) : zmod m) = x, by rwa [← coe_coe] at this, by rw [zmod.coe_val_cast_int, zmod.eq_iff_modeq_int]; exact int.mod_mod_of_dvd _ ⟨k, by exact_mod_cast hk⟩ example (x y : ℤ) (H : x^2 - 2*y^2 = 10003) : x%2=1 ∧ y%2=1 := begin apply_fun (coe : ℤ → zmod 4) at H, rw ← zmod.cast_mod_int 4 10003 at H, have h1 : (10003 % ((4:ℕ+):ℕ) : ℤ) = 3, norm_num, rw h1 at H, clear h1, change x≡1[ZMOD((2:ℕ+):ℕ)] ∧ y≡1[ZMOD((2:ℕ+):ℕ)], iterate 2 { rw ← zmod.eq_iff_modeq_int }, iterate 3 { rw ← @zmod_communication 2 4 ⟨2, rfl⟩ }, -- you can make a tactic out of this revert H, push_cast, generalize : (x : zmod 4) = x4, generalize : (y : zmod 4) = y4, revert x4 y4, exact dec_trivial end

#### Johan Commelin (Apr 15 2020 at 18:30):

@Kenny Lau Your tactic is called norm_cast or push_cast

#### Kevin Buzzard (Apr 15 2020 at 19:50):

@Kenny Lau do the kata about sum of cubes being square of sum of numbers on codewars and then see my solution

#### Kenny Lau (Apr 15 2020 at 19:52):

oh wow the Lean translation is out

#### Kenny Lau (Apr 15 2020 at 19:52):

I did it in Coq

#### Kevin Buzzard (Apr 15 2020 at 19:53):

I think my solution is better than everyone else's

#### Kevin Buzzard (Apr 15 2020 at 19:53):

Which is an extremely rare occurrence

#### Chris Hughes (Apr 15 2020 at 19:58):

example (x y : ℤ) (H : x^2 - 2*y^2 = 10003) : false := suffices ∀ x y : zmod 4, x^2 - 2 * y^2 ≠ 10003, from this x y (by norm_cast; rw H; simp), dec_trivial

#### Kenny Lau (Apr 15 2020 at 19:59):

@Kevin Buzzard I translated my Coq solution into Lean and posted it

#### Kenny Lau (Apr 15 2020 at 20:00):

wow, monadius learnt Lean?

#### Kevin Buzzard (Apr 15 2020 at 20:08):

I don't have to fart around trying to get a 2 next to my sum from 1 to n, because it's now painless to work in the rationals because of push_cast

#### Kevin Buzzard (Apr 15 2020 at 20:09):

Thanks for all these ideas. I'm doing real life stuff at the minute so haven't had a chance to look at any of them but I'm trying to create a kata

#### Kevin Buzzard (Apr 15 2020 at 20:09):

I'll get back to it later

#### Andrew Ashworth (Apr 15 2020 at 20:42):

Kenny Lau said:

wow, monadius learnt Lean?

His LinkedIn profile is too intimidating... apparently he was a PhD student and postdoc with both Tom Hales and Georges Gonthier...

#### Kevin Buzzard (Apr 15 2020 at 20:54):

@Chris Hughes and @Alex J. Best this is great, thanks a lot. Kenny, your code looks like mine (in fact mine looks worse), which is exactly why I asked. Chris' method is exactly what I need in my use case.

#### Kevin Buzzard (Apr 15 2020 at 21:04):

*sigh*

example (a : ℤ) (h : (a : zmod 4) = 3) : a % 4 = 3 := sorry

#### Kevin Buzzard (Apr 15 2020 at 21:06):

`val_cast_nat`

or `eq_iff_modeq_int`

#### Jesse Michael Han (Apr 15 2020 at 21:15):

Andrew Ashworth said:

Kenny Lau said:

wow, monadius learnt Lean?

His LinkedIn profile is too intimidating... apparently he was a PhD student and postdoc with both Tom Hales and Georges Gonthier...

alexey is part of this chat

Last updated: May 18 2021 at 08:14 UTC