inductive Circuit (α : Type u) : Type u

Circuit α is a type of (partly normalized) Boolean circuits, where α gives the type of free variables in the circuit.

Morally, it represents a function Bool → ⋯ → Bool, where the number of Bool arguments is equal to the arity of α. See also eval for the explicit conversion of a circuit to a similar function

• tru: {α : Type u} → Circuit α
• fals: {α : Type u} → Circuit α
• var: {α : Type u} → Bool → α → Circuit α

  var b x represents literal x or the negated literat ¬x, depending on the value of b

• and: {α : Type u} → Circuit α → Circuit α → Circuit α
• or: {α : Type u} → Circuit α → Circuit α → Circuit α
• xor: {α : Type u} → Circuit α → Circuit α → Circuit α

instance instReprCircuit : {α : Type u_1} → [inst : Repr α] → Repr (Circuit α)

Equations

• instReprCircuit = { reprPrec := reprCircuit✝ }

def Circuit.vars {α : Type u} [DecidableEq α] : Circuit α → List α

Equations

• Circuit.tru.vars = []
• Circuit.fals.vars = []
• (Circuit.var a a_1).vars = [a_1]
• (a.and a_1).vars = (a.vars ++ a_1.vars).dedup
• (a.or a_1).vars = (a.vars ++ a_1.vars).dedup
• (a.xor a_1).vars = (a.vars ++ a_1.vars).dedup

theorem Circuit.nodup_vars {α : Type u} [DecidableEq α] (c : Circuit α) : c.vars.Nodup

def Circuit.varsFinset {α : Type u} [DecidableEq α] (c : Circuit α) : Finset α

Equations

• c.varsFinset = { val := ↑c.vars, nodup := ⋯ }

theorem Circuit.mem_varsFinset {α : Type u} [DecidableEq α] {c : Circuit α} {x : α} : x ∈ c.varsFinset ↔ x ∈ c.vars

def Circuit.eval {α : Type u} : Circuit α → (α → Bool) → Bool

Equations

• Circuit.tru.eval x = true
• Circuit.fals.eval x = false
• (Circuit.var b x_2).eval x = if b = true then x x_2 else !x x_2
• (c₁.and c₂).eval x = (c₁.eval x && c₂.eval x)
• (c₁.or c₂).eval x = (c₁.eval x || c₂.eval x)
• (c₁.xor c₂).eval x = (c₁.eval x ^^ c₂.eval x)

def Circuit.evalv {α : Type u} [DecidableEq α] (c : Circuit α) : ((a : α) → a ∈ c.vars → Bool) → Bool

Equations

• Circuit.tru.evalv x_2 = true
• Circuit.fals.evalv x_2 = false
• (Circuit.var b x_2).evalv f = if b = true then f x_2 ⋯ else !f x_2 ⋯
• (c₁.and c₂).evalv f = ((c₁.evalv fun (i : α) (hi : i ∈ c₁.vars) => f i ⋯) && c₂.evalv fun (i : α) (hi : i ∈ c₂.vars) => f i ⋯)
• (c₁.or c₂).evalv f = ((c₁.evalv fun (i : α) (hi : i ∈ c₁.vars) => f i ⋯) || c₂.evalv fun (i : α) (hi : i ∈ c₂.vars) => f i ⋯)
• (c₁.xor c₂).evalv f = ((c₁.evalv fun (i : α) (hi : i ∈ c₁.vars) => f i ⋯) ^^ c₂.evalv fun (i : α) (hi : i ∈ c₂.vars) => f i ⋯)

theorem Circuit.eval_eq_evalv {α : Type u} [DecidableEq α] (c : Circuit α) (f : α → Bool) : c.eval f = c.evalv fun (x : α) (x_1 : x ∈ c.vars) => f x

def Circuit.ofBool {α : Type u} (b : Bool) : Circuit α

Equations

