If p has more than two divisors, then p is not prime.

Stream: new members

[Kajani Kaunda]

Hello friends.
Below is a full non-working example of some code. I am trying to prove that given the following hypothesis:

p=6n+0; p>3; 2|p.

then p cannot be prime because it has more than two trivial factors. Now I am having trouble using the tactic
Nat.not_prime_mul' in the section marked "FAULTY CODE". The error I am getting is:
ERROR message & goal state:

tactic 'apply' failed, failed to unify
  False
with
  ∃ n_1, 6 * n + 0 = 6 * n_1 + 1 ∨ 6 * n + 0 = 6 * n_1 + 5
case intro.intro.intro.«0»
p : ℕ
hprime : Nat.Prime p
hgt3 : p > 3
k n : ℕ
hp : p = 6 * n + 0
hk : 0 ∈ Finset.range 6
hl : 0 ≤ 0
hu : 0 < 6
hdiv3 : 3 ∣ p
hdiv2 : 2 ∣ p
hpp : 2 * (3 * n) = p
hfactor1✝ : 2 ≠ 1
hfactor2✝ : 3 * n ≠ 1
hfactor1 : 2 ≠ 1
hfactor2 : 3 * n ≠ 1
⊢ ∃ n_1, 6 * n + 0 = 6 * n_1 + 1 ∨ 6 * n + 0 = 6 * n_1 + 5

Lean 4
Nat.not_prime_mul' {a b n : ℕ} (h : a * b = n) (h₁ : a ≠ 1) (h₂ : b ≠ 1) : ¬Nat.Prime n

import Mathlib

-- Assumes lemma A: all natural numbers can be expressed in the form 6n + k, with k in {0,1,2,3,4,5}
theorem all_ints_of_form_6n_plus_k (p : ℕ) : ∃ k n, p = 6 * n + k ∧ k ∈ (Finset.range 6 : Finset ℕ) := by
  -- Let n be the quotient when dividing p by 6
  let n := p / 6
  let k := p % 6
  use k, n
  -- The division algorithm guarantees p = 6 * n + k
  have div_mod := Nat.div_add_mod p 6
  symm at div_mod -- flip the equality to match the goal
  -- Prove that k ∈ {0, 1, 2, 3, 4, 5} using the fact that k is the remainder mod 6
  have k_in_range : k ∈ (Finset.range 6 : Finset ℕ) := Finset.mem_range.mpr (Nat.mod_lt p (Nat.succ_pos 5))
  -- Return both parts: the equality and the membership in the range
  exact ⟨div_mod, k_in_range⟩

