Proving Primality and working with arrays

Stream: new members

[Kajani Kaunda]

I need some help with this problem. The technics learned will help me resolve some other similar problems.

We have a 10×10 array where:

1. The first row contains the first 10 prime numbers starting at 2 (i.e., [2, 3, 5, 7, 11, 13, 17, 19, 23, 29]).
2. The third row is obtained by subtracting 3 from each prime in the first row (e.g., the first number in the third row would be 2 - 3 = -1, the second would be 3 - 3 = 0, etc.).

We want to prove:
If you take any number in the third row and add 3 back to it, the result will always be a prime number from the first row.

Thank you.

[Matt Diamond]

Do you mean something like this?

import Mathlib

example
  (row1 : Array ℤ)
  (row3 : Array ℤ)
  (_ : row3.size ≤ row1.size)
  (h : ∀ (i : Fin row3.size), row3[i] = row1[i] - 3) :
  ∀ (i : Fin row3.size), row3[i] + 3 = row1[i] :=
fun i => by simp [h i]

[Kajani Kaunda]

Matt Diamond said:

Do you mean something like this?

import Mathlib

example
  (row1 : Array ℤ)
  (row3 : Array ℤ)
  (_ : row3.size ≤ row1.size)
  (h : ∀ (i : Fin row3.size), row3[i] = row1[i] - 3) :
  ∀ (i : Fin row3.size), row3[i] + 3 = row1[i] :=
fun i => by simp [h i]

Yes Sir. Something like that would work!

[Kajani Kaunda]

Since I already have a defined array, I guess I would just have to define the elements in the first and third rows with the rest to follow.

[Kajani Kaunda]

The following is my defined array:

import Mathlib
import Mathlib.Data.Nat.Prime.Basic
import Mathlib.Data.List.Basic
import Mathlib.Tactic.Linarith
import Mathlib.Data.Int.Defs
import Mathlib.Tactic.Basic
import Mathlib.Data.Finset.Basic
import Mathlib.Tactic.ModCases
import Mathlib.Data.Set.Basic
import Mathlib.Tactic.NormNum
import Mathlib.Algebra.ModEq
import Mathlib.Order.Filter.Basic
import Mathlib.Topology.Filter
import Init.Data.Option.Basic

open List Nat

-- Define a finite portion of a Cayley table.
def cayley_table (n : ℕ) : List (List ℤ) :=
  let primes := (List.range n).filter Nat.Prime |>.map (λ p => ↑p)
  let inverses := primes.map (λ p => -p)
  let first_row := 0 :: primes
  let table := inverses.map (λ inv => inv :: (primes.map (λ p => p + inv)))
  first_row :: table

#eval "valid cayley table"
def cayleytable := cayley_table 71
#eval cayleytable

Thank you Matt. Let me try and work on it. ...

[Matt Diamond]

@Kajani Kaunda Had a thought: why not represent the entire table as a function instead of nested lists? I had suggested this before but I just realized there's a way to do it computably:

import Mathlib

def primes_set := { n | Nat.Prime n }
instance : Infinite primes_set := Nat.infinite_setOf_prime.to_subtype
instance : DecidablePred (fun n => n ∈ primes_set) := fun n => Nat.decidablePrime n

def primes (n : ℕ) : ℕ := if (n = 0) then 0 else Nat.Subtype.ofNat primes_set (n - 1)

lemma primes_zero : primes 0 = 0 := rfl

def cayley_table (row col : ℕ) : ℤ := primes col - primes row

example (row) : ∀ col, cayley_table row col + primes row = primes col:=
by
  intro col
  simp [cayley_table]

def tableAsLists (size : ℕ) : List (List ℤ) :=
(List.range size).map (fun i =>
  (List.range size).map (fun j =>
    cayley_table i j
  )
)

#eval tableAsLists 20

[Matt Diamond]

I added a function called tableAsLists which will translate a portion of the table into nested arrays so you can still #eval it

[Matt Diamond]

you could even turn it into a Matrix like so:

def cayley_matrix : Matrix ℕ ℕ ℤ := Matrix.of cayley_table

[Matt Diamond]

it's infinite and it's computable!

[Matt Diamond]

as a bonus, here's a proof of your original question using this new structure (row 2 is the third row counting from 0):

example : ∀ col, cayley_table 2 col + 3 = cayley_table 0 col :=
by
  intro col
  unfold cayley_table
  have : primes 2 = 3 := by native_decide
  rw [this, primes_zero]
  simp

[Kajani Kaunda]

Matt Diamond said:

as a bonus, here's a proof of your original question using this new structure (row 2 is the third row counting from 0):

example : ∀ col, cayley_table 2 col + 3 = cayley_table 0 col :=
by
  intro col
  unfold cayley_table
  have : primes 2 = 3 := by native_decide
  rw [this, primes_zero]
  simp

Wow! I am at a loss for words to thank to thank you. You have done so much work!

Its infinite, computable and one can even turn it into a Matrix. Then there is the bonus! Thank you so much. I will have to see about re-writing the code done so far.