• Circuit.ofBool b = if b = true then Circuit.tru else Circuit.fals

instance Circuit.instLE {α : Type u} : LE (Circuit α)

Equations

• Circuit.instLE = { le := fun (c₁ c₂ : Circuit α) => ∀ (f : α → Bool), c₁.eval f = true → c₂.eval f = true }

instance Circuit.instPreorder {α : Type u} : Preorder (Circuit α)

Equations

• Circuit.instPreorder = Preorder.mk ⋯ ⋯ ⋯

theorem Circuit.le_def {α : Type u} (c₁ : Circuit α) (c₂ : Circuit α) : c₁ ≤ c₂ ↔ ∀ (f : α → Bool), c₁.eval f = true → c₂.eval f = true

theorem Circuit.exists_eval_iff_exists_evalv {α : Type u} [DecidableEq α] (c : Circuit α) : (∃ (x : α → Bool), c.eval x = true) ↔ ∃ (x : (a : α) → a ∈ c.vars → Bool), c.evalv x = true

def Circuit.simplifyAnd {α : Type u} : Circuit α → Circuit α → Circuit α

Equations

• Circuit.tru.simplifyAnd x = x
• x.simplifyAnd Circuit.tru = x
• Circuit.fals.simplifyAnd x = Circuit.fals
• x.simplifyAnd Circuit.fals = Circuit.fals
• x✝.simplifyAnd x = x✝.and x

instance Circuit.instAndOp {α : Type u} : AndOp (Circuit α)

Equations

• Circuit.instAndOp = { and := Circuit.simplifyAnd }

@[simp]

theorem Circuit.eval_and {α : Type u} (c₁ : Circuit α) (c₂ : Circuit α) (f : α → Bool) : (c₁ &&& c₂).eval f = (c₁.eval f && c₂.eval f)

theorem Circuit.varsFinset_and {α : Type u} [DecidableEq α] (c₁ : Circuit α) (c₂ : Circuit α) : (c₁ &&& c₂).varsFinset ⊆ c₁.varsFinset ∪ c₂.varsFinset

def Circuit.simplifyOr {α : Type u} : Circuit α → Circuit α → Circuit α

Equations

• Circuit.tru.simplifyOr x = Circuit.tru
• x.simplifyOr Circuit.tru = Circuit.tru
• Circuit.fals.simplifyOr x = x
• x.simplifyOr Circuit.fals = x
• x✝.simplifyOr x = x✝.or x

instance Circuit.instOrOp {α : Type u} : OrOp (Circuit α)

Equations

• Circuit.instOrOp = { or := Circuit.simplifyOr }

@[simp]

theorem Circuit.eval_or {α : Type u} (c₁ : Circuit α) (c₂ : Circuit α) (f : α → Bool) : (c₁ ||| c₂).eval f = (c₁.eval f || c₂.eval f)

theorem Circuit.vars_or {α : Type u} [DecidableEq α] (c₁ : Circuit α) (c₂ : Circuit α) : (c₁ ||| c₂).vars ⊆ (c₁.vars ++ c₂.vars).dedup

theorem Circuit.varsFinset_or {α : Type u} [DecidableEq α] (c₁ : Circuit α) (c₂ : Circuit α) : (c₁ ||| c₂).varsFinset ⊆ c₁.varsFinset ∪ c₂.varsFinset

def Circuit.simplifyNot {α : Type u} : Circuit α → Circuit α

Equations

• Circuit.tru.simplifyNot = Circuit.fals
• Circuit.fals.simplifyNot = Circuit.tru
• (a.xor b).simplifyNot = a.simplifyNot.xor b
• (a.and b).simplifyNot = a.simplifyNot.or b.simplifyNot
• (a.or b).simplifyNot = a.simplifyNot.and b.simplifyNot
• (Circuit.var b a).simplifyNot = Circuit.var (!b) a

instance Circuit.instComplement {α : Type u} : Complement (Circuit α)

