Prove decidable statement by evaluation

Stream: new members

[Jack Valmadre]

Hi! For a proof that I'm writing, I need to prove that a list of numbers are prime:
def nums := [2, 3, 5, 7, 13, 23, 43, 83, 163, 317, 631, 1259, 2503, 4001]
I can check this myself using:
#eval to_bool (list.all₂ nat.prime nums)
Is there a way to turn this into a proof by evaluation?
lemma nums_prime : list.all₂ nat.prime nums := ??

[Alex J. Best]

Looks like you are using lean 3 which is now end of life, I definitely recommend you switch to lean 4 which has lots of nice new features (including some that would probably make answering this easier).
That said if you want to prove numbers prime its better to use the dedicated norm_num extension rather than try and have the kernel do it.

import tactic
import data.nat.prime
import data.nat.prime_norm_num
def nums := [2, 3, 5, 7, 13, 23, 43, 83, 163, 317, 631, 1259, 2503, 4001]
#eval to_bool (list.all₂ nat.prime nums)
lemma nums_prime : list.all₂ nat.prime nums :=
begin
  rw nums,
  norm_num,
end

[Bolton Bailey]

You can see how this was done for the proof of Bertrand's postulate in docs#Nat.bertrand. (This list of primes looks suspiciously similar to yours, so beware of spoilers).

[Jack Valmadre]

Thank you! norm_num with import data.nat.prime_norm_num worked perfectly. I'll move to Lean 4. And thanks for the spoiler warning - that's exactly the theorem that I'm proving as an exercise :)

[Jack Valmadre]

Do you know if there is something similar for list.sorted? It works with #eval to_bool ... but neither of these worked:

import tactic
import data.list

def nums := [2, 3, 5, 7, 13, 23, 43, 83, 163, 317, 631, 1259, 2503, 4001]

#eval to_bool (list.sorted nat.lt nums)

lemma sorted_nums : list.sorted nat.lt nums :=
begin
  rw nums,
  norm_num,  -- slow (n^2?); does not evaluate inequalities
  sorry,
end

lemma eq_insertion_sort_nums : nums = list.insertion_sort nat.lt nums :=
begin
  rw nums,
  simp,
  norm_num,  -- failed to simplify
end

I think I need norm_num.eval_ineq with expr.lt but I'm not sure how to use it.

[Jack Valmadre]

Update: I was able to solve it using refl although it does seem a bit slow. Is this an acceptable way to do it? (Had to switch from lt to le to have total ordering for list.sorted_insertion_sort)

lemma nums_eq_insertion_sort_self : nums = list.insertion_sort nat.le nums :=
begin
  rw nums,
  refl,
end

lemma sorted_nums : list.sorted nat.le nums :=
begin
  rw nums_eq_insertion_sort_self,
  apply list.sorted_insertion_sort,
end

[Kevin Buzzard]

Doing anything new in lean 3 is not really an acceptable way to do it any more

[Jack Valmadre]

OK, sounds good. Thanks for the responses!

[Kevin Buzzard]

More precisely, I mean "nobody is going to be motivated to work on fixing something which is slow in Lean 3" because there is an obvious fix for this.

[Jack Valmadre]

Ah ok, makes sense, thank you!

[Jack Valmadre]

Hi! I'm now trying to do the same thing in Lean 4: I would like to prove List.All₂ Nat.Prime nums where nums is a list of 14 primes. #eval decide ... is fast but proving with norm_num times out (even after importing Mathlib.Tactic.NormNum.Prime). Is there an easy way to achieve this? Thanks!

import Mathlib.Data.List.Defs
import Mathlib.Data.Nat.Prime
import Mathlib.Tactic.NormNum
import Mathlib.Tactic.NormNum.Prime

def nums := [2, 3, 5, 7, 13, 23, 43, 83, 163, 317, 631, 1259, 2503, 4001]

-- Fast
#eval decide (List.All₂ Nat.Prime nums)

-- Fast
lemma largest : Nat.Prime 4001 := by norm_num

-- Slow (maximum number of heartbeats (200000) has been reached)
lemma allPrimeNums : List.All₂ Nat.Prime nums := by
  rw [nums]
  norm_num

[Kevin Buzzard]

simp is timing out, it seems.

lemma allPrimeNums : List.All₂ Nat.Prime nums := by
  simp [nums] -- deterministic timeout

[Mario Carneiro]

I think it is using decide

[Mario Carneiro]

this works:

lemma allPrimeNums : List.All₂ Nat.Prime nums := by
  simp (config := {decide := false}) only [nums, List.All₂]
  norm_num1
  simp

[Kevin Buzzard]

This doesn't:

lemma not_largest : Nat.Prime 317 := by norm_num -- timeout

[Mario Carneiro]

here's a slightly more manual version:

lemma allPrimeNums : List.All₂ Nat.Prime nums := by
  iterate 13 refine ⟨by norm_num1, ?_⟩
  simp; norm_num1

[Kevin Buzzard]

lemma allPrimeNums : List.All₂ Nat.Prime nums := by
  simp (config := {decide := false})
  constructor; norm_num
  constructor; norm_num
  constructor; norm_num
  constructor; norm_num
  constructor; norm_num
  constructor; norm_num
  constructor; norm_num
  constructor; norm_num
  constructor; norm_num
  constructor; sorry -- ignore 317
  constructor; norm_num
  constructor; norm_num
  constructor; norm_num
  norm_num

[Damiano Testa]

317 is the new 37...

[Kevin Buzzard]

norm_num1 does 317 shrug

[Damiano Testa]

I see a pattern here.

[Mario Carneiro]

By the way, this list of primes looks familiar: are you aware that mathlib has a proof of Bertrand's postulate?

[Kevin Buzzard]

Indeed Jack is: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Prove.20decidable.20statement.20by.20evaluation/near/390081954

[Mario Carneiro]

It appears that for the numbers less than 317, the proof generated by norm_num looks like of_eq_true (eq_true_of_decide (Eq.refl true)), and for the ones greater than it it produces

of_eq_true
  (eq_true
    (Mathlib.Meta.NormNum.isNat_prime_2 (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 631)) (Eq.refl true)
      (Mathlib.Meta.NormNum.isNat_minFac_4 (Mathlib.Meta.NormNum.IsNat.raw_refl 631)
        (Mathlib.Meta.NormNum.minFacHelper_2 (Eq.refl 27)
          (Mathlib.Meta.NormNum.not_prime_mul_of_ble 5 5 25 (Eq.refl 25) (Eq.refl false) (Eq.refl false))
...

In other words, simp is using decide sometimes and just giving up and letting norm_num core have a shot when it gets too hard

[Mario Carneiro]

and 317 seems to be just on the edge where decide thinks it can take it but it can't really

[Damiano Testa]

Btw, for numbers of the form 311...17, every third one is divisible by 3, the next one is divisible by 37, of the remaining ones, 317 is prime and then they are all composite at least until 311111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111117, although a formal proof of this fact is lacking.

[Jack Valmadre]

Thanks very much! That's interesting! I'll use the config := {decide := false} and norm_num1 approach :+1:

[Kevin Buzzard]

311111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111117 is prime.

[Richard Copley]

The next two primes in the sequence are (28/9)(10^692-1)+9 and (28/9)(10^1805-1)+9.

[Mario Carneiro]

#7112 (sadly not a prime) implements norm_num (config := ...) so you should be able to do this with just norm_num (config := {decide := false}) [nums, List.All₂]