Interface

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

definition abbreviation lemma theorem

legend

NoteInterfaceOld

interfaces

structure InterfaceOld : Type 1

• Ports : Type

• Port : self.Ports → Type

• nonempty : ∀ (i : self.Ports), Nonempty (self.Port i)

• size : (i : self.Ports) → Norm (self.Port i)

• Coherent : Finset self.Ports → Prop

• coherent_empty : self.Coherent ∅

• coherent_singleton : ∀ (i : self.Ports), self.Coherent {i}

• coherent_downward : ∀ {a b : Finset self.Ports}, self.Coherent a → b ⊆ a → self.Coherent b

Show details

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.ext_of_fired_eq, InterfaceOld.Value.join, InterfaceOld.Value.join_disjoint, InterfaceOld.Value.join_fired_inl, InterfaceOld.Value.join_fired_inr, 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

structure InterfaceOld.Value (I : InterfaceOld) : Type

• fired : Finset I.Ports

• coherent : I.Coherent self.fired

• value : (i : ↥self.fired) → I.Port ↑i

Show details

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.ext_of_fired_eq, InterfaceOld.Value.join, InterfaceOld.Value.join_disjoint, InterfaceOld.Value.join_fired_inl, InterfaceOld.Value.join_fired_inr, 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

instance 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

instance instNormValue (I : InterfaceOld) : Norm I.Value

Show details

| instNormValue 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

def InterfaceOld.unit : InterfaceOld

Show details

