Zulip Chat Archive

Stream: Is there code for X?

Topic: Totient decidability

Will Midwood (Nov 26 2022 at 18:09):

Hi everyone,

I was wondering if nat.totient is decidable, and if not is there a way to make it? Thanks.

Johan Commelin (Nov 26 2022 at 18:22):

Do you mean computable?

Johan Commelin (Nov 26 2022 at 18:22):

The file where nat.totient is defined does not contain the word noncomputable. So you should be good to go.

Will Midwood (Nov 27 2022 at 14:51):

How does one compute it then? Say nat.totient 9

Kevin Buzzard (Nov 27 2022 at 14:57):

Are you confusing Lean with a computer algebra package? Lean is designed to prove theorems about nat.totient, not compute it!

import data.nat.totient

#eval nat.totient 9

works, but don't expect to go much higher; this is just evaluating the definition, which was written to be useful for proving, not optimal for computing.

Eric Rodriguez (Nov 27 2022 at 15:09):

Is there a norm_num plugin?

Kevin Buzzard (Nov 27 2022 at 15:14):

import data.nat.totient

example : nat.totient 1000 = 37 :=
begin
  norm_num, -- failed to simplify
end

doesn't look like it

Scott Morrison (Nov 27 2022 at 16:02):

Lean could/should be a computer algebra system, as well as a theorem prover, it just needs "some work".

Kevin Buzzard (Nov 27 2022 at 16:38):

I have never really understood how one would go about this work. Let's stick to Lean 4, because that's presumably where it will happen if it happens. If the definition of nat.totient is "the number of units in Z/nZ", which it probably should be if one wants to prove theorems about it, then where does the more efficient $\phi(n)=n\prod_{p\mid n}(1-p^{-1})$ fit in? This will be a theorem, but it's probably the thing one would want to use for efficient computations.

Adam Topaz (Nov 27 2022 at 16:41):

IIRC, in Lean4 you can provide alternative efficient implementations for functions.

Adam Topaz (Nov 27 2022 at 16:42):

Does anyone know of an example where this is done?

Matthew Ballard (Nov 27 2022 at 17:03):

docs4#List.set_eq_setTR is an example tagged with the csimp attribute. There are good deal more in Std.Data.List.Basic

Adam Topaz (Nov 27 2022 at 17:22):

I'm more thinking of this implementedBy (I think) attribute... maybe I'm misremembering

Adam Topaz (Nov 27 2022 at 17:29):

https://github.com/leanprover-community/mathlib4/blob/5230db6df2ef97710db9e1c217513ec17566814c/Mathlib/Init/Logic.lean#L530

Matthew Ballard (Nov 27 2022 at 17:39):

:+1: But then the efficient implementation can't be reasoned about right?

Adam Topaz (Nov 27 2022 at 17:41):

I thought there was a way to reason about the alt def (assuming lean has a proof that the implementation is correct), but I can't seem to find any examples of this

Matthew Ballard (Nov 27 2022 at 17:59):

Yeah. Outside of test files I cannot find any use that does not involve unsafe.

Junyan Xu (Nov 27 2022 at 18:45):

From the example at the bottom of this page it seems at least GMP isn't considered unsafe... but it seems Lean 4 does offer an option to build Lean without GMP lean4#827

Last updated: Dec 20 2023 at 11:08 UTC