Interface

Difficulty: optional — 8 definitions, 2 abbreviations, 1 lemmas, 5 theorems, 0 examples.

definition abbreviation lemma theorem

legend

NoteInterfaceOld

interfaces

InterfaceOld : Type 1

Show details

| InterfaceOld.mk : (Ports : Type) →
  (Port : Ports → Type) →
    (∀ (i : Ports), Nonempty (Port i)) →
      ((i : Ports) → Norm (Port i)) →
        (Coherent : Finset Ports → Prop) →
          Coherent ∅ →
            (∀ (i : Ports), Coherent {i}) →
              (∀ {a b : Finset Ports}, Coherent a → b ⊆ a → Coherent b) → InterfaceOld

Outer dependencies: (none)

Mathlib dependencies: Finset, Norm

Lean core dependencies: Eq, HEq, Nat, Nonempty

Used by: ApplicationLayer.interface, DataLinkLayer.interface, DataLinkLayer.links, InterfaceOld.Value, InterfaceOld.Value.assocLR, InterfaceOld.Value.eq_of_heq, InterfaceOld.Value.join, InterfaceOld.Value.join_left_right, InterfaceOld.Value.left, InterfaceOld.Value.left_join, InterfaceOld.Value.right, InterfaceOld.Value.right_join, InterfaceOld.homogeneous, InterfaceOld.single, InterfaceOld.tensor, InterfaceOld.unit, Layer, Layer.Realizable, Layer.Univalent, Layer.eq_toFun_of_univalent, Layer.id, Layer.id_rel, Layer.id_sequential, Layer.loop, Layer.parallel, Layer.parallel_rel, Layer.rel, Layer.sequential, Layer.sequential_assoc, Layer.sequential_id, Layer.sequential_rel, Layer.symmetry, Layer.toFun, Layer.toFun_spec, Layer.trace, Layer.trace_naturality_left, Layer.trace_naturality_right, Layer.trace_sliding, Layer.trace_superposing, Layer.trace_vanishing, Layer.trace_yanking, NetworkArchitecture.application, NetworkArchitecture.dataLink, NetworkArchitecture.network, NetworkArchitecture.physical, NetworkArchitecture.transport, NetworkLayer.interface, PhysicalLayer.interface, Specification, Specification.binaryCone, Specification.cartesianMonoidalCategory, Specification.category, Specification.closed, Specification.galoisConnection, Specification.monoidalClosed, Specification.terminalCone, TransportLayer.interface, instNonemptyValue, instNormValue

NoteInterfaceOld.Value

InterfaceOld.Value (I : InterfaceOld) : Type

Show details

| InterfaceOld.Value.mk : {I : InterfaceOld} →
  (fired : Finset I.Ports) → I.Coherent fired → ((i : ↥fired) → I.Port ↑i) → I.Value

Outer dependencies: InterfaceOld

Mathlib dependencies: Finset

Lean core dependencies: Eq, HEq, Nat, Subtype, eq_of_heq

Used by: DataLinkLayer.network, DataLinkLayer.physical, InterfaceOld.Value.assocLR, InterfaceOld.Value.eq_of_heq, InterfaceOld.Value.join, InterfaceOld.Value.join_left_right, InterfaceOld.Value.left, InterfaceOld.Value.left_join, InterfaceOld.Value.observe, InterfaceOld.Value.observeAll, InterfaceOld.Value.right, InterfaceOld.Value.right_join, InterfaceOld.unit.Value.subsingleton, Layer.Realizable, Layer.Univalent, Layer.eq_toFun_of_univalent, Layer.id, Layer.id_rel, Layer.id_sequential, Layer.loop, Layer.parallel, Layer.parallel_rel, Layer.rel, Layer.sequential, Layer.sequential_assoc, Layer.sequential_id, Layer.sequential_rel, Layer.symmetry, Layer.toFun, Layer.toFun_spec, Layer.trace, Layer.trace_naturality_left, Layer.trace_naturality_right, Layer.trace_sliding, Layer.trace_superposing, Layer.trace_vanishing, Layer.trace_yanking, NetworkLayer.forwards, NetworkLayer.resolves, NetworkLayer.transport, Specification, Specification.binaryCone, Specification.category, Specification.closed, Specification.galoisConnection, Specification.terminalCone, TransportLayer.application, instNonemptyValue, instNormValue

ImportantinstNonemptyValue

instNonemptyValue (I : InterfaceOld) : Nonempty I.Value

Show details

fun I =>
  Nonempty.intro
    { fired := ∅, coherent := I.coherent_empty,
      value := fun i => (Finset.notMem_empty (↑i) i.property).elim }

Complexity: 271 (size of the value term)

Outer dependencies: InterfaceOld, InterfaceOld.Value

Mathlib dependencies: Finset, Finset.notMem_empty

Lean core dependencies: False.elim, Nonempty, Subtype

Used by: Layer.trace_vanishing, Layer.trace_yanking

ImportantinstNormValue

instNormValue (I : InterfaceOld) : Norm I.Value

Show details

fun I => { norm := fun v => ∑ i ∈ v.fired.attach, ‖v.value i‖ }

Complexity: 243 (size of the value term)

Outer dependencies: InterfaceOld, InterfaceOld.Value

Mathlib dependencies: Finset, Finset.attach, Finset.sum, Norm, Real

Lean core dependencies: Subtype

Used by: (none)

NoteInterfaceOld.unit

InterfaceOld.unit : InterfaceOld

Show details

{ Ports := Empty, Port := Empty.elim, nonempty := InterfaceOld.unit._proof_1,
  size := fun i => i.elim, Coherent := fun x => True, coherent_empty := trivial,
  coherent_singleton := ⋯, coherent_downward := ⋯ }

Complexity: 77 (size of the value term)

Outer dependencies: InterfaceOld

Mathlib dependencies: Finset, Norm

Lean core dependencies: Empty, Empty.elim, Nonempty, True, trivial

Used by: InterfaceOld.unit.Value.subsingleton, Layer.loop, Layer.trace_vanishing, Layer.trace_yanking

NoteInterfaceOld.tensor

InterfaceOld.tensor (I J : InterfaceOld) : InterfaceOld

Show details

fun I J =>
  { Ports := I.Ports ⊕ J.Ports, Port := Sum.elim I.Port J.Port, nonempty := ⋯,
    size := fun x =>
      match x with
      | Sum.inl i => I.size i
      | Sum.inr j => J.size j,
    Coherent := fun a => I.Coherent (a.preimage Sum.inl ⋯) ∧ J.Coherent (a.preimage Sum.inr ⋯),
    coherent_empty := ⋯, coherent_singleton := ⋯, coherent_downward := ⋯ }

Complexity: 225 (size of the value term)

Outer dependencies: InterfaceOld

Mathlib dependencies: Finset, Finset.ext, Finset.mem_preimage, Finset.preimage, Finset.preimage_empty, Finset.preimage_inl, Finset.preimage_inr, Finset.toLeft, Finset.toRight, Function.Injective.injOn, Norm, Set.InjOn, Set.preimage, Sum.inl_injective, Sum.inr_injective

Lean core dependencies: And, Eq, Eq.mp, Eq.mpr, Eq.trans, False, False.elim, Iff, Nonempty, Sum, Sum.elim, True, congr, congrArg, congrFun', eq_false', id, iff_self, noConfusion_of_Nat, of_eq_true

Used by: DataLinkLayer.network, DataLinkLayer.physical, InterfaceOld.Value.assocLR, InterfaceOld.Value.join, InterfaceOld.Value.join_left_right, InterfaceOld.Value.left, InterfaceOld.Value.right, Layer, Layer.eq_toFun_of_univalent, Layer.id, Layer.id_sequential, Layer.loop, Layer.parallel, Layer.parallel_rel, Layer.sequential, Layer.sequential_assoc, Layer.sequential_id, Layer.sequential_rel, Layer.symmetry, Layer.trace, Layer.trace_naturality_left, Layer.trace_naturality_right, Layer.trace_sliding, Layer.trace_superposing, Layer.trace_vanishing, Layer.trace_yanking, NetworkLayer.forwards, NetworkLayer.resolves, NetworkLayer.transport, TransportLayer.application

NoteInterfaceOld.homogeneous

InterfaceOld.homogeneous (Wire : Type) [Nonempty Wire] [Norm Wire] (n : ℕ) : InterfaceOld

Show details

fun Wire [Nonempty Wire] [inst_1 : Norm Wire] n =>
  { Ports := Fin n, Port := fun x => Wire, nonempty := ⋯, size := fun x => inst_1,
    Coherent := fun x => True, coherent_empty := trivial, coherent_singleton := ⋯,
    coherent_downward := ⋯ }

Complexity: 101 (size of the value term)

Outer dependencies: InterfaceOld

Mathlib dependencies: Finset, Norm

Lean core dependencies: Fin, Nat, Nonempty, True, trivial

Used by: DataLinkLayer.links, InterfaceOld.single, PhysicalLayer.interface

