De Morgan expressions compiled to circuits

This is a small tree language for Boolean formulas over the manuscript's actual basis. Unlike the Boolean-ring compiler, it emits NOT, AND, and OR directly, which is useful for zero tests, comparisons, selectors, and sorting-network records. Constants are represented by nullary gates but are free under DeMorgan.standardCost.

inductive Algebraic.DeMorgan.Expression (n : ℕ) : Type

Tree-shaped expressions over the De Morgan basis.

• input {n : ℕ} (index : Fin n) : Expression n
• constant {n : ℕ} (value : Bool) : Expression n
• not {n : ℕ} (child : Expression n) : Expression n
• and {n : ℕ} (left right : Expression n) : Expression n
• or {n : ℕ} (left right : Expression n) : Expression n

@[reducible]

def Algebraic.DeMorgan.Expression.gateCount {n : ℕ} : Expression n → ℕ

Number of program gates emitted by tree compilation.

Equations

• (Algebraic.DeMorgan.Expression.input index).gateCount = 0
• (Algebraic.DeMorgan.Expression.constant value).gateCount = 1
• child.not.gateCount = child.gateCount + 1
• (left.and right).gateCount = left.gateCount + right.gateCount + 1
• (left.or right).gateCount = left.gateCount + right.gateCount + 1

@[reducible]

def Algebraic.DeMorgan.Expression.standardCost {n : ℕ} : Expression n → ℕ

Standard charged cost: constants and inputs are free, and each logical operation costs one.

Equations

• (Algebraic.DeMorgan.Expression.input index).standardCost = 0
• (Algebraic.DeMorgan.Expression.constant value).standardCost = 0
• child.not.standardCost = child.standardCost + 1
• (left.and right).standardCost = left.standardCost + right.standardCost + 1
• (left.or right).standardCost = left.standardCost + right.standardCost + 1

def Algebraic.DeMorgan.Expression.eval {n : ℕ} (input : Fin n → Bool) : Expression n → Bool

Direct Boolean semantics.

Equations

• Algebraic.DeMorgan.Expression.eval input (Algebraic.DeMorgan.Expression.input index) = input index
• Algebraic.DeMorgan.Expression.eval input (Algebraic.DeMorgan.Expression.constant value) = value
• Algebraic.DeMorgan.Expression.eval input child.not = !Algebraic.DeMorgan.Expression.eval input child
• Algebraic.DeMorgan.Expression.eval input (left.and right) = (Algebraic.DeMorgan.Expression.eval input left && Algebraic.DeMorgan.Expression.eval input right)
• Algebraic.DeMorgan.Expression.eval input (left.or right) = (Algebraic.DeMorgan.Expression.eval input left || Algebraic.DeMorgan.Expression.eval input right)

def Algebraic.DeMorgan.Expression.mapInputs {sourceInputs targetInputs : ℕ} (inputMap : Fin sourceInputs → Fin targetInputs) : Expression sourceInputs → Expression targetInputs

Rename the input coordinates of an expression.

Equations

• Algebraic.DeMorgan.Expression.mapInputs inputMap (Algebraic.DeMorgan.Expression.input index) = Algebraic.DeMorgan.Expression.input (inputMap index)
• Algebraic.DeMorgan.Expression.mapInputs inputMap (Algebraic.DeMorgan.Expression.constant value) = Algebraic.DeMorgan.Expression.constant value
• Algebraic.DeMorgan.Expression.mapInputs inputMap child.not = (Algebraic.DeMorgan.Expression.mapInputs inputMap child).not
• Algebraic.DeMorgan.Expression.mapInputs inputMap (left.and right) = (Algebraic.DeMorgan.Expression.mapInputs inputMap left).and (Algebraic.DeMorgan.Expression.mapInputs inputMap right)
• Algebraic.DeMorgan.Expression.mapInputs inputMap (left.or right) = (Algebraic.DeMorgan.Expression.mapInputs inputMap left).or (Algebraic.DeMorgan.Expression.mapInputs inputMap right)

@[simp]

theorem Algebraic.DeMorgan.Expression.mapInputs_eval {sourceInputs targetInputs : ℕ} (inputMap : Fin sourceInputs → Fin targetInputs) (expression : Expression sourceInputs) (input : Fin targetInputs → Bool) : eval input (mapInputs inputMap expression) = eval (input ∘ inputMap) expression

