Boolean circuits

InductiveBoolean gates#✓fully proved

The Boolean gates are a NOT gate and, for each natural number \(a\), an AND gate and an OR gate indexed by \(a\), which stand for gates with \(a + 1\) inputs. The numbers of inputs are assigned by the Boolean signature, so there is no AND or OR gate with zero inputs.

inductive BooleanGate where
  | not
  | and (arityMinusOne : Nat)
  | or (arityMinusOne : Nat)
  deriving Repr, DecidableEq

Used by 5

Used byBoolean interpretation · Boolean AND as a left fold · Boolean NOT · Boolean OR as a left fold · Boolean signature

DefinitionBoolean signature#✓fully proved

The Boolean signature has the Boolean gates as its operation symbols, where NOT has arity \(1\) and, for each natural number \(a\), the AND gate and the OR gate indexed by \(a\) have arity \(a + 1\). In particular, no AND or OR gate takes zero inputs.

def booleanSignature : Signature where
  Op := BooleanGate
  Arity
    | .not => 1
    | .and a => a + 1
    | .or a => a + 1

Uses 1 · Used by 8

Statement usesBoolean gates

Used byBoolean interpretation · Boolean certificate verifier · Completeness of the Boolean certificate verifier · Characterization of accepted certificates · Short accepted certificates exist exactly for satisfiable circuits · Soundness of the Boolean certificate verifier · Cost of the Boolean certificate verifier · Linear cost of the Boolean certificate verifier

DefinitionBoolean interpretation#✓fully proved

The Boolean interpretation evaluates the gates of the Boolean signature on the truth values \(\{\mathrm{false}, \mathrm{true}\}\): NOT sends its input \(x\) to \(\lnot x\), and for each natural number \(a\), the AND gate and the OR gate with inputs \(x_0, \dots, x_a\) return \((\cdots((\mathrm{true} \land x_0) \land x_1) \cdots) \land x_a\) and \((\cdots((\mathrm{false} \lor x_0) \lor x_1) \cdots) \lor x_a\) respectively, that is, the conjunction and the disjunction of the inputs.

def booleanInterpretation : Interpretation booleanSignature Bool
  | .not, f => !(f ⟨0, by decide⟩)
  | .and a, f => Fin.foldl (a + 1) (fun acc k => acc && f k) true
  | .or a, f => Fin.foldl (a + 1) (fun acc k => acc || f k) false

Uses 2 · Used by 9

Statement usesBoolean gates · Boolean signature

Used byBoolean AND as a left fold · Boolean NOT · Boolean OR as a left fold · Boolean certificate verifier · Completeness of the Boolean certificate verifier · Characterization of accepted certificates · Short accepted certificates exist exactly for satisfiable circuits · Soundness of the Boolean certificate verifier · Cost of the Boolean certificate verifier

TheoremBoolean NOT#✓fully proved

Under the Boolean interpretation, the NOT gate applied to a truth value \(x\) returns its negation \(\lnot x\).

@[simp] theorem booleanInterpretation_not (f : Fin 1 → Bool) :
    booleanInterpretation .not f = !(f 0)

Uses 2

Statement usesBoolean gates · Boolean interpretation

TheoremBoolean AND as a left fold#✓fully proved

For every natural number \(a\) and truth values \(x_0, \dots, x_a\), the Boolean interpretation of the AND gate with \(a + 1\) inputs, applied to \(x_0, \dots, x_a\), returns \((\cdots((\mathrm{true} \land x_0) \land x_1) \cdots) \land x_a\), folding conjunction over the inputs from left to right starting from true.

theorem booleanInterpretation_and (a : Nat) (f : Fin (a + 1) → Bool) :
    booleanInterpretation (.and a) f =
      Fin.foldl (a + 1) (fun acc k => acc && f k) true

Uses 2

Statement usesBoolean gates · Boolean interpretation

TheoremBoolean OR as a left fold#✓fully proved

For every natural number \(a\) and truth values \(x_0, \dots, x_a\), the Boolean interpretation of the OR gate with \(a + 1\) inputs, applied to \(x_0, \dots, x_a\), returns \((\cdots((\mathrm{false} \lor x_0) \lor x_1) \cdots) \lor x_a\), folding disjunction over the inputs from left to right starting from false.

theorem booleanInterpretation_or (a : Nat) (f : Fin (a + 1) → Bool) :
    booleanInterpretation (.or a) f =
      Fin.foldl (a + 1) (fun acc k => acc || f k) false

Uses 2

Statement usesBoolean gates · Boolean interpretation

6 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.