Wires

References

• [Ghica, Kaye, and Sprunger, A Complete Theory of Sequential Digital Circuits][Ghica2025]

def Circuit.Wires (V : Type u) (I : ℕ) : Type u

A bundle of I wires, each carrying a value of type V.

Equations

• Circuit.Wires V I = Vector V I

@[instance_reducible]

instance Circuit.instPreorderWires {V : Type u_1} {I : ℕ} [Preorder V] : Preorder (Wires V I)

Equations

• Circuit.instPreorderWires = { le := fun (a b : Circuit.Wires V I) => ∀ (i : Fin I), Vector.get a i ≤ Vector.get b i, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯ }

theorem Circuit.Wires.ext {V : Type u_1} {n : ℕ} {a b : Wires V n} : (∀ (i : Fin n), Vector.get a i = Vector.get b i) → a = b

@[simp]

theorem Circuit.Wires.get_ofFn {n : ℕ} {α : Type u} (f : Fin n → α) (i : Fin n) : (Vector.ofFn f).get i = f i

@[simp]

theorem Circuit.Wires.get_cast {V : Type u_1} {n m : ℕ} (h : n = m) (v : Wires V n) (i : Fin m) : (Vector.cast h v).get i = Vector.get v ⟨↑i, ⋯⟩

theorem Circuit.Wires.get_append_left {V : Type u_1} {n m : ℕ} (a : Wires V n) (b : Wires V m) (i : Fin n) : (Vector.append a b).get (Fin.castAdd m i) = Vector.get a i

theorem Circuit.Wires.get_append_right {V : Type u_1} {n m : ℕ} (a : Wires V n) (b : Wires V m) (i : Fin m) : (Vector.append a b).get (Fin.natAdd n i) = Vector.get b i

theorem Circuit.Wires.get_append {V : Type u_1} {n m : ℕ} (a : Wires V n) (b : Wires V m) (i : Fin (n + m)) : (Vector.append a b).get i = if h : ↑i < n then Vector.get a ⟨↑i, h⟩ else Vector.get b ⟨↑i - n, ⋯⟩

theorem Circuit.Wires.get_take {V : Type u_1} {n k : ℕ} (a : Wires V n) (i : Fin (min k n)) : (Vector.take a k).get i = Vector.get a ⟨↑i, ⋯⟩

theorem Circuit.Wires.get_drop {V : Type u_1} {n k : ℕ} (a : Wires V n) (i : Fin (n - k)) : (Vector.drop a k).get i = Vector.get a ⟨k + ↑i, ⋯⟩

The lemmas above are stated for Wires. Vector.cast, Vector.take, Vector.drop and Vector.append all report their results at type Vector, and simp matches argument types up to reducible unfolding only, so the same facts are restated below for Vector-typed arguments.

theorem Circuit.Wires.get_cast_vector {V : Type u_1} {n m : ℕ} (h : n = m) (v : Vector V n) (i : Fin m) : (Vector.cast h v).get i = v.get ⟨↑i, ⋯⟩

theorem Circuit.Wires.get_append_vector {V : Type u_1} {n m : ℕ} (a : Vector V n) (b : Vector V m) (i : Fin (n + m)) : (a.append b).get i = if h : ↑i < n then a.get ⟨↑i, h⟩ else b.get ⟨↑i - n, ⋯⟩

theorem Circuit.Wires.get_append_wires_vector {V : Type u_1} {n m : ℕ} (a : Wires V n) (b : Vector V m) (i : Fin (n + m)) : (Vector.append a b).get i = if h : ↑i < n then Vector.get a ⟨↑i, h⟩ else b.get ⟨↑i - n, ⋯⟩

theorem Circuit.Wires.get_append_vector_wires {V : Type u_1} {n m : ℕ} (a : Vector V n) (b : Wires V m) (i : Fin (n + m)) : (a.append b).get i = if h : ↑i < n then a.get ⟨↑i, h⟩ else Vector.get b ⟨↑i - n, ⋯⟩

theorem Circuit.Wires.get_take_vector {V : Type u_1} {n k : ℕ} (a : Vector V n) (i : Fin (min k n)) : (a.take k).get i = a.get ⟨↑i, ⋯⟩

theorem Circuit.Wires.get_drop_vector {V : Type u_1} {n k : ℕ} (a : Vector V n) (i : Fin (n - k)) : (a.drop k).get i = a.get ⟨k + ↑i, ⋯⟩