@[simp]

theorem Algebraic.DeMorgan.Expression.mapInputs_gateCount {sourceInputs targetInputs : ℕ} (inputMap : Fin sourceInputs → Fin targetInputs) (expression : Expression sourceInputs) : (mapInputs inputMap expression).gateCount = expression.gateCount

@[simp]

theorem Algebraic.DeMorgan.Expression.mapInputs_standardCost {sourceInputs targetInputs : ℕ} (inputMap : Fin sourceInputs → Fin targetInputs) (expression : Expression sourceInputs) : (mapInputs inputMap expression).standardCost = expression.standardCost

def Algebraic.DeMorgan.Expression.constantCircuit (value : Bool) (n : ℕ) : Circuit signature n 1

One free constant gate.

Equations

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

@[simp]

theorem Algebraic.DeMorgan.Expression.constantCircuit_size (value : Bool) (n : ℕ) : (constantCircuit value n).size = 1

constantCircuit is a single constant gate.

def Algebraic.DeMorgan.Expression.notCircuit : Circuit signature 1 1

One direct NOT gate.

Equations

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

@[simp]

theorem Algebraic.DeMorgan.Expression.notCircuit_size : notCircuit.size = 1

notCircuit is a single gate.

def Algebraic.DeMorgan.Expression.andCircuit : Circuit signature 2 1

One direct AND gate.

Equations

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

@[simp]

theorem Algebraic.DeMorgan.Expression.andCircuit_size : andCircuit.size = 1

andCircuit is a single gate.

def Algebraic.DeMorgan.Expression.orCircuit : Circuit signature 2 1

One direct OR gate.

Equations

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

@[simp]

theorem Algebraic.DeMorgan.Expression.orCircuit_size : orCircuit.size = 1

orCircuit is a single gate.

def Algebraic.DeMorgan.Expression.circuit {n : ℕ} (expression : Expression n) : Circuit signature n 1

Compile an expression into a one-output De Morgan circuit.

Equations

• (Algebraic.DeMorgan.Expression.input index).circuit = (Cslib.Circuits.Circuit.id Algebraic.DeMorgan.signature n).mapOutputs fun (x : Fin 1) => index
• (Algebraic.DeMorgan.Expression.constant value).circuit = Algebraic.DeMorgan.Expression.constantCircuit value n
• child.not.circuit = Algebraic.DeMorgan.Expression.notCircuit.comp child.circuit
• (left.and right).circuit = Algebraic.DeMorgan.Expression.andCircuit.comp (left.circuit.parallel right.circuit)
• (left.or right).circuit = Algebraic.DeMorgan.Expression.orCircuit.comp (left.circuit.parallel right.circuit)

@[simp]

theorem Algebraic.DeMorgan.Expression.circuit_size {n : ℕ} (expression : Expression n) : expression.circuit.size = expression.gateCount

Compilation emits exactly gateCount program gates.

@[simp]

theorem Algebraic.DeMorgan.Expression.circuit_eval {n : ℕ} (expression : Expression n) (input : Fin n → Bool) : expression.circuit.eval interpretation input 0 = eval input expression

Compilation preserves Boolean semantics.

@[simp]

theorem Algebraic.DeMorgan.Expression.circuit_cost {n : ℕ} (expression : Expression n) : expression.circuit.cost DeMorgan.standardCost = expression.standardCost

Compilation realizes the expression's standard charged cost exactly.

def Algebraic.DeMorgan.Expression.xor {n : ℕ} (left right : Expression n) : Expression n

De Morgan implementation of Boolean XOR.

Equations

• left.xor right = (left.or right).and (left.and right).not

@[simp]

theorem Algebraic.DeMorgan.Expression.xor_eval {n : ℕ} (left right : Expression n) (input : Fin n → Bool) : eval input (left.xor right) = eval input left + eval input right

def Algebraic.DeMorgan.Expression.finXor {n : ℕ} (count : ℕ) : (Fin count → Expression n) → Expression n

XOR a finite expression family, with false for the empty family.

Equations

• Algebraic.DeMorgan.Expression.finXor 0 x_2 = Algebraic.DeMorgan.Expression.constant false
• Algebraic.DeMorgan.Expression.finXor count.succ terms = (Algebraic.DeMorgan.Expression.finXor count fun (index : Fin count) => terms index.castSucc).xor (terms (Fin.last count))

