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: