The binary AND/OR basis

This basis is the common syntax for Boolean AND/OR circuits and set-theoretic intersection/union constructions. Separate operation costs can charge either kind of binary gate; andCost is the intersection-complexity convention used by the set-theoretic fusion method.

inductive Algebraic.AndOr.Op : Type

Operation symbols in the binary AND/OR basis.

• and : Op
• or : Op

@[instance_reducible]

instance Algebraic.AndOr.instDecidableEqOp : DecidableEq Op

Equations

• Algebraic.AndOr.instDecidableEqOp x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Algebraic.AndOr.instFintypeOp : Fintype Op

The AND/OR basis has two operation symbols.

Equations

• Algebraic.AndOr.instFintypeOp = Fintype.ofList [Algebraic.AndOr.Op.and, Algebraic.AndOr.Op.or] Algebraic.AndOr.instFintypeOp._proof_1

@[reducible]

def Algebraic.AndOr.arity : Op → ℕ

Both AND/OR operations have arity two.

Equations

• Algebraic.AndOr.arity x✝ = 2

@[simp]

theorem Algebraic.AndOr.arity_and : arity Op.and = 2

@[simp]

theorem Algebraic.AndOr.arity_or : arity Op.or = 2

@[reducible, inline]

abbrev Algebraic.AndOr.signature : Signature

Signature of the binary AND/OR basis.

Equations

• Algebraic.AndOr.signature = { Op := Algebraic.AndOr.Op, Arity := Algebraic.AndOr.arity }

def Algebraic.AndOr.boolInterpretation : Interpretation signature Bool

Standard Boolean interpretation of AND and OR.

Equations

• Algebraic.AndOr.boolInterpretation Algebraic.AndOr.Op.and input = (input ⟨0, Algebraic.AndOr.boolInterpretation._proof_3⟩ && input ⟨1, Algebraic.AndOr.boolInterpretation._proof_4⟩)
• Algebraic.AndOr.boolInterpretation Algebraic.AndOr.Op.or input = (input ⟨0, Algebraic.AndOr.boolInterpretation._proof_5⟩ || input ⟨1, Algebraic.AndOr.boolInterpretation._proof_6⟩)

def Algebraic.AndOr.setInterpretation (Γ : Type u) : Interpretation signature (Set Γ)

Interpret AND as intersection and OR as union.

Equations

• Algebraic.AndOr.setInterpretation Γ Algebraic.AndOr.Op.and input = input ⟨0, Algebraic.AndOr.boolInterpretation._proof_3⟩ ∩ input ⟨1, Algebraic.AndOr.boolInterpretation._proof_4⟩
• Algebraic.AndOr.setInterpretation Γ Algebraic.AndOr.Op.or input = input ⟨0, Algebraic.AndOr.boolInterpretation._proof_5⟩ ∪ input ⟨1, Algebraic.AndOr.boolInterpretation._proof_6⟩

def Algebraic.AndOr.andCost : OperationCost signature

Charge AND gates and treat OR gates as free.

Equations

• Algebraic.AndOr.andCost Algebraic.AndOr.Op.and = 1
• Algebraic.AndOr.andCost Algebraic.AndOr.Op.or = 0

def Algebraic.AndOr.orCost : OperationCost signature

Charge OR gates and treat AND gates as free.

Equations

• Algebraic.AndOr.orCost Algebraic.AndOr.Op.and = 0
• Algebraic.AndOr.orCost Algebraic.AndOr.Op.or = 1

@[simp]

theorem Algebraic.AndOr.andCost_and : andCost Op.and = 1

@[simp]

theorem Algebraic.AndOr.andCost_or : andCost Op.or = 0

@[simp]

theorem Algebraic.AndOr.orCost_and : orCost Op.and = 0

@[simp]

theorem Algebraic.AndOr.orCost_or : orCost Op.or = 1

noncomputable def Algebraic.AndOr.membership {Γ : Type u_1} (point : Γ) (set : Set Γ) : Bool

Boolean characteristic value of membership in a set.

Equations

• Algebraic.AndOr.membership point set = decide (point ∈ set)

@[simp]

theorem Algebraic.AndOr.membership_eq_true {Γ : Type u_1} (point : Γ) (set : Set Γ) : membership point set = true ↔ point ∈ set

@[simp]

theorem Algebraic.AndOr.membership_eq_false {Γ : Type u_1} (point : Γ) (set : Set Γ) : membership point set = false ↔ point ∉ set

theorem Algebraic.AndOr.membership_eq_iff {Γ : Type u_1} (point : Γ) (left right : Set Γ) : membership point left = membership point right ↔ (point ∈ left ↔ point ∈ right)

Equality of characteristic values is pointwise equivalence of membership.

theorem Algebraic.AndOr.membership_points_eq_iff {Γ : Type u_1} (left right : Γ) (set : Set Γ) : membership left set = membership right set ↔ (left ∈ set ↔ right ∈ set)

Equality of characteristic values at two points is equivalence of their membership in the set.

@[simp]

theorem Algebraic.AndOr.membership_setOf_bool_eq_true {Γ : Type u_1} (point : Γ) (value : Γ → Bool) : membership point {candidate : Γ | value candidate = true} = value point

@[simp]

theorem Algebraic.AndOr.membership_setOf_bool_eq_false {Γ : Type u_1} (point : Γ) (value : Γ → Bool) : membership point {candidate : Γ | value candidate = false} = !value point

noncomputable def Algebraic.AndOr.membershipHomomorphism {Γ : Type u_1} (point : Γ) : Homomorphism (setInterpretation Γ) boolInterpretation

Membership at a fixed point is a homomorphism from sets to Booleans.

Equations

• Algebraic.AndOr.membershipHomomorphism point = { map := Algebraic.AndOr.membership point, homomorphic := ⋯ }

@[simp]

theorem Algebraic.AndOr.membershipHomomorphism_map {Γ : Type u_1} (point : Γ) (set : Set Γ) : (membershipHomomorphism point).map set = membership point set