BooleanCircuit
A Boolean circuit with n inputs over the standard De Morgan basis, with constructors for input variables indexed by Fin n, Boolean constants, negation (NOT), conjunction (AND), and disjunction (OR).
Statement
inductive BooleanCircuit (n : Nat)- Source
- Arora & Barak, Section 6.1; Jukna, Section 1.1
- Verified
- 10 Sep 2026
- Axioms
- none listed
- Used by 3
- boolean_circuit_eval_demorgan_andFor any Boolean circuits c₁ and c₂ on n variables and any input assignment x : Fin n → Bool, evaluating the negation of their conjunction…
- boolean_circuit_eval_not_notFor any Boolean circuit c on n variables and any input assignment x : Fin n → Bool, evaluating the double negation BooleanCircuit.not…
- boolean_circuit_evalEvaluates a Boolean circuit c with n inputs on a variable truth assignment x : Fin n → Bool, by structural recursion: variables look up…
Read back from the Lean
An inductive datatype BooleanCircuit (n : Nat), parameterized by a natural number n, representing Boolean expressions/circuits over n input variables. It has five constructors:
- var: takes an index i : Fin n (an integer $0 \le i < n$) representing the $i$-th variable.
- const: takes a Boolean value b : Bool (true or false).
- not: takes a c : BooleanCircuit n and forms its negation.
- and: takes two subcircuits c₁, c₂ : BooleanCircuit n and forms their conjunction.
- or: takes two subcircuits c₁, c₂ : BooleanCircuit n and forms their disjunction.
Written by a model that saw only the Lean, never the English above. If the two disagree, that is worth a challenge.
Lean source view module on GitHub
/-- A Boolean circuit on n inputs over the standard De Morgan basis (AND, OR, NOT). -/ inductive BooleanCircuit (n : Nat) where | var (i : Fin n) : BooleanCircuit n | const (b : Bool) : BooleanCircuit n | not (c : BooleanCircuit n) : BooleanCircuit n | and (c₁ c₂ : BooleanCircuit n) : BooleanCircuit n | or (c₁ c₂ : BooleanCircuit n) : BooleanCircuit n