Circuit wires and renamings

A Wire inputCount gateCount refers to an original input or an internal gate. Wire.Renaming fixes the original inputs and maps each gate to an input or gate in the target namespace. This file provides identity and composition, extension by a gate, replacement of the last gate, and renaming by a permutation.

@[reducible, inline]

abbrev Cslib.Circuits.Wire (inputCount gateCount : ℕ) : Type

A wire is either an original input or the output of an earlier gate.

Equations

• Cslib.Circuits.Wire inputCount gateCount = Fin (inputCount + gateCount)

@[reducible, inline]

abbrev Cslib.Circuits.Wire.input {inputCount gateCount : ℕ} (input : Fin inputCount) : Wire inputCount gateCount

Regard an original input as a wire.

Equations

• Cslib.Circuits.Wire.input input = Fin.castAdd gateCount input

@[reducible, inline]

abbrev Cslib.Circuits.Wire.gate {inputCount gateCount : ℕ} (gate : Fin gateCount) : Wire inputCount gateCount

Regard a gate output as a wire.

Equations

• Cslib.Circuits.Wire.gate gate = Fin.natAdd inputCount gate

structure Cslib.Circuits.Wire.Renaming (inputCount sourceGateCount targetGateCount : ℕ) : Type

A renaming of gate wires that fixes every original input. Gate wires may be sent to either inputs or gates in the target namespace.

• gates : Fin sourceGateCount → Wire inputCount targetGateCount

  The target wire representing each source gate.

def Cslib.Circuits.Wire.Renaming.apply {inputCount sourceGateCount targetGateCount : ℕ} (ρ : Renaming inputCount sourceGateCount targetGateCount) : Wire inputCount sourceGateCount → Wire inputCount targetGateCount

Apply an input-fixing wire renaming.

Equations

• ρ.apply i = Fin.addCases Cslib.Circuits.Wire.input ρ.gates i

@[instance_reducible]

instance Cslib.Circuits.Wire.Renaming.instCoeFunForall {inputCount sourceGateCount targetGateCount : ℕ} : CoeFun (Renaming inputCount sourceGateCount targetGateCount) fun (x : Renaming inputCount sourceGateCount targetGateCount) => Wire inputCount sourceGateCount → Wire inputCount targetGateCount

Equations

• Cslib.Circuits.Wire.Renaming.instCoeFunForall = { coe := Cslib.Circuits.Wire.Renaming.apply }

@[simp]

theorem Cslib.Circuits.Wire.Renaming.apply_input {inputCount sourceGateCount targetGateCount : ℕ} (ρ : Renaming inputCount sourceGateCount targetGateCount) (input : Fin inputCount) : ρ.apply (Wire.input input) = Wire.input input

@[simp]

theorem Cslib.Circuits.Wire.Renaming.apply_gate {inputCount sourceGateCount targetGateCount : ℕ} (ρ : Renaming inputCount sourceGateCount targetGateCount) (gate : Fin sourceGateCount) : ρ.apply (Wire.gate gate) = ρ.gates gate

def Cslib.Circuits.Wire.Renaming.id {inputCount gateCount : ℕ} : Renaming inputCount gateCount gateCount

The identity wire renaming.

Equations

• Cslib.Circuits.Wire.Renaming.id = { gates := Cslib.Circuits.Wire.gate }

@[simp]

theorem Cslib.Circuits.Wire.Renaming.id_apply {inputCount gateCount : ℕ} (wire : Wire inputCount gateCount) : id.apply wire = wire

def Cslib.Circuits.Wire.Renaming.comp {inputCount sourceGateCount middleGateCount targetGateCount : ℕ} (outer : Renaming inputCount middleGateCount targetGateCount) (inner : Renaming inputCount sourceGateCount middleGateCount) : Renaming inputCount sourceGateCount targetGateCount

Compose input-fixing wire renamings.

Equations

• outer.comp inner = { gates := outer.apply ∘ inner.gates }

@[simp]

theorem Cslib.Circuits.Wire.Renaming.comp_apply {inputCount sourceGateCount middleGateCount targetGateCount : ℕ} (outer : Renaming inputCount middleGateCount targetGateCount) (inner : Renaming inputCount sourceGateCount middleGateCount) (wire : Wire inputCount sourceGateCount) : (outer.comp inner).apply wire = outer.apply (inner.apply wire)

def Cslib.Circuits.Wire.Renaming.castSucc {inputCount gateCount : ℕ} : Renaming inputCount gateCount (gateCount + 1)

Include all wires into a namespace with one additional gate.

Equations

• Cslib.Circuits.Wire.Renaming.castSucc = { gates := fun (gate : Fin gateCount) => Cslib.Circuits.Wire.gate gate.castSucc }

@[simp]

theorem Cslib.Circuits.Wire.Renaming.castSucc_apply {inputCount gateCount : ℕ} (wire : Wire inputCount gateCount) : castSucc.apply wire = Fin.castSucc wire

def Cslib.Circuits.Wire.Renaming.skipLast {inputCount sourceGateCount targetGateCount : ℕ} (prior : Renaming inputCount sourceGateCount targetGateCount) (replacement : Wire inputCount targetGateCount) : Renaming inputCount (sourceGateCount + 1) targetGateCount

Extend a renaming while replacing the new last gate by an existing wire.

Equations

• prior.skipLast replacement = { gates := fun (i : Fin (sourceGateCount + 1)) => Fin.lastCases replacement prior.gates i }

theorem Cslib.Circuits.Wire.Renaming.skipLast_gate_last {inputCount sourceGateCount targetGateCount : ℕ} (prior : Renaming inputCount sourceGateCount targetGateCount) (replacement : Wire inputCount targetGateCount) : (prior.skipLast replacement).apply (gate (Fin.last sourceGateCount)) = replacement

@[simp]

theorem Cslib.Circuits.Wire.Renaming.skipLast_lastWire {inputCount sourceGateCount targetGateCount : ℕ} (prior : Renaming inputCount sourceGateCount targetGateCount) (replacement : Wire inputCount targetGateCount) : (prior.skipLast replacement).apply (Fin.last (inputCount + sourceGateCount)) = replacement

@[simp]

theorem Cslib.Circuits.Wire.Renaming.skipLast_castSucc {inputCount sourceGateCount targetGateCount : ℕ} (prior : Renaming inputCount sourceGateCount targetGateCount) (replacement : Wire inputCount targetGateCount) (wire : Wire inputCount sourceGateCount) : (prior.skipLast replacement).apply (Fin.castSucc wire) = prior.apply wire

def Cslib.Circuits.Wire.Renaming.appendLast {inputCount sourceGateCount targetGateCount : ℕ} (prior : Renaming inputCount sourceGateCount targetGateCount) : Renaming inputCount (sourceGateCount + 1) (targetGateCount + 1)

Extend a renaming and retain the new last gate as a fresh target gate.

Equations

• One or more equations did not get rendered due to their size.

theorem Cslib.Circuits.Wire.Renaming.appendLast_gate_last {inputCount sourceGateCount targetGateCount : ℕ} (prior : Renaming inputCount sourceGateCount targetGateCount) : prior.appendLast.apply (gate (Fin.last sourceGateCount)) = gate (Fin.last targetGateCount)

@[simp]

theorem Cslib.Circuits.Wire.Renaming.appendLast_lastWire {inputCount sourceGateCount targetGateCount : ℕ} (prior : Renaming inputCount sourceGateCount targetGateCount) : prior.appendLast.apply (Fin.last (inputCount + sourceGateCount)) = gate (Fin.last targetGateCount)

@[simp]

theorem Cslib.Circuits.Wire.Renaming.appendLast_castSucc {inputCount sourceGateCount targetGateCount : ℕ} (prior : Renaming inputCount sourceGateCount targetGateCount) (wire : Wire inputCount sourceGateCount) : prior.appendLast.apply (Fin.castSucc wire) = Fin.castSucc (prior.apply wire)

def Cslib.Circuits.Wire.Renaming.ofPermutation {inputCount gateCount : ℕ} (permutation : Equiv.Perm (Fin gateCount)) : Renaming inputCount gateCount gateCount

Rename gate wires by a permutation.

Equations

• Cslib.Circuits.Wire.Renaming.ofPermutation permutation = { gates := fun (gate : Fin gateCount) => Cslib.Circuits.Wire.gate (permutation gate) }

theorem Cslib.Circuits.Wire.Renaming.ofPermutation_gate {inputCount gateCount : ℕ} (permutation : Equiv.Perm (Fin gateCount)) (gate : Fin gateCount) : (ofPermutation permutation).apply (Wire.gate gate) = Wire.gate (permutation gate)

theorem Cslib.Circuits.Wire.Renaming.value_apply {inputCount sourceGateCount targetGateCount : ℕ} {U : Type u_1} (ρ : Renaming inputCount sourceGateCount targetGateCount) (inputs : Fin inputCount → U) (oldGates : Fin sourceGateCount → U) (newGates : Fin targetGateCount → U) (preservesGates : ∀ (gate : Fin sourceGateCount), (fun (i : Fin (inputCount + targetGateCount)) => Fin.addCases inputs newGates i) (ρ.gates gate) = oldGates gate) (wire : Wire inputCount sourceGateCount) : (fun (i : Fin (inputCount + targetGateCount)) => Fin.addCases inputs newGates i) (ρ.apply wire) = (fun (i : Fin (inputCount + sourceGateCount)) => Fin.addCases inputs oldGates i) wire

A source and target gate valuation agree along a renaming when they agree on the image of every source gate. Original inputs agree automatically.