quickest way to kill "trivial mod N"?

Stream: maths

[Kevin Buzzard]

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]

It seems like you should be able to apply coe : int -> zmod 4 and then simp it down to the leaves

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Kenny Lau]

thank the lord that these are not natural numbers

[Kevin Buzzard]

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]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

for q2, you might be able to use dec_trivial

[Mario Carneiro]

if you revert x4 and y4

[Johan Commelin]

Why is that not exact_mod_cast h?

[Mario Carneiro]

it probably is that too

[Mario Carneiro]

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

[Kenny Lau]

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]

where are my decidable equalities on zmod 4

[Alex J. Best]

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]

oh, I misread the question

[Mario Carneiro]

I feel like there should be a way to combine generalize and revert in Alex's proof

[Kenny Lau]

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]

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]

oh right

[Reid Barton]

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

[Kenny Lau]

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

[Johan Commelin]

Sounds like a good starter project

[Kenny Lau]

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]

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]

@Kenny Lau Your tactic is called norm_cast or push_cast

[Kevin Buzzard]

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

[Kenny Lau]

oh wow the Lean translation is out

[Kenny Lau]

I did it in Coq

[Kevin Buzzard]

I think my solution is better than everyone else's

[Kevin Buzzard]

Which is an extremely rare occurrence

[Chris Hughes]

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]

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

[Kenny Lau]

wow, monadius learnt Lean?

[Kevin Buzzard]

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]

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]

I'll get back to it later

[Andrew Ashworth]

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]

@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]

sigh

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

[Kevin Buzzard]

val_cast_nat or eq_iff_modeq_int

[Jesse Michael Han]

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