LRAT to Lean

This is an experimental project on translating a proof from a SAT solver directly into a Lean expression, compared to the approach used by bv_decide which uses a proof by reflection.

Upsides:

• Do not require extra axioms (except classical logic), so its proof would be supported by more Lean checkers.
• Operates directly on Prop, no necessity for a detour through Bool, or bitvector.
• Should be more efficient to verify by a Lean kernel than a proof by reflection that Lean kernel tries to evaluate (hypothesis to be tested).

Current status

The implementation of a translation from a LRAT proof into a Lean expression is implemented. So far, there is no connection to a SAT solver (I hope to use some of the machinery used by bv_decide).

The datastructure used should not be too distant from bv_decide, although here, we index from zero instead of one.

Files

• BinaryPack.lean -- Packing an array into a balanced tree (of And's).
• LRAT.lean -- The main file containing the data structures, and the translation.
• Test.lean -- Test & showcase.