Equations

• Circuit.instComplement = { complement := Circuit.simplifyNot }

@[simp]

theorem Circuit.simplifyNot_eq_complement {α : Type u} (c : Circuit α) : c.simplifyNot = ~~~c

@[simp]

theorem Circuit.eval_complement {α : Type u} (c : Circuit α) (f : α → Bool) : (~~~c).eval f = !c.eval f

theorem Circuit.varsFinset_complement {α : Type u} [DecidableEq α] (c : Circuit α) : (~~~c).varsFinset ⊆ c.varsFinset

def Circuit.simplifyXor {α : Type u} : Circuit α → Circuit α → Circuit α

Equations

• Circuit.fals.simplifyXor x = x
• x.simplifyXor Circuit.fals = x
• Circuit.tru.simplifyXor x = ~~~x
• x.simplifyXor Circuit.tru = ~~~x
• x✝.simplifyXor x = x✝.xor x

theorem Bool.xor_not_left' (a : Bool) (b : Bool) : (!a ^^ b) = !(a ^^ b)

instance Circuit.instXor {α : Type u} : Xor (Circuit α)

Equations

• Circuit.instXor = { xor := Circuit.simplifyXor }

@[simp]

theorem Circuit.eval_xor {α : Type u} (c₁ : Circuit α) (c₂ : Circuit α) (f : α → Bool) : (c₁ ^^^ c₂).eval f = (c₁.eval f ^^ c₂.eval f)

theorem Circuit.vars_simplifyXor {α : Type u} [DecidableEq α] (c₁ : Circuit α) (c₂ : Circuit α) : (c₁.simplifyXor c₂).vars ⊆ (c₁.vars ++ c₂.vars).dedup

theorem Circuit.varsFinset_simplifyXor {α : Type u} [DecidableEq α] (c₁ : Circuit α) (c₂ : Circuit α) : (c₁.simplifyXor c₂).varsFinset ⊆ c₁.varsFinset ∪ c₂.varsFinset

theorem Circuit.varsFinset_xor {α : Type u} [DecidableEq α] (c₁ : Circuit α) (c₂ : Circuit α) : (c₁ ^^^ c₂).varsFinset ⊆ c₁.varsFinset ∪ c₂.varsFinset

def Circuit.map {α : Type u} {β : Type v} (_c : Circuit α) (_f : α → β) : Circuit β

Equations

• Circuit.tru.map x = Circuit.tru
• Circuit.fals.map x = Circuit.fals
• (Circuit.var b x_2).map x = Circuit.var b (x x_2)
• (c₁.and c₂).map x = c₁.map x &&& c₂.map x
• (c₁.or c₂).map x = c₁.map x ||| c₂.map x
• (c₁.xor c₂).map x = c₁.map x ^^^ c₂.map x

theorem Circuit.eval_map {α : Type u} {β : Type v} {c : Circuit α} {f : α → β} {g : β → Bool} : (c.map f).eval g = c.eval fun (x : α) => g (f x)

def Circuit.simplify {α : Type u} (_c : Circuit α) : Circuit α

Equations

• Circuit.tru.simplify = Circuit.tru
• Circuit.fals.simplify = Circuit.fals
• (Circuit.var a a_1).simplify = Circuit.var a a_1
• (a.and a_1).simplify = a.simplify &&& a_1.simplify
• (a.or a_1).simplify = a.simplify ||| a_1.simplify
• (a.xor a_1).simplify = a.simplify ^^^ a_1.simplify

@[simp]

theorem Circuit.eval_simplify {α : Type u} (c : Circuit α) (f : α → Bool) : c.simplify.eval f = c.eval f

def Circuit.sumVarsLeft {α : Type u} {β : Type v} [DecidableEq α] [DecidableEq β] : Circuit (α ⊕ β) → List α

Equations

