Difficulty: optional — 2 definitions, 0 abbreviations, 0 lemmas, 6 theorems.
Feedback is what happens when a wire coming out of something is wired straight back into an input of that very same thing. Nothing about a specification (see Component.Spec in the Computer Networks course) rules this out: some of its input wires and some of its output wires can simply be declared to be the same wires, folded back on themselves, leaving only the wires that are genuinely left over as the visible input and output.
This file builds that folding-back as an operation on specifications, Component.Spec.trace, and proves the handful of laws that make it well-behaved: whatever feeds the fold from outside, or reads out of it, can be applied before or after the fold indifferently; folding back a bundle of wires all at once is the same as folding them back one at a time; a straight crossing folded back on itself unfolds to a plain wire; and a piece sitting inline in the loop can be slid to the other side of the fold. Together these are exactly what makes feedback trustworthy to reason about: a circuit with a loop in it can be redrawn, piece by piece, without ever having to recheck the whole loop from scratch.
Fold k of a specification’s wires back onto themselves: the wires it would send those k values are instead required to feed straight back in as the very values it read them from. What is left over is a specification purely in terms of the remaining input and output wires — an existential over the folded-back value, since nothing says there has to be only one, or any at all, satisfying the fold.
feedback
def Component.Spec.trace {Wire : Type} {n m k : Nat}
(f : Component.Spec Wire Wire (n + k) (m + k)) : Component.Spec Wire Wire n m :=
fun i o => ∃ w : Fin k → Wire, f (Fin.append i w) (Fin.append o w)
Whatever feeds the fold from outside can equally well be applied before folding: routing g into the visible input wires and then folding back agrees with folding back first and routing g in alongside the fold’s own wires, left untouched.
theorem Component.Spec.trace_naturality_left {Wire : Type} {n n' m k : Nat}
(g : Component.Spec Wire Wire n' n) (f : Component.Spec Wire Wire (n + k) (m + k)) :
Component.Spec.sequential g (Component.Spec.trace f) =
Component.Spec.trace
(Component.Spec.sequential (Component.Spec.parallel g (Component.Spec.id Wire k)) f) := by
Lean core dependencies: And, Eq, Eq.mp, Eq.mpr, Eq.symm, Eq.trans, Fin, Fin.castAdd, Fin.natAdd, Nat, True, congr, congrArg, congrFun, congrFun', eq_self, funext, id, of_eq_true
Whatever the fold’s output feeds into from outside can equally well be applied after folding: folding back first and then routing h out of the visible output wires agrees with routing h in alongside the fold’s own wires, left untouched, and folding back afterwards.
theorem Component.Spec.trace_naturality_right {Wire : Type} {n m m' k : Nat}
(f : Component.Spec Wire Wire (n + k) (m + k)) (h : Component.Spec Wire Wire m m') :
Component.Spec.sequential (Component.Spec.trace f) h =
Component.Spec.trace
(Component.Spec.sequential f (Component.Spec.parallel h (Component.Spec.id Wire k))) := by
Lean core dependencies: And, Eq, Eq.mp, Eq.mpr, Eq.trans, Fin, Fin.castAdd, Fin.natAdd, Nat, True, congr, congrArg, congrFun, congrFun', eq_self, funext, id, of_eq_true
Folding back nothing at all leaves a specification exactly as it was — there are no wires to fold, so the fold contributes nothing beyond matching up the (absent) rest.
theorem Component.Spec.trace_vanishing {Wire : Type} {n m : Nat}
(f : Component.Spec Wire Wire n m) :
Component.Spec.trace (k := 0) f = f := by
Lean core dependencies: Eq, Eq.mp, Eq.mpr, Eq.symm, Eq.trans, Fin, Fin.cast, Fin.cast_refl, Fin.elim0, Function.comp, Nat, Nat.add_zero, congr, congrArg, funext, id
Folding back k1 + k2 wires all in one go is the same as folding back k2 of them first and the remaining k1 afterwards: a large loop can always be drawn as smaller loops nested inside one another, in either order, without changing what the whole thing allows.
theorem Component.Spec.trace_superposing {Wire : Type} {n m k1 k2 : Nat}
(f : Component.Spec Wire Wire (n + k1 + k2) (m + k1 + k2)) :
Component.Spec.trace (k := k1) (Component.Spec.trace (k := k2) f) =
Component.Spec.trace (k := k1 + k2)
(fun i o => f (i ∘ Fin.cast (Nat.add_assoc n k1 k2))
(o ∘ Fin.cast (Nat.add_assoc m k1 k2))) := by
Lean core dependencies: Eq, Eq.mpr, Eq.symm, Fin, Fin.cast, Fin.castAdd, Fin.natAdd, Function.comp, Nat, Nat.add_assoc, congrArg, funext, id
Fold every one of a specification’s wires back on itself, leaving nothing visible at all: the special case of Component.Spec.trace where there is no input or output left over once the fold is done.
def Component.Spec.loop {Wire : Type} {k : Nat} (f : Component.Spec Wire Wire k k) :
Component.Spec Wire Wire 0 0 :=
fun _ _ => ∃ w : Fin k → Wire, f w w
A straight crossing, folded back on its own two wires, unfolds to a plain wire: swapping two loop wires with each other and then feeding both back changes nothing at all, since whichever wire you look at, it still carries exactly what it started with — some value has to be on the wires for this to be witnessed at all, which is the only place Wire being inhabited is needed.
theorem Component.Spec.trace_yanking {Wire : Type} [Nonempty Wire] (k : Nat) :
Component.Spec.loop (Component.Spec.symmetry Wire k k) = Component.Spec.id Wire 0 := by
Lean core dependencies: Eq, Eq.trans, Fin, Fin.castAdd, Fin.elim0, Fin.natAdd, Nat, Nonempty, True, congr, congrArg, eq_self, funext, id, of_eq_true
A piece sitting inline in the loop, right after the rest, can just as well be moved to sit right before it instead: sliding a component all the way around a feedback loop once changes nothing about what the loop as a whole allows.
theorem Component.Spec.trace_sliding {Wire : Type} {n m k : Nat}
(f : Component.Spec Wire Wire (n + k) (m + k)) (g : Component.Spec Wire Wire k k) :
Component.Spec.trace
(Component.Spec.sequential f (Component.Spec.parallel (Component.Spec.id Wire m) g)) =
Component.Spec.trace
(Component.Spec.sequential (Component.Spec.parallel (Component.Spec.id Wire n) g) f) := by
Lean core dependencies: And, Eq, Eq.mp, Eq.mpr, Eq.symm, Eq.trans, Fin, Fin.castAdd, Fin.natAdd, Nat, True, congr, congrArg, congrFun, congrFun', eq_self, funext, id, of_eq_true
Dependency diagram
Drag to pan, Ctrl+scroll (or Cmd+scroll) to zoom, click a node to jump to it.
definitiontheoremdeclared elsewheredependencyproof dependency
legend