A simple number theory problem to practice lean basics

Stream: new members

[Ryan Smith]

I am trying to show that n^7 − n is divisible by 42 for every positive integer n. Pretty easy if you know basic number theory, but it has exposed a lot of rough edges in learning how to interact with lean to do basic stuff. Here is an outline so far which has several issues:

example (n : ℕ) (h : n > 0) : n^7 - n ≡ 0 [MOD 42] := by
  have hf' : 42 = 6 * 7 := by decide
  rw [hf']
  have h67cop : Coprime 6 7 := by decide
  -- this line fails
  apply Nat.modEq_and_modEq_iff_modEq_mul h67cop
  sorry

The version of the chinese remainder theorem I'm trying to invoke says

Nat.modEq_and_modEq_iff_modEq_mul {a b m n : ℕ} (hmn : m.Coprime n) : a ≡ b [MOD m] ∧ a ≡ b [MOD n] ↔ a ≡ b [MOD m * n]

Since my goal is ⊢ n ^ 7 - n ≡ 0 [MOD 6 * 7] I would have thought I could apply the chinese remainder theorem successfully since I've provided a hypothesis that 6 and 7 are coprime as required. I tried a couple variations such as modEq_and_modEq_iff_modEq_mul.mpr since I really want the left part of an iff statement but I can't get the syntax correct.

The second part of my question for this basic exercise comes from figuring out how to justify my steps in a calc block:

  have h3 : n ^ 7 - n ≡ 0 [MOD 3] := by
    calc
      n ^ 7 - n ≡ n ^ 6 * n - n [MOD 3] := by ring  -- fails
      _ ≡ (n ^ 2) ^ 3 * n - n [MOD 3] := by sorry
      _ ≡ 1 ^ 3 * n - n [MOD 3] := by sorry
      _ ≡ 0 [MOD 3] := by sorry
    sorry

Tactics such as ring and simp fail even though we are in a field? Is this even the right way to use a calc block?

I'm still learning lean, there's a bit of a learning curve to express basic arguments at the beginning.

[Kenny Lau]

Please include import Mathlib in the beginning of your code blocks so the code can just be run by themselves

[Kenny Lau]

(and open Nat too)

[Kenny Lau]

ring is for equalities, so here you can use instead ring_nf; rfl

[Kenny Lau]

@Ryan Smith that line fails because apply is strictly for implications, but you have an iff.

[Kenny Lau]

Basically, if your goal is ⊢ q and you have some_theorem_name : p → q, then apply some_theorem_name changes the goal to ⊢ p. See the following example:

def p : Prop := sorry
def q : Prop := sorry
theorem some_thm_name : p → q := sorry
theorem foo : q := by
  apply some_thm_name

[Kenny Lau]

move your cursor from before apply to after apply to see how the goal changes.

[Kenny Lau]

so, if you want to use an iff, you use rw instead

[Kenny Lau]

so the correct code is:

import Mathlib

open Nat

example (n : ℕ) (h : n > 0) : n^7 - n ≡ 0 [MOD 42] := by
  have hf' : 42 = 6 * 7 := by decide
  rw [hf']
  have h67cop : Coprime 6 7 := by decide
  -- this line works now!
  rw [← Nat.modEq_and_modEq_iff_modEq_mul h67cop]
  sorry

[Ryan Smith]

Thanks! calc still dislikes rewriting n^7 however,

import Mathlib
open Nat

-- Show that n^7 − n is divisible by 42 for every positive integer n.
example (n : ℕ) (h : n > 0) : n^7 - n ≡ 0 [MOD 42] := by
  have hf' : 42 = 6 * 7 := by decide
  rw [hf']
  have h67cop : Coprime 6 7 := by decide
  rw [← Nat.modEq_and_modEq_iff_modEq_mul h67cop]

  have h3 : n ^ 7 - n ≡ 0 [MOD 3] := by
    calc
      n ^ 7 - n ≡ n ^ 6 * n - n [MOD 3] := ring_nf; rfl
      _ ≡ (n ^ 2) ^ 3 * n - n [MOD 3] := by sorry
      _ ≡ 1 ^ 3 * n - n [MOD 3] := by sorry
      _ ≡ 0 [MOD 3] := by sorry
    sorry
  sorry

[Kenny Lau]

@Ryan Smith you forgot the by that time

[Ryan Smith]

Thank you. So we apply results to hypotheses but rewrite our goal?

[Ryan Smith]

Stylistically, is the hypothesis that 42 = 6 * 7 required or could one of the tactics justified that automatically?

[Kenny Lau]

Ryan Smith said:

Thank you. So we apply results to hypotheses but rewrite our goal?

as i've explained, they differ by what things you can feed them with; apply is for p -> q only; and rw is for p <-> q only (and equalities too)

[Kenny Lau]

in informal maths you would call both "apply", but Lean is not informal maths

[Kenny Lau]

btw here's my "standard" proof:

import Mathlib

set_option trace.profiler true
-- Show that n^7 − n is divisible by 42 for every positive integer n.
-- 0.186 seconds
theorem Nat.pow_seven_sub_modEq_zero (n : ℕ) : n^7 - n ≡ 0 [MOD 42] := by
  rw [← ZMod.eq_iff_modEq_nat, Nat.cast_sub (Nat.le_self_pow (by norm_num) _),
    Nat.cast_pow, Nat.cast_zero]
  generalize (n : ZMod 42) = m
  decide +revert

[Kenny Lau]

in words, reduce this to a problem in Z/42Z, which can then be "checked by brute force" (that's the decide)

[Ryan Smith]

Wow, that is quite terse. What does +revert mean?

[Kenny Lau]

Ryan Smith said:

Wow, that is quite terse. What does +revert mean?

when you check by brute force (i.e. decide), the statement cannot have free variables, so revert will make the variables bounded first (i.e. quantified under forall), and then decide it

[Kenny Lau]

you can try revert n by itself to see what it does

[Ryan Smith]

Updated version. Clearly we are doing some of these things the hard way but the goal is to figure out how to translate an argument into lean

import Mathlib
open Nat

-- Show that n^7 − n is divisible by 42 for every positive integer n.
example (n : ℕ) (h : n > 0) : n^7 - n ≡ 0 [MOD 42] := by
  have hf : 42 = 6 * 7 := by decide
  rw [hf]
  have h67cop : Coprime 6 7 := by decide
  rw [← Nat.modEq_and_modEq_iff_modEq_mul h67cop]

  have hf' : 6 = 2 * 3 := by decide
  rw [hf']
  have h23cop : Coprime 2 3 := by decide
  rw [← Nat.modEq_and_modEq_iff_modEq_mul h23cop]

  have h2 : n ^ 7 - n ≡ 0 [MOD 2] := by sorry
  have h3 : n ^ 7 - n ≡ 0 [MOD 3] := by
    calc
      n ^ 7 - n ≡ (n ^ 3) ^ 2 * n - n [MOD 3] := by ring_nf; rfl
      _ ≡ n ^ 2 * n - n [MOD 3] := sorry
      _ ≡ n ^ 3 - n [MOD 3] := by ring_nf; rfl
      _ ≡ n - n [MOD 3] := sorry
      _ ≡ 0 [MOD 3] := by ring_nf; simp; rfl
  have h7 : n ^ 7 - n ≡ 0 [MOD 7] := by
    calc
      n ^ 7 - n ≡ n - n [MOD 7] := by rw [ZMod.pow_card (n ^ 7)]
      _ ≡ 0 [MOD 7] := by ring_nf; simp; rfl
  tauto

A question about the follow up. The use of rw with ZMod.pow_card fails when I try to use it to simplify n^7 mod 7 to n mod 7

ZMod.pow_card {p : ℕ} [Fact (Nat.Prime p)] (x : ZMod p) : x ^ p = x

This seems like a valid use of rw but I'm guessing lean is unhappy about n being a natural number and not an element of Z/7Z ?

For teaching purposes when p=2 is there a way I could express there are two cases to lean so either n \== 0 mod 2 or 1 mod 2 and then do each of those cases separately? Seems so easy to say in English :)

[Kenny Lau]

Ryan Smith said:

This seems like a valid use of rw but I'm guessing lean is unhappy about n being a natural number and not an element of Z/7Z ?

You exactly spelled out why this was not a valid use of rw. Be wary of the mathematician's trap where things that are "obviously the same" in maths are not the same in Lean. In this case in particular you exactly said that a ≡ b [MOD 7] is not the same as being equal in Z/7Z.

Ryan Smith said:

when p=2 is there a way I could express there are two cases to lean

That's exactly the line in my code that again does this transformation which is obvious to a mathematician. Refer to the first three lines in my proof provided above.