• Circuit.tru.sumVarsLeft = []
• Circuit.fals.sumVarsLeft = []
• (Circuit.var a (Sum.inl x_1)).sumVarsLeft = [x_1]
• (Circuit.var a (Sum.inr val)).sumVarsLeft = []
• (c₁.and c₂).sumVarsLeft = (c₁.sumVarsLeft ++ c₂.sumVarsLeft).dedup
• (c₁.or c₂).sumVarsLeft = (c₁.sumVarsLeft ++ c₂.sumVarsLeft).dedup
• (c₁.xor c₂).sumVarsLeft = (c₁.sumVarsLeft ++ c₂.sumVarsLeft).dedup

def Circuit.sumVarsRight {α : Type u} {β : Type v} [DecidableEq α] [DecidableEq β] : Circuit (α ⊕ β) → List β

Equations

• Circuit.tru.sumVarsRight = []
• Circuit.fals.sumVarsRight = []
• (Circuit.var a (Sum.inl x_1)).sumVarsRight = []
• (Circuit.var a (Sum.inr val)).sumVarsRight = [val]
• (c₁.and c₂).sumVarsRight = (c₁.sumVarsRight ++ c₂.sumVarsRight).dedup
• (c₁.or c₂).sumVarsRight = (c₁.sumVarsRight ++ c₂.sumVarsRight).dedup
• (c₁.xor c₂).sumVarsRight = (c₁.sumVarsRight ++ c₂.sumVarsRight).dedup

theorem Circuit.eval_eq_of_eq_on_vars {α : Type u} [DecidableEq α] {c : Circuit α} {f : α → Bool} {g : α → Bool} (_h : ∀ x ∈ c.vars, f x = g x) : c.eval f = c.eval g

@[simp]

theorem Circuit.mem_vars_iff_mem_sumVarsLeft {α : Type u} {β : Type v} [DecidableEq α] [DecidableEq β] {c : Circuit (α ⊕ β)} {x : α} : x ∈ c.sumVarsLeft ↔ Sum.inl x ∈ c.vars

@[simp]

theorem Circuit.mem_vars_iff_mem_sumVarsRight {α : Type u} {β : Type v} [DecidableEq α] [DecidableEq β] {c : Circuit (α ⊕ β)} {x : β} : x ∈ c.sumVarsRight ↔ Sum.inr x ∈ c.vars

theorem Circuit.eval_eq_of_eq_on_sumVarsLeft_right {α : Type u} {β : Type v} [DecidableEq α] [DecidableEq β] {c : Circuit (α ⊕ β)} {f : α ⊕ β → Bool} {g : α ⊕ β → Bool} (_h₁ : ∀ x ∈ c.sumVarsLeft, f (Sum.inl x) = g (Sum.inl x)) (_h₂ : ∀ x ∈ c.sumVarsRight, f (Sum.inr x) = g (Sum.inr x)) : c.eval f = c.eval g

def Circuit.bOr {α : Type u} {β : Type v} (_s : List α) (_f : α → Circuit β) : Circuit β

Equations

• Circuit.bOr [] x = Circuit.fals
• Circuit.bOr (a :: l) x = List.foldl (fun (c : Circuit β) (x_1 : α) => c ||| x x_1) (x a) l

@[simp]

theorem Circuit.eval_foldl_or {α : Type u} {β : Type v} (s : List α) (f : α → Circuit β) (c : Circuit β) (g : β → Bool) : (List.foldl (fun (c : Circuit β) (x : α) => c ||| f x) c s).eval g = true ↔ c.eval g = true ∨ ∃ a ∈ s, (f a).eval g = true

@[simp]

theorem Circuit.eval_bOr {α : Type u} {β : Type v} {s : List α} {f : α → Circuit β} {g : β → Bool} : ((Circuit.bOr s f).eval g = true) = ∃ a ∈ s, (f a).eval g = true

def Circuit.bAnd {α : Type u} {β : Type v} (_s : List α) (_f : α → Circuit β) : Circuit β