-- Prove that a number p can only be prime if it is in the form 6n + 1 or 6n + 5
theorem ppp --prime_form_6n_plus_1_or_6n_plus_5
 (p : ℕ) (hprime : Nat.Prime p) (hgt3 : p > 3) :
  ∃ n, (p = 6 * n + 1 ∨ p = 6 * n + 5)  := by
  -- Obtain k and n such that p = 6 * n + k and k ∈ {0, 1, 2, 3, 4, 5}
  obtain ⟨k, n, hp, hk⟩ := all_ints_of_form_6n_plus_k p

  --#check n
  --#check k
  --#check hp
  --#check hk
  --#check p

  -- Substitute p = 6 * n + k into the goal
  rw [hp]

  -- Use interval_cases to analyze each possible value of k
  have hl : 0 ≤ k := Nat.zero_le k
  have hu : k < 6 := Finset.mem_range.mp hk
  interval_cases k using hl, hu

  -- Case when k = 0
  {
    -- We have hp : p = 6 * n
    have hdiv3 : 3 ∣ p := by use 2 * n; rw [hp]; ring
    have hdiv2 : 2 ∣ p := by use 3 * n; rw [hp]; ring

    -- Now we need to rewrite p in the form `2 * (3 * n)`
    have hpp : 2 * (3 * n) = p := by
      rw [hp]
      ring  -- Simplifies 2 * (3 * n) to 6 * n, matching hp
    --

    -- Show that 2 and 3 * n are both greater than 1
    have hfactor1 : 2 ≠ 1 := by norm_num
    have hfactor2 : 3 * n ≠ 1 := by
      linarith [hgt3] -- since p > 3, we must have n > 0, so 3 * n > 1, which implies 3 * n ≠ 1

    /- GOOD CODE HERE?! -/

    /- GOOD CODE HERE?! -/

    /-
    --FAULTY CODE 1
    -- Show that 2 and 3 * n are both not equal to 1
    have hfactor1 : 2 ≠ 1 := by norm_num
    have hfactor2 : 3 * n ≠ 1 := by
      linarith [hgt3] -- since p > 3, we must have n > 0, so 3 * n > 1, which implies 3 * n ≠ 1

    #check hpp
    -- correctly displays hpp : 2 * (3 * n) = p
    #check hfactor1
    -- correctly displays hfactor1 : 2 ≠ 1
    #check hfactor2
    -- correctly displays hfactor2 : 3 * n ≠ 1

    -- Apply `Nat.not_prime_mul'` with the
    -- appropriate conditions
    apply Nat.not_prime_mul' hpp
    exact hfactor1
    exact hfactor2
    --FAULTY CODE 1
    -/

    /-
    --FAULTY CODE 2
    -- Show that 2 and 3 * n are both greater than 1, so p cannot be prime.
    have hfactor1 : 2 > 1 := by norm_num
    have hfactor2 : 3 * n > 1 := by
      linarith [hgt3]
      -- since p > 3, we must have n > 0, so 3 * n > 1

    #check hpp
    #check hfactor1
    #check hfactor2

    apply Nat.not_prime_mul' hpp
    . hfactor1
    . hfactor2
    --FAULTY CODE 2
    -/

    /-
    --FAULTY CODE 3
    -- Conclude that p is not prime because it has a non-trivial factori zation.
    have hnotprime : ¬ Prime p := by
      apply Nat.not_prime_mul' hpp hfactor1 hfactor2
      exact hpp
      exact hfactor1
      exact hfactor2
    --FAULTY CODE 3
    -/

    /-
    --FAULTY CODE 4
    -- Now we can use `hpp` to apply `Nat.not_prime_mul'`
    apply Nat.not_prime_mul' hpp
    · norm_num
    · omega
    · exact hprime
    --FAULTY CODE 4
    -/

    --last gasp...
    --sorry

  }
  { sorry }
  { sorry }
  { sorry }
  { sorry }
  { sorry }

[Henrik Böving]

I would probably do your proof in this way:

import Mathlib

example (p : Nat) (n : Nat) (h1 : p = 6 * n) (h2 : p > 3) (h3 : 2 ∣ p) : ¬Nat.Prime p := by
  match n with
  | 0 =>
    exfalso
    omega
  | 1 =>
    rw [h1]
    decide
  | n + 2 =>
    rw [h1]
    apply Nat.not_prime_mul
    · decide
    · omega

[Kajani Kaunda]

Henrik Böving said:

I would probably do your proof in this way:

import Mathlib

example (p : Nat) (n : Nat) (h1 : p = 6 * n) (h2 : p > 3) (h3 : 2 ∣ p) : ¬Nat.Prime p := by
  match n with
  | 0 =>
    exfalso
    omega
  | 1 =>
    rw [h1]
    decide
  | n + 2 =>
    rw [h1]
    apply Nat.not_prime_mul
    · decide
    · omega

Oh!, Ok. Your method works and it looks more elegant. Let me try to use it. Thank you very much! I will let you know how it goes.

[Michael Bucko]

Henrik Böving schrieb:

  | n + 2 =>
    rw [h1]
    apply Nat.not_prime_mul
    · decide
    · omega

As for the $n\ge2$ case, is there any tool that could suggest a decide-omega line in this case?

[Kajani Kaunda]

Michael Bucko said:

Henrik Böving schrieb:

  | n + 2 =>
    rw [h1]
    apply Nat.not_prime_mul
    · decide
    · omega

As for the $n\ge2$ case, is there any tool that could suggest a decide-omega line in this case?

I found out that in the math n with tactic the | n + 2 syntax is a "catch-all" phrase.

[Kajani Kaunda]

@Henrik Böving . Hi, I managed to use your code and code ideas to work-out my lemma's. My work is messy, but it works and I am happy! I will not hesitate to ask for help next time I am stuck! Thank you!