how to ask Lean to *not* normalize a numeric expression?

Stream: Is there code for X?

[David Renshaw]

Is there a way to tell Lean to not try normalizing the big Nat in the following?

import Mathlib.Data.Nat.Basic
import Mathlib.Tactic

abbrev solution_value : ℕ := (2^·)^[1984] 1 - 3

theorem Imo1981Q6 (f : ℕ → ℕ → ℕ)
    (h1 : ∀ y, f 0 y = y + 1)
    (h2 : ∀ x, f (x + 1) 0 = f x 1)
    (h3 : ∀ x y, f (x + 1) (y + 1) = f x (f (x + 1) y)) :
    f 4 1981 = solution_value := by
  have h4 : ∀ y, f 1 y = y + 2 := by sorry
  have h5 : ∀ y, f 1 (y + 1) = f 1 y + 1 := by sorry
  have h6 : ∀ y, f 4 (y + 1) + 3 = 2^(f 4 y + 3) := by sorry
  have h7 : ∀ y, f 4 y = (2^·)^[y+3] 1 - 3 := sorry
  have h8 := h7 1981
  rw [show 1981 + 3 = 1984 by rfl] at h8

  -- I think that `exact h8` should work here, but I get
  -- `Nat.pow exponent is too big`
  -- Is there a way to tell Lean to avoid trying to normalize these numbers?

  sorry

[David Renshaw]

I thought that maybe sprinkling in with_reducible might help, but it does not seem to

[David Renshaw]

smaller example:

import Mathlib.Data.Nat.Basic
import Mathlib.Tactic

abbrev solution_value : ℕ := (2^·)^[1984] 1 - 3

example : solution_value = (2^·)^[1984] 1 - 3 := by sorry
-- rfl fails with `INTERNAL PANIC: Nat.pow exponent is too big`

[David Renshaw]

hm... this works

abbrev solution_value' : ℕ := (2^·)^[1984] 1

example : solution_value' = (2^·)^[1984] 1 := rfl

but somehow adding the subtraction as above makes it fail

[David Renshaw]

this also works

def Nat.sub' (a b : ℕ) := a - b

abbrev solution_value3 : ℕ := Nat.sub' ((2^·)^[1984] 1) 3

example : solution_value3 = Nat.sub' ((2^·)^[1984] 1) 3 := rfl

[David Renshaw]

My hypothesis is that the extern-ness of Nat.sub is interfering with how reducibility usually works: https://github.com/leanprover/lean4/blob/e6292bc0b890aed51447c1f6ef1cd503bd3abf0f/src/Init/Prelude.lean#L1715-L1718

[Mario Carneiro]

My guess is that it has to do more with the fact that Nat.sub is known to the kernel

[Mario Carneiro]

to see whether you are right or I am try the same test with Int.sub

[David Renshaw]

I don't know what "known to the kernel" means. Can something be "known to the kernel" without being extern?

[Mario Carneiro]

It is one of a fixed list of functions that the kernel has special support for

[Mario Carneiro]

https://github.com/leanprover/lean4/blob/e6292bc0b890aed51447c1f6ef1cd503bd3abf0f/src/Lean/Meta/WHNF.lean#L818-L824

[David Renshaw]

Hm... but even if it decides to try reducing the Nat.sub, why would it then try to reduce the Nat.iterate? That's not marked reducible.

[Mario Carneiro]

do we know whether this reduction is happening in the kernel or the elaborator?

[Mario Carneiro]

here's my trick for bypassing the elaborator:

import Mathlib.Logic.Function.Iterate

open Lean Elab Term List
elab "force" e:term : tactic => do
  let e ← elabTerm e none
  Tactic.liftMetaTactic1 fun g => g.assign e *> pure none

abbrev solution_value : Nat := Nat.sub ((2^·)^[1984] 1) 3

example : solution_value = Nat.sub ((2^·)^[1984] 1) 3 := by force Eq.refl solution_value

It still panics, so I guess the kernel is the one that does the reduction

[Mario Carneiro]

which also explains why reducibility doesn't matter

[Mario Carneiro]

This works without error:

abbrev solution_value : Nat := Nat.sub ((2^·)^[1984] 1) 3

#check (by force Eq.refl solution_value : solution_value = Nat.sub ((2^·)^[1984] 1) 3)

so the elaborator's type checker is fine with this

[Mario Carneiro]

replacing #check by example := calls the kernel typechecker as well, causing the panic

[David Renshaw]

Now I'm staring at the trace output of

abbrev solution_value3 : ℕ := (2^·)^[4] 1 - 3

set_option trace.Meta.isDefEq true in
example : solution_value3 = (2^·)^[4] 1 - 3 := by rfl

[Mario Carneiro]

that's the elaborator typechecker, it won't help

[David Renshaw]

Here's my current workaround:

import Mathlib.Data.Nat.Basic
import Mathlib.Tactic

def no_eval (x : ℕ) : ℕ := x

abbrev solution_value : ℕ := no_eval ((2^·)^[1984] 1 - 3)

example : solution_value = no_eval ((2^·)^[1984] 1 - 3) := rfl

[David Renshaw]

https://github.com/dwrensha/math-puzzles-in-lean4/blob/4feee9db9752acbc42417253ddb4c56e2c578a00/MathPuzzles/Imo1981P6.lean#L29-L35

[Eric Rodriguez]

can you sprinkle some ids instead of no_eval?

[David Renshaw]

Unfortunately, no, I was unable to get that to work. It seems to me that the Lean kernel eagerly reduces id similar to how it apparently eagerly reduces Nat.sub and Nat.add.

[David Renshaw]

(this might have to do with id's inline attribute)

[Kyle Miller]

As far as I understand it, inline should only affect the compiler, not the kernel

[Kyle Miller]

There's a hint attached to definitions (the "definitional height") that affects which definitions the kernel will unfold before others. I don't understand it very well, but maybe somehow no_eval has a different definitional height from id so is unfolded differently?

I don't see any special cases for id in the kernel, unlike nat operations which are special cased.