Zulip Chat Archive

Stream: maths

Topic: Proving congruences by cases

Filippo A. E. Nuccio (Dec 15 2023 at 18:04):

With @Cyril Cohen we were discussing about how nice the proof that a natural that is a square and a cube is either $0$ or $1$ modulo $7$ can be made. He had a super-cool 3-lines proof in Coq, and challenged me on Lean. I came up with the following one, and I would be happy to see some :golf: :

example (a b c : ℕ) (hab : a = b^3) (hac : a=c^2) : (a % 7 = 1 ∨ a % 7 = 0) := by
  have hb1 := (b % 7).zero_le
  have hb2 : (b % 7) < 7 := Nat.mod_lt _ (by linarith)
  have hc1 := (c % 7).zero_le
  have hc2 : (c % 7) < 7 := Nat.mod_lt _ (by linarith)
  have : (a % 7 = 1 ∨ a % 7 = 0 ∨ a % 7 = 6) ∧ (a % 7 = 0 ∨ a % 7  = 1 ∨ a % 7  = 4 ∨ a % 7  = 2)
  · rw (config := {occs := .pos {1,2,3}}) [hab]
    rw [hac, Nat.pow_mod (b := 3), Nat.pow_mod (b := 2)]
    fconstructor
    · interval_cases (b % 7) using hb1, hb2
      all_goals aesop
    · interval_cases (c % 7) using hc1, hc2
      all_goals aesop
  aesop

Up to increasing the maximal recursion from 512 to 700 I can improve it to

set_option maxRecDepth 700

example (a b c : ℕ) (hab : a = b^3) (hac : a=c^2) : (a % 7 = 1 ∨ a % 7 = 0) := by
  have hb1 := (b % 7).zero_le
  have hb2 : (b % 7) < 7 := Nat.mod_lt _ (by linarith)
  have hc1 := (c % 7).zero_le
  have hc2 : (c % 7) < 7 := Nat.mod_lt _ (by linarith)
  have : (a % 7 = 1 ∨ a % 7 = 0 ∨ a % 7 = 6) ∧ (a % 7 = 0 ∨ a % 7  = 1 ∨ a % 7  = 4 ∨ a % 7  = 2)
  rw (config := {occs := .pos {1,2,3}}) [hab]
  rw [hac, Nat.pow_mod (b := 3), Nat.pow_mod (b := 2)]
  interval_cases (b % 7) using hb1, hb2
  all_goals interval_cases (c % 7) using hc1, hc2
  all_goals aesop

A part from the :golf: ing contest, I was unable to insert in the interval_cases the proof term directly, writing for instance interval_cases (b % 7) using (b % 7).zero_le, Nat.mod_lt _ (by linarith) (at least the first one...); this forced the first four "useless" have. Am I missing something, is it intentional?

Filippo A. E. Nuccio (Dec 15 2023 at 18:11):

I should probably add that we were aiming at a proof that does not go "modulo $7$ , but sticks to Nat`; most probably one can work in the finite field with $7$ elements, but that was not the point of our discussion.

Eric Rodriguez (Dec 15 2023 at 18:15):

example (a b c : ℕ) (hab : a = b^3) (hac : a=c^2) : (a % 7 = 1 ∨ a % 7 = 0) := by
  rw [←Nat.one_mod, ←Nat.zero_mod, ←ZMod.nat_cast_eq_nat_cast_iff', ←ZMod.nat_cast_eq_nat_cast_iff']
  apply_fun (fun x : ℕ ↦ (x : ZMod 7)) at hab hac
  generalize hx : (a : ZMod 7) = x
  generalize hy : (b : ZMod 7) = y
  generalize hz : (c : ZMod 7) = z
  simp [hx, hy, hz] at *
  revert x y z
  decide

I just wrote this to come back to your second message :b the simp line is ostentively a bug in generalize; it should generalise everywhere, I'd say.

Eric Rodriguez (Dec 15 2023 at 18:16):

what's the coq proof?

Filippo A. E. Nuccio (Dec 15 2023 at 18:16):

Eric Rodriguez said:

example (a b c : ℕ) (hab : a = b^3) (hac : a=c^2) : (a % 7 = 1 ∨ a % 7 = 0) := by
  rw [←Nat.one_mod, ←Nat.zero_mod, ←ZMod.nat_cast_eq_nat_cast_iff', ←ZMod.nat_cast_eq_nat_cast_iff']
  apply_fun (fun x : ℕ ↦ (x : ZMod 7)) at hab hac
  generalize hx : (a : ZMod 7) = x
  generalize hy : (b : ZMod 7) = y
  generalize hz : (c : ZMod 7) = z
  simp [hx, hy, hz] at *
  revert x y z
  decide