Equations

• Circuit.bAnd [] x = Circuit.tru
• Circuit.bAnd (a :: l) x = List.foldl (fun (c : Circuit β) (x_1 : α) => c &&& x x_1) (x a) l

@[simp]

theorem Circuit.eval_foldl_and {α : Type u} {β : Type v} (s : List α) (f : α → Circuit β) (c : Circuit β) (g : β → Bool) : (List.foldl (fun (c : Circuit β) (x : α) => c &&& f x) c s).eval g = true ↔ c.eval g = true ∧ ∀ a ∈ s, (f a).eval g = true

@[simp]

theorem Circuit.eval_bAnd {α : Type u} {β : Type v} {s : List α} {f : α → Circuit β} {g : β → Bool} : (Circuit.bAnd s f).eval g = true ↔ ∀ a ∈ s, (f a).eval g = true

def Circuit.assignVars {α : Type u} {β : Type v} [DecidableEq α] (c : Circuit α) (_f : (a : α) → a ∈ c.vars → β ⊕ Bool) : Circuit β

Equations

• Circuit.tru.assignVars x_2 = Circuit.tru
• Circuit.fals.assignVars x_2 = Circuit.fals
• (Circuit.var b x_2).assignVars f = Sum.elim (Circuit.var b) (fun (c : Bool) => if (b ^^ c) = true then Circuit.fals else Circuit.tru) (f x_2 ⋯)
• (c₁.and c₂).assignVars f = (c₁.assignVars fun (x : α) (hx : x ∈ c₁.vars) => f x ⋯) &&& c₂.assignVars fun (x : α) (hx : x ∈ c₂.vars) => f x ⋯
• (c₁.or c₂).assignVars f = (c₁.assignVars fun (x : α) (hx : x ∈ c₁.vars) => f x ⋯) ||| c₂.assignVars fun (x : α) (hx : x ∈ c₂.vars) => f x ⋯
• (c₁.xor c₂).assignVars f = (c₁.assignVars fun (x : α) (hx : x ∈ c₁.vars) => f x ⋯) ^^^ c₂.assignVars fun (x : α) (hx : x ∈ c₂.vars) => f x ⋯

theorem List.length_le_of_subset_of_nodup {α : Type u} {l₁ : List α} {l₂ : List α} (hs : l₁ ⊆ l₂) (hnd : l₁.Nodup) : l₁.length ≤ l₂.length

theorem Circuit.varsFinset_assignVars {α : Type u} {β : Type v} [DecidableEq α] [DecidableEq β] (c : Circuit α) (f : (a : α) → a ∈ c.vars → β ⊕ Bool) : (c.assignVars f).varsFinset ⊆ c.varsFinset.biUnion fun (a : α) => if ha : a ∈ c.vars then match f a ha with | Sum.inl b => {b} | Sum.inr val => ∅ else ∅

theorem Circuit.card_varsFinset_assignVars_lt {α : Type u} {β : Type v} [DecidableEq α] [DecidableEq β] (c : Circuit α) (f : (a : α) → a ∈ c.vars → β ⊕ Bool) (a : α) (ha : a ∈ c.vars) (b : Bool) (hfa : f a ha = Sum.inr b) : (c.assignVars f).varsFinset.card < c.varsFinset.card

theorem Circuit.eval_assignVars {α : Type u} {β : Type v} [DecidableEq α] {c : Circuit α} {f : (a : α) → a ∈ c.vars → β ⊕ Bool} {g : β → Bool} : (c.assignVars f).eval g = c.evalv fun (a : α) (ha : a ∈ c.vars) => Sum.elim g id (f a ha)

def Circuit.fst {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] (c : Circuit (α ⊕ β)) : Circuit α

Equations

• One or more equations did not get rendered due to their size.

