feat: implement `ac_nf'`, an alternative normalizer that takes terms shared across both sides of an equality into account #43

alexkeizer · 2025-01-22T17:34:03Z

This PR adds ac_nf', a tactic that normalizes terms up to commutativity and associativity, much like ac_nf, but does it in a way that exposes common terms among both sides of an equality. For example, x₁ * (y₁ * z) = x₂ * (y₂ * z) is normalized to z * (x₁ * y₁) = z * (x₂ * y₂), pulling the shared variable z to the front on both sides. The PR also replaces the use of ac_nf in the normalization pass of bv_decide.

This tactic reuses the existing ac_nf implementation to (a) normalize compound atomic expression (e.g., x + y and y + x in x * (y + x) * (x + y)) and (b) produce an equivalence proof once a sharing-aware normal form has been determined. The new ac_nf' tactic is thus not a replacement for ac_nf.

Furthermore, we only run the normalization on terms of the form (a * b) = (c * d) for a, b, c, d bitvectors. This mirrors Bitwuzla's PassNormalize::process's PassNormalize::normalize_eq_add_mul. We leave the implementation of PassNormalize::normalize_comm_assoc, which is called when the toplevel terms are different for a subsequent patch.

For posterity, we record the precise location in Bitwuzla where the codepath occurs:

-- https://github.com/bitwuzla/bitwuzla/blob/d1f1bc2ad3963936d3167afb879867364554cee7/src/preprocess/pass/normalize.cpp#L1550-L1554
        Kind k = cur.kind();
        if (k == Kind::EQUAL && children[0].kind() == children[1].kind()
            && (children[0].kind() == Kind::BV_ADD
                || children[0].kind() == Kind::BV_MUL))
        {
          auto [res, norm] = normalize_eq_add_mul(children[0], children[1]);
          ...

…shared across both sides of an equality into account

src/Lean/Meta/Tactic/AC/Main.lean

src/Lean/Meta/Tactic/AC/Sharing.lean

alexkeizer · 2025-01-23T12:55:54Z

Currently, I've deliberately implemented the new ac_nf! without touching the implementation of ac_nf at all -- I do use ac_nf, but simply by calling the tactic to construct a proof, I don't share any datastructures or computation in the implementation.

This was deliberate, as I'd expect changes to ac_nf to invite additional scrutiny in review, but it does mean we're wasting some time by computing similar things twice. Then again, as the benchmark showed, tactic runtime is not a bottleneck at all, so this might be entirely fine. We might be able to also generate a more optimized proof-term by sharing implementation, which would be slightly more significant, but I'm not a 100% sure how much benefit there is on that side.

@bollu @hargoniX, thoughts?

tobiasgrosser · 2025-01-23T12:59:07Z

I think this was mostly fine. There was one change to ac_nf that deliberately changes the proof terms it generates to avoid overly eager kernel reduction. We should make sure these fixes also work in our case (change ac_nf history for details).

Turns out the sharing behaviour the example was meant to highlight is not actually implemented

This emphasizes that it only works for binary applications

The hyp is exactly the theorem statement, nothing is being tested