Update to Lean 2024-09-26 broke bv_automata

[luisacicolini]

Updating to the new Mathlib version (2024-09-26) broke AliveStatement bv_AddSub_1556:

theorem broken {x y : BitVec 1} : y - x = y ^^^ x := by
  bv_automata

The offending commit is likely leanprover/lean4-nightly@a3ca15d.

[tobiasgrosser]

A branch with the broken test case is available in #662.

[ineol]

I think the issue is that the statement is false (?). The error message is

application type mismatch
  Lean.ofReduceBool toto._nativeDecide_1 true (Eq.refl true)
argument has type
  true = true
but function has type
  Lean.reduceBool toto._nativeDecide_1 = true → broken._nativeDecide_1 = true

and Lean.reduceBool toto._nativeDecide_1 reduces to false, which makes the function application ill-typed.

There is the same error with an obviously false statement x = y.

In any case it would be good to have a more informative error message.

[tobiasgrosser]

The same issue arises with BitVec 1 instead of BitVec w. For BitVec 1, bv_decide successfully proofs the relevant statement.

[ineol]

As far as I understand, the bv_automata is a decision procedure for infinite bitstreams, so implicitly, it proves the result with arbitrary length.

Which version of Lean worked? I tried with 2024-09-20 and it has the same behavior.

[luisacicolini]

works for me at e6e6f63 - maybe try with bv_auto instead of bv_automata ?

[ineol]

I haven't found the source of the issue yet, but the problem is that now the bv_automata closes all the goals even if it fails, and produces an ill-typed proof. So in the bv_auto it stops the proof before bv_decide is able to prove the result. In the old version, it would leave the goal untouched, and bv_auto would try the next tactic.

[ineol]

I think what was happening is that before the update, ring_nf was broken (it had a multiplication by 1), and produced a goal that was refused by bv_automata before calling native_decide, which let the bv_decide tactic close the goal.

[tobiasgrosser]

I think what was happening is that before the update, ring_nf was broken (it had a multiplication by 1), and produced a goal that was refused by bv_automata before calling native_decide, which let the bv_decide tactic close the goal.

Indeed.