theorem Circuit.eval_fst {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] (c : Circuit (α ⊕ β)) (g : α → Bool) : c.fst.eval g = true ↔ ∃ (g' : β → Bool), c.eval (Sum.elim g g') = true

def Circuit.snd {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] (c : Circuit (α ⊕ β)) : Circuit β

Equations

• One or more equations did not get rendered due to their size.

theorem Circuit.eval_sn.d {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] (c : Circuit (α ⊕ β)) (g : β → Bool) : c.snd.eval g = true ↔ ∃ (g' : α → Bool), c.eval (Sum.elim g' g) = true

def Circuit.bind {α : Type u} {β : Type v} (_c : Circuit α) (_f : α → Circuit β) : Circuit β

Equations

• Circuit.tru.bind x = Circuit.tru
• Circuit.fals.bind x = Circuit.fals
• (Circuit.var b x_2).bind x = if b = true then x x_2 else ~~~x x_2
• (c₁.and c₂).bind x = c₁.bind x &&& c₂.bind x
• (c₁.or c₂).bind x = c₁.bind x ||| c₂.bind x
• (c₁.xor c₂).bind x = c₁.bind x ^^^ c₂.bind x

theorem Circuit.eval_bind {α : Type u} {β : Type v} (c : Circuit α) (f : α → Circuit β) (g : β → Bool) : (c.bind f).eval g = c.eval fun (a : α) => (f a).eval g

def Circuit.single {α : Type u} [DecidableEq α] {s : List α} (x : (a : α) → a ∈ s → Bool) : Circuit α

Equations

• Circuit.single x = Circuit.bAnd s fun (i : α) => if hi : i ∈ s then Circuit.var (x i hi) i else Circuit.tru

@[simp]

theorem Circuit.eval_single {α : Type u} [DecidableEq α] {s : List α} (x : (a : α) → a ∈ s → Bool) (g : α → Bool) : (Circuit.single x).eval g = true ↔ ∀ (a : α) (ha : a ∈ s), g a = x a ha

@[irreducible]

def Circuit.nonemptyAux {α : Type u} [DecidableEq α] (c : Circuit α) (l : List α) (_hL : c.vars = l) : { b : Bool // (∃ (x : α → Bool), c.eval x = true) = (b = true) }

Equations

• One or more equations did not get rendered due to their size.
• Circuit.tru.nonemptyAux x✝ x = ⟨true, ⋯⟩
• Circuit.fals.nonemptyAux x✝ x = ⟨false, ⋯⟩
• (Circuit.var b x_3).nonemptyAux x✝ x = ⟨true, ⋯⟩
• x.nonemptyAux [] hv = ⟨x.eval fun (x : α) => false, ⋯⟩

def Circuit.nonempty {α : Type u} [DecidableEq α] (c : Circuit α) : Bool

Equations

• c.nonempty = ↑(c.nonemptyAux c.vars ⋯)

theorem Circuit.nonempty_iff {α : Type u} [DecidableEq α] (c : Circuit α) : c.nonempty = true ↔ ∃ (x : α → Bool), c.eval x = true

theorem Circuit.nonempty_eq_false_iff {α : Type u} [DecidableEq α] (c : Circuit α) : c.nonempty = false ↔ ∀ (x : α → Bool), ¬c.eval x = true

def Circuit.always_true {α : Type u} [DecidableEq α] (c : Circuit α) : Bool

Equations

• c.always_true = !(~~~c).nonempty

theorem Circuit.always_true_iff {α : Type u} [DecidableEq α] (c : Circuit α) : c.always_true = true ↔ ∀ (x : α → Bool), c.eval x = true

instance Circuit.instDecidableRelLeOfDecidableEq {α : Type u} [DecidableEq α] : DecidableRel fun (x1 x2 : Circuit α) => x1 ≤ x2

Equations

• c₁.instDecidableRelLeOfDecidableEq c₂ = decidable_of_iff (((~~~c₁).or c₂).always_true = true) ⋯