Panic in rw: Nat.pow exponent is too big

Stream: general

[Eric Wieser]

This works in Lean 3:

import data.nat.basic

example : 1 + 2 + 2^(2^32) = 2^(2^32) + 1 + 2 :=
begin
  rw [add_right_comm],
  rw [add_comm 1 _],
end

but in Lean 4 this panics:

import Mathlib.Data.Nat.Basic
import Mathlib.Algebra.Group.Basic

#eval Lean.versionString

example : 1 + 2 + 2^(2^32) = 2^(2^32) + 1 + 2 := by
  rewrite [add_right_comm]
  sorry

This looks to me like some numeric normalizer issue; the analogous version not in Nat works fine:

example {α} [Semiring α] :
    (1 : α) + 2 + 2^(2^32) = 2^(2^32) + 1 + 2 := by
  rewrite [add_right_comm]
  sorry

[Eric Wieser]

It's pretty unexpected to me that rewrite is even performing this normalization; but maybe I'm misdiagnosing and this is coming from the kernel

[Mario Carneiro]

large closed terms of type nat are kind of like live hand grenades, because calling whnf on them will cause them to be worked out in full, and many tactics do this when looking for structure

[Eric Wieser]

Is whnf in a tactic an anti-pattern? (vs let ~q(desiredHead $args) := e or the sugar-free alternative, for instance)

[Mario Carneiro]

I think even whnfR is bad, although this may depend on the nat function

[Eric Wieser]

Surely whnfR shouldn't be unfolding + / Nat.add?

[Mario Carneiro]

there's an issue open about that (lean4#1994)

[Mario Carneiro]

it does

[Mario Carneiro]

even though Nat.add is not reducible

[Mario Carneiro]

example : 2 + 2 = 4 := by with_reducible rfl
example : 2 + 2 = 4 := by with_reducible exact rfl
example : 2 + 2 = 4 := by with_reducible eq_refl

[Eric Wieser]

docs#OfNat.ofNat is also not reducible and yet gets unfolded here too, I guess

[Mario Carneiro]

just tested, 2 ^ 2 = 4 also works, so I think this is the culprit

[Eric Wieser]

Defining a Mathlib.Nat that is a copy of Nat would fix all this, right? Because whatever strange special casing that is going on would presumably not apply here?

[Eric Wieser]

