De Morgan formulas

A De Morgan formula is a formula over the De Morgan signature, Formula Boolean.signature n, evaluated under Boolean.interpretation. Negations may appear anywhere. Pushing them to the leaves by De Morgan's laws does not change the leaf size, so lower bounds on the leaf size of these formulas are at least as strong as for formulas whose negations sit at the leaves Jukna, Chapter 6.

Main definitions

• Cslib.Circuits.Formula.const, Cslib.Circuits.Formula.not, Cslib.Circuits.Formula.and, Cslib.Circuits.Formula.or: De Morgan formulas built from constants and smaller formulas.
• Cslib.Circuits.Formula.xor: the exclusive or (F ∧ ¬G) ∨ (¬F ∧ G).
• Cslib.Circuits.Formula.orList, Cslib.Circuits.Formula.andList: the disjunction and the conjunction of a list of formulas as balanced trees of binary gates (Formula.balanced).
• Cslib.Circuits.Formula.literal: the literal of bit i that is true at z.
• Cslib.Circuits.Boolean.formulaDepth: the least depth of a De Morgan formula for a function, with negations and constants free.

Main results

• Cslib.Circuits.Formula.size_orList_add_one, Cslib.Circuits.Formula.depthWith_orList_le, Cslib.Circuits.Formula.size_andList_add_one, Cslib.Circuits.Formula.depthWith_andList_le: a balanced tree of k ≥ 1 formulas adds k - 1 nodes and ⌈log₂ k⌉ levels.
• Cslib.Circuits.Formula.exists_computes: every Boolean function has a De Morgan formula.
• Cslib.Circuits.Boolean.exists_computes_depthWith_eq_formulaDepth: some formula attains the formula depth.
• Cslib.Circuits.Boolean.arity_le_two: the De Morgan basis has fan-in at most two.

References

• S. Jukna, Boolean Function Complexity: Advances and Frontiers

def Cslib.Circuits.Formula.const {n : ℕ} (c : Bool) : Formula Boolean.signature n

The constant De Morgan formula.

def Cslib.Circuits.Formula.not {n : ℕ} (F : Formula Boolean.signature n) : Formula Boolean.signature n

The negation of a De Morgan formula.

def Cslib.Circuits.Formula.and {n : ℕ} (F G : Formula Boolean.signature n) : Formula Boolean.signature n

The conjunction of two De Morgan formulas.

def Cslib.Circuits.Formula.or {n : ℕ} (F G : Formula Boolean.signature n) : Formula Boolean.signature n

The disjunction of two De Morgan formulas.

def Cslib.Circuits.Formula.xor {n : ℕ} (F G : Formula Boolean.signature n) : Formula Boolean.signature n

The exclusive or of two De Morgan formulas, (F ∧ ¬G) ∨ (¬F ∧ G).

@[simp]

theorem Cslib.Circuits.Formula.eval_const {n : ℕ} (x : BitString n) (c : Bool) : (const c).eval Boolean.interpretation x = c

Evaluating const c returns c.

@[simp]

theorem Cslib.Circuits.Formula.eval_not {n : ℕ} (F : Formula Boolean.signature n) (x : BitString n) : F.not.eval Boolean.interpretation x = !F.eval Boolean.interpretation x

Evaluating F.not negates the value of F.

@[simp]

theorem Cslib.Circuits.Formula.eval_and {n : ℕ} (F G : Formula Boolean.signature n) (x : BitString n) : (F.and G).eval Boolean.interpretation x = (F.eval Boolean.interpretation x && G.eval Boolean.interpretation x)

Evaluating F.and G takes the conjunction of the values of F and G.

@[simp]

theorem Cslib.Circuits.Formula.eval_or {n : ℕ} (F G : Formula Boolean.signature n) (x : BitString n) : (F.or G).eval Boolean.interpretation x = (F.eval Boolean.interpretation x || G.eval Boolean.interpretation x)

Evaluating F.or G takes the disjunction of the values of F and G.

@[simp]

theorem Cslib.Circuits.Formula.eval_xor {n : ℕ} (F G : Formula Boolean.signature n) (x : BitString n) : (F.xor G).eval Boolean.interpretation x = (F.eval Boolean.interpretation x ^^ G.eval Boolean.interpretation x)

Evaluating F.xor G takes the exclusive or of the values of F and G.

@[simp]

theorem Cslib.Circuits.Formula.leafSize_not {n : ℕ} (F : Formula Boolean.signature n) : F.not.leafSize = F.leafSize

