Circuit encodings under maps of signatures

Main results

• Cslib.Circuits.Circuit.code_mapOp: mapping the operations maps the gate list and preserves the output wires.
• Cslib.Circuits.Circuit.mapOp_injective: an injective map of operations induces an injective map of circuits.

theorem Cslib.Circuits.Line.code_mapOp {σ : Signature} {τ : Signature} (φ : σ.Hom τ) {n g : ℕ} (line : Line σ n g) : (mapOp φ line).code = (φ line.op, line.code.2)

The code of a translated line: the translated operation on the same wires.

theorem Cslib.Circuits.Program.code_mapOp {σ : Signature} {τ : Signature} (φ : σ.Hom τ) {n g : ℕ} (p : Program σ n g) : (mapOp φ p).code = List.map (fun (g : σ.Op × List ℕ) => (φ g.1, g.2)) p.code

The code of a translated program: the operations of its gates translated.

theorem Cslib.Circuits.Circuit.code_mapOp {σ : Signature} {τ : Signature} (φ : σ.Hom τ) {n m : ℕ} (c : Circuit σ n m) : (mapOp φ c).code = (List.map (fun (g : σ.Op × List ℕ) => (φ g.1, g.2)) c.code.1, c.code.2)

The code of a translated circuit: the operations of its gates translated, the same output wires.

theorem Cslib.Circuits.Circuit.mapOp_injective {σ : Signature} {τ : Signature} (φ : σ.Hom τ) {n m : ℕ} (hφ : Function.Injective ⇑φ) : Function.Injective (mapOp φ)

Translation along an injective map of operations is injective.