Transforming circuits line by line

Program.mapLines f replaces every line of a program by its image under f, a map of lines over one signature to lines over another that keeps the number of earlier gates, so the program keeps its shape and its size. If f keeps the value of every line, the transformed program computes the same gate values (Program.eval_mapLines), and if f never makes a line deeper, no gate becomes deeper (Program.depths_mapLines_le); if it keeps the depth of every line, it keeps the depth of every gate (Program.depths_mapLines). Translating the operations along a map of signatures (Program.mapOp) is the special case changing only the operations; removing repeated arguments of idempotent gates is another.

Main definitions

• Cslib.Circuits.Program.mapLines, Cslib.Circuits.Circuit.mapLines: the program or circuit with every line transformed.

Main results

• Cslib.Circuits.Program.eval_mapLines, Cslib.Circuits.Circuit.eval_mapLines: transforming lines that keep their values keeps the function computed. Their _at variants need the line condition only at the given input, permitting interpretations with fixed context.
• Cslib.Circuits.Program.cost_mapLines: transforming lines with matching operation costs preserves total program cost.
• Cslib.Circuits.Program.depths_mapLines_le, Cslib.Circuits.Circuit.depth_mapLines_le: transforming lines that get no deeper keeps the depth bounded.
• Cslib.Circuits.Program.depths_mapLines, Cslib.Circuits.Circuit.depth_mapLines: transforming lines that keep their depth keeps the depth.

def Cslib.Circuits.Program.mapLines {σ : Signature} {τ : Signature} {n : ℕ} (f : {g : ℕ} → Line σ n g → Line τ n g) {g : ℕ} : Program σ n g → Program τ n g

The program with every line line replaced by f line.

def Cslib.Circuits.Circuit.mapLines {σ : Signature} {τ : Signature} {n m : ℕ} (f : {g : ℕ} → Line σ n g → Line τ n g) (c : Circuit σ n m) : Circuit τ n m

The circuit with every line line of its program replaced by f line.

@[simp]

theorem Cslib.Circuits.Program.mapLines_empty {σ : Signature} {τ : Signature} {n : ℕ} {f : {g : ℕ} → Line σ n g → Line τ n g} : mapLines (fun {g : ℕ} => f) empty = empty

Transforming the lines of the empty program gives the empty program.

@[simp]

theorem Cslib.Circuits.Program.mapLines_gate {σ : Signature} {τ : Signature} {n g : ℕ} {f : {g : ℕ} → Line σ n g → Line τ n g} (p : Program σ n g) (line : Line σ n g) : mapLines (fun {g : ℕ} => f) (p.gate line) = (mapLines (fun {g : ℕ} => f) p).gate (f line)

Transforming the lines of a program transforms its last line and the lines before it.

@[simp]

theorem Cslib.Circuits.Circuit.mapLines_program {σ : Signature} {τ : Signature} {n m : ℕ} {f : {g : ℕ} → Line σ n g → Line τ n g} (c : Circuit σ n m) : (mapLines (fun {g : ℕ} => f) c).program = Program.mapLines (fun {g : ℕ} => f) c.program

The program of the transformed circuit is the transformed program.

@[simp]

theorem Cslib.Circuits.Circuit.mapLines_outputs {σ : Signature} {τ : Signature} {n m : ℕ} {f : {g : ℕ} → Line σ n g → Line τ n g} (c : Circuit σ n m) : (mapLines (fun {g : ℕ} => f) c).outputs = c.outputs

Transforming the lines keeps the outputs.

@[simp]

theorem Cslib.Circuits.Circuit.size_mapLines {σ : Signature} {τ : Signature} {n m : ℕ} {f : {g : ℕ} → Line σ n g → Line τ n g} (c : Circuit σ n m) : (mapLines (fun {g : ℕ} => f) c).size = c.size

Transforming the lines keeps the size.

theorem Cslib.Circuits.Program.cost_mapLines {σ : Signature} {τ : Signature} {n g : ℕ} {f : {g : ℕ} → Line σ n g → Line τ n g} {cost : σ.Op → ℕ} {cost' : τ.Op → ℕ} (hf : ∀ {g : ℕ} (line : Line σ n g), cost' (f line).op = cost line.op) (p : Program σ n g) : (mapLines (fun {g : ℕ} => f) p).cost cost' = p.cost cost

Transforming lines with matching operation costs preserves total cost.

theorem Cslib.Circuits.Program.eval_mapLines_at {σ : Signature} {τ : Signature} {n g : ℕ} {U : Type u} {f : {g : ℕ} → Line σ n g → Line τ n g} {I : Interpretation σ U} {J : Interpretation τ U} (x : Fin n → U) (hf : ∀ {g : ℕ} (line : Line σ n g) (gates : Fin g → U), (f line).eval J x gates = line.eval I x gates) (p : Program σ n g) : (mapLines (fun {g : ℕ} => f) p).eval J x = p.eval I x

At a fixed input, preserving every line value preserves every gate value.