Negation preserves the leaf size of a formula.

@[simp]

theorem Cslib.Circuits.Formula.leafSize_and {n : ℕ} (F G : Formula Boolean.signature n) : (F.and G).leafSize = F.leafSize + G.leafSize

The leaf size of a conjunction is the sum of the leaf sizes of its conjuncts.

@[simp]

theorem Cslib.Circuits.Formula.leafSize_or {n : ℕ} (F G : Formula Boolean.signature n) : (F.or G).leafSize = F.leafSize + G.leafSize

The leaf size of a disjunction is the sum of the leaf sizes of its disjuncts.

@[simp]

theorem Cslib.Circuits.Formula.leafSize_xor {n : ℕ} (F G : Formula Boolean.signature n) : (F.xor G).leafSize = 2 * F.leafSize + 2 * G.leafSize

The leaf size of F.xor G is twice the sum of the leaf sizes of F and G.

@[simp]

theorem Cslib.Circuits.Formula.leafSize_const {n : ℕ} (c : Bool) : (const c).leafSize = 0

A constant formula has no input leaves.

@[simp]

theorem Cslib.Circuits.Formula.leafSizeIn_const {n : ℕ} (Y : Finset (Fin n)) (c : Bool) : leafSizeIn Y (const c) = 0

A constant formula has no leaves in Y.

@[simp]

theorem Cslib.Circuits.Formula.leafSizeIn_not {n : ℕ} (F : Formula Boolean.signature n) (Y : Finset (Fin n)) : leafSizeIn Y F.not = leafSizeIn Y F

Negation preserves the number of leaves in Y.

@[simp]

theorem Cslib.Circuits.Formula.leafSizeIn_and {n : ℕ} (F G : Formula Boolean.signature n) (Y : Finset (Fin n)) : leafSizeIn Y (F.and G) = leafSizeIn Y F + leafSizeIn Y G

The number of leaves in Y of a conjunction is the sum of those of its conjuncts.

@[simp]

theorem Cslib.Circuits.Formula.leafSizeIn_or {n : ℕ} (F G : Formula Boolean.signature n) (Y : Finset (Fin n)) : leafSizeIn Y (F.or G) = leafSizeIn Y F + leafSizeIn Y G

The number of leaves in Y of a disjunction is the sum of those of its disjuncts.

@[simp]

theorem Cslib.Circuits.Formula.size_const {n : ℕ} (c : Bool) : (const c).size = 1

A constant is one operation node.

@[simp]

theorem Cslib.Circuits.Formula.size_not {n : ℕ} (F : Formula Boolean.signature n) : F.not.size = F.size + 1

A negation adds one operation node.

@[simp]

theorem Cslib.Circuits.Formula.size_and {n : ℕ} (F G : Formula Boolean.signature n) : (F.and G).size = F.size + G.size + 1

A conjunction adds one operation node.

@[simp]

theorem Cslib.Circuits.Formula.size_or {n : ℕ} (F G : Formula Boolean.signature n) : (F.or G).size = F.size + G.size + 1

A disjunction adds one operation node.

@[simp]

theorem Cslib.Circuits.Formula.size_xor {n : ℕ} (F G : Formula Boolean.signature n) : (F.xor G).size = 2 * F.size + 2 * G.size + 5

Exclusive or uses two copies of each argument and five operation nodes.

@[simp]

theorem Cslib.Circuits.Formula.depth_const {n : ℕ} (c : Bool) : (const c).depth = 1

A constant has depth one.

@[simp]

theorem Cslib.Circuits.Formula.depth_not {n : ℕ} (F : Formula Boolean.signature n) : F.not.depth = F.depth + 1

A negation is one deeper than its argument.

@[simp]

theorem Cslib.Circuits.Formula.depth_and {n : ℕ} (F G : Formula Boolean.signature n) : (F.and G).depth = max F.depth G.depth + 1

A conjunction is one deeper than the deeper conjunct.

@[simp]

theorem Cslib.Circuits.Formula.depth_or {n : ℕ} (F G : Formula Boolean.signature n) : (F.or G).depth = max F.depth G.depth + 1

A disjunction is one deeper than the deeper disjunct.

theorem Cslib.Circuits.Formula.depth_xor_le {n : ℕ} (F G : Formula Boolean.signature n) : (F.xor G).depth ≤ max F.depth G.depth + 3

Exclusive or adds at most three levels beyond its deeper argument.

@[simp]

theorem Cslib.Circuits.Formula.depthWith_const {n : ℕ} (cost : Boolean.Op → ℕ) (c : Bool) : depthWith cost (const c) = cost (Boolean.Op.const c)

The weighted depth of const c is cost (.const c).

@[simp]

theorem Cslib.Circuits.Formula.depthWith_not {n : ℕ} (F : Formula Boolean.signature n) (cost : Boolean.Op → ℕ) : depthWith cost F.not = depthWith cost F + cost Boolean.Op.not

The weighted depth of F.not adds cost .not to the weighted depth of F.

@[simp]

theorem Cslib.Circuits.Formula.depthWith_and {n : ℕ} (F G : Formula Boolean.signature n) (cost : Boolean.Op → ℕ) : depthWith cost (F.and G) = max (depthWith cost F) (depthWith cost G) + cost Boolean.Op.and

The weighted depth of F.and G adds cost .and to the maximum weighted depth of F and G.

@[simp]

theorem Cslib.Circuits.Formula.depthWith_or {n : ℕ} (F G : Formula Boolean.signature n) (cost : Boolean.Op → ℕ) : depthWith cost (F.or G) = max (depthWith cost F) (depthWith cost G) + cost Boolean.Op.or

The weighted depth of F.or G adds cost .or to the maximum weighted depth of F and G.

@[simp]

theorem Cslib.Circuits.Formula.gate₂_and {n : ℕ} (F G : Formula Boolean.signature n) : gate₂ Boolean.Op.and ⋯ F G = F.and G

A conjunction is the binary node of .and.

@[simp]

theorem Cslib.Circuits.Formula.gate₂_or {n : ℕ} (F G : Formula Boolean.signature n) : gate₂ Boolean.Op.or ⋯ F G = F.or G

A disjunction is the binary node of .or.

def Cslib.Circuits.Formula.orList {n : ℕ} (l : List (Formula Boolean.signature n)) : Formula Boolean.signature n

The disjunction of a list of De Morgan formulas, as a balanced tree (Formula.balanced); the constant false for no formulas.

def Cslib.Circuits.Formula.andList {n : ℕ} (l : List (Formula Boolean.signature n)) : Formula Boolean.signature n

The conjunction of a list of De Morgan formulas, as a balanced tree (Formula.balanced); the constant true for no formulas.

@[simp]

theorem Cslib.Circuits.Formula.eval_orList {n : ℕ} (x : BitString n) (l : List (Formula Boolean.signature n)) : (orList l).eval Boolean.interpretation x = l.any fun (F : Formula Boolean.signature n) => F.eval Boolean.interpretation x

Evaluating orList l tests whether any formula in l evaluates to true.

@[simp]

theorem Cslib.Circuits.Formula.eval_andList {n : ℕ} (x : BitString n) (l : List (Formula Boolean.signature n)) : (andList l).eval Boolean.interpretation x = l.all fun (F : Formula Boolean.signature n) => F.eval Boolean.interpretation x

Evaluating andList l tests whether every formula in l evaluates to true.

@[simp]

theorem Cslib.Circuits.Formula.orList_nil {n : ℕ} : orList [] = const false

The disjunction of no formulas is the constant false.

@[simp]

theorem Cslib.Circuits.Formula.orList_singleton {n : ℕ} (F : Formula Boolean.signature n) : orList [F] = F

The disjunction of one formula is that formula.

@[simp]

theorem Cslib.Circuits.Formula.andList_nil {n : ℕ} : andList [] = const true

The conjunction of no formulas is the constant true.

@[simp]

theorem Cslib.Circuits.Formula.andList_singleton {n : ℕ} (F : Formula Boolean.signature n) : andList [F] = F

The conjunction of one formula is that formula.

theorem Cslib.Circuits.Formula.size_orList_add_one {n : ℕ} {l : List (Formula Boolean.signature n)} (hl : l ≠ []) : (orList l).size + 1 = (List.map size l).sum + l.length

A balanced disjunction of k ≥ 1 formulas has k - 1 operation nodes besides theirs.

theorem Cslib.Circuits.Formula.size_andList_add_one {n : ℕ} {l : List (Formula Boolean.signature n)} (hl : l ≠ []) : (andList l).size + 1 = (List.map size l).sum + l.length

A balanced conjunction of k ≥ 1 formulas has k - 1 operation nodes besides theirs.

