Circuit wires and renamings

A Wire inputCount gateCount refers to an original input or an internal gate. A valuation of wires is assembled with Wire.elim from values for the inputs and values for the gates.

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.

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

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

• input {inputCount gateCount : ℕ} (input : Fin inputCount) : Wire inputCount gateCount

  An original input.

• gate {inputCount gateCount : ℕ} (gate : Fin gateCount) : Wire inputCount gateCount

  The output of an internal gate.

@[instance_reducible]

instance Cslib.Circuits.instDecidableEqWire {inputCount✝ gateCount✝ : ℕ} : DecidableEq (Wire inputCount✝ gateCount✝)

Equations

• Cslib.Circuits.instDecidableEqWire = Cslib.Circuits.instDecidableEqWire.decEq

def Cslib.Circuits.instDecidableEqWire.decEq {inputCount✝ gateCount✝ : ℕ} (x✝ x✝¹ : Wire inputCount✝ gateCount✝) : Decidable (x✝ = x✝¹)

Equations

• Cslib.Circuits.instDecidableEqWire.decEq (Cslib.Circuits.Wire.input a) (Cslib.Circuits.Wire.input b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Cslib.Circuits.instDecidableEqWire.decEq (Cslib.Circuits.Wire.input input) (Cslib.Circuits.Wire.gate gate) = isFalse ⋯
• Cslib.Circuits.instDecidableEqWire.decEq (Cslib.Circuits.Wire.gate gate) (Cslib.Circuits.Wire.input input) = isFalse ⋯
• Cslib.Circuits.instDecidableEqWire.decEq (Cslib.Circuits.Wire.gate a) (Cslib.Circuits.Wire.gate b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

def Cslib.Circuits.Wire.elim {inputCount gateCount : ℕ} {α : Sort u_1} (inputs : Fin inputCount → α) (gates : Fin gateCount → α) : Wire inputCount gateCount → α

Define a function on wires from its values on inputs and on gates.

Equations

• Cslib.Circuits.Wire.elim inputs gates (Cslib.Circuits.Wire.input i) = inputs i
• Cslib.Circuits.Wire.elim inputs gates (Cslib.Circuits.Wire.gate j) = gates j

@[simp]

theorem Cslib.Circuits.Wire.elim_input {inputCount gateCount : ℕ} {α : Sort u_1} (inputs : Fin inputCount → α) (gates : Fin gateCount → α) (i : Fin inputCount) : elim inputs gates (input i) = inputs i

@[simp]

theorem Cslib.Circuits.Wire.elim_gate {inputCount gateCount : ℕ} {α : Sort u_1} (inputs : Fin inputCount → α) (gates : Fin gateCount → α) (j : Fin gateCount) : elim inputs gates (gate j) = gates j

def Cslib.Circuits.Wire.equiv (inputCount gateCount : ℕ) : Wire inputCount gateCount ≃ Fin inputCount ⊕ Fin gateCount

A wire is an input or a gate.

Equations

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

@[instance_reducible]

instance Cslib.Circuits.Wire.instFintype {inputCount gateCount : ℕ} : Fintype (Wire inputCount gateCount)

Equations

• Cslib.Circuits.Wire.instFintype = Fintype.ofEquiv (Fin inputCount ⊕ Fin gateCount) (Cslib.Circuits.Wire.equiv inputCount gateCount).symm

@[simp]

theorem Cslib.Circuits.Wire.card {inputCount gateCount : ℕ} : Fintype.card (Wire inputCount gateCount) = inputCount + gateCount

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

Regard a wire as a wire in a namespace with one additional gate.

Equations

• (Cslib.Circuits.Wire.input i).castSucc = Cslib.Circuits.Wire.input i
• (Cslib.Circuits.Wire.gate j).castSucc = Cslib.Circuits.Wire.gate j.castSucc

@[simp]

theorem Cslib.Circuits.Wire.castSucc_input {inputCount gateCount : ℕ} (i : Fin inputCount) : (input i).castSucc = input i

@[simp]

theorem Cslib.Circuits.Wire.castSucc_gate {inputCount gateCount : ℕ} (j : Fin gateCount) : (gate j).castSucc = gate j.castSucc

def Cslib.Circuits.Wire.castAdd {inputCount gateCount : ℕ} (extra : ℕ) : Wire inputCount gateCount → Wire inputCount (gateCount + extra)

Regard a wire as a wire of the same program continued by extra further gates.

Equations

• Cslib.Circuits.Wire.castAdd extra (Cslib.Circuits.Wire.input i) = Cslib.Circuits.Wire.input i
• Cslib.Circuits.Wire.castAdd extra (Cslib.Circuits.Wire.gate j) = Cslib.Circuits.Wire.gate (Fin.castAdd extra j)

@[simp]

theorem Cslib.Circuits.Wire.castAdd_input {inputCount gateCount : ℕ} (extra : ℕ) (i : Fin inputCount) : castAdd extra (input i) = input i

@[simp]

theorem Cslib.Circuits.Wire.castAdd_gate {inputCount gateCount : ℕ} (extra : ℕ) (j : Fin gateCount) : castAdd extra (gate j) = gate (Fin.castAdd extra j)

def Cslib.Circuits.Wire.lastCases {inputCount gateCount : ℕ} {motive : Wire inputCount (gateCount + 1) → Sort u_2} (last : motive (gate (Fin.last gateCount))) (castSucc : (wire : Wire inputCount gateCount) → motive wire.castSucc) (wire : Wire inputCount (gateCount + 1)) : motive wire

A wire in a namespace with one additional gate is either the new last gate or an earlier wire.

Equations

• Cslib.Circuits.Wire.lastCases last castSucc (Cslib.Circuits.Wire.input i) = castSucc (Cslib.Circuits.Wire.input i)
• Cslib.Circuits.Wire.lastCases last castSucc (Cslib.Circuits.Wire.gate j) = Fin.lastCases last (fun (j : Fin gateCount) => castSucc (Cslib.Circuits.Wire.gate j)) j

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 = Cslib.Circuits.Wire.elim Cslib.Circuits.Wire.input ρ.gates

@[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 = wire.castSucc

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 }

@[simp]

theorem Cslib.Circuits.Wire.Renaming.skipLast_gates_last {inputCount sourceGateCount targetGateCount : ℕ} (prior : Renaming inputCount sourceGateCount targetGateCount) (replacement : Wire inputCount targetGateCount) : (prior.skipLast replacement).gates (Fin.last 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 wire.castSucc = 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.

@[simp]

theorem Cslib.Circuits.Wire.Renaming.appendLast_gates_last {inputCount sourceGateCount targetGateCount : ℕ} (prior : Renaming inputCount sourceGateCount targetGateCount) : prior.appendLast.gates (Fin.last 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 wire.castSucc = (prior.apply wire).castSucc

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), elim inputs newGates (ρ.gates gate) = oldGates gate) (wire : Wire inputCount sourceGateCount) : elim inputs newGates (ρ.apply wire) = elim inputs oldGates 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.