NoteInterfaceOld.single

InterfaceOld.single (Wire : Type) [Nonempty Wire] [Norm Wire] : InterfaceOld

Show details

fun Wire [Nonempty Wire] [Norm Wire] => InterfaceOld.homogeneous Wire 1

Complexity: 27 (size of the value term)

Outer dependencies: InterfaceOld

Inner dependencies: InterfaceOld.homogeneous

Mathlib dependencies: Norm

Lean core dependencies: Nat, Nonempty

Used by: DataLinkLayer.interface, InterfaceOld.Value.observe, NetworkLayer.interface, TransportLayer.interface

NoteInterfaceOld.Value.observe

InterfaceOld.Value.observe {Wire : Type} [Nonempty Wire] [Norm Wire]
  (v : (InterfaceOld.single Wire).Value) : Option Wire

Show details

fun {Wire} [Nonempty Wire] [Norm Wire] v => if h : 0 ∈ v.fired then some (v.value ⟨0, h⟩) else none

Complexity: 563 (size of the value term)

Outer dependencies: InterfaceOld.Value, InterfaceOld.single

Mathlib dependencies: Finset, Norm

Lean core dependencies: Fin, Nat, Nonempty, Not, Option, dite

Used by: DataLinkLayer.network, DataLinkLayer.physical, NetworkLayer.forwards, NetworkLayer.resolves, NetworkLayer.transport, TransportLayer.application

NoteInterfaceOld.Value.left

InterfaceOld.Value.left {I J : InterfaceOld} (v : (I.tensor J).Value) : I.Value

Show details

fun {I J} v =>
  { fired := v.fired.preimage Sum.inl ⋯, coherent := ⋯, value := fun p => v.value ⟨Sum.inl ↑p, ⋯⟩ }

Complexity: 345 (size of the value term)

Outer dependencies: InterfaceOld, InterfaceOld.Value, InterfaceOld.tensor

Mathlib dependencies: Finset, Finset.mem_preimage, Finset.preimage, Function.Injective.injOn, Set.preimage, Sum.inl_injective

Lean core dependencies: Subtype, Sum

Used by: DataLinkLayer.network, DataLinkLayer.physical, InterfaceOld.Value.assocLR, InterfaceOld.Value.join_left_right, InterfaceOld.Value.left_join, Layer.eq_toFun_of_univalent, Layer.id, Layer.id_rel, Layer.id_sequential, Layer.parallel, Layer.parallel_rel, Layer.sequential, Layer.sequential_assoc, Layer.sequential_id, Layer.sequential_rel, Layer.symmetry, Layer.trace, Layer.trace_naturality_left, Layer.trace_naturality_right, Layer.trace_sliding, Layer.trace_superposing, Layer.trace_vanishing, Layer.trace_yanking, NetworkLayer.forwards, NetworkLayer.resolves, NetworkLayer.transport, TransportLayer.application

NoteInterfaceOld.Value.right

InterfaceOld.Value.right {I J : InterfaceOld} (v : (I.tensor J).Value) : J.Value

Show details

fun {I J} v =>
  { fired := v.fired.preimage Sum.inr ⋯, coherent := ⋯, value := fun p => v.value ⟨Sum.inr ↑p, ⋯⟩ }

Complexity: 345 (size of the value term)

Outer dependencies: InterfaceOld, InterfaceOld.Value, InterfaceOld.tensor

Mathlib dependencies: Finset, Finset.mem_preimage, Finset.preimage, Function.Injective.injOn, Set.preimage, Sum.inr_injective

Lean core dependencies: Subtype, Sum

Used by: DataLinkLayer.network, DataLinkLayer.physical, InterfaceOld.Value.assocLR, InterfaceOld.Value.join_left_right, InterfaceOld.Value.right_join, Layer.eq_toFun_of_univalent, Layer.id, Layer.id_rel, Layer.id_sequential, Layer.parallel, Layer.parallel_rel, Layer.sequential, Layer.sequential_assoc, Layer.sequential_id, Layer.sequential_rel, Layer.symmetry, Layer.trace, Layer.trace_naturality_left, Layer.trace_naturality_right, Layer.trace_sliding, Layer.trace_superposing, Layer.trace_vanishing, Layer.trace_yanking, NetworkLayer.forwards, NetworkLayer.resolves, NetworkLayer.transport, TransportLayer.application

NoteInterfaceOld.Value.join

InterfaceOld.Value.join {I J : InterfaceOld} (a : I.Value) (b : J.Value) : (I.tensor J).Value

Show details

