nat.pow

Stream: general

[Kevin Buzzard]

Someone just privately asked me how to prove 1 <= 2^k, and applying one_le_pow_of_one_le doesn't work because nat.has_pow is not definitionally monoid.has_pow. We were always told that nothing could be done about this because it was in core. Is this something which can now be changed though? Or would it just break a gazillion things and nobody can be bothered to fix them? The issue I'm concerned about is that the two functions have different conventions about the succ case: nat.pow is b^n*b and monoid.pow is a*a^n :-(

[Patrick Massot]

I think it mostly requires having someone with enough time and energy.

[Mario Carneiro]

there is a theorem to rewrite one in terms of the other

[Gabriel Ebner]

https://github.com/leanprover-community/lean/pull/128#issuecomment-610281436

[Reid Barton]

an amusing proof that relies on the current nat.pow, perhaps found by library_search?
https://github.com/leanprover-community/mathlib/blob/master/src/number_theory/primorial.lean#L163-L164

[Johan Commelin]

Gabriel Ebner said:

https://github.com/leanprover-community/lean/pull/128#issuecomment-610281436

I replied to this on github, but let me also ask it here. Lean has VM implementations for nat.pow for reasons of efficiency. But does the VM care whether nat.pow is defined as a*a^n or a^n*a?
If I understand things correctly, it doesn't, right?

[Mario Carneiro]

It doesn't use either one

[Mario Carneiro]

But it does care that the function being called is nat.pow

[Mario Carneiro]

if you call another function it won't be automagically replaced with the efficient C++ implementation

[Johan Commelin]

Right. Than it is like I expected.

[Reid Barton]

I've seen contradictory comments on whether nat.pow actually has special VM support at all. It seems to me that it doesn't:

rwbarton@scw-capybara:~/lean/lean$ git grep '"pow"'
src/library/vm/vm_float.cpp:    DECLARE_VM_BUILTIN(name({"native", "float", "pow"}),   [](vm_obj const & a1, vm_obj const & a2) {return mk_vm_float(std::pow(to_float(a1), to_float(a2)));});
rwbarton@scw-capybara:~/lean/lean$ git grep '"mul"'
src/library/vm/vm_float.cpp:    DECLARE_VM_BUILTIN(name({"native", "float", "mul"}),   [](vm_obj const & a1, vm_obj const & a2) {return mk_vm_float(to_float(a1) * to_float(a2));});
src/library/vm/vm_int.cpp:    DECLARE_VM_BUILTIN(name({"int", "mul"}),              int_mul);
src/library/vm/vm_nat.cpp:    DECLARE_VM_BUILTIN(name({"nat", "mul"}),              nat_mul);

[Gabriel Ebner]

You're right, only the bitwise operations have VM support. Feel free to r+ merge master into the nat.pow removal then.

[Johan Commelin]

Whut? So we can just remove nat.pow from core?

[Johan Commelin]

Wouldn't it actually be better to add VM support?

[Reid Barton]

Do you mean Chris's old PR? It didn't build because some of the removed lemmas are used elsewhere in core.
But I'm preparing a new PR that removes everything that depends on nat.pow (including the whole of data.bitvec) with the intention of adding corresponding lemmas about ^ = monoid.pow to mathlib.

[Reid Barton]

I wasn't necessarily expecting that to work, but it seems to be working.

[Reid Barton]

There's not really that much point in using an optimized nat.pow implementation unless you're calculating 0^n or 1^n for large n.

[Reid Barton]

Removing nat.pow completely is preferable to having nat.pow with the old implementation because it means there won't be lemmas about the old nat.pow.

[Gabriel Ebner]

I'm pretty sure that you can do better than the naive recursive version though. You can do $n^{32}$ in 5 multiplications instead of 31. There is also a dedicated pow function in gmp.

[Johan Commelin]

@Gabriel Ebner the naive version uses 32 multiplications, right :grinning_face_with_smiling_eyes: :stuck_out_tongue_wink:

[Reid Barton]

The change to Lean has landed, so here's my current progrress on the required mathlib changes. Primarily I still need to finish splitting up algebra.group_power and seeing what lemmas I can reuse in data.nat.lemmas. Later, if there are lemmas in the nat namespace that are exactly specializations of their general group_power counterparts, we can remove them completely.

Question: Is it worth adding a has_pow nat nat instance with the normal priority 1000, to be picked up immediately by instance search? I'm inclined to say it doesn't matter much since there are only a total of 12 instances of has_pow in mathlib, and 2 in core. If we do add it (now or in the future) we need to add back the corresponding parts of norm_num and ring (which I have just commented out for now).

[Floris van Doorn]

I think it is not necessary to have a separate instance has_pow nat nat.

[Kevin Buzzard]

If the plan is to make it defeq to the monoid pow one then do we need it? If the plan is to make it the other one then...well, this can't be the plan, because the plan is to solve the problem, and this is the problem.

[Reid Barton]

There isn't going to be any other one.

[Reid Barton]

The only reason to add it would be so that it gets tried earlier in the instance search order