@[simp]

theorem Algebraic.DeMorgan.Expression.finXor_eval {n : ℕ} (count : ℕ) (terms : Fin count → Expression n) (input : Fin n → Bool) : eval input (finXor count terms) = ∑ index : Fin count, eval input (terms index)

def Algebraic.DeMorgan.Expression.finAnd {n : ℕ} (count : ℕ) : (Fin count → Expression n) → Expression n

Conjunction of a finite expression family, with true as the empty conjunction.

Equations

• Algebraic.DeMorgan.Expression.finAnd 0 x_2 = Algebraic.DeMorgan.Expression.constant true
• Algebraic.DeMorgan.Expression.finAnd count.succ terms = (Algebraic.DeMorgan.Expression.finAnd count fun (index : Fin count) => terms index.castSucc).and (terms (Fin.last count))

def Algebraic.DeMorgan.Expression.finOr {n : ℕ} (count : ℕ) : (Fin count → Expression n) → Expression n

Disjunction of a finite expression family, with false as the empty disjunction.

Equations

• Algebraic.DeMorgan.Expression.finOr 0 x_2 = Algebraic.DeMorgan.Expression.constant false
• Algebraic.DeMorgan.Expression.finOr count.succ terms = (Algebraic.DeMorgan.Expression.finOr count fun (index : Fin count) => terms index.castSucc).or (terms (Fin.last count))

def Algebraic.DeMorgan.Expression.finAndValue (count : ℕ) : (Fin count → Bool) → Bool

Boolean fold matching finAnd's constructor order.

Equations

• Algebraic.DeMorgan.Expression.finAndValue 0 x_2 = true
• Algebraic.DeMorgan.Expression.finAndValue count.succ values = ((Algebraic.DeMorgan.Expression.finAndValue count fun (index : Fin count) => values index.castSucc) && values (Fin.last count))

def Algebraic.DeMorgan.Expression.finOrValue (count : ℕ) : (Fin count → Bool) → Bool

Boolean fold matching finOr's constructor order.

Equations

• Algebraic.DeMorgan.Expression.finOrValue 0 x_2 = false
• Algebraic.DeMorgan.Expression.finOrValue count.succ values = ((Algebraic.DeMorgan.Expression.finOrValue count fun (index : Fin count) => values index.castSucc) || values (Fin.last count))

@[simp]

theorem Algebraic.DeMorgan.Expression.finAnd_eval {n : ℕ} (count : ℕ) (terms : Fin count → Expression n) (input : Fin n → Bool) : eval input (finAnd count terms) = finAndValue count fun (index : Fin count) => eval input (terms index)

@[simp]

theorem Algebraic.DeMorgan.Expression.finOr_eval {n : ℕ} (count : ℕ) (terms : Fin count → Expression n) (input : Fin n → Bool) : eval input (finOr count terms) = finOrValue count fun (index : Fin count) => eval input (terms index)

theorem Algebraic.DeMorgan.Expression.finAndValue_eq_true_iff (count : ℕ) (values : Fin count → Bool) : finAndValue count values = true ↔ ∀ (index : Fin count), values index = true

theorem Algebraic.DeMorgan.Expression.finOrValue_eq_true_iff (count : ℕ) (values : Fin count → Bool) : finOrValue count values = true ↔ ∃ (index : Fin count), values index = true

theorem Algebraic.DeMorgan.Expression.finOrValue_oneHot (count : ℕ) (selected : Fin count) (flags values : Fin count → Bool) (selectedTrue : flags selected = true) (unique : ∀ (index : Fin count), flags index = true → index = selected) : (finOrValue count fun (index : Fin count) => flags index && values index) = values selected

A disjunction selected by a one-hot flag family returns the selected value.

theorem Algebraic.DeMorgan.Expression.finAnd_standardCost {n : ℕ} (count : ℕ) (terms : Fin count → Expression n) : (finAnd count terms).standardCost = ∑ index : Fin count, (terms index).standardCost + count

Exact charged cost of a finite conjunction.

theorem Algebraic.DeMorgan.Expression.finOr_standardCost {n : ℕ} (count : ℕ) (terms : Fin count → Expression n) : (finOr count terms).standardCost = ∑ index : Fin count, (terms index).standardCost + count

Exact charged cost of a finite disjunction.