(obviously that's a bad idea for other reasons, but panicking in a proof is pretty awful too)

[Mario Carneiro]

yes, let me double check what the check is

[Mario Carneiro]

it's a hard coded list of nat functions, including pow:

    match fn with
    | ``Nat.add => reduceBinNatOp Nat.add a1 a2
    | ``Nat.sub => reduceBinNatOp Nat.sub a1 a2
    | ``Nat.mul => reduceBinNatOp Nat.mul a1 a2
    | ``Nat.div => reduceBinNatOp Nat.div a1 a2
    | ``Nat.mod => reduceBinNatOp Nat.mod a1 a2
    | ``Nat.pow => reduceBinNatOp Nat.pow a1 a2
    | ``Nat.gcd => reduceBinNatOp Nat.gcd a1 a2
    | ``Nat.beq => reduceBinNatPred Nat.beq a1 a2
    | ``Nat.ble => reduceBinNatPred Nat.ble a1 a2
    | ``Nat.land => reduceBinNatOp Nat.land a1 a2
    | ``Nat.lor  => reduceBinNatOp Nat.lor a1 a2
    | ``Nat.xor  => reduceBinNatOp Nat.xor a1 a2
    | ``Nat.shiftLeft  => reduceBinNatOp Nat.shiftLeft a1 a2
    | ``Nat.shiftRight => reduceBinNatOp Nat.shiftRight a1 a2
    | _ => return none

[Eric Wieser]

Should this be conditioned on the reducibility being "default" or higher?

[Mario Carneiro]

I think it should

[Eric Wieser]

This optimized reduction seems like a good idea, but only in the cases where reduction should happen in the first place

[Mario Carneiro]

it's a bit unclear whether Nat.succ 3 = 4 should be considered a reducible defeq or not

[Mario Carneiro]

since Nat.succ isn't a function with a definition in the first place

[Eric Wieser]

attribute [reducible] Nat.succ is legal

[Mario Carneiro]

yeah but that doesn't mean anything, it has no associated defeq

[Mario Carneiro]

it's an opaque

[Eric Wieser]

Ah, I'm thinking of projections not constructors

[Mario Carneiro]

I guess ditto for Nat.zero = 0

[Eric Wieser]

Both of these should be not reducible because OfNat.ofNat isn't reducible, right?

[Mario Carneiro]

I think these are operating on raw literals?

[Mario Carneiro]

that actually seems somewhat surprising, this is the elaborator's WHNF function

[Mario Carneiro]

I guess the literal-wrapping must happen somewhere else, after getting the result of the WHNF

[Timo Carlin-Burns]

I don't know if this is related, but I've found that in unification, ground Nat terms often get normalized into numerals. e.g.

-- `Nat.zero.succ` gets normalized to `1`:
#check (show Nat.zero.succ.succ = Nat.succ _ by with_reducible rfl)
-- Nat.zero.succ.succ = Nat.succ 1

[Mario Carneiro]

yes, that would definitely explain the rw behavior, even if the matching itself is not at fault

[Jeremy Tan]

This alone gives (kernel) deep recursion detected already (from IMO 2010 Q5):

lemma bomb : 2010 ^ 2010 ^ 2010 ≤ 2 ^ 2 ^ 2 ^ 2 ^ 2 ^ 11 :=
  calc
    _ ≤ 2 ^ (11 * 2010 ^ 2010) := by rw [pow_mul]; gcongr; norm_num
    _ ≤ _ := by
      apply Nat.pow_le_pow_right zero_lt_two
      calc
        _ ≤ 2 ^ (4 + 11 * 2010) := by rw [pow_add, pow_mul]; gcongr <;> norm_num
        _ ≤ _ := by
          apply Nat.pow_le_pow_right zero_lt_two
          calc
            _ ≤ 2 ^ 2 ^ 2 ^ 2 := by norm_num
            _ ≤ _ := by gcongr <;> norm_num

[Jeremy Tan]

How do I get this error-free? No amount of set_option exponentiation.threshold will work

[Jeremy Tan]

Is there an option to "exclude exponentiation from kernel reduction"?

[Aaron Liu]

I was able to hack this together

import Mathlib

lemma bomb : 2010 ^ 2010 ^ 2010 ≤ 2 ^ 2 ^ 2 ^ 2 ^ 2 ^ 11 := by
  obtain ⟨pow, pow_def⟩ : ∃ (f : ℕ → ℕ → ℕ), ∀ a b, f a b = a ^ b := ⟨(· ^ ·), fun _ _ => rfl⟩
  simp_rw [← pow_def]
  calc
    _ ≤ pow 2 (11 * pow 2010 2010) := by
      rw [pow_def 2, pow_mul, pow_def]
      gcongr
      norm_num
    _ ≤ _ := by
      rw [pow_def 2, pow_def 2]
      apply Nat.pow_le_pow_right zero_lt_two
      calc
        _ ≤ pow 2 (4 + 11 * 2010) := by
          rw [pow_def 2, pow_add, pow_mul, pow_def]
          gcongr <;> norm_num
        _ ≤ _ := by
          rw [pow_def 2, pow_def 2]
          apply Nat.pow_le_pow_right zero_lt_two
          calc
            _ ≤ 2 ^ 2 ^ 2 ^ 2 := by norm_num
            _ ≤ _ := by
              repeat (rw [pow_def]; gcongr; (· norm_num); try (norm_num; done))

[Jeremy Tan]

We need a more elegant solution

[Jeremy Tan]

@Eric Wieser do you have any suggestions?

[Eric Wieser]

Eric Wieser said:

Defining a Mathlib.Nat that is a copy of Nat would fix all this, right? Because whatever strange special casing that is going on would presumably not apply here?

We could do this, but without actually doing a global replace

[Eric Wieser]

That is, have a SafeNat type that we copy all the Nat instances to, and some Equivs / induction principles to transport back and forth

[Eric Wieser]

This would be a leaf file in mathlib with a module doc summarizing this thread

[Jz Pan]

Maybe we need a mechanism temporarily marking some functions/expressions as irreducible, like Hold in Mathematica

[Jz Pan]

maybe irreducible_def hold := id, and (hold 2010) ^ (hold 2010) ^ (hold 2010) ≤ ....

[Niels Voss]

Would generalize h : 2010 = x work for this?