kernel hangs on ac_nf expression

[tobiasgrosser]

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

The following test case hangs in the kernel

axiom foo {p : Prop} {x : BitVec 32} (h : (!x == x + 0#32) = true) : p

theorem add_eq_sub_not_sub_one (x : BitVec 32) (h : (!x == x + (1#32 + 4294967295#32)) = true) : False := by
  simp only [BitVec.reduceAdd] at h
  exact foo h -- this works

theorem add_eq_sub_not_sub_one' (x : BitVec 32) (h : (!x == x + 1#32 + 4294967295#32) = true) : False := by
  ac_nf0 at h
  simp only [BitVec.reduceAdd] at h
  exact foo h -- this hangs here

Context

This issue arose when testing bv_decide with ac_nf enabled.

Steps to Reproduce

1. Copy into Lean
2. Wait for it to run
3. Observe yellow line next to exact foo h not disappearing

Expected behavior: Proof should be confirmed by kernel

Actual behavior: Kernel is hanging

Versions

"4.12.0, commit 225e089"

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

[nomeata]

Didn't look closely yet. This might have a similar cause as #5384

[nomeata]

Fun fact: Enabling set_option debug.skipKernelTC true makes it go through (as expected), but then trying to paste the proof term into a theorem, to play around with it, makes the elaborator hit the recursion depth:

theorem add_eq_sub_not_sub_one'' : ∀ (x : BitVec 32), (!x == x + 1#32 + 4294967295#32) = true → False :=
fun x h =>
  foo
    (Eq.mp
      (congrArg (fun x_1 => (!x == x_1) = true)
        (Lean.Data.AC.Context.eq_of_norm
          { op := HAdd.hAdd, assoc := BitVec.instAssociativeHAdd, comm := some { down := BitVec.instCommutativeHAdd },
            idem := none,
            vars :=
              [{ value := x, neutral := none }, { value := 1#32, neutral := none },
                { value := 4294967295#32, neutral := none }],
            arbitrary := x }
          (((Lean.Data.AC.Expr.var 0).op (Lean.Data.AC.Expr.var 1)).op (Lean.Data.AC.Expr.var 2))
          ((Lean.Data.AC.Expr.var 0).op ((Lean.Data.AC.Expr.var 1).op (Lean.Data.AC.Expr.var 2))) (Eq.refl true)))
      h)

I'm fairly certain that it’s the same issue as #5384; like there, a strategically placed id can do wonders:

theorem add_eq_sub_not_sub_one'' : ∀ (x : BitVec 32), (!x == x + 1#32 + 4294967295#32) = true → False :=
fun x h =>
  foo
    (Eq.mp
      (congrArg (fun x_1 => (!x == x_1) = true)
        (@id (∀ (x y z : BitVec 32), x + y + z = x + (y + z))
        (fun (x y z : BitVec 32) =>
        (Lean.Data.AC.Context.eq_of_norm
          { op := HAdd.hAdd, assoc := BitVec.instAssociativeHAdd, comm := some { down := BitVec.instCommutativeHAdd },
            idem := none,
            vars :=
              [{ value := x, neutral := none }, { value := y, neutral := none },
                { value := z, neutral := none }],
            arbitrary := x }
          (((Lean.Data.AC.Expr.var 0).op (Lean.Data.AC.Expr.var 1)).op (Lean.Data.AC.Expr.var 2))
          ((Lean.Data.AC.Expr.var 0).op ((Lean.Data.AC.Expr.var 1).op (Lean.Data.AC.Expr.var 2))) (Eq.refl true))) x 1#32 4294967295#32))
      h)

[nomeata]

Indeed, and the fix seems to work (#5708).

[tobiasgrosser]

Wow, what a fast turnaround. Thank you! 🥳