Lax Lean Archive

Boolean circuits

Lax429075.Circuits · concepts/Lax429075/Circuits.lean · lax-429075

definition

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Definition

    A circuit is a finite sequence of input, constant, negation, conjunction, and disjunction gates. Every wire refers to an earlier gate, and the output is a gate of the circuit. A satisfying wire assignment respects every gate and makes the output true.

    Concept map
    3 concepts; 4 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    In the paper

    • page 2 of this submission's paper

    Lean source view on GitHub

    1import Lax429075.CNF
    2
    3/-!
    4---
    5title: Boolean circuits
    6type: definition
    7---
    8A circuit is a finite sequence of input, constant, negation, conjunction,
    9and disjunction gates. Every wire refers to an earlier gate, and the output
    10is a gate of the circuit. A satisfying wire assignment respects every gate
    11and makes the output true.
    12-/
    13
    14namespace Lax429075.Circuits
    15
    16open CNF
    17
    18inductive Gate
    19 | input
    20 | constant (value : Bool)
    21 | neg (a : ℕ)
    22 | conj (a b : ℕ)
    23 | disj (a b : ℕ)
    24 deriving DecidableEq
    25
    26def Gate.inputs : Gate → List ℕ
    27 | .input | .constant _ => []
    28 | .neg a => [a]
    29 | .conj a b | .disj a b => [a, b]
    30
    31structure Circuit where
    32 gates : List Gate
    33 output : Fin gates.length
    34 ordered : ∀ g i, (g, i) ∈ gates.zipIdx → ∀ j ∈ g.inputs, j < i
    35
    36def Gate.check (ρ : Assignment) (i : ℕ) : Gate → Bool
    37 | .input => true
    38 | .constant b => ρ i == b
    39 | .neg a => ρ i == !(ρ a)
    40 | .conj a b => ρ i == (ρ a && ρ b)
    41 | .disj a b => ρ i == (ρ a || ρ b)
    42
    43def check (C : Circuit) (ρ : Assignment) : Bool :=
    44 ρ C.output && C.gates.zipIdx.all (fun gi => gi.1.check ρ gi.2)
    45
    46def Satisfiable (C : Circuit) : Prop := ∃ ρ, check C ρ = true
    47
    48end Lax429075.Circuits
    49
    Builds on
    Used by
    From Mathlib

    none

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…