Performance discrepancy between let and let_fun in bv_decide.

[hargoniX]

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”) (not applicable, bv_decide doesn't run there)

Description

This issue concerns a proof extracted from SMTLIB: smt/non-incremental/QF_BV/sage/app8/bench_1804.smt2:

example : ∀ (T1_6131 : BitVec 8),
  (!let_fun v_0 := BitVec.zeroExtend 32 T1_6131;
      true && (1578966#32).ult (v_0 + 1#32 + 1578140#32 + 2#32) && !v_0 == 1#32) =
    true := by

applying bv_decide to this hangs in the kernel, however if we apply bv_normalize and manually extract the goal state afterwards:

example (T1_6131 : BitVec 8) (h1 : (1578966#32).ult (1578143#32 + BitVec.zeroExtend 32 T1_6131) = true)
    (h2 : (!BitVec.zeroExtend 32 T1_6131 == 1#32) = true) : False := by

Is instantly solvable with bv_decide. Furthermore if we replace let_fun with let:

example : ∀ (T1_6131 : BitVec 8),
  (!let v_0 := BitVec.zeroExtend 32 T1_6131;
      ((1578966#32).ult (v_0 + 1#32 + 1578140#32 + 2#32) && !v_0 == 1#32)) = true := by

This is also perfectly solvable with bv_decide.

Based on this data it seems that:

1. Just working on the goal state after preprocessing passes the kernel trivially so the part of the proof term that the pre processing generates seems to confuse the kernel.
2. It makes a difference whether let or let_fun is used so the pass that removes lets is likely at fault, this is the code here: https://github.com/leanprover/lean4/blob/master/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize.lean#L193-L212. In particular given that we have recently done work on let_fun in simp it is likely that simp is at fault.

Expected behavior: let_fun and let should behave the same performance wise in this situation. In general let_fun should of course be faster.

Actual behavior: The let_fun version hangs, let doesn't.

Versions

Lean master at commit 37b53b7. In particular this is after fixing #6043 which also exposed issues while typechecking in the kernel.

Impact

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