Read-once De Morgan formulas and unateness

A read-once formula uses each input at most once, including through negation. It is unate: each input has a fixed direction of influence over all contexts. The substitution API is used to recover read-once formulas from tight shared circuits.

def Algebraic.DeMorgan.UnateAt {n : ℕ} (function : ScalarFunction Bool n) (i : Fin n) : Prop

A Boolean function has a fixed increasing or decreasing direction at a coordinate.

Equations

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

def Algebraic.DeMorgan.Unate {n : ℕ} (function : ScalarFunction Bool n) : Prop

Every input has a fixed direction of influence, possibly a different direction for each input.

Equations

• Algebraic.DeMorgan.Unate function = ∀ (i : Fin n), Algebraic.DeMorgan.UnateAt function i

theorem Algebraic.DeMorgan.unate_of_monotone {n : ℕ} {function : ScalarFunction Bool n} (monotone : Monotone function) : Unate function

Every monotone Boolean function is unate.

theorem Algebraic.DeMorgan.UnateAt.not {n : ℕ} {function : ScalarFunction Bool n} {i : Fin n} (h : UnateAt function i) : UnateAt (fun (input : Fin n → Bool) => !function input) i

Output complementation preserves unateness.

theorem Algebraic.DeMorgan.unateAt_not_iff {n : ℕ} (function : ScalarFunction Bool n) (i : Fin n) : UnateAt (fun (input : Fin n → Bool) => !function input) i ↔ UnateAt function i

A function and its complement are unate at exactly the same coordinates.

def Algebraic.DeMorgan.Expression.inputList {n : ℕ} : Expression n → List (Fin n)

Input occurrences in a formula, preserving repetitions and their order.

Equations

• (Algebraic.DeMorgan.Expression.input i).inputList = [i]
• (Algebraic.DeMorgan.Expression.constant value).inputList = []
• child.not.inputList = child.inputList
• (left.and right).inputList = left.inputList ++ right.inputList
• (left.or right).inputList = left.inputList ++ right.inputList

def Algebraic.DeMorgan.Expression.ReadOnce {n : ℕ} (expression : Expression n) : Prop

A formula is read-once when no input occurrence is repeated.

Equations

• expression.ReadOnce = expression.inputList.Nodup

def Algebraic.DeMorgan.Expression.substitute {n m : ℕ} (expression : Expression n) (replacement : Fin n → Expression m) : Expression m

Substitute an arbitrary formula for each input.

Equations

• (Algebraic.DeMorgan.Expression.input i).substitute replacement = replacement i
• (Algebraic.DeMorgan.Expression.constant value).substitute replacement = Algebraic.DeMorgan.Expression.constant value
• child.not.substitute replacement = (child.substitute replacement).not
• (left.and right).substitute replacement = (left.substitute replacement).and (right.substitute replacement)
• (left.or right).substitute replacement = (left.substitute replacement).or (right.substitute replacement)

theorem Algebraic.DeMorgan.Expression.eval_substitute {n m : ℕ} (expression : Expression n) (replacement : Fin n → Expression m) (input : Fin m → Bool) : eval input (expression.substitute replacement) = eval (fun (i : Fin n) => eval input (replacement i)) expression

Formula substitution composes the corresponding Boolean functions.

theorem Algebraic.DeMorgan.Expression.inputList_substitute {n m : ℕ} (expression : Expression n) (replacement : Fin n → Expression m) : (expression.substitute replacement).inputList = List.flatMap (fun (i : Fin n) => (replacement i).inputList) expression.inputList

Substitution replaces each input occurrence by the occurrences of its replacement.

theorem Algebraic.DeMorgan.Expression.eval_congr_inputList {n : ℕ} (expression : Expression n) (left right : Fin n → Bool) (agree : ∀ i ∈ expression.inputList, left i = right i) : eval left expression = eval right expression

Formula semantics depend only on the inputs occurring in the formula.

theorem Algebraic.DeMorgan.Expression.eval_update_eq_of_not_mem {n : ℕ} (expression : Expression n) {i : Fin n} (absent : i ∉ expression.inputList) (input : Fin n → Bool) (value : Bool) : eval (Function.update input i value) expression = eval input expression

Changing an absent input leaves the formula value unchanged.

theorem Algebraic.DeMorgan.Expression.ReadOnce.unate {n : ℕ} {expression : Expression n} (once : expression.ReadOnce) : Unate fun (input : Fin n → Bool) => eval input expression

A read-once De Morgan formula is unate, including formulas with internal negations.