fix: reduceNat? match terms with free or meta variables

[joehendrix]

This removes checks in Lean.Meta.reduceNat? that caused it to fail on terms it could handle because they contain meta variables in arguments. This lead to those operations being reduced using their equational definitions and slow performance on large patterns:

set_option profiler true
set_option profiler.threshold 1

def testMod (x:Nat) :=
  match x with
  | 128 % 1024 => true
  | _ => false
-- elaboration took 3.02ms

def testMul (x:Nat) :=
  match x with
  | 128 * 1 => true
  | _ => false
-- type checking took 11.1ms
-- compilation of testMul.match_1 took 313ms
-- compilation of testMul took 65.7ms
-- elaboration took 58.9ms

Performance is slower on testMul than testMod because whnf ends up evaluateing 128 * 1 using Peano arithmetic while 128 % 1024 is able to avoid that treatment since 128 < 1024.

[leanprover-community-mathlib4-bot]

• ❗ Mathlib CI will not be attempted unless you rebase your PR onto the 'nightly' branch. (2024-01-04 19:22:41)

[leodemoura]

@joehendrix Thanks for catching this issue. Could you please add new tests using set_option maxHeartbeats <small-value> that fail without the fix?

[joehendrix]

Yes, I validated on my machine, and reordered the commits too so hopefully the CI will report the first commit fails.

[joehendrix]

Oh, I'm not sure if it ran the tests after all, but the commit shows a failure. If there's something else that needs to be done with this, let me know.

[joehendrix]

!bench

[leanprover-bot]

Here are the benchmark results for commit d0d3678.
There were significant changes against commit 7d90b05:

  Benchmark   Metric       Change
  =========================================
+ stdlib      wall-clock    -1.1% (-34.9 σ)

[semorrison]

Uh oh, this has caused a bunch of timeouts in Mathlib. I wish that we had tested Mathlib first before merging! (Per the bot's instructions above, this requires basing the Lean PR off nightly, or even better nightly-with-mathlib.)