Lean 4 mechanized proofs for the paper "Bolt: LTLf and LTL Learning Meet Boolean Set Cover".
The development is self-contained and does not depend on Mathlib or any external library beyond the Lean 4 core.
It is built with Lean 4 version v4.29.1 (see lean-toolchain).
The repository is organized into two modules corresponding to the two main theoretical parts of the paper.
Basic.lean
Defines LTLf formulas in negation normal form (Formula) and their semantics (Formula.accepts) on finite traces (Trace).
Negations are pushed to variables; the operators are True, False, Var, Next, WeakNext, Globally, Finally, Or, And, and Until.
UpperBound.lean
Proves the separability upper bound: for any non-empty finite trace t, the function Trace.exact t constructs an LTLf formula accepted by t and only by t.
Taking the disjunction over all positive traces then yields a separating formula for any consistent set of examples.
Basic.lean
Defines Boolean formulas in negation normal form (BoolFormula) over a set of atomic sets indexed by Fin n_sets.
A Valuation records membership of an element in each atomic set.
Also defines the domination preorder: f1.dominates f2 holds when f1 has no greater weight than f2 and correctly classifies a superset of the elements that f2 classifies correctly.
Domination.lean
Proves the key substitution lemma domin_replace: if f1 dominates f2, then replacing any occurrence of f2 by f1 in a Boolean formula yields a formula that dominates the original.
This is the formal justification for pruning the candidate family to an antichain during the Boolean Set Cover search.
UpperBound.lean
Proves the Boolean Set Cover upper bound: Valuation.exact v constructs a Boolean formula accepted by exactly the valuation v, establishing that a separating formula always exists when the instance is feasible.