theorem Cslib.Circuits.Formula.depthWith_orList_le {n : ℕ} {cost : Boolean.Op → ℕ} {l : List (Formula Boolean.signature n)} {d : ℕ} (hl : ∀ F ∈ l, depthWith cost F ≤ d) (hnil : l = [] → cost (Boolean.Op.const false) ≤ d) : depthWith cost (orList l) ≤ d + cost Boolean.Op.or * Nat.clog 2 l.length

A balanced disjunction is deeper than its disjuncts by ⌈log₂⌉ of their number times the cost of a disjunction; the disjunction of no formulas is a constant.

theorem Cslib.Circuits.Formula.depthWith_andList_le {n : ℕ} {cost : Boolean.Op → ℕ} {l : List (Formula Boolean.signature n)} {d : ℕ} (hl : ∀ F ∈ l, depthWith cost F ≤ d) (hnil : l = [] → cost (Boolean.Op.const true) ≤ d) : depthWith cost (andList l) ≤ d + cost Boolean.Op.and * Nat.clog 2 l.length

A balanced conjunction is deeper than its conjuncts by ⌈log₂⌉ of their number times the cost of a conjunction; the conjunction of no formulas is a constant.

theorem Cslib.Circuits.Formula.depthWith_binaryCost_orList_le {n : ℕ} {l : List (Formula Boolean.signature n)} {d : ℕ} (hl : ∀ F ∈ l, depthWith Boolean.binaryCost F ≤ d) : depthWith Boolean.binaryCost (orList l) ≤ d + Nat.clog 2 l.length

With negations and constants free, a balanced disjunction is deeper than its disjuncts by ⌈log₂⌉ of their number.

theorem Cslib.Circuits.Formula.depthWith_binaryCost_andList_le {n : ℕ} {l : List (Formula Boolean.signature n)} {d : ℕ} (hl : ∀ F ∈ l, depthWith Boolean.binaryCost F ≤ d) : depthWith Boolean.binaryCost (andList l) ≤ d + Nat.clog 2 l.length

With negations and constants free, a balanced conjunction is deeper than its conjuncts by ⌈log₂⌉ of their number.

def Cslib.Circuits.Formula.literal {n : ℕ} (z : BitString n) (i : Fin n) : Formula Boolean.signature n

The literal of bit i that is true at z.

@[simp]

theorem Cslib.Circuits.Formula.eval_literal {n : ℕ} (x z : BitString n) (i : Fin n) : (literal z i).eval Boolean.interpretation x = (x i == z i)

Evaluating literal z i at x tests whether x i equals z i.

@[simp]

theorem Cslib.Circuits.Formula.depthWith_literal {n : ℕ} (z : BitString n) (i : Fin n) : depthWith Boolean.binaryCost (literal z i) = 0

A literal has binary-gate depth zero.

theorem Cslib.Circuits.Formula.exists_computes {n : ℕ} (f : BooleanFunction n) : ∃ (F : Formula Boolean.signature n), F.Computes Boolean.interpretation f

Every Boolean function has a De Morgan formula: its disjunctive normal form.

theorem Cslib.Circuits.Boolean.arity_le_two (op : Op) : signature.Arity op ≤ 2

The De Morgan basis has fan-in at most two.

noncomputable def Cslib.Circuits.Boolean.formulaDepth {n : ℕ} (f : BooleanFunction n) : ℕ

The least depth of a De Morgan formula computing f, with negations and constants free: the least depth with costs binaryCost (Formula.minDepthWith), which is finite because every function has a formula (Formula.exists_computes).

@[simp]

theorem Cslib.Circuits.Boolean.natCast_formulaDepth {n : ℕ} (f : BooleanFunction n) : ↑(formulaDepth f) = Formula.minDepthWith interpretation binaryCost f

The formula depth is the least depth with costs binaryCost.

theorem Cslib.Circuits.Boolean.formulaDepth_le {n : ℕ} {f : BooleanFunction n} {F : Formula signature n} (hF : F.Computes interpretation f) : formulaDepth f ≤ Formula.depthWith binaryCost F

The formula depth is at most the depth of every formula computing the function.

theorem Cslib.Circuits.Boolean.exists_computes_depthWith_eq_formulaDepth {n : ℕ} (f : BooleanFunction n) : ∃ (F : Formula signature n), F.Computes interpretation f ∧ Formula.depthWith binaryCost F = formulaDepth f

Some formula attains the formula depth.