fix: ac_nf0, simp_arith: don't tempt the kernel to reduce atoms

[nomeata]

this fixes #5699 and fixes #5384.

[nomeata]

This breaks handling of neutrals, it seems. Will need to have a closer look, but I think I know what to do.

[leanprover-community-bot]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-5708 has successfully built against this PR. (2024-10-14 14:29:17) View Log
• 🟡 Mathlib branch lean-pr-testing-5708 build against this PR was cancelled. (2024-10-15 16:45:25) View Log
• 🟡 Mathlib branch lean-pr-testing-5708 build against this PR was cancelled. (2024-10-15 17:00:23) View Log
• ✅ Mathlib branch lean-pr-testing-5708 has successfully built against this PR. (2024-10-15 18:03:13) View Log
• ✅ Mathlib branch lean-pr-testing-5708 has successfully built against this PR. (2024-10-15 19:27:10) View Log

[nomeata]

Is this tactic unused in mathlib? I am surprised mathlib CI passed before my latest commit!

[tobiasgrosser]

Is this tactic unused in mathlib? I am surprised mathlib CI passed before my latest commit!

There are 70 uses in mathlib. I skimmed them quickly and many of them seem to be symbolic. I could not spot neutral elements being used.

Thank you for the quick turnaround. It is great to see this bug resolved.

[bollu]

@nomeata do you think a similar issue could be behind omega's mysterious slowdowns with subtraction with made us change toNat_sub to toNat_sub' (/~https://github.com/leanprover/lean4/blob/master/src/Init/Data/BitVec/Lemmas.lean#L1977-L1982), with the test case here(/~https://github.com/leanprover/lean4/blob/master/tests/lean/run/omega.lean#L492-L505), inlined below:

-- This example, reported from LNSym,
-- started failing when we changed the definition of `Fin.sub` in /~https://github.com/leanprover/lean4/pull/4421.
-- When we use the new definition, `omega` produces a proof term that the kernel is very slow on.
-- To work around this for now, I've removed `BitVec.toNat_sub` from the `bv_toNat` simp set,
-- and replaced it with `BitVec.toNat_sub'` which uses the old definition for subtraction.
-- This is only a workaround, and I would like to understand why the term chokes the kernel.
example
    (n : Nat)
    (addr2 addr1 : BitVec 64)
    (h0 : n ≤ 18446744073709551616)
    (h1 : addr2 + 18446744073709551615#64 - addr1 ≤ BitVec.ofNat 64 (n - 1))
    (h2 : addr2 - addr1 ≤ addr2 + 18446744073709551615#64 - addr1) :
    n = 18446744073709551616 := by
  bv_omega

[nomeata]

That’s somewhat likely. In general, the test I would apply here: If the runtime changes if you change the constants, although the proof terms look otherwise the same, then the kernel is looking at the atoms of the proof when it shouldn’t.

Do we have an actual not-worked-around issue with omega to investigate?