theorem Cslib.Circuits.Program.eval_mapLines {σ : Signature} {τ : Signature} {n g : ℕ} {U : Type u} {f : {g : ℕ} → Line σ n g → Line τ n g} {I : Interpretation σ U} {J : Interpretation τ U} (hf : ∀ {g : ℕ} (line : Line σ n g) (x : Fin n → U) (gates : Fin g → U), (f line).eval J x gates = line.eval I x gates) (p : Program σ n g) (x : Fin n → U) : (mapLines (fun {g : ℕ} => f) p).eval J x = p.eval I x

Transforming lines that keep their values keeps the value of every gate.

theorem Cslib.Circuits.Circuit.eval_mapLines_at {σ : Signature} {τ : Signature} {n m : ℕ} {U : Type u} {f : {g : ℕ} → Line σ n g → Line τ n g} {I : Interpretation σ U} {J : Interpretation τ U} (x : Fin n → U) (hf : ∀ {g : ℕ} (line : Line σ n g) (gates : Fin g → U), (f line).eval J x gates = line.eval I x gates) (c : Circuit σ n m) : (mapLines (fun {g : ℕ} => f) c).eval J x = c.eval I x

At a fixed input, preserving every line value preserves every output value.

theorem Cslib.Circuits.Circuit.eval_mapLines {σ : Signature} {τ : Signature} {n m : ℕ} {U : Type u} {f : {g : ℕ} → Line σ n g → Line τ n g} {I : Interpretation σ U} {J : Interpretation τ U} (hf : ∀ {g : ℕ} (line : Line σ n g) (x : Fin n → U) (gates : Fin g → U), (f line).eval J x gates = line.eval I x gates) (c : Circuit σ n m) : (mapLines (fun {g : ℕ} => f) c).eval J = c.eval I

Transforming lines that keep their values keeps the function computed.

theorem Cslib.Circuits.Program.depths_mapLines_le {σ : Signature} {τ : Signature} {n g : ℕ} {f : {g : ℕ} → Line σ n g → Line τ n g} (hf : ∀ {g : ℕ} (line : Line σ n g) (depths : Wire n g → ℕ), (f line).depth depths ≤ line.depth depths) (p : Program σ n g) (k : Fin g) : (mapLines (fun {g : ℕ} => f) p).depths k ≤ p.depths k

Transforming lines that get no deeper makes no gate deeper.

theorem Cslib.Circuits.Program.wireDepths_mapLines_le {σ : Signature} {τ : Signature} {n g : ℕ} {f : {g : ℕ} → Line σ n g → Line τ n g} (hf : ∀ {g : ℕ} (line : Line σ n g) (depths : Wire n g → ℕ), (f line).depth depths ≤ line.depth depths) (p : Program σ n g) (w : Wire n g) : (mapLines (fun {g : ℕ} => f) p).wireDepths w ≤ p.wireDepths w

Transforming lines that get no deeper makes no wire deeper.

theorem Cslib.Circuits.Circuit.depth_mapLines_le {σ : Signature} {τ : Signature} {n m : ℕ} {f : {g : ℕ} → Line σ n g → Line τ n g} (hf : ∀ {g : ℕ} (line : Line σ n g) (depths : Wire n g → ℕ), (f line).depth depths ≤ line.depth depths) (c : Circuit σ n m) : (mapLines (fun {g : ℕ} => f) c).depth ≤ c.depth

Transforming lines that get no deeper keeps the depth bounded.

theorem Cslib.Circuits.Program.depths_mapLines {σ : Signature} {τ : Signature} {n g : ℕ} {f : {g : ℕ} → Line σ n g → Line τ n g} (hf : ∀ {g : ℕ} (line : Line σ n g) (depths : Wire n g → ℕ), (f line).depth depths = line.depth depths) (p : Program σ n g) : (mapLines (fun {g : ℕ} => f) p).depths = p.depths

Transforming lines that keep their depth keeps the depth of every gate.

theorem Cslib.Circuits.Program.wireDepths_mapLines {σ : Signature} {τ : Signature} {n g : ℕ} {f : {g : ℕ} → Line σ n g → Line τ n g} (hf : ∀ {g : ℕ} (line : Line σ n g) (depths : Wire n g → ℕ), (f line).depth depths = line.depth depths) (p : Program σ n g) : (mapLines (fun {g : ℕ} => f) p).wireDepths = p.wireDepths

Transforming lines that keep their depth keeps the depth of every wire.

theorem Cslib.Circuits.Circuit.outputDepths_mapLines {σ : Signature} {τ : Signature} {n m : ℕ} {f : {g : ℕ} → Line σ n g → Line τ n g} (hf : ∀ {g : ℕ} (line : Line σ n g) (depths : Wire n g → ℕ), (f line).depth depths = line.depth depths) (c : Circuit σ n m) : (mapLines (fun {g : ℕ} => f) c).outputDepths = c.outputDepths

Transforming lines that keep their depth keeps the depth of every output.

theorem Cslib.Circuits.Circuit.depth_mapLines {σ : Signature} {τ : Signature} {n m : ℕ} {f : {g : ℕ} → Line σ n g → Line τ n g} (hf : ∀ {g : ℕ} (line : Line σ n g) (depths : Wire n g → ℕ), (f line).depth depths = line.depth depths) (c : Circuit σ n m) : (mapLines (fun {g : ℕ} => f) c).depth = c.depth

Transforming lines that keep their depth keeps the depth.