# Zulip Chat Archive

## Stream: new members

### Topic: Why doesn't dec_trivial solve `prime 3`?

#### Abhimanyu Pallavi Sudhir (Oct 24 2018 at 15:20):

In `prime.lean`

, the following statements are made:

theorem prime_two : prime 2 := dec_trivial theorem prime_three : prime 3 := dec_trivial

And both work. However if I reproduce the same code on another lean file, e.g.

import data.real.basic import data.nat.prime open nat theorem prime_two : prime 2 := dec_trivial theorem prime_three : prime 3 := dec_trivial

Only `prime_two`

works. What's going on?

#### Bryan Gin-ge Chen (Oct 24 2018 at 15:38):

The crucial line in `data.nat.prime`

seems to be `local attribute [instance] decidable_prime_1`

. If you include that, then `prime_three`

works.

#### Bryan Gin-ge Chen (Oct 24 2018 at 15:39):

I guess what's initially surprising is how lean knows `prime 2`

is decidable without that instance.

#### Bryan Gin-ge Chen (Oct 24 2018 at 15:40):

`decidable_prime_1`

just says:

def decidable_prime_1 (p : ℕ) : decidable (prime p) := decidable_of_iff' _ prime_def_lt'

#### Bryan Gin-ge Chen (Oct 24 2018 at 15:46):

Here's the definition of `prime`

:

def prime (p : ℕ) := p ≥ 2 ∧ ∀ m ∣ p, m = 1 ∨ m = p

and here's the type of `prime_def_lt`

:

theorem prime_def_lt' {p : ℕ} : prime p ↔ p ≥ 2 ∧ ∀ m, 2 ≤ m → m < p → ¬ m ∣ p

When `p=2`

it's obvious to lean that `prime p`

is decidable, but when `p > 2`

it needs the extra hint that you only need to check `m < p`

.

#### Abhimanyu Pallavi Sudhir (Oct 24 2018 at 15:47):

Ah ok. Interestingly if the file contains `local attribute [instance] classical.prop_decidable`

(and not `nat.decidable_prime_1`

), then even `prime 2`

gets messed up.

#### Bryan Gin-ge Chen (Oct 24 2018 at 15:55):

Yes, that makes sense. I don't think `dec_trivial`

can do very much for you when every proposition is declared to be decidable.

#### Kevin Buzzard (Oct 24 2018 at 17:59):

If every proposition is declared to be decidable, but you still want to use `dec_trivial`

, the trick is `local attribute [instance, priority 0] classical.prop_decidable`

#### Kevin Buzzard (Oct 24 2018 at 18:00):

Then the "fake" decidabilty is always used after the "real" one, if a real one can be found.

#### Abhimanyu Pallavi Sudhir (Oct 24 2018 at 18:01):

If every proposition is declared to be decidable, but you still want to use

`dec_trivial`

, the trick is`local attribute [instance, priority 0] classical.prop_decidable`

Yeah, I know that -- but I don't get why exactly it is that the fake decidability isn't enough for dec_trivial.

#### Kenny Lau (Oct 24 2018 at 18:02):

because it uses `choice`

and the VM can't evaluate `choice`

#### Kevin Buzzard (Oct 24 2018 at 18:02):

fake decidability just confuses `dec_trivial`

. We saw another instance of `dec_trivial`

getting confused in the `even`

thread a week or so ago. I am very much not an expert in these matters, but it's something to do with what the VM does

#### Kenny Lau (Oct 24 2018 at 18:02):

`decidable`

isn't a Prop, it's data

#### Kevin Buzzard (Oct 24 2018 at 18:02):

what Kenny said

#### Kevin Buzzard (Oct 24 2018 at 18:04):

Yeah. I don't understand this properly. I don't even really know what the kernel and the VM are. I suspect that this might be quite a good way of learning what the difference is between them.

#### Kevin Buzzard (Oct 24 2018 at 18:06):

`decidable blah`

usually encodes some sort of way of computing whether blah is true or false. But if you make a random instance of it using classical mathematics then the algorithm isn't actually there. What does the kernel think of this situation? What about the VM?

#### Kevin Buzzard (Oct 24 2018 at 18:07):

What would happen if there were no VM? The kernel does all the typechecking, right? Why do we even need the VM?

#### Kevin Buzzard (Oct 24 2018 at 18:08):

Sorry for my dumb questions -- given that we are on the "new members" stream I figure they would be OK.

#### Chris Hughes (Oct 24 2018 at 18:09):

The VM is faster than the kernel. This is useful for executing tactics.

#### Reid Barton (Oct 24 2018 at 18:18):

If every proposition is declared to be decidable, but you still want to use

`dec_trivial`

, the trick is`local attribute [instance, priority 0] classical.prop_decidable`

Yeah, I know that -- but I don't get why exactly it is that the fake decidability isn't enough for dec_trivial.

The idea behind `dec_trivial`

is basically that the value of type `decidable P`

given by the instance is going to reduce to either `is_false p`

(where `p : not P`

) or `is_true p`

(where `p : P`

). But if you use an axiom to define the instance, like `classical.prop_decidable`

does, then that axiom won't be reducible.

#### Reid Barton (Oct 24 2018 at 18:19):

I *think* the VM is actually not involved here. But some things about `dec_trivial`

still confuse me.

#### Reid Barton (Oct 24 2018 at 18:22):

(Like why do we need this tactic `meta def triv : tactic unit := mk_const `trivial >>= exact`

? Could we just have defined `notation `dec_trivial` := of_as_true trivial`

?)

#### Reid Barton (Oct 24 2018 at 18:23):

Maybe this is the `by exact`

trick to defer type checking a term, in the hopes that its expected type will be known later?

#### Bryan Gin-ge Chen (Oct 24 2018 at 18:31):

I'm intrigued. I've never heard of the `by exact`

trick. Where (else) is it used?

#### Reid Barton (Oct 24 2018 at 18:32):

whenever Lean is being dumb

#### Reid Barton (Oct 24 2018 at 18:32):

that is to say, I don't really understand when or why it works--I have used it successfully once or twice though

#### Reid Barton (Oct 24 2018 at 18:34):

I guess something like: if there is a subterm which should type check, but Lean is rejecting it, and there are metavariables in its expected type, then maybe wrapping the subterm in `by exact`

will cause those metavariables to be solved for earlier relative to Lean trying to check the subterm

#### Reid Barton (Oct 24 2018 at 18:35):

I think it's the kind of thing which only crops up in situations which are a bit complicated

#### Bryan Gin-ge Chen (Oct 24 2018 at 18:40):

I did a search for "`by exact`

" in mathlib and it looks like there's a concrete example in `set_theory/cardinal.lean`

:

theorem add_one_le_succ (c : cardinal) : c + 1 ≤ succ c := begin refine quot.induction_on c (λ α, _) (lt_succ_self c), refine quot.induction_on (succ (quot.mk setoid.r α)) (λ β h, _), cases h.left with f, have : ¬ surjective f := λ hn, ne_of_lt h (quotient.sound ⟨equiv.of_bijective ⟨f.inj, hn⟩⟩), cases classical.not_forall.1 this with b nex, refine ⟨⟨sum.rec (by exact f) _, _⟩⟩, { exact λ _, b }, { intros a b h, rcases a with a|⟨⟨⟨⟩⟩⟩; rcases b with b|⟨⟨⟨⟩⟩⟩, { rw f.inj h }, { exact nex.elim ⟨_, h⟩ }, { exact nex.elim ⟨_, h.symm⟩ }, { refl } } end

Removing `by exact`

from the line `refine ⟨⟨sum.rec (by exact f) _, _⟩⟩,`

causes lean to complain:

type mismatch at application sum.rec ⇑f term ⇑f has type has_coe_to_fun.F f : Type u_1 but is expected to have type Π (val : ?m_1), ?m_2 (sum.inl val) : Sort (imax (?+1) ?)

I guess this is what you're describing?

(on the other hand, the `by exact`

at line 296 can be removed, at least when I play around with this in VS code.)

#### Reid Barton (Oct 24 2018 at 18:41):

Yeah, there are metavariables in the expected type, and in this case those prevent the coercion from triggering, I guess

#### Bryan Gin-ge Chen (Oct 24 2018 at 18:56):

Returning to your question about why `dec_trivial`

isn't just notation for `of_as_true trivial`

, the `prime 2`

and `prime 3`

examples can be proved with `of_as_true trivial`

, which is also disposing of all the other `dec_trivial`

examples I'm throwing at it at the moment. Can we cook up an example where `of_as_true trivial`

fails and the current `dec_trivial`

works?

#### Rob Lewis (Oct 24 2018 at 18:59):

example : 0 = 0 := dec_trivial example : 0 = 0 := of_as_true trivial

#### Rob Lewis (Oct 24 2018 at 19:04):

But returning to the original original question: I think there's something wrong with the current `nat.decidable_prime`

instance. For `n > 2`

it depends on evaluating `min_fac`

, and reducing `min_fac 3`

takes an implausible amount of time.

#### Reid Barton (Oct 24 2018 at 19:06):

I remember being confused by exactly this original issue about `is_prime 2`

and `is_prime 3`

as well when I was starting out using Lean. It would be nice if it could be fixed somehow.

#### Rob Lewis (Oct 24 2018 at 19:06):

`nat.decidable_prime`

should evaluate faster than `nat.decidable_prime_1`

in the VM, I think, but apparently not in the kernel.

#### Rob Lewis (Oct 24 2018 at 19:08):

Maybe this isn't "wrong," it could be the right default for the way `prime`

is used right now.

#### Rob Lewis (Oct 24 2018 at 19:08):

But it is confusing.

#### Bryan Gin-ge Chen (Oct 24 2018 at 19:13):

This works:

example : 0 = 0 := of_as_true (by exact trivial)

Is the current definition of `dec_trivial`

using `meta def triv : tactic unit := mk_const `trivial >>= exact`

equivalent to `of_as_true (by exact trivial)`

?

#### Mario Carneiro (Oct 24 2018 at 19:14):

yes, this is just the situation. `decidable_prime_1`

is faster in the kernel, `decidable_prime`

is faster in the VM (and also incorporates some tricks to speed up the checking of largeish numbers)

#### Mario Carneiro (Oct 24 2018 at 19:15):

I recommend using `by norm_num`

if you want a proof that a number is prime, though, since this builds a proof using similar tricks but the kernel will accept it

#### Rob Lewis (Oct 24 2018 at 19:16):

Oh, cool, I didn't know `norm_num`

did primality proofs.

#### Mario Carneiro (Oct 24 2018 at 19:17):

it's a recently added module

#### Reid Barton (Oct 24 2018 at 19:17):

Is the current definition of

`dec_trivial`

using`meta def triv : tactic unit := mk_const `trivial >>= exact`

equivalent to`of_as_true (by exact trivial)`

?

It should be, though maybe `tactic.interactive.exact`

is not available yet when `dec_trivial`

is being defined

#### Kevin Buzzard (Oct 24 2018 at 19:28):

Oh, cool, I didn't know

`norm_num`

did primality proofs.

https://xenaproject.wordpress.com/2018/07/26/617-is-prime/ -- last line!

#### Reid Barton (Oct 24 2018 at 19:30):

Now I'm wondering: what's the largest number formally proven to be prime

#### Kevin Buzzard (Oct 24 2018 at 19:31):

I would definitely start with the largest known Mersenne prime (i.e. the largest known prime).

#### Kevin Buzzard (Oct 24 2018 at 19:31):

Aren't the primality tests pretty low-level and trivial?

#### Kevin Buzzard (Oct 24 2018 at 19:31):

I think they take a couple of weeks to run though :-/

#### Reid Barton (Oct 24 2018 at 19:31):

You'd probably have to do a bit of elementary number theory to prove they are correct

#### Kenny Lau (Oct 24 2018 at 19:31):

Aren't the primality tests pretty low-level and trivial?

...

#### Kevin Buzzard (Oct 24 2018 at 19:31):

right

#### Kevin Buzzard (Oct 24 2018 at 19:32):

They are specific primality tests for Mersenne numbers

#### Reid Barton (Oct 24 2018 at 19:32):

A separate question is, if I gave you a "random" 256-bit prime, could we prove it's prime using the AKS primality test or something like that

#### Mario Carneiro (Oct 24 2018 at 19:33):

The current algorithm is just trial division with some optimizations

#### Mario Carneiro (Oct 24 2018 at 19:33):

so it is still exponential in the bits of the number

#### Mario Carneiro (Oct 24 2018 at 19:34):

I thought about implementing AKS, but it probably won't show an advantage until at least 15-digit primes

#### Rob Lewis (Oct 24 2018 at 19:35):

http://www.lix.polytechnique.fr/~werner/publis/flops06.pdf has some benchmarks.

#### Reid Barton (Oct 24 2018 at 19:46):

Apparently the answer was probably the 20th Mersenne prime $2^{4423} - 1$, at least as of whenever that paper was written

#### Kevin Buzzard (Oct 24 2018 at 19:49):

Is that all??

#### Kevin Buzzard (Oct 24 2018 at 19:49):

People aren't trying hard enough

#### Reid Barton (Oct 24 2018 at 19:52):

If I understood the paper correctly, they are using a mode of Coq with a VM implementation of reduction in the kernel, so it's a rather large trusted kernel code base as well

#### Reid Barton (Oct 24 2018 at 19:53):

though apparently they don't use native machine arithmetic, so I'm not really sure

#### Kevin Buzzard (Oct 28 2018 at 21:05):

So I finally had a chance to look at the paper Rob linked to. So they seem to be doing lots of things at once. They have implemented a generic primality test (this is before AKS I guess -- IIRC that was discovered around the same time). But I am not sure if people care about 10 more primes being verified prime -- people care about the *biggest* one. So forget Pocklington -- one wants to go straight for the Mersenne primes and probably use the polynomial time Lucas method. So the thing to go for is $P:=2^{9689}-1$. This can be proved prime if one can knock off a proof of the Lucas-Lehmer primality test, which looks well within reach, and then one has to basically square 9689 numbers modulo $P$. How feasible is that? I just ran the entire test in 217 ms in pari-gp.

#### Kevin Buzzard (Oct 28 2018 at 21:09):

The next question of course is how feasible it is to square 77232917 numbers modulo $2^{77232917}-1$.

#### Kevin Buzzard (Oct 28 2018 at 21:16):

It's probably worth pointing out that if numbers are somehow being stored in binary, then reducing modulo a number of the form $2^n-1$ can be done using specialised code which would perhaps be more efficient than usual Euclid? But I have no idea whatsoever how reasonable it would be to expect Lean to do any arithmetic at all with numbers so large.

Last updated: May 13 2021 at 23:16 UTC