check all the cases mod 4

Stream: Is there code for X?

[Kevin Buzzard]

This is more annoying than I want it to be. What tricks am I missing? The proof is "check all the cases mod 4".

import tactic
import data.zmod.basic

-- This was a mild pain. Can it be golfed?
lemma x_eq_1_zmod4 (x y : ℤ) (h : y^2 ≡ x^3 - 5 [ZMOD 4]) :
  (x ≡ 1 [ZMOD 4]) :=
begin
  -- It's a finite check!
  change _ ≡ _ [ZMOD (4 : ℕ)] at h,
  change _ ≡ _ [ZMOD (4 : ℕ)],
  rw ← zmod.int_coe_eq_int_coe_iff at h ⊢,
  push_cast at h ⊢,
  revert h, -- generalize misbehaves otherwise?
  generalize : (↑x : zmod 4) = xbar,
  generalize : (↑y : zmod 4) = ybar,
  intro h,
  -- aaand...just check all the cases!
  dec_trivial!,
end

-- idea for removing `change`

notation a ` ≡ `:50 b ` [ZMOD' `:50 n `]`:0 := int.modeq ((n : ℕ) : ℤ) a b

example (x y : ℤ) (h : y^2 ≡ x^3 - 5 [ZMOD' 4]) :
  (x ≡ 1 [ZMOD' 4]) :=
begin
  rw ← zmod.int_coe_eq_int_coe_iff at h ⊢,
  push_cast at h ⊢,
  revert h,
  generalize : (↑x : zmod 4) = xbar,
  generalize : (↑y : zmod 4) = ybar,
  intro h,
  dec_trivial!,
end

[Kevin Buzzard]

A related thing that came up when thinking about this: The maths proof of the below is "(note that p is odd)".

import tactic
import data.zmod.basic

lemma annoying
  (p : ℕ)
  [fact (nat.prime p)]
  (h8 : p ≡ 3 [MOD 4]) :
  1 / (4 : zmod p) ≠ 0 :=
begin
  suffices : (4 : zmod p) ≠ 0, simpa, -- put there so nobody can cheat and remove the `fact`
  have hpne2 : p ≠ 2,
  { unfreezingI {rintro rfl},
    delta nat.modeq at h8,
    norm_num at h8, },
  intro h,
  have h3 : p ∣ 4 := (zmod.nat_coe_zmod_eq_zero_iff_dvd 4 p).mp (by assumption_mod_cast),
  have h4 : p ≤ 4 := nat.le_of_dvd (by norm_num) h3,
  have h5 : p ≠ 4,
  { unfreezingI {rintro rfl}, have : nat.prime 4 := fact.out _, norm_num at this, },
  delta nat.modeq at h8,
  rw nat.mod_eq_of_lt (lt_of_le_of_ne h4 h5) at h8,
  unfreezingI {subst h8},
  norm_num at h3,
end

[Damiano Testa]

The first lemma can be proved as follows:

import tactic
import data.zmod.basic

lemma x_eq_1_zmod4_aux (x y : zmod 4) (h : y^2 = x^3 - 5) :
  (x = 1) :=
by dec_trivial!

lemma pro (x y : ℤ) (n : ℕ) :
  (x ≡ y [ZMOD n]) ↔ (x : zmod n) = y :=
by rw [zmod.int_coe_eq_int_coe_iff_dvd_sub, int.modeq_iff_dvd]

-- This was a mild pain. Can it be golfed?
lemma x_eq_1_zmod4 (x y : ℤ) (h : y^2 ≡ x^3 - 5 [ZMOD 4]) :
  (x ≡ 1 [ZMOD 4]) :=
begin
  refine (pro x 1 4).mpr ( x_eq_1_zmod4_aux x y _),
  convert (pro _ _ 4).mp h;
  simp,
end

You can also compress the last to a single line, if you really want to:

lemma x_eq_1_zmod4 (x y : ℤ) (h : y^2 ≡ x^3 - 5 [ZMOD 4]) :
  (x ≡ 1 [ZMOD 4]) :=
(pro _ _ _).mpr (x_eq_1_zmod4_aux x y (by convert (pro _ _ _).mp h; simp))

[Damiano Testa]

This is also a possibility for the second one:

lemma annoying
  (p : ℕ)
  [fact (nat.prime p)]
  (h8 : p ≡ 3 [MOD 4]) :
  1 / (4 : zmod p) ≠ 0 :=
begin
  suffices : (4 : zmod p) ≠ 0, simpa, -- put there so nobody can cheat and remove the `fact`
  suffices : (2 : zmod p) ^ 2 ≠ 0, norm_num at this,
  apply pow_ne_zero,
  convert zmod.prime_ne_zero p 2 _,
  { norm_num },
  { intros p2,
    rw p2 at h8,
    exfalso,
    refine not_ne_iff.mpr h8 _,
    norm_num }
end

Not sure if it is really better.

[Stuart Presnell]

This can probably be tidied up a bit:

lemma annoying
  (p : ℕ)
  [fact (nat.prime p)]
  (h8 : p ≡ 3 [MOD 4]) :
  1 / (4 : zmod p) ≠ 0 :=
begin
  suffices : (4 : zmod p) ≠ 0, simpa, -- put there so nobody can cheat and remove the `fact`
  suffices : ¬ p ∣ 4, { rw ←zmod.nat_coe_zmod_eq_zero_iff_dvd at this, simpa using this },

  intro hp4,
  have hp3 : p ∣ 3,
  { apply nat.dvd_of_mod_eq_zero,
    rw [eq_comm, ←nat.mod_self p],
    exact nat.modeq.modeq_of_dvd hp4 h8 },
  have hp1 := nat.dvd_gcd_iff.2 ⟨hp3, hp4⟩,
  norm_num at hp1,

  apply nat.not_prime_one,
  rw ←hp1,
  apply fact_iff.1,
  assumption,
end