| InterfaceOld.unit =
  { 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, instIsEmptyPortsUnit_computerChips

NoteInterfaceOld.tensor

def InterfaceOld.tensor (I J : InterfaceOld) : InterfaceOld

Show details

| I.tensor 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_fired_inl, InterfaceOld.Value.join_fired_inr, 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

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

Show details

| InterfaceOld.homogeneous Wire n =
  { Ports := Fin n, Port := fun x => Wire, nonempty := ⋯, size := fun x => inst✝,
    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

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

Show details

| InterfaceOld.single 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

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

Show details

| v.observe = 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

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

Show details

| v.left =
  { 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

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

Show details

| v.right =
  { 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

TipInterfaceOld.Value.join_disjoint

theorem InterfaceOld.Value.join_disjoint✝ {I J : InterfaceOld} (a : I.Value) (b : J.Value) :
  Disjoint (Finset.map { toFun := Sum.inl, inj' := ⋯ } a.fired)
    (Finset.map { toFun := Sum.inr, inj' := ⋯ } b.fired)

Show details

fun {I J} a b =>
  Eq.mpr (id (congrArg (fun _a => _a) (propext Finset.disjoint_left))) fun ⦃x⦄ hxa hxb =>
    Exists.casesOn (Eq.mp InterfaceOld.Value.join_disjoint._simp_1_1✝ hxa) fun p h =>
      And.casesOn h fun left hp =>
        Exists.casesOn (Eq.mp InterfaceOld.Value.join_disjoint._simp_1_1✝ hxb) fun q h =>
          And.casesOn h fun left hq =>
            absurd (Eq.mp (congrArg (fun _a => Sum.inr q = _a) (Eq.symm hp)) hq)
              (of_eq_true
                (Eq.trans
                  (congrArg Not (eq_false' fun h => False.elim (noConfusion_of_Nat Sum.ctorIdx h)))
                  not_false_eq_true))

Complexity: 3861 (size of the value term)

Dependencies: InterfaceOld, InterfaceOld.Value

Mathlib dependencies: Disjoint, Finset, Finset.disjoint_left, Finset.map, Finset.mem_map, Function.Embedding, Sum.inl_injective, Sum.inr_injective

Lean core dependencies: And, Eq, Eq.mp, Eq.mpr, Eq.symm, Eq.trans, Exists, False, False.elim, Not, Sum, True, absurd, congrArg, eq_false', id, noConfusion_of_Nat, not_false_eq_true, of_eq_true

Used by: InterfaceOld.Value.join, InterfaceOld.Value.join_fired_inl, InterfaceOld.Value.join_fired_inr, InterfaceOld.Value.join_left_right

NoteInterfaceOld.Value.join

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

Show details

| a.join 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: 9485 (size of the value term)

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

Inner dependencies: InterfaceOld.Value.join_disjoint

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_fired_inl, InterfaceOld.Value.join_fired_inr, 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.join_fired_inl

theorem InterfaceOld.Value.join_fired_inl✝ {I J : InterfaceOld} (a : I.Value) (b : J.Value) :
  (a.join b).fired.preimage Sum.inl ⋯ = a.fired

Show details

fun {I J} a b =>
  id
    (Finset.ext fun x =>
      of_eq_true
        (Eq.trans
          (congrFun'
            (congrArg Iff
              (Eq.trans
                (Eq.trans
                  (congrFun'
                    (congrArg Membership.mem
                      (Finset.preimage_inl
                        ((Finset.map { toFun := Sum.inl, inj' := Sum.inl_injective }
                              a.fired).disjUnion
                          (Finset.map { toFun := Sum.inr, inj' := Sum.inr_injective } b.fired)
                          (InterfaceOld.Value.join_disjoint✝ a b))))
                    x)
                  Finset.mem_toLeft._simp_1)
                (Eq.trans Finset.mem_disjUnion._simp_1
                  (Eq.trans
                    (congr (congrArg Or (Finset.mem_map_mk._simp_1 Sum.inl Sum.inl_injective))
                      (Eq.trans Finset.mem_map._simp_1
                        (Eq.trans
                          (congrArg Exists
                            (funext fun a =>
                              Eq.trans
                                (congrArg (And (a ∈ b.fired))
                                  (eq_false' fun h =>
                                    False.elim (noConfusion_of_Nat Sum.ctorIdx h)))
                                (and_false (a ∈ b.fired))))
                          exists_false._simp_1)))
                    (or_false (x ∈ a.fired))))))
            (x ∈ a.fired))
          (iff_self (x ∈ a.fired))))

Complexity: 12570 (size of the value term)

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

Proof dependencies: InterfaceOld.Value.join_disjoint

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

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

Used by: InterfaceOld.Value.left_join

TipInterfaceOld.Value.join_fired_inr

theorem InterfaceOld.Value.join_fired_inr✝ {I J : InterfaceOld} (a : I.Value) (b : J.Value) :
  (a.join b).fired.preimage Sum.inr ⋯ = b.fired

Show details

fun {I J} a b =>
  id
    (Finset.ext fun x =>
      of_eq_true
        (Eq.trans
          (congrFun'
            (congrArg Iff
              (Eq.trans
                (Eq.trans
                  (congrFun'
                    (congrArg Membership.mem
                      (Finset.preimage_inr
                        ((Finset.map { toFun := Sum.inl, inj' := Sum.inl_injective }
                              a.fired).disjUnion
                          (Finset.map { toFun := Sum.inr, inj' := Sum.inr_injective } b.fired)
                          (InterfaceOld.Value.join_disjoint✝ a b))))
                    x)
                  Finset.mem_toRight._simp_1)
                (Eq.trans Finset.mem_disjUnion._simp_1
                  (Eq.trans
                    (congr
                      (congrArg Or
                        (Eq.trans Finset.mem_map._simp_1
                          (Eq.trans
                            (congrArg Exists
                              (funext fun a_1 =>
                                Eq.trans
                                  (congrArg (And (a_1 ∈ a.fired))
                                    (eq_false' fun h =>
                                      False.elim (noConfusion_of_Nat Sum.ctorIdx h)))
                                  (and_false (a_1 ∈ a.fired))))
                            exists_false._simp_1)))
                      (Finset.mem_map_mk._simp_1 Sum.inr Sum.inr_injective))
                    (false_or (x ∈ b.fired))))))
            (x ∈ b.fired))
          (iff_self (x ∈ b.fired))))

Complexity: 12534 (size of the value term)

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

Proof dependencies: InterfaceOld.Value.join_disjoint

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

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

Used by: InterfaceOld.Value.right_join

TipInterfaceOld.Value.eq_of_heq

theorem 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.Value.ext_of_fired_eq, InterfaceOld.unit.Value.subsingleton

TipInterfaceOld.Value.ext_of_fired_eq

theorem InterfaceOld.Value.ext_of_fired_eq✝ {I : InterfaceOld} {a b : I.Value} (hfired : a.fired = b.fired)
  (hval :
    ∀ (x : I.Ports) (ha : x ∈ a.fired) (hb : x ∈ b.fired), a.value ⟨x, ha⟩ = b.value ⟨x, hb⟩) :
  a = b

Show details

fun {I} {a b} hfired hval =>
  InterfaceOld.Value.eq_of_heq hfired
    (Function.hfunext (congrArg (fun s => ↥s) hfired) fun p q hpq =>
      have hval' :=
        (Subtype.heq_iff_coe_eq fun x =>
              Eq.mpr (id (congrArg (fun _a => x ∈ _a ↔ x ∈ b.fired) hfired)) Iff.rfl).mp
          hpq;
      have this := hval (↑p) p.property (hfired ▸ p.property);
      have hpq2 := Subtype.ext hval';
      Eq.ndrec (motive := fun q => p ≍ q → ↑p = ↑q → a.value p ≍ b.value q)
        (fun hpq hval' => heq_of_eq this) hpq2 hpq hval')

Complexity: 5164 (size of the value term)

Dependencies: InterfaceOld, InterfaceOld.Value

Proof dependencies: InterfaceOld.Value.eq_of_heq

Mathlib dependencies: Finset, Function.hfunext, Subtype.heq_iff_coe_eq

Lean core dependencies: Eq, Eq.mpr, HEq, Iff, Iff.rfl, Subtype, Subtype.ext, congrArg, heq_of_eq, id

Used by: InterfaceOld.Value.join_left_right, InterfaceOld.Value.left_join, InterfaceOld.Value.right_join

ImportantInterfaceOld.Value.left_join

theorem 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: 18091 (size of the value term)

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

Proof dependencies: InterfaceOld.Value.ext_of_fired_eq, InterfaceOld.Value.join_fired_inl

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

theorem 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: 18055 (size of the value term)

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

Proof dependencies: InterfaceOld.Value.ext_of_fired_eq, InterfaceOld.Value.join_fired_inr

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

TipFinset.sum_preimage_map_disjUnion

theorem Finset.sum_preimage_map_disjUnion✝ {α β : Type} (s : Finset (α ⊕ β))
  (h :
    Disjoint (Finset.map { toFun := Sum.inl, inj' := ⋯ } (s.preimage Sum.inl ⋯))
      (Finset.map { toFun := Sum.inr, inj' := ⋯ } (s.preimage Sum.inr ⋯))) :
  (Finset.map { toFun := Sum.inl, inj' := ⋯ } (s.preimage Sum.inl ⋯)).disjUnion
      (Finset.map { toFun := Sum.inr, inj' := ⋯ } (s.preimage Sum.inr ⋯)) h =
    s

Show details

fun {α β} s h =>
  Finset.ext fun x =>
    Sum.casesOn (motive := fun t =>
      x = t →
        (x ∈
            (Finset.map { toFun := Sum.inl, inj' := Sum.inl_injective }
                  (s.preimage Sum.inl (Function.Injective.injOn Sum.inl_injective))).disjUnion
              (Finset.map { toFun := Sum.inr, inj' := Sum.inr_injective }
                (s.preimage Sum.inr (Function.Injective.injOn Sum.inr_injective)))
              h ↔
          x ∈ s))
      x
      (fun a h_1 =>
        Eq.symm h_1 ▸
          of_eq_true
            (Eq.trans
              (congrFun'
                (congrArg Iff
                  (Eq.trans
                    (Eq.trans
                      (congrFun'
                        (congrArg Membership.mem
                          (Finset.disjUnion.congr_simp
                            (Finset.map { toFun := Sum.inl, inj' := Sum.inl_injective }
                              (s.preimage Sum.inl (Function.Injective.injOn Sum.inl_injective)))
                            (Finset.map { toFun := Sum.inl, inj' := Sum.inl_injective } s.toLeft)
                            (congrArg (Finset.map { toFun := Sum.inl, inj' := Sum.inl_injective })
                              (Finset.preimage_inl s))
                            (Finset.map { toFun := Sum.inr, inj' := Sum.inr_injective }
                              (s.preimage Sum.inr (Function.Injective.injOn Sum.inr_injective)))
                            (Finset.map { toFun := Sum.inr, inj' := Sum.inr_injective } s.toRight)
                            (congrArg (Finset.map { toFun := Sum.inr, inj' := Sum.inr_injective })
                              (Finset.preimage_inr s))
                            h))
                        (Sum.inl a))
                      Finset.mem_disjUnion._simp_1)
                    (Eq.trans
                      (congr
                        (congrArg Or
                          (Eq.trans (Finset.mem_map_mk._simp_1 Sum.inl Sum.inl_injective)
                            Finset.mem_toLeft._simp_1))
                        (Eq.trans Finset.mem_map._simp_1
                          (Eq.trans
                            (congrArg Exists
                              (funext fun a_1 =>
                                Eq.trans
                                  (congr (congrArg And Finset.mem_toRight._simp_1)
                                    (eq_false' fun h =>
                                      False.elim (noConfusion_of_Nat Sum.ctorIdx h)))
                                  (and_false (Sum.inr a_1 ∈ s))))
                            exists_false._simp_1)))
                      (or_false (Sum.inl a ∈ s)))))
                (Sum.inl a ∈ s))
              (iff_self (Sum.inl a ∈ s))))
      (fun b h_1 =>
        Eq.symm h_1 ▸
          of_eq_true
            (Eq.trans
              (congrFun'
                (congrArg Iff
                  (Eq.trans
                    (Eq.trans
                      (congrFun'
                        (congrArg Membership.mem
                          (Finset.disjUnion.congr_simp
                            (Finset.map { toFun := Sum.inl, inj' := Sum.inl_injective }
                              (s.preimage Sum.inl (Function.Injective.injOn Sum.inl_injective)))
                            (Finset.map { toFun := Sum.inl, inj' := Sum.inl_injective } s.toLeft)
                            (congrArg (Finset.map { toFun := Sum.inl, inj' := Sum.inl_injective })
                              (Finset.preimage_inl s))
                            (Finset.map { toFun := Sum.inr, inj' := Sum.inr_injective }
                              (s.preimage Sum.inr (Function.Injective.injOn Sum.inr_injective)))
                            (Finset.map { toFun := Sum.inr, inj' := Sum.inr_injective } s.toRight)
                            (congrArg (Finset.map { toFun := Sum.inr, inj' := Sum.inr_injective })
                              (Finset.preimage_inr s))
                            h))
                        (Sum.inr b))
                      Finset.mem_disjUnion._simp_1)
                    (Eq.trans
                      (congr
                        (congrArg Or
                          (Eq.trans Finset.mem_map._simp_1
                            (Eq.trans
                              (congrArg Exists
                                (funext fun a =>
                                  Eq.trans
                                    (congr (congrArg And Finset.mem_toLeft._simp_1)
                                      (eq_false' fun h =>
                                        False.elim (noConfusion_of_Nat Sum.ctorIdx h)))
                                    (and_false (Sum.inl a ∈ s))))
                              exists_false._simp_1)))
                        (Eq.trans (Finset.mem_map_mk._simp_1 Sum.inr Sum.inr_injective)
                          Finset.mem_toRight._simp_1))
                      (false_or (Sum.inr b ∈ s)))))
                (Sum.inr b ∈ s))
              (iff_self (Sum.inr b ∈ s))))
      (Eq.refl x)

Complexity: 21041 (size of the value term)

Dependencies: (none)

Mathlib dependencies: Disjoint, Finset, Finset.disjUnion, Finset.ext, Finset.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.symm, Eq.trans, Exists, False, False.elim, Iff, Or, Sum, True, and_false, congr, congrArg, congrFun', eq_false', false_or, funext, iff_self, noConfusion_of_Nat, of_eq_true, or_false

Used by: InterfaceOld.Value.join_left_right

ImportantInterfaceOld.Value.join_left_right

theorem 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: 33316 (size of the value term)

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

Proof dependencies: Finset.sum_preimage_map_disjUnion, InterfaceOld.Value.ext_of_fired_eq, InterfaceOld.Value.join_disjoint

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