Provide divisors of number to prove it's prime

Stream: new members

[Bernardo Borges]

The proof that a number is prime as stated in Theorem Proving in Lean 4 tells us to prove that any number that divides our prime is either 1 or p itself.
https://live.lean-lang.org/#codez=JYWwDg9gTgLgBAWQIYwBYBtgCMB0ARFJHAORRwAUpQBTfagMwGcAoZgEwbmoDdqA7OAAoBALjikYASjhjKEMDIC8cQMBEcANYzxKADRwBygEwAqdaw704bYN2AdGQq/q0S402VHlLVGl7ufK6sZs5pxgVCDUQqLaUlpyCiLKwnCABkRwAAzSgORE0WlwAIw5QoAARE5iEnrWtvZOAoBJhEJscMoCgBRETspFkqxo1NDUIHAwAO4QAPrAjOPhNFqzkXCG3lgAnsxwcADGEHyMMFAArlsw0BtcAB5IJ+K0jKsgQ4ISOABe1J7jfNTjSGxs412USK5x2ewOx1OUHO1CuNxejGOW3GiK2yO+gO+mXOwD4BwgTkAF+TqHSodSAS/JzgB6AC0oKQjCiVAA5qgYDgWWzzs1NGJAKiE5zJWmWgTgxis50ARUSdJZwDrNLrnGlU86MaBQdbMIA

How can I "iterate" or expand the divisors? Is there another way around?

[Ruben Van de Velde]

I approached it with a case bash:

import Mathlib.Data.Nat.Prime.Defs

def even (n : Nat) : Prop := ∃ k : Nat, n = 2*k

def divides ( d n : Nat ) : Prop := ∃ k : Nat, n = k*d

def prime (n : Nat) : Prop := (n ≠ 0) ∧ (n ≠ 1) ∧ (∀ d : Nat, divides d n → (d = n ∨ d = 1))

theorem two_is_prime : prime 2 := by
  constructor
  exact Ne.symm (Nat.zero_ne_add_one 1)
  constructor
  exact Nat.succ_succ_ne_one 0
  intro d ⟨k,hk⟩
  match d with
  | 0 => simp at hk
  | 1 => simp
  | 2 => simp
  | n + 3 =>
    contrapose! hk with _hk
    match k with
    | 0 => simp
    | k + 1 =>
      apply ne_of_lt
      rw [← one_mul 2]
      apply Nat.mul_lt_mul_of_le_of_lt <;> omega

[Damiano Testa]

I followed a similar approach:

theorem two_is_prime : prime 2 := by
  constructor
  exact Ne.symm (Nat.zero_ne_add_one 1)
  constructor
  exact Nat.succ_succ_ne_one 0
  intro d ⟨k,hk⟩
  obtain _|d := d <;> obtain _|k := k <;>
    simp [mul_add, add_mul] at hk; omega

[Bernardo Borges]

Very nice! I'm trying to understand what _|d means tho. Is this a common pattern in case-by-case analysis? @Damiano Testa

[Bernardo Borges]

theorem three_is_prime : prime 3 := by
  constructor
  exact Ne.symm (Nat.zero_ne_add_one 2)
  constructor
  exact Nat.succ_succ_ne_one 1
  intro d ⟨k,hk⟩
  obtain _|d := d <;>
  obtain _|k := k <;>
  simp [mul_add,add_mul] at hk ⊢
  obtain _|k := k <;>
  simp [mul_add,add_mul] at hk <;>
  omega

This works, and I don't know why

[Kevin Buzzard]

_|d by itself doesn't mean anything, this is syntax specific to a couple of tactics like obtain or rcases. In a perfect world this syntax would be documented in eg the docstring of the rcases tactic but I'm not at lean right now so can't check if it is. obtain _|d := h means something like "h is an or statement (or more generally something with two constructors) and we deconstruct this hypothesis (so we're moving from one goal to two); in the first branch we assume the hypothesis on the left and don't give it a name, and in the second we assume the right hypothesis and call it d"

