More synthesis rules over the De Morgan basis

Rules for synthesis bounds stated through the truth values of their targets, which is how semantic arguments (simulations, reductions) produce Boolean functions: change a target to one with the same truth values (Synthesis.congr_iff), a constant, bounded disjunctions and conjunctions with uniform costs, disjunctions of conjunctions of literals, that is of available functions and their negations (Synthesis.any_all_literal), exclusive ors and their finite sums, and arbitrary functions of a few selected inputs (Synthesis.selected). Also bounds on the circuit complexity of negations, conjunctions, disjunctions and exclusive ors, as instances of Cslib.Circuits.complexity_single_unary_le and Cslib.Circuits.complexity_single_binary_le.

Main results

• Cslib.Circuits.Synthesis.congr_iff, Cslib.Circuits.Synthesis.of_forall_eq_const.
• Cslib.Circuits.Synthesis.exists_exists_mem, Cslib.Circuits.Synthesis.exists_forall_mem.
• Cslib.Circuits.Synthesis.literal, Cslib.Circuits.Synthesis.all_literal, Cslib.Circuits.Synthesis.any_all_literal.
• Cslib.Circuits.Synthesis.xor: an exclusive or costs four gates.
• Cslib.Circuits.Synthesis.sum: a finite exclusive or costs four gates per term.
• Cslib.Circuits.Synthesis.selected: any function of k selected inputs costs 2 ^ k * (2 * k + 2) + 1 gates.
• Cslib.Circuits.Boolean.complexity_not_le, Cslib.Circuits.Boolean.complexity_and_le, Cslib.Circuits.Boolean.complexity_or_le, Cslib.Circuits.Boolean.complexity_xor_le.

theorem Cslib.Circuits.Synthesis.congr_iff {n : ℕ} {s : Set (BooleanFunction n)} {f g : BooleanFunction n} {a : ℕ} (h : Synthesis Boolean.interpretation s {f} a) (hfg : ∀ (x : BitString n), f x = true ↔ g x = true) : Synthesis Boolean.interpretation s {g} a

Change the target of a synthesis bound to a function with the same truth values.

theorem Cslib.Circuits.Synthesis.of_forall_eq_const {n : ℕ} {s : Set (BooleanFunction n)} {f : BooleanFunction n} (b : Bool) (h : ∀ (x : BitString n), f x = b) : Synthesis Boolean.interpretation s {f} 1

A constant function costs one gate.

theorem Cslib.Circuits.Synthesis.exists_exists_mem {n : ℕ} {s : Set (BooleanFunction n)} {ι : Type u_1} (indices : Finset ι) (F : ι → BooleanFunction n) {c m : ℕ} (hcard : indices.card ≤ m) (h : ∀ i ∈ indices, Synthesis Boolean.interpretation s {F i} c) : ∃ (g : BooleanFunction n), (∀ (x : BitString n), g x = true ↔ ∃ i ∈ indices, F i x = true) ∧ Synthesis Boolean.interpretation s {g} (m * (c + 1) + 1)

A bounded disjunction, with a uniform bound c on the cost of its terms and a bound m on their number.

theorem Cslib.Circuits.Synthesis.exists_forall_mem {n : ℕ} {s : Set (BooleanFunction n)} {ι : Type u_1} (indices : Finset ι) (F : ι → BooleanFunction n) {c m : ℕ} (hcard : indices.card ≤ m) (h : ∀ i ∈ indices, Synthesis Boolean.interpretation s {F i} c) : ∃ (g : BooleanFunction n), (∀ (x : BitString n), g x = true ↔ ∀ i ∈ indices, F i x = true) ∧ Synthesis Boolean.interpretation s {g} (m * (c + 1) + 1)

A bounded conjunction, with a uniform bound c on the cost of its terms and a bound m on their number.

theorem Cslib.Circuits.Synthesis.literal {n : ℕ} {s : Set (BooleanFunction n)} {f : BooleanFunction n} (hf : f ∈ s) (b : Bool) : Synthesis Boolean.interpretation s {fun (x : BitString n) => decide (f x = b)} 1

A literal, an available function f asked to take the value b, costs at most one gate.

theorem Cslib.Circuits.Synthesis.all_literal {n : ℕ} {s : Set (BooleanFunction n)} {c : List (BooleanFunction n × Bool)} (hc : ∀ l ∈ c, l.1 ∈ s) : Synthesis Boolean.interpretation s {fun (x : BitString n) => c.all fun (l : BooleanFunction n × Bool) => decide (l.1 x = l.2)} (2 * c.length + 1)

