## 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


#### 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?

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 ns

#### 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

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

#### 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:

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: