Documentation

CslibFrontier.Computability.Circuit.WireNumber

Wire numbers #

Wires are numbered inputs first, as in Cslib.Circuits.Circuit.trace: input i is wire i and gate j is wire n + j, where n is the number of inputs.

Main definitions #

Main results #

source
def Cslib.Circuits.Wire.equivFin (inputCount gateCount : ℕ) :
Wire inputCount gateCount ≃ Fin (inputCount + gateCount)

Wires numbered inputs first: input i is i and gate j is inputCount + j, the order of Circuit.trace.

Instances For
    source
    @[simp]
    theorem Cslib.Circuits.Wire.equivFin_input {n k : ℕ} (i : Fin n) :
    (equivFin n k) (input i) = Fin.castAdd k i

    Input wire i maps to Fin.castAdd k i under equivFin.

    source
    @[simp]
    theorem Cslib.Circuits.Wire.equivFin_gate {n k : ℕ} (j : Fin k) :
    (equivFin n k) (gate j) = Fin.natAdd n j

    Gate wire j maps to Fin.natAdd n j under equivFin.

    source
    def Cslib.Circuits.Wire.toNat {n k : ℕ} (w : Wire n k) :
    ℕ

    The number of a wire: input i is i and gate j is inputCount + j.

    Instances For
      source
      @[simp]
      theorem Cslib.Circuits.Wire.toNat_input {n k : ℕ} (i : Fin n) :
      (input i).toNat = ↑i

      Input wire i has wire number i.

      source
      @[simp]
      theorem Cslib.Circuits.Wire.toNat_gate {n k : ℕ} (j : Fin k) :
      (gate j).toNat = n + ↑j

      Gate wire j has wire number n + j.

      source
      theorem Cslib.Circuits.Wire.toNat_lt {n k : ℕ} (w : Wire n k) :
      w.toNat < n + k

      Every wire in a circuit with n inputs and k gates has wire number strictly less than n + k.

      source
      def Cslib.Circuits.Wire.ofNat {n k : ℕ} (i : ℕ) (h : i < n + k) :
      Wire n k

      The wire with number i, for i < inputCount + gateCount.

      Instances For
        source
        @[simp]
        theorem Cslib.Circuits.Wire.ofNat_toNat {n k : ℕ} (w : Wire n k) :
        ofNat w.toNat ⋯ = w

        Decoding the wire number of w recovers w.

        source
        @[simp]
        theorem Cslib.Circuits.Wire.toNat_ofNat {n k : ℕ} (i : ℕ) (h : i < n + k) :
        (ofNat i h).toNat = i

        The wire number of ofNat i h is i.

        source
        theorem Cslib.Circuits.Wire.toNat_injective {n k : ℕ} :
        Function.Injective toNat

        Wire numbering toNat is injective.

        source
        @[simp]
        theorem Cslib.Circuits.Wire.toNat_castSucc {n k : ℕ} (w : Wire n k) :
        w.castSucc.toNat = w.toNat

        Widening a wire by castSucc preserves its wire number.