fun {I J} a b =>
  {
    fired :=
      (Finset.map { toFun := Sum.inl, inj' := ⋯ } a.fired).disjUnion
        (Finset.map { toFun := Sum.inr, inj' := ⋯ } b.fired) ⋯,
    coherent := ⋯,
    value := fun p =>
      match hp : ↑p, ⋯ with
      | Sum.inl x, hmem => a.value ⟨x, ⋯⟩
      | Sum.inr y, hmem => b.value ⟨y, ⋯⟩ }

Complexity: 1763 (size of the value term)

Outer dependencies: InterfaceOld, InterfaceOld.Value, InterfaceOld.tensor

Mathlib dependencies: Disjoint, Finset, Finset.disjUnion, Finset.ext, Finset.map, Finset.mem_disjUnion, Finset.mem_map, Finset.preimage, Finset.preimage_inl, Finset.preimage_inr, Finset.toLeft, Finset.toRight, Function.Embedding, Function.Injective.injOn, Set.preimage, Sum.inl_injective, Sum.inr_injective

Lean core dependencies: And, Eq, Eq.mp, Eq.mpr, Eq.trans, Exists, False, False.elim, Iff, Or, Subtype, Sum, True, and_false, congr, congrArg, congrFun', eq_false, eq_false', exists_eq_right, exists_false, false_or, funext, id, iff_self, noConfusion_of_Nat, of_eq_true, or_false

Used by: InterfaceOld.Value.assocLR, InterfaceOld.Value.join_left_right, InterfaceOld.Value.left_join, InterfaceOld.Value.right_join, Layer.Realizable, Layer.Univalent, Layer.eq_toFun_of_univalent, Layer.id_rel, Layer.id_sequential, Layer.parallel, Layer.parallel_rel, Layer.rel, Layer.sequential, Layer.sequential_assoc, Layer.sequential_id, Layer.sequential_rel, Layer.toFun, Layer.toFun_spec, Layer.trace, Layer.trace_naturality_left, Layer.trace_naturality_right, Layer.trace_sliding, Layer.trace_superposing, Layer.trace_vanishing, Layer.trace_yanking

TipInterfaceOld.Value.eq_of_heq

InterfaceOld.Value.eq_of_heq {I : InterfaceOld} {a b : I.Value} (hfired : a.fired = b.fired)
  (hval : a.value ≍ b.value) : a = b

Show details

fun {I} {a b} hfired hval =>
  InterfaceOld.Value.casesOn (motive := fun t => a = t → a = b) a
    (fun aFired aCoh aVal h =>
      Eq.ndrec (motive := fun {a} => a.fired = b.fired → a.value ≍ b.value → a = b)
        (fun hfired hval =>
          InterfaceOld.Value.casesOn (motive := fun t =>
            b = t → { fired := aFired, coherent := aCoh, value := aVal } = b) b
            (fun bFired bCoh bVal h =>
              Eq.ndrec (motive := fun {b} =>
                { fired := aFired, coherent := aCoh, value := aVal }.fired = b.fired →
                  { fired := aFired, coherent := aCoh, value := aVal }.value ≍ b.value →
                    { fired := aFired, coherent := aCoh, value := aVal } = b)
                (fun hfired hval =>
                  Eq.ndrec (motive := fun bFired =>
                    ∀ (bCoh : I.Coherent bFired) (bVal : (i : ↥bFired) → I.Port ↑i),
                      { fired := aFired, coherent := aCoh, value := aVal }.value ≍
                          { fired := bFired, coherent := bCoh, value := bVal }.value →
                        { fired := aFired, coherent := aCoh, value := aVal } =
                          { fired := bFired, coherent := bCoh, value := bVal })
                    (fun bCoh bVal hval =>
                      have this := eq_of_heq hval;
                      Eq.ndrec (motive := fun bVal =>
                        { fired := aFired, coherent := aCoh, value := aVal }.value ≍
                            { fired := aFired, coherent := bCoh, value := bVal }.value →
                          { fired := aFired, coherent := aCoh, value := aVal } =
                            { fired := aFired, coherent := bCoh, value := bVal })
                        (fun hval => Eq.refl { fired := aFired, coherent := aCoh, value := aVal })
                        this hval)
                    hfired bCoh bVal hval)
                (Eq.symm h) hfired hval)
            (Eq.refl b))
        (Eq.symm h) hfired hval)
    (Eq.refl a)

Complexity: 3536 (size of the value term)

Dependencies: InterfaceOld, InterfaceOld.Value

Mathlib dependencies: Finset

Lean core dependencies: Eq, Eq.symm, HEq, Subtype, eq_of_heq

Used by: InterfaceOld.unit.Value.subsingleton

ImportantInterfaceOld.Value.left_join

InterfaceOld.Value.left_join {I J : InterfaceOld} (a : I.Value) (b : J.Value) : (a.join b).left = a

Show details

fun {I J} a b =>
  InterfaceOld.Value.ext_of_fired_eq✝ (InterfaceOld.Value.join_fired_inl✝ a b) fun x ha hb =>
    Eq.refl ((a.join b).left.value ⟨x, ha⟩)

Complexity: 357 (size of the value term)

Dependencies: InterfaceOld, InterfaceOld.Value, InterfaceOld.Value.join, InterfaceOld.Value.left

Mathlib dependencies: Finset

Lean core dependencies: Eq

Used by: Layer.id_rel, Layer.id_sequential, Layer.parallel_rel, Layer.sequential_assoc, Layer.sequential_id, Layer.sequential_rel, Layer.trace_naturality_left, Layer.trace_naturality_right, Layer.trace_sliding, Layer.trace_superposing, Layer.trace_vanishing, Layer.trace_yanking

ImportantInterfaceOld.Value.right_join

InterfaceOld.Value.right_join {I J : InterfaceOld} (a : I.Value) (b : J.Value) :
  (a.join b).right = b

Show details

fun {I J} a b =>
  InterfaceOld.Value.ext_of_fired_eq✝ (InterfaceOld.Value.join_fired_inr✝ a b) fun x ha hb =>
    Eq.refl ((a.join b).right.value ⟨x, ha⟩)

Complexity: 357 (size of the value term)

Dependencies: InterfaceOld, InterfaceOld.Value, InterfaceOld.Value.join, InterfaceOld.Value.right

Mathlib dependencies: Finset

Lean core dependencies: Eq

Used by: Layer.id_rel, Layer.id_sequential, Layer.parallel_rel, Layer.sequential_assoc, Layer.sequential_id, Layer.sequential_rel, Layer.trace_naturality_left, Layer.trace_naturality_right, Layer.trace_sliding, Layer.trace_superposing, Layer.trace_vanishing, Layer.trace_yanking

ImportantInterfaceOld.Value.join_left_right

InterfaceOld.Value.join_left_right {I J : InterfaceOld} (v : (I.tensor J).Value) :
  v.left.join v.right = v

Show details

fun {I J} v =>
  have hfired :=
    id
      (Finset.sum_preimage_map_disjUnion✝ v.fired
        (InterfaceOld.Value.join_disjoint✝ v.left v.right));
  InterfaceOld.Value.ext_of_fired_eq✝ hfired fun x ha hb =>
    Sum.casesOn (motive := fun t => x = t → (v.left.join v.right).value ⟨x, ha⟩ = v.value ⟨x, hb⟩) x
      (fun a h =>
        Eq.ndrec (motive := fun x =>
          ∀ (ha : x ∈ (v.left.join v.right).fired) (hb : x ∈ v.fired),
            (v.left.join v.right).value ⟨x, ha⟩ = v.value ⟨x, hb⟩)
          (fun ha hb => Eq.refl ((v.left.join v.right).value ⟨Sum.inl a, ha⟩)) (Eq.symm h) ha hb)
      (fun b h =>
        Eq.ndrec (motive := fun x =>
          ∀ (ha : x ∈ (v.left.join v.right).fired) (hb : x ∈ v.fired),
            (v.left.join v.right).value ⟨x, ha⟩ = v.value ⟨x, hb⟩)
          (fun ha hb => Eq.refl ((v.left.join v.right).value ⟨Sum.inr b, ha⟩)) (Eq.symm h) ha hb)
      (Eq.refl x)

Complexity: 3250 (size of the value term)

Dependencies: InterfaceOld, InterfaceOld.Value, InterfaceOld.Value.join, InterfaceOld.Value.left, InterfaceOld.Value.right, InterfaceOld.tensor

Mathlib dependencies: Finset

Lean core dependencies: Eq, Eq.symm, Sum, id

Used by: Layer.eq_toFun_of_univalent, Layer.id_sequential, Layer.sequential_id, Layer.trace_naturality_left, Layer.trace_naturality_right, Layer.trace_sliding, Layer.trace_vanishing

Dependency diagram

Drag to pan, Ctrl+scroll (or Cmd+scroll, or pinch on a touch screen) to zoom, click a node to jump to it.

definitionabbreviationlemmatheoremdeclared elsewheredependencyproof dependency

legend