I just wrote this to come back to your second message :b the simp line is ostentively a bug in generalize; it should generalise everywhere, I'd say.

Nice!

Filippo A. E. Nuccio (Dec 15 2023 at 18:16):

Eric Rodriguez said:

what's the coq proof?

I leave it to @Cyril Cohen

Cyril Cohen (Dec 15 2023 at 18:20):

From mathcomp Require Import all_ssreflect.

Lemma test (m n p : nat) : m = n ^ 2 -> m = p ^ 3 ->
  (m == 0 %[mod 7]) || (m == 1 %[mod 7]).
Proof.
move=> -> /(congr1 (modn^~ 7)); rewrite -modnXm -[in RHS]modnXm.
move: (n %% 7) (p %% 7) (@ltn_pmod n 7 isT) (@ltn_pmod p 7 isT).
by do 7?[case=> //]; do 7?[case=> //].
Qed.

Cyril Cohen (Dec 15 2023 at 18:21):

(but I'm still working on the ½ line version :wink: )

Eric Rodriguez (Dec 15 2023 at 18:28):

example (a b c : ℕ) (hab : a = b^3) (hac : a=c^2) : (a % 7 = 1 ∨ a % 7 = 0) := by
  suffices : ∀ a < 7, ∀ b < 7, ∀ c < 7, a = (b^3 % 7) → a=(c^2%7) → (a % 7 = 1 ∨ a % 7 = 0)
  · simpa using this (a % 7) (a.mod_lt <| by linarith) (b % 7) (b.mod_lt <| by linarith) (c % 7) (c.mod_lt <| by linarith) (by simp [hab, Nat.pow_mod]) (by simp [hac, Nat.pow_mod])
  decide

a Lean 3-liner (although you can argue one of the lines is a bit long!)

Riccardo Brasca (Dec 15 2023 at 18:36):

Does decide immediately prove the same statement modulo 7?

Riccardo Brasca (Dec 15 2023 at 18:36):

I mean, when all the variables are module 7

Riccardo Brasca (Dec 15 2023 at 18:37):

decide or fin_cases

Michael Stoll (Dec 15 2023 at 18:37):

Yes: This works (although it is not exactly the statement you want):

example : ∀ a : ZMod 7, (∃ b c : ZMod 7, a = b ^ 3 ∧ a = c ^ 2) → a = 0 ∨ a = 1 := by decide

Michael Stoll (Dec 15 2023 at 18:37):

I would argue that the statement mod 7 is the good one.

Michael Stoll (Dec 15 2023 at 18:38):

It seems to be the least painful way of proving statements about conguences.

Filippo A. E. Nuccio (Dec 15 2023 at 18:39):

Sure, we agree; but we arrived at the discussion coming from a different path, so the point was "try to make it readable even before introducing (to students) the ring-hom of reduction modulo $p$ ".

Riccardo Brasca (Dec 15 2023 at 18:39):

maybe some meta code magic could automatize that we can move to ZMod 7 even if we want a statement about Nat

Filippo A. E. Nuccio (Dec 15 2023 at 18:39):

This "meta code magic" will soon exist in Coq....

Riccardo Brasca (Dec 15 2023 at 18:40):

well, then we also want it!

Cyril Cohen (Dec 15 2023 at 18:45):

Yes, actually that's the ½ line proof I'm still working on

Eric Rodriguez (Dec 15 2023 at 18:56):

Eric Rodriguez said:

example (a b c : ℕ) (hab : a = b^3) (hac : a=c^2) : (a % 7 = 1 ∨ a % 7 = 0) := by
  suffices : ∀ a < 7, ∀ b < 7, ∀ c < 7, a = (b^3 % 7) → a=(c^2%7) → (a % 7 = 1 ∨ a % 7 = 0)
  · simpa using this (a % 7) (a.mod_lt <| by linarith) (b % 7) (b.mod_lt <| by linarith) (c % 7) (c.mod_lt <| by linarith) (by simp [hab, Nat.pow_mod]) (by simp [hac, Nat.pow_mod])
  decide

a Lean 3-liner (although you can argue one of the lines is a bit long!)

I'd argue this proof could be much nicer if we could do ?_s in the simpa invocation, as every required parameter could be solved by (probably, on tube) simp_arith [*, Nat.pow_mod]