Depth of composed circuits

Continuing a program does not change the depths of its wires (Program.wireDepths_append_castAdd), and the wires of the continuation are at most as deep as in the continuation alone, plus the depth of the wires feeding it (Program.wireDepths_append_appendedWire_le). So sequential composition adds depths (Circuit.depth_comp_le) and parallel composition takes their maximum (Circuit.depth_append_le).

Main results

• Cslib.Circuits.Program.wireDepths_append_castAdd, Cslib.Circuits.Program.wireDepths_append_appendedWire_le: depths in a continued program.
• Cslib.Circuits.Circuit.depth_comp_le: depth (d.comp c) ≤ depth d + depth c.
• Cslib.Circuits.Circuit.depth_append_le: depth (c.append d) ≤ max (depth c) (depth d).
• Cslib.Circuits.Circuit.depthWith_comp_le, Cslib.Circuits.Circuit.depthWith_append_le: the same for depths with costs.

@[simp]

theorem Cslib.Circuits.Program.wireDepthsWith_append_castAdd {σ : Signature} {n k g₁ g₂ : ℕ} (P : Program σ n g₁) (feed : Fin k → Wire n g₁) (cost : σ.Op → ℕ) (q : Program σ k g₂) (w : Wire n g₁) : wireDepthsWith cost (P.append feed q) (Wire.castAdd g₂ w) = wireDepthsWith cost P w

Continuing a program does not change the depths with costs of its wires.

theorem Cslib.Circuits.Program.wireDepthsWith_append_appendedWire_le {σ : Signature} {n k g₁ g₂ : ℕ} (P : Program σ n g₁) (feed : Fin k → Wire n g₁) (cost : σ.Op → ℕ) {D : ℕ} (hD : ∀ (i : Fin k), wireDepthsWith cost P (feed i) ≤ D) (q : Program σ k g₂) (w : Wire k g₂) : wireDepthsWith cost (P.append feed q) (appendedWire feed w) ≤ wireDepthsWith cost q w + D

With costs, a wire of the continuation is at most as deep as in the continuation alone, plus the depth of the wires feeding it.

@[simp]

theorem Cslib.Circuits.Program.wireDepths_append_castAdd {σ : Signature} {n k g₁ g₂ : ℕ} (P : Program σ n g₁) (feed : Fin k → Wire n g₁) (q : Program σ k g₂) (w : Wire n g₁) : (P.append feed q).wireDepths (Wire.castAdd g₂ w) = P.wireDepths w

Continuing a program does not change the depths of its wires.

theorem Cslib.Circuits.Program.wireDepths_append_appendedWire_le {σ : Signature} {n k g₁ g₂ : ℕ} (P : Program σ n g₁) (feed : Fin k → Wire n g₁) {D : ℕ} (hD : ∀ (i : Fin k), P.wireDepths (feed i) ≤ D) (q : Program σ k g₂) (w : Wire k g₂) : (P.append feed q).wireDepths (appendedWire feed w) ≤ q.wireDepths w + D

A wire of the continuation is at most as deep as in the continuation alone, plus the depth of the wires feeding it.

@[simp]

theorem Cslib.Circuits.Circuit.outputs_append_castAdd {σ : Signature} {n m p : ℕ} (c : Circuit σ n m) (d : Circuit σ n p) (o : Fin m) : (c.append d).outputs (Fin.castAdd p o) = Wire.castAdd d.size (c.outputs o)

@[simp]

theorem Cslib.Circuits.Circuit.outputs_append_natAdd {σ : Signature} {n m p : ℕ} (c : Circuit σ n m) (d : Circuit σ n p) (o : Fin p) : (c.append d).outputs (Fin.natAdd m o) = Program.appendedWire Wire.input (d.outputs o)

theorem Cslib.Circuits.Circuit.depthWith_comp_le {σ : Signature} {n m p : ℕ} (cost : σ.Op → ℕ) (d : Circuit σ m p) (c : Circuit σ n m) : depthWith cost (d.comp c) ≤ depthWith cost d + depthWith cost c

Sequential composition adds depths with costs.

theorem Cslib.Circuits.Circuit.depthWith_append_le {σ : Signature} {n m p : ℕ} (cost : σ.Op → ℕ) (c : Circuit σ n m) (d : Circuit σ n p) : depthWith cost (c.append d) ≤ max (depthWith cost c) (depthWith cost d)

Parallel composition takes the larger depth with costs.

theorem Cslib.Circuits.Circuit.depth_comp_le {σ : Signature} {n m p : ℕ} (d : Circuit σ m p) (c : Circuit σ n m) : (d.comp c).depth ≤ d.depth + c.depth

Sequential composition adds depths.

theorem Cslib.Circuits.Circuit.depth_append_le {σ : Signature} {n m p : ℕ} (c : Circuit σ n m) (d : Circuit σ n p) : (c.append d).depth ≤ max c.depth d.depth

Parallel composition takes the larger depth.