[Kevin Buzzard]

I'm not at lean right now but I'm guessing that actually in this case d is a natural in which case it means "split into two cases: either that d=0 or d is of the form x+1 and call the new variable x also d"

[Damiano Testa]

Yes, indeed, Kevin's explanation is exactly right: d (and k) are both natural numbers and the syntax is used to separate the case where they are 0 or the successor of something.

[Damiano Testa]

Bernardo Borges said:

theorem three_is_prime : prime 3 := by
  constructor
  exact Ne.symm (Nat.zero_ne_add_one 2)
  constructor
  exact Nat.succ_succ_ne_one 1
  intro d ⟨k,hk⟩
  obtain _|d := d <;>
  obtain _|k := k <;>
  simp [mul_add,add_mul] at hk ⊢
  obtain _|k := k <;>
  simp [mul_add,add_mul] at hk <;>
  omega

This works, and I don't know why

You can also add the further case split on k to the previous syntax and compress this a little more:

theorem three_is_prime : prime 3 := by
  constructor
  exact Ne.symm (Nat.zero_ne_add_one 2)
  constructor
  exact Nat.succ_succ_ne_one 1
  intro d ⟨k,hk⟩
  obtain _|d := d <;> obtain _|_|k := k <;>   --  <---  note the further cases split: "`k=0|k=1|k+2`"
    simp [mul_add,add_mul] at hk ⊢ <;> omega

[Johan Commelin]

Note that $n \ne 0$ branch in your definition of prime is redundant. It follows from the other part.

[Bernardo Borges]

Very interesting:

theorem five_is_prime : prime 5 := by
  constructor
  exact Ne.symm (Nat.zero_ne_add_one 4)
  constructor
  exact Nat.succ_succ_ne_one 3
  intro d ⟨k,hk⟩
  obtain _|d := d <;> obtain _|_|_|k := k <;>
    simp [mul_add,add_mul] at hk ⊢ <;> omega

theorem seven_is_prime : prime 7 := by
  constructor
  exact Ne.symm (Nat.zero_ne_add_one 6)
  constructor
  exact Nat.succ_succ_ne_one 5
  intro d ⟨k,hk⟩
  obtain _|d := d <;> obtain _|_|_|_|k := k <;>
    simp [mul_add,add_mul] at hk ⊢ <;> omega

I feel like this could be a tactic of itself. How hard would it be to implement one?
I would just need this scaffold:

theorem p_is_prime : prime p := by
  constructor
  exact Ne.symm (Nat.zero_ne_add_one <p-1>)
  constructor
  exact Nat.succ_succ_ne_one <p-2>
  intro d ⟨k,hk⟩
  obtain _|d := d <;> obtain _|_|_|_|k := k <;>   --  <---  as many case splits as needed
    simp [mul_add,add_mul] at hk ⊢ <;> omega

[Johan Commelin]

Can you avoid figuring out how many case splits you need, by using repeat?

[Johan Commelin]

Also... I think it would be a nice follow-up exercise to improve the running time of your tactic by showing that you only need to check divisors up to $\sqrt p$

[Bernardo Borges]

Yes, I think I could argue that swapping d and k folds the proof like we want. But then I have to argue this translation.
Also, if I use the try combinator I will have to change from the obtain _|k syntax, right?

[Damiano Testa]

Here is a hack to make this work, although it clearly has its limitations:

theorem one_hundred_and_one_is_prime : prime 101 := by
  constructor
  exact Ne.symm (Nat.zero_ne_add_one _)
  constructor
  exact Nat.succ_succ_ne_one _
  intro d ⟨k,hk⟩
  obtain _|d := d <;>
    repeat obtain _|k := k <;> try (simp [mul_add,add_mul] at hk ⊢ <;> omega)

(I really wanted to break the 10^2 barrier. :smile: )