Shared Boolean minterms

The circuit computes the indicator of every assignment to its input bits. Each stage retains the preceding minterms and extends them by one new bit. Sharing the preceding table gives a linear bound in the number of assignments, including all constants and negations.

Main definitions

• Cslib.Circuits.Boolean.mintermCircuit: all assignment indicators in BitString.equivFin order.

Main results

• Cslib.Circuits.Boolean.eval_mintermCircuit: the output is the indicator of the input's index.
• Cslib.Circuits.Boolean.size_mintermCircuit_add_three_le: at most 4 * 2 ^ n - 3 gates.

References

• Adapted from MassProduction/ShannonCircuit.lean in S. Schlesinger, Boolean circuit mass production formalization.

def Cslib.Circuits.Boolean.mintermExtension (n : ℕ) (a : Fin (2 ^ (n + 1))) : Formula signature (2 ^ n + 1)

One extension reads a preceding minterm and tests the new head bit.

def Cslib.Circuits.Boolean.mintermCircuit (n : ℕ) : Circuit signature n (2 ^ n)

Shared indicators of all n-bit assignments, indexed least significant bit first.

@[simp]

theorem Cslib.Circuits.Boolean.eval_mintermCircuit (n : ℕ) (x : BitString n) (a : Fin (2 ^ n)) : (mintermCircuit n).eval interpretation x a = decide ((BitString.equivFin n) x = a)

Each output is true precisely for the assignment bearing that index.

theorem Cslib.Circuits.Boolean.size_mintermCircuit_add_three_le (n : ℕ) : (mintermCircuit n).size + 3 ≤ 4 * 2 ^ n

All minterms together use at most 4 * 2 ^ n - 3 gates, counting constants too.