boolean_circuit_eval

def

Evaluates a Boolean circuit c with n inputs on a variable truth assignment x : Fin n → Bool, by structural recursion: variables look up their value in x, constants return their Boolean value, and NOT, AND, OR gates apply the corresponding Boolean operations to the evaluations of their subcircuits.

Statement

def boolean_circuit_eval {n : Nat} (c : BooleanCircuit n) (x : Fin n → Bool) : Bool

Source

Arora & Barak, Def 6.1

Verified

10 Sep 2026

Axioms

none listed

Built on 1

BooleanCircuitA Boolean circuit with n inputs over the standard De Morgan basis, with constructors for input variables indexed by Fin n, Boolean…

Used by 2

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…

Read back from the Lean

Given a natural number $n$, a Boolean circuit (formula) $c$ on $n$ variables, and an input assignment $x : \text{Fin } n \to \text{Bool}$, boolean_circuit_eval evaluates $c$ on $x$ to produce a Bool by recursion on $c$: - If $c = \text{var } i$, it returns $x(i)$. - If $c = \text{const } b$, it returns $b$. - If $c = \text{not } c'$, it returns the boolean negation of the evaluation of $c'$ on $x$. - If $c = \text{and } c_1\ c_2$, it returns the boolean conjunction of the evaluation of $c_1$ on $x$ and the evaluation of $c_2$ on $x$. - If $c = \text{or } c_1\ c_2$, it returns the boolean disjunction of the evaluation of $c_1$ on $x$ and the evaluation of $c_2$ on $x$.

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

/-- Evaluates a Boolean circuit on a truth assignment to its input variables. -/
def boolean_circuit_eval {n : Nat} (c : BooleanCircuit n) (x : Fin n → Bool) : Bool :=
  match c with
  | BooleanCircuit.var i => x i
  | BooleanCircuit.const b => b
  | BooleanCircuit.not c' => !boolean_circuit_eval c' x
  | BooleanCircuit.and c₁ c₂ => boolean_circuit_eval c₁ x && boolean_circuit_eval c₂ x
  | BooleanCircuit.or c₁ c₂ => boolean_circuit_eval c₁ x || boolean_circuit_eval c₂ x

Discuss this result Challenge it