How to decide prime without `Classical.choice`

Stream: new members

[Yijun Leng]

Prime can be decided without LEM and Classical.choice (correct me if I'm wrong)

My failed try

import Mathlib
import Mathlib.Tactic.Tauto
import Mathlib.Data.Nat.Prime.Defs

theorem hello : True :=
if Nat.Prime 10
then
  by tauto
else
  by tauto

lemma hello : True := by
cases Nat.decidablePrime 10 with
| isTrue _ => simp
| isFalse _ => simp

#print axioms hello

-- depends on axioms: [propext, Classical.choice, Quot.sound]

I want to decide prime without Classical.choice

[Yijun Leng]

related discussions
https://leanprover.zulipchat.com/#narrow/stream/348111-batteries/topic/Batteries.20and.20LEM/near/472756638

[Ruben Van de Velde]

Why?

[Philippe Duchon]

Primeness in $\mathbb{N}$ is clearly decidable, so if the Lean version depends on additional axioms, I would suspect it is because it is written in a much more general context where things are not always decidable? (like, since operations in $\mathbb{R}$ are not computable, I suspect primeness in $\mathbb{R}[X]$ is not decidable either)

(Is primeness a word? Not sure)

[Yijun Leng]

Ruben Van de Velde said:

Why?

I come from coq and I prefer constructive logic

[Yijun Leng]

is there any tactic specific to Decidable and can avoid LEM ?

[Riccardo Brasca]

Mathlib is not designed to use constructive logic. By this I mean that if you start using tactics it's very difficult to avoid choice. This is because we essentially didn't pay too much attention to do so, even if in principle it is possible.

[Kevin Buzzard]

You could certainly write your own decidability instance for the predicate because it's certainly decidable. The moment you do this though, you run into the issue that there are people who just want an abstract decidability algorithm and those who actually want to run something because they care about examples, ie "theoretical decidability" v "decidability in practice". The mathlib approach in general is just to ignore all of these questions because we're mostly focused on proving theorems in classical mathematics.

[Eric Wieser]

To be clear, your objection is that

#print axioms Nat.decidablePrime

emits Classical.choice, right?

[Eric Wieser]

Kevin Buzzard said:

ie "theoretical decidability" v "decidability in practice". The mathlib approach in general is just to ignore all of these questions because we're mostly focused on proving theorems in classical mathematics.

I don't think this is true. Nat.decidablePrime is an example of something that is "decidable in practice" (as it is computable), but might not be considered "theoretically decidable" to a strict constructivist.

[Yijun Leng]

Eric Wieser said:

To be clear, your objection is that

#print axioms Nat.decidablePrime

emits Classical.choice, right?

yes

[Eric Wieser]

The presence of Classical.choice here does not mean "the decision procedure uses the axiom of choice", but rather "the proof that the decision procedure is correct uses the axiom of choice".

[Eric Wieser]

If it were the former, then Lean would additionally tell you it was noncomputable

[Luigi Massacci]

As a further example

theorem hello'' : ¬(Nat.Prime 10) := by norm_num

#print axioms hello''
-- depends on axioms: [propext]

[Yijun Leng]

Luigi Massacci said:

As a further example

theorem hello'' : ¬(Nat.Prime 10) := by norm_num

#print axioms hello''
-- depends on axioms: [propext]

nice
But I need to judge prime on variable in practise

[Kevin Buzzard]

Then you don't need an abstract decidability proof, you need a practical algorithm

[Kevin Buzzard]

And mathlib has the abstract prerequisites you'll need to write such an algorithm, but nobody wrote a practical algorithm yet as far as I know. Most algorithms one uses in practice are probabilistic but of course there are good non-probabilistic ones nowadays after the breakthroughs from the beginning of this century. But proving such an algorithm correct might be a nontrivial project.

[Eric Wieser]

Kevin, isn't docs#Nat.decidablePrime precisely the algorithm in question?

[Kevin Buzzard]

Without even looking at the code I would confidently guess that this is an exponential time algorithm. Polynomial time algorithms for primality testing have been known for around 20 years.

[Kevin Buzzard]

However probabilistic poly time algorithms are much older, and when you're at the point where the chances that the algorithm is failing is smaller than the chance that a gamma ray flipped a bit then this is in practice good enough for most people in practice.

[Eric Wieser]

#eval Nat.Prime 109139149179199 takes about 1.5s, so I guess "practical" really depends on how large the inputs @lengyijun cares about are

[Eric Wieser]

If they only care about n = 10, a practical algorithm is return false!

[Kevin Buzzard]

? isprime(109139149179199)
%5 = 1
? ##
  ***   last result: cpu time 0 ms, real time 0 ms.

Pari-GP seems to be infinitely faster! (modulo rounding errors)

[Luigi Massacci]

Kevin Buzzard said:

Without even looking at the code I would confidently guess that this is an exponential time algorithm. Polynomial time algorithms for primality testing have been known for around 20 years.

Do you mean exponential time in the number of bits? Because minFac just does the very basic “keep dividing until you get to $\sqrt n$” thing, so it is in fact poly-time in $n$

[Yaël Dillies]

Luigi Massacci said:

Do you mean exponential time in the number of bits?

Yes, because that's the size of the input

[Kyle Miller]

Just to check @lengyijun, are you aware that even if #print axioms shows Classical.choice that Nat.Prime can still be computable? If I write

def calcIsPrime (n : Nat) : Bool := decide (Nat.Prime n)

then since there are no warnings, Lean has succeeded in compiling it to executable code.

This isn't even just a compiler trick. In this case, it also is reducible:

#reduce decide (Nat.Prime 131)
-- true
#reduce decide (Nat.Prime 132)
-- false

[Yijun Leng]

I'm working on https://github.com/lengyijun/goldbach_tm

I hope all theorems don't depend on Classical.choice

[Henrik Böving]

Why?

[Yijun Leng]

Henrik Böving said:

Why?

prime should be decidable without Classical.choice

[Ruben Van de Velde]

Most people here don't care about that. You're unlikely to convince anyone by just blandly asserting that this should be a goal

[Mario Carneiro]

Kevin Buzzard said:

Without even looking at the code I would confidently guess that this is an exponential time algorithm. Polynomial time algorithms for primality testing have been known for around 20 years.

Note that this conflates "polynomial time" and "practical algorithm". The AKS algorithm is generally not regarded as practically useful, compared to probabilistic algorithms that run much faster.

[Mario Carneiro]

I think some elliptic curve algorithms (which are subexponential) are not probabilistic and still run faster in practice than AKS except on some really stupidly large primes

[Kevin Buzzard]

If they're not polynomial then I can guarantee that they'll not run faster than AKS on some really stupidly large primes :-) And of course this set does represent 100% of primes :-)

[Daniel Weber]

Apparently ECPP is conjectured to be asymptotically faster than AKS

[Kevin Buzzard]

Ah so indeed I'm wrong! The ECPP algorithm seems to be "polynomial time most of the time" but not (yet?) provably poly time. So perhaps that's the one we want. There might be some large random primes where AKS is better but I hadn't until now grokked that a non poly time algo can often be poly time anyway (so my 100% claim falls over). I guess this is also true for the simplex algorithm.

[Philippe Duchon]

This is, in a sense, proved for the simplex algorithm. IIRC, every neighborhood of an instance contains mostly instances for which the simplex algorithm performs efficiently (though I am not sure of the exact statement).