A conjunction of literals over available functions costs two gates per literal and a constant.

theorem Cslib.Circuits.Synthesis.any_all_literal {n : ℕ} {s : Set (BooleanFunction n)} {D : List (List (BooleanFunction n × Bool))} {w : ℕ} (hw : ∀ c ∈ D, c.length ≤ w) (hD : ∀ c ∈ D, ∀ l ∈ c, l.1 ∈ s) : Synthesis Boolean.interpretation s {fun (x : BitString n) => D.any fun (c : List (BooleanFunction n × Bool)) => c.all fun (l : BooleanFunction n × Bool) => decide (l.1 x = l.2)} (D.length * (2 * w + 2) + 1)

A disjunction of conjunctions of at most w literals over available functions.

theorem Cslib.Circuits.Synthesis.xor {n : ℕ} {s : Set (BooleanFunction n)} {f g : BooleanFunction n} {a b : ℕ} (hf : Synthesis Boolean.interpretation s {f} a) (hg : Synthesis Boolean.interpretation s {g} b) : Synthesis Boolean.interpretation s {fun (x : BitString n) => f x ^^ g x} (a + b + 4)

The exclusive or f ⊕ g = (f ∨ g) ∧ ¬(f ∧ g) costs four gates beyond its arguments.

theorem Cslib.Circuits.Synthesis.sum {n : ℕ} {s : Set (BooleanFunction n)} {ι : Type u_1} (indices : Finset ι) (F : ι → BooleanFunction n) (cost : ι → ℕ) (h : ∀ i ∈ indices, Synthesis Boolean.interpretation s {F i} (cost i)) : Synthesis Boolean.interpretation s {fun (x : BitString n) => ∑ i ∈ indices, F i x} (∑ i ∈ indices, (cost i + 4) + 1)

A finite sum in the Boolean ring, an exclusive or of its terms, costs four gates per term and a constant.

theorem Cslib.Circuits.Synthesis.selected {n k : ℕ} (wires : Fin k → Fin n) (φ : BooleanFunction k) : Synthesis Boolean.interpretation (inputs n) {fun (x : Fin n → Bool) => φ (x ∘ wires)} (2 ^ k * (2 * k + 2) + 1)

A function of k selected inputs costs at most 2 ^ k * (2 * k + 2) + 1 gates: its disjunctive normal form tests every accepted assignment of the selected inputs. Selectors may repeat inputs.

Complexity of Boolean operations

theorem Cslib.Circuits.Boolean.complexity_not_le {n : ℕ} (f : BooleanFunction n) : complexity interpretation (single fun (x : Fin n → Bool) => !f x) ≤ complexity interpretation (single f) + 1

Negating the output costs one gate.

theorem Cslib.Circuits.Boolean.complexity_binary_le {n : ℕ} (f g : BooleanFunction n) (op : Bool → Bool → Bool) {c : ℕ} (hop : Synthesis interpretation (inputs 2) {fun (y : Fin 2 → Bool) => op (y 0) (y 1)} c) : complexity interpretation (single fun (x : Fin n → Bool) => op (f x) (g x)) ≤ complexity interpretation (single f) + complexity interpretation (single g) + c

Combining two outputs with a binary operation that costs c gates on two inputs costs c gates.

theorem Cslib.Circuits.Boolean.complexity_and_le {n : ℕ} (f g : BooleanFunction n) : complexity interpretation (single fun (x : Fin n → Bool) => f x && g x) ≤ complexity interpretation (single f) + complexity interpretation (single g) + 1

A conjunction of two outputs costs one gate.

theorem Cslib.Circuits.Boolean.complexity_or_le {n : ℕ} (f g : BooleanFunction n) : complexity interpretation (single fun (x : Fin n → Bool) => f x || g x) ≤ complexity interpretation (single f) + complexity interpretation (single g) + 1

A disjunction of two outputs costs one gate.

theorem Cslib.Circuits.Boolean.complexity_xor_le {n : ℕ} (f g : BooleanFunction n) : complexity interpretation (single fun (x : Fin n → Bool) => f x ^^ g x) ≤ complexity interpretation (single f) + complexity interpretation (single g) + 4

An exclusive or of two outputs costs four gates.