Stop unfolding expensive definitions

Stream: lean4

[Martin Dvořák]

How can I stop Lean from unfolding definitions that would lead to large terms?

import Mathlib.Data.Nat.Hyperoperation

def googol : ℕ := 10 ^ 100

def googolplex : ℕ := 10 ^ googol

theorem googolplex_gt_ho425 : hyperoperation 4 2 5 < googolplex := by
  simp [hyperoperation]
  rw [show 1+1=2 from rfl]
  simp [hyperoperation]
  have h1 : 2 ^ 2 ^ 2 ^ 2 ^ 2 < 2 ^ googol
  · apply pow_lt_pow_right <;> decide
  have h2 : 2 ^ googol < googolplex
  · apply pow_lt_pow_left <;> decide
  have result : 2 ^ 2 ^ 2 ^ 2 ^ 2 < googolplex := sorry -- h1.trans h2
  exact result

Uncommenting h1.trans h2 leads to a crash.
Maybe I am naïve, but I think that Lean should be able to check that h1.trans h2 has type 2 ^ 2 ^ 2 ^ 2 ^ 2 < googolplex without unfolding what googolplex is.

[David Renshaw]

My workaround for a similar issue: https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/how.20to.20ask.20Lean.20to.20*not*.20normalize.20a.20numeric.20expression.3F/near/394218219

[David Renshaw]

This seems to work:

theorem googolplex_gt_ho425 : hyperoperation 4 2 5 < 10 ^ googol := by
  simp [hyperoperation]
  rw [show 1+1=2 from rfl]
  simp [hyperoperation]
  have h1 : 2 ^ 2 ^ 2 ^ 2 ^ 2 < 2 ^ googol :=
    pow_lt_pow_right one_lt_two (by norm_num[googol])
  have h2 : 2 ^ googol < 10 ^ googol :=
    pow_lt_pow_left (by norm_num) zero_le_two (Nat.succ_ne_zero _)
  exact h1.trans h2

[David Renshaw]

I think the problem boils down to

lemma googleplex_def : googolplex = 10 ^ googol := by sorry

[David Renshaw]

I haven't found a way to prove that.

[David Renshaw]

Pulled into a self-contained example (no imports needed):

def googol : Nat := 10 ^ 100
def googolplex : Nat := 10 ^ googol

-- How can we prove this?
theorem googolplex_def : googolplex = 10 ^ googol := by
  sorry
  -- The proof should be `rfl`
  -- or perhaps `unfold googolplex; rfl`,
  -- but those hit "INTERNAL PANIC: Nat.pow exponent is too big"

  -- Adding @[irreducible] to the above defs does not help.

[Damiano Testa]

It seems that mathlibs irreducible_def is enough:

import Mathlib.Tactic.IrreducibleDef

irreducible_def googol : Nat := 10 ^ 100
def googolplex : Nat := 10 ^ googol

theorem googleplex_def : googolplex = 10 ^ googol := rfl

[Damiano Testa]

and the initial result also works:

import Mathlib.Data.Nat.Hyperoperation

irreducible_def googol : Nat := 10 ^ 100
def googolplex : Nat := 10 ^ googol

theorem googolplex_gt_ho425 : hyperoperation 4 2 5 < googolplex := by
  simp [hyperoperation]
  rw [show 1+1=2 from rfl]
  simp [hyperoperation]
  have h1 : 2 ^ 2 ^ 2 ^ 2 ^ 2 < 2 ^ googol
  · apply pow_lt_pow_right
    · decide
    · rw [googol_def]
      decide
  have h2 : 2 ^ googol < googolplex
  · apply pow_lt_pow_left
    · decide
    · decide
    · rw [googol_def]
      decide
  have result : 2 ^ 2 ^ 2 ^ 2 ^ 2 < googolplex := h1.trans h2
  exact result