What's under the hood of of_decide_eq_true?

Stream: new members

[Kevin Cheung]

I am happy to see that it is so easy to prove that a particular (small) number is prime. For example,

def prime_7 : Nat.Prime 7 := by decide

#print prime_7

When I look at the proof term, it's simply of_decide_eq_true (Eq.refl true). I tried looking into the source code for of_decide_eq_true but got completely lost. What is under the hood of this magic function? Pointers and insights greatly appreciated.

[Riccardo Brasca]

Here lean uses docs#Nat.decidablePrime (or docs#Nat.decidablePrime1), that essentially is the fact the "being a prime" is decidable, meaning there is an algorithm do check primality.

[Riccardo Brasca]

Note that this is a terrible algorithm, in practice using norm_num is much better.

[Kevin Cheung]

Does norm_num basically do a brute force search for prime factors?

[Riccardo Brasca]

I don't know exactly what it does, but the doc says "It also has a relatively simple primality prover" so, even if it's not super sophisticated it's not trivial either.

[Riccardo Brasca]

You can have a look at the code source if you are interested

[Kevin Cheung]

I am willing to go down the rabbit hole. It's just that reading Lean code is not that easy at the moment given my limited experience programming anything nontrivial in Lean.

[Riccardo Brasca]

here

[Kevin Cheung]

Thank you.

[Riccardo Brasca]

Are you interested in writing math proof or rather programming in Lean?

[Kevin Cheung]

Both.

[Kevin Cheung]

I will need the programming part because I will need to develop my own tactics for the project I have in mind.

[Riccardo Brasca]

Note that norm_num is a complicated tactic, it's maybe better to start with something easier.

[Kevin Cheung]

Sure. Thanks for the tip.

[Riccardo Brasca]

here you can find several learning resources, including about metaprogramming. And of course asking here is always a good idea.

[Kyle Miller]

Kevin Cheung said:

When I look at the proof term, it's simply of_decide_eq_true (Eq.refl true). I tried looking into the source code for of_decide_eq_true but got completely lost. What is under the hood of this magic function? Pointers and insights greatly appreciated.

To figure out what Riccardo pointed out, when you hover over of_decide_eq_true, you want to look at its second argument, which is the Decidable argument. Here it's Nat.decidablePrime 7. A Decidable p value is like Bool, but it contains a proof that the boolean is the evaluation of the proposition p.

The magic is that of_decide_eq_true is causing typechecker to see that Nat.decidablePrime 7 : Decidable (Nat.Prime 7) evaluates to true.

[Kevin Cheung]

Is the evaluation performed in the Lean VM or in the Lean proof kernel?

[Kyle Miller]

It's evaluated twice, once by the elaborator's typechecker (which is also what's responsible for finding the instances using typeclass instance search), and once again by the kernel.

[Kyle Miller]

The norm_num code for Nat.Prime computes docs#Nat.minFac, which (1) returns 2 if the number is even and otherwise (2) does trial division using 3,5,7,9,... up to the square root of the number. This function is evaluated by the VM.

If the number's composite, then the norm_num extension proves it's composite by showing it's a nontrivial product. Otherwise, it constructs a proof that Nat.minFac equals what it equals. It looks like the proof isn't super big, so it must be sending some of it to the kernel for evaluation-by-reduction. These evaluations are done by the kernel using reduction.

[Kevin Cheung]

Interesting. So much magic going on behind the scenes.