Changing types from Nat to Zmod and other confusion

Stream: new members

[Ryan Smith]

I'm still working on my first baby steps problems in lean, a basic number theory question using the Chinese remainder theorem and Fermat's little theorem for a prime modulus. (I know there are other ways we could potentially solve this).

My problems are coming when I try to use Zmod.pow_card to replace n^7 [MOD 7] with n [MOD 7]. My understanding is that since n is a natural number we have a type issue. Do we need to somehow pass from n \in N to n \in Z mod 7 in order to do this?

I tried writing a lemma which would state that x^p \== x [MOD p] for natural numbers. That lemma would be another way forward but is failing since I can't perform basic simplifications? Also this must be one of the ugliest ways of handing cases where we wouldn't need one, but since I can't lift the Zmod.pow_card result we need to use Fermat's little theorem and handle the not coprime case separately?

Lean has a learning curve to express simple proofs.

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
  have hf' : 6 = 2 * 3 := by decide

  have h67cop : Coprime 6 7 := by decide
  have h23cop : Coprime 2 3 := by decide

  rw [hf, ← Nat.modEq_and_modEq_iff_modEq_mul h67cop]
  rw [hf', ← 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
    have h7p : Nat.Prime 7 := by decide
    calc
      n ^ 7 - n ≡ n - n [MOD 7] := by rw [ZMod.pow_card]  -- fails here
      _ ≡ 0 [MOD 7] := by ring_nf; simp; rfl
  tauto


lemma fermat_little_ap {a p : ℕ} (hp : Nat.Prime p) : a ^ p  - a ≡ 0 [MOD p] := by
  have h : Coprime a p ∨ ¬ Coprime a p := by tauto
  have hcp : Coprime a p → a ^ p ≡ a [MOD p] := by
    sorry
  have hncp : ¬ Coprime a p → a ^ p ≡ a [MOD p] := by
    sorry
  have h' : a ^ p ≡ a [MOD p] := by tauto
  apply Nat.ModEq.add_right (0 - a) at h'
  -- stuck here as well
  sorry

[Ruben Van de Velde]

\== [MOD p] is indeed not very easy to work with because it's not a real equality. You can pass to values of type docs#ZMod where you can actually rewrite etc

[Mario Carneiro]

(I wonder whether grw has made this better?)

[Kenny Lau]

@Ryan Smith natural numbers with subtraction are hard to work with because 3-5 = 0

[Kenny Lau]

I would recommend you to do it for integer first

[Ryan Smith]

Rewriting with integers instead of naturals sounds like a good idea.

So here we have the constants 6 and 7 being viewed as naturals in our hypothesis that they are coprime (is there a reason we can't directly state two integers are coprime, ie their gcd is a unit?). The theorem we are trying to use for rw is

Int.modEq_and_modEq_iff_modEq_mul {a b m n : ℤ} (hmn : m.natAbs.Coprime n.natAbs) :
  a ≡ b [ZMOD m] ∧ a ≡ b [ZMOD n] ↔ a ≡ b [ZMOD m * n]

So I'm guessing the reason we cannot find a match in rw in order to use the integer version of the Chinese remainder theorem because our hypothesis somehow has the wrong type?

import Mathlib
open Nat

#check Int.modEq_and_modEq_iff_modEq_mul
#check Int.coprime_iff_nat_coprime

-- Show that n^7 − n is divisible by 42 for every positive integer n.
example (n : ℤ) (h : n > 0) : n^7 - n ≡ 0 [ZMOD 42] := by
  have hf : 42 = 6 * 7 := by decide
  have hf' : 6 = 2 * 3 := by decide

  have h67cop : Coprime 6 7 := by decide
  have h23cop : Coprime 2 3 := by decide

  rw [hf, ← Int.modEq_and_modEq_iff_modEq_mul h67cop] -- fails

[Kenny Lau]

@Ryan Smith this is where good hygiene comes in, to a mathematician 42 just means 42, but to Lean, (42 : Z) and (42 : N) are two different objects

[Kenny Lau]

so the goal has (42 : Z) but hf is about (42 : N)

[Kenny Lau]

(you can check the types by clicking on stuff)

[Ryan Smith]

Thank you for your long standing patience, although I see a few New Members posts w/ such basic questions it's not many. So can we explicitly tell lean which category we mean when we write a constant such as 42 in order to fix this?

[Kevin Buzzard]

You probably mean "type" rather than "category" but (42 : ℤ) is exactly the way to tell Lean "the integer 42".

[Ryan Smith]

Maybe the right question is: how do I construct the hypothesis (hmn : m.natAbs.Coprime n.natAbs) to use the integer version of the theorem? Nat.Coprime has the wrong type somehow even though Int.natAbs is an integer isn't it?

application type mismatch
  Int.modEq_and_modEq_iff_modEq_mul h67cop
argument
  h67cop
has type
  Coprime 6 7 : Prop
but is expected to have type
  (Int.natAbs ?m.1055).Coprime (Int.natAbs ?m.1056) : PropLean 4
h67cop : Coprime 6 7

Current version:

import Mathlib
open Nat

#check Int.modEq_and_modEq_iff_modEq_mul
#check Int.coprime_iff_nat_coprime
-- Show that n^7 − n is divisible by 42 for every positive integer n.
example (n : ℤ) (h : n > 0) : n^7 - n ≡ 0 [ZMOD 42] := by
  have hf : (42 : ℤ) = (6 : ℤ) * (7 : ℤ) := by decide
  have hf' : 6 = 2 * 3 := by decide

  have h67cop : Coprime 6 7 := by decide
  have h23cop : Coprime 2 3 := by decide

  rw [hf, ← Int.modEq_and_modEq_iff_modEq_mul h67cop] -- fails

[Aaron Liu]

It fails to match (Int.natAbs ?_).Coprime (Int.natAbs ?_) to Nat.Coprime 6 7

[Aaron Liu]

Try doing have h67cop : (Int.natAbs 6).Coprime (Int.natAbs 7) := by decide instead