Proof breaks when I `import Mathlib.Algebra.Group.Nat`

Stream: mathlib4

[Bhavik Mehta]

Here's my example:

import Mathlib.Algebra.Group.Nat.Defs

theorem me : (2 ^ 3 ^ 4 ^ 5 ^ 8) % 2 = (2 % 2) ^ 3 ^ 4 ^ 5 ^ 8 % 2 :=
  Nat.pow_mod 2 (3 ^ 4 ^ 5 ^ 8) 2

The proof is fine if I don't have imports, but breaks if I import that file. What's going on here?

[Junyan Xu]

Copying the error messages:

mathlib-demo.lean:4:2
exponent 390625 exceeds the threshold 256, exponentiation operation was not evaluated, use `set_option exponentiation.threshold <num>` to set a new threshold

mathlib-demo.lean:3:0
maximum recursion depth has been reached
use `set_option maxRecDepth <num>` to increase limit
use `set_option diagnostics true` to get diagnostic information

[Junyan Xu]

It's strange because the statement compiles if you use sorry:

theorem me : (2 ^ 3 ^ 4 ^ 5 ^ 8) % 2 = (2 % 2) ^ 3 ^ 4 ^ 5 ^ 8 % 2 := by
  sorry

but both the statement and proof are squiggle-lined when you supply the proof.

[Ruben Van de Velde]

It works just before Nat.instCommMonoid and fails just after, presumably because of the npow setup

[Jovan Gerbscheid]

The lemma Nat.pow_mod uses the direct instance of instNatPowNat, whereas the expression you wrote down uses Nat.instCommMonoid for the exponentiation. To unify them, lean needs to check that the two instances are the same. It does this using WHNF. But that leads to a very big natural number that is too big.

[Eric Wieser]

docs#instNatPowNat, docs#Nat.instCommMonoid

[Eric Wieser]

Do you think replacing npow : _ -> _ -> M with [toNatPow : Pow Nat M] would help?

[Jovan Gerbscheid]

No, I think the problem arises as soon as the instance isn't == to instNatPowNat. As long as it goes through Monoid, the instance won't be ==. So this leads to lean calling WHNF on the expression :boom:

[Eric Wieser]

Is this a job for unification hints?

[Eric Wieser]

Or perhaps for reducibility hints, which I think exist somewhere?

[Jovan Gerbscheid]

It is an inherent limitation in whnf. whnf is (naturally) the first thing that isDefEq does. But when combined with natural number exponentiation, it blows up.

[Jovan Gerbscheid]

When the exponents aren't too big, you can set the exponentiation limit to be high enough

set_option exponentiation.threshold 1000000

But for really large exponents you get into trouble :(

[Jovan Gerbscheid]

The only way around it I can think of is to have Nat.pow being marked as irreducible, but of course this isn't desirable globally.

Edit: we can't set this in the kernel, so the problem remains

[Jeremy Tan]

Jovan Gerbscheid said:

Edit: we can't set this in the kernel, so the problem remains

Then make it settable!

[Jovan Gerbscheid]

Arguably, the implementation of Lean.Meta.reduceNat? should be changed so that if the number is too big, it still returns a (as much as possible) reduced expression. And in particular it then avoids doing whnf.

The trouble is, if we make this change, whnf doesn't anymore do what its name claims. Because e.g. 2 ^ 1000 isn't actually in weak head normal form.

[Jovan Gerbscheid]

Jeremy Tan said:

Then make it settable!

I would agree it makes sense to make the kernel aware of what constants are irreducible. But making changes to the kernel is dangerous of course.