Zulip Chat Archive

Stream: maths

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


view this post on Zulip Kevin Buzzard (Apr 15 2020 at 17:07):

If x,yZx,y\in\mathbb{Z} and x22y2=10003x^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 x2y21x^2\equiv y^2\equiv1 mod 4 and hence both xx and yy 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 x22y2x^2-2y^2 is 2 mod 4. I really want to drop straight into Z/4Z\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?

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Apr 15 2020 at 17:29):

although you will have to do something extra to get 10003 to simplify to 3

view this post on Zulip 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.

view this post on Zulip Kenny Lau (Apr 15 2020 at 17:30):

thank the lord that these are not natural numbers

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Apr 15 2020 at 17:33):

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

view this post on Zulip Mario Carneiro (Apr 15 2020 at 17:34):

for q2, you might be able to use dec_trivial

view this post on Zulip Mario Carneiro (Apr 15 2020 at 17:34):

if you revert x4 and y4

view this post on Zulip Johan Commelin (Apr 15 2020 at 17:34):

Why is that not exact_mod_cast h?

view this post on Zulip Mario Carneiro (Apr 15 2020 at 17:35):

it probably is that too

view this post on Zulip Mario Carneiro (Apr 15 2020 at 17:35):

well, you still have to use congr_arg (or apply_fun) on h

view this post on Zulip 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

view this post on Zulip Kenny Lau (Apr 15 2020 at 17:39):

where are my decidable equalities on zmod 4

view this post on Zulip 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

view this post on Zulip Kenny Lau (Apr 15 2020 at 17:40):

oh, I misread the question

view this post on Zulip 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

view this post on Zulip 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 (x1[ZMOD((4:ℕ+):)]  x3[ZMOD((4:ℕ+):)])  (y1[ZMOD((4:ℕ+):)]  y3[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

view this post on Zulip 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?

view this post on Zulip Kenny Lau (Apr 15 2020 at 17:55):

oh right

view this post on Zulip 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.

view this post on Zulip Kenny Lau (Apr 15 2020 at 18:02):

it looks like there is not much communication between different zmod ns

view this post on Zulip Johan Commelin (Apr 15 2020 at 18:03):

Sounds like a good starter project

view this post on Zulip 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

view this post on Zulip 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 x1[ZMOD((2:ℕ+):)]  y1[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

view this post on Zulip Johan Commelin (Apr 15 2020 at 18:30):

@Kenny Lau Your tactic is called norm_cast or push_cast

view this post on Zulip 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

view this post on Zulip Kenny Lau (Apr 15 2020 at 19:52):

oh wow the Lean translation is out

view this post on Zulip Kenny Lau (Apr 15 2020 at 19:52):

I did it in Coq

view this post on Zulip Kevin Buzzard (Apr 15 2020 at 19:53):

I think my solution is better than everyone else's

view this post on Zulip Kevin Buzzard (Apr 15 2020 at 19:53):

Which is an extremely rare occurrence

view this post on Zulip 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

view this post on Zulip Kenny Lau (Apr 15 2020 at 19:59):

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

view this post on Zulip Kenny Lau (Apr 15 2020 at 20:00):

wow, monadius learnt Lean?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 15 2020 at 20:09):

I'll get back to it later

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Apr 15 2020 at 21:04):

sigh

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

view this post on Zulip Kevin Buzzard (Apr 15 2020 at 21:06):

val_cast_nat or eq_iff_modeq_int

view this post on Zulip 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