@[simp]

theorem Listed.array_sum_eq_finset_sum {ι : Type u_1} {α : Type u_2} [Listed ι] [AddCommMonoid α] (f : ι → α) : (Array.map f array).sum = ∑ i : Fin (size ι), f (decodeFin i)

structure WeightedNetKAT.EWNKA (F N 𝒮 Q : Type) [Semiring 𝒮] [Listed F] [Listed N] [Listed Q] : Type

An efficient version of [WNKA] that uses explicit matrices.

• ι : EMatrix Unit Q 𝒮

  ι is the initial weightings.

• δ : EMatrix Pk[F,N] Pk[F,N] (EMatrix Q Q 𝒮)

  δ is a family of transition functions δ[α,β] : Q → 𝒞 𝒮 Q indexed by packet pairs.

• 𝒪 : EMatrix Pk[F,N] Pk[F,N] (EMatrix Q Unit 𝒮)

  𝒪 is a family of output weightings 𝒪[α,β] : 𝒞 𝒮 Q indexed by packet pairs. Note that we use 𝒪 instead of λ, since λ is the function symbol in Lean.

def WeightedNetKAT.«termEWNKA[_,_,_,_]» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def WeightedNetKAT.S.Eι {𝒮 X Y : Type} [Listed X] [Listed Y] : EMatrix Unit X 𝒮 → EMatrix Unit Y 𝒮 → EMatrix Unit (X ⊕ Y) 𝒮

Equations

• Eι[m₁,m₂] = EMatrix.ofFnSlow fun (x : Unit) (x_1 : X ⊕ Y) => Sum.elim (fun (x : X) => m₁ () x) (fun (x : Y) => m₂ () x) x_1

def WeightedNetKAT.«termEι[_,_]» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem WeightedNetKAT.S.Eι_eq_ι {𝒮 X Y : Type} [Listed X] [Listed Y] {m₁ : EMatrix Unit X 𝒮} {m₂ : EMatrix Unit Y 𝒮} {i : Unit} {j : X ⊕ Y} : Eι[m₁,m₂] i j = m₁.asMatrix.fromCols m₂.asMatrix i j

def WeightedNetKAT.S.E𝒪_lambda {𝒮 X Y : Type} [Listed X] [Listed Y] : EMatrix X Unit 𝒮 → EMatrix Y Unit 𝒮 → EMatrix (X ⊕ Y) Unit 𝒮

Equations

• E𝒪_lambda[m₁,m₂] = EMatrix.ofFnSlow fun (x : X ⊕ Y) (x_1 : Unit) => Sum.elim (fun (x : X) => m₁ x ()) (fun (x : Y) => m₂ x ()) x

def WeightedNetKAT.«termE𝒪_lambda[_,_]» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem WeightedNetKAT.S.E𝒪_lambda_eq_𝒪 {𝒮 X Y : Type} [Listed X] [Listed Y] {m₁ : EMatrix X Unit 𝒮} {m₂ : EMatrix Y Unit 𝒮} {i : X ⊕ Y} {j : Unit} : E𝒪_lambda[m₁,m₂] i j = m₁.asMatrix.fromRows m₂.asMatrix i j

theorem WeightedNetKAT.S.E𝒪_lambda_eq_𝒪' {𝒮 X Y : Type} [Listed X] [Listed Y] {m₁ : Matrix X Unit 𝒮} {m₂ : Matrix Y Unit 𝒮} {i : X ⊕ Y} {j : Unit} : m₁.fromRows m₂ i j = E𝒪_lambda[EMatrix.ofMatrix m₁,EMatrix.ofMatrix m₂] i j

def WeightedNetKAT.S.Eδ_delta {𝒮 : Type} {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {W : Type u_4} [Listed X] [Listed Y] [Listed Z] [Listed W] : EMatrix X Y 𝒮 → EMatrix X W 𝒮 → EMatrix Z Y 𝒮 → EMatrix Z W 𝒮 → EMatrix (X ⊕ Z) (Y ⊕ W) 𝒮

Equations

• One or more equations did not get rendered due to their size.

def WeightedNetKAT.«termEδ_delta[[_,_],[_,_]]» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem WeightedNetKAT.S.Eδ_delta_eq_δ {𝒮 : Type} {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {W : Type u_4} [Listed X] [Listed Y] [Listed Z] [Listed W] (mxy : EMatrix X Y 𝒮) (mxw : EMatrix X W 𝒮) (mzy : EMatrix Z Y 𝒮) (mzw : EMatrix Z W 𝒮) {i : X ⊕ Z} {j : Y ⊕ W} : Eδ_delta[[mxy,mxw],[mzy,mzw]] i j = Matrix.fromBlocks mxy.asMatrix mxw.asMatrix mzy.asMatrix mzw.asMatrix i j

@[reducible, inline]

abbrev WeightedNetKAT.Eη₂ {𝒮 : Type} [Semiring 𝒮] {X Y : Type} [instX : Listed X] [instY : Listed Y] (i : X) (j : Y) : EMatrix X Y 𝒮

Equations

• WeightedNetKAT.Eη₂ i j = EMatrix.ofFn fun (i' : Li[X]) (j' : Li[Y]) => if Listed.encode i = ↑i' ∧ Listed.encode j = ↑j' then 1 else 0

def WeightedNetKAT.Eι {F : Type} [Listed F] {N 𝒮 : Type} [Semiring 𝒮] (p : RPol 𝒮) : EMatrix Unit (S p) 𝒮

Equations

• WeightedNetKAT.Eι WeightedNetKAT.RPol.Drop = WeightedNetKAT.Eη₂ () ()
• WeightedNetKAT.Eι wnk_rpol {skip} = WeightedNetKAT.Eη₂ () ()
• WeightedNetKAT.Eι wnk_rpol {@test ~pk} = WeightedNetKAT.Eη₂ () ()
• WeightedNetKAT.Eι wnk_rpol {@mod ~pk} = WeightedNetKAT.Eη₂ () ()
• WeightedNetKAT.Eι wnk_rpol {dup} = WeightedNetKAT.Eη₂ () (Sum.inl ())
• WeightedNetKAT.Eι wnk_rpol {~w ⨀ ~p₁} = w • WeightedNetKAT.Eι p₁
• WeightedNetKAT.Eι wnk_rpol {~p₁ ⨁ ~p₂} = Eι[WeightedNetKAT.Eι p₁,WeightedNetKAT.Eι p₂]
• WeightedNetKAT.Eι wnk_rpol {~p₁; ~q} = Eι[WeightedNetKAT.Eι p₁,0]
• WeightedNetKAT.Eι wnk_rpol {~p_2*} = Eι[0,1]

def WeightedNetKAT.boxₑ {Pk : Type} [Listed Pk] {X : Type u_1} [Listed X] {Q : Type} [Mul Q] [AddCommMonoid Q] {Z : Type} [Listed Z] [Unique Z] (l : EMatrix Z X Q) (r : EMatrix Pk Pk (EMatrix X Z Q)) : EMatrix Pk Pk Q

Equations

• (l ⊠ₑ r) = EMatrix.ofFn fun (α β : Li[Pk]) => (l * r.asNMatrix α β).asNMatrix ⟨0, ⋯⟩ ⟨0, ⋯⟩

def WeightedNetKAT.«term_⊠ₑ_» : Lean.TrailingParserDescr

Equations

• WeightedNetKAT.«term_⊠ₑ_» = Lean.ParserDescr.trailingNode `WeightedNetKAT.«term_⊠ₑ_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊠ₑ ") (Lean.ParserDescr.cat `term 50))

@[simp]

theorem Liste.decodeFin_unique {α : Type u_1} [Listed α] [Unique α] (i : Li[α]) : Listed.decodeFin i = default

@[simp]

theorem WeightedNetKAT.boxₑ_eq_box {Pk : Type} [Listed Pk] {X : Type u_1} [Listed X] [Fintype X] {Q : Type} [Mul Q] [AddCommMonoid Q] {Z : Type} [Listed Z] [Unique Z] (l : EMatrix Z X Q) (r : EMatrix Pk Pk (EMatrix X Z Q)) : (l ⊠ₑ r) = EMatrix.ofMatrix (l.asMatrix ⊠ r.asMatrix₂)

def WeightedNetKAT.foxₑ {Pk : Type} [Listed Pk] {A B C Q : Type} [AddCommMonoid Q] [Mul Q] [Listed A] [Listed B] [Listed C] (l : EMatrix A B Q) (r : EMatrix Pk Pk (EMatrix B C Q)) : EMatrix Pk Pk (EMatrix A C Q)

Equations

• (l ⊡ₑ r) = EMatrix.ofFn fun (α β : Li[Pk]) => l * r.asNMatrix α β

def WeightedNetKAT.«term_⊡ₑ_» : Lean.TrailingParserDescr

Equations

• WeightedNetKAT.«term_⊡ₑ_» = Lean.ParserDescr.trailingNode `WeightedNetKAT.«term_⊡ₑ_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊡ₑ ") (Lean.ParserDescr.cat `term 50))

@[simp]

theorem WeightedNetKAT.foxₑ_eq_fox {Pk : Type} [Listed Pk] {A B C Q : Type} [AddCommMonoid Q] [Mul Q] [Listed A] [Listed B] [Listed C] [Fintype A] [Fintype B] [Fintype C] (l : EMatrix A B Q) (r : EMatrix Pk Pk (EMatrix B C Q)) : (l ⊡ₑ r) = EMatrix.ofMatrix₂ (l.asMatrix ⊡ r.asMatrix₂)

@[inline, specialize #[]]

def WeightedNetKAT.soxₑ {Pk : Type} [Listed Pk] {A B Q : Type} [AddCommMonoid Q] [Mul Q] [Listed A] [Listed B] (l : EMatrix Pk Pk Q) (r : EMatrix Pk Pk (EMatrix A B Q)) : EMatrix Pk Pk (EMatrix A B Q)

Equations

• (l ⊟ₑ r) = EMatrix.ofFn fun (α β : Li[Pk]) => ∑ m : Li[Pk], l.asNMatrix α m • r.asNMatrix m β

def WeightedNetKAT.«term_⊟ₑ_» : Lean.TrailingParserDescr

Equations

• WeightedNetKAT.«term_⊟ₑ_» = Lean.ParserDescr.trailingNode `WeightedNetKAT.«term_⊟ₑ_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊟ₑ ") (Lean.ParserDescr.cat `term 50))

@[simp]

theorem WeightedNetKAT.soxₑ_eq_sox {Pk : Type} [Listed Pk] {A B Q : Type} [AddCommMonoid Q] [Mul Q] [Listed A] [Listed B] [Fintype A] [Fintype B] [Fintype Pk] (l : EMatrix Pk Pk Q) (r : EMatrix Pk Pk (EMatrix A B Q)) : (l ⊟ₑ r) = EMatrix.ofMatrix₂ (l.asMatrix ⊟> r.asMatrix₂)

def WeightedNetKAT.sox'ₑ {Pk : Type} [Listed Pk] {A B Q : Type} [AddCommMonoid Q] [Mul Q] [Listed A] [Listed B] (l : EMatrix Pk Pk (EMatrix A B Q)) (r : EMatrix Pk Pk Q) : EMatrix Pk Pk (EMatrix A B Q)

Equations

• (l ⊟'ₑ r) = EMatrix.ofFn fun (α β : Li[Pk]) => ∑ m : Li[Pk], MulOpposite.op (r.asNMatrix m β) • l.asNMatrix α m

def WeightedNetKAT.«term_⊟'ₑ_» : Lean.TrailingParserDescr

Equations

• WeightedNetKAT.«term_⊟'ₑ_» = Lean.ParserDescr.trailingNode `WeightedNetKAT.«term_⊟'ₑ_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊟'ₑ ") (Lean.ParserDescr.cat `term 50))

@[simp]

theorem WeightedNetKAT.sox'ₑ_eq_sox' {Pk : Type} [Listed Pk] {A B Q : Type} [AddCommMonoid Q] [Mul Q] [Listed A] [Listed B] [Fintype A] [Fintype B] [Fintype Pk] (l : EMatrix Pk Pk (EMatrix A B Q)) (r : EMatrix Pk Pk Q) : (l ⊟'ₑ r) = EMatrix.ofMatrix₂ (l.asMatrix₂ <⊟ r.asMatrix)

def WeightedNetKAT.croxₑ {Pk : Type} [Listed Pk] {A B C Q : Type} [AddCommMonoid Q] [Mul Q] [Listed A] [Listed B] [DecidableEq C] [Listed C] (l : EMatrix Pk Pk (EMatrix A B Q)) (r : EMatrix Pk Pk (EMatrix B C Q)) : EMatrix Pk Pk (EMatrix A C Q)

Equations

• (l ⊞ₑ r) = EMatrix.ofFn fun (α β : Li[Pk]) => ∑ m : Li[Pk], l.asNMatrix α m * r.asNMatrix m β

def WeightedNetKAT.«term_⊞ₑ_» : Lean.TrailingParserDescr

Equations

• WeightedNetKAT.«term_⊞ₑ_» = Lean.ParserDescr.trailingNode `WeightedNetKAT.«term_⊞ₑ_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊞ₑ ") (Lean.ParserDescr.cat `term 50))

@[simp]

theorem WeightedNetKAT.croxₑ_eq_crox {Pk : Type} [Listed Pk] {A B C Q : Type} [AddCommMonoid Q] [Mul Q] [Listed A] [Listed B] [DecidableEq C] [Listed C] [Fintype A] [Fintype B] [Fintype C] [Fintype Pk] (l : EMatrix Pk Pk (EMatrix A B Q)) (r : EMatrix Pk Pk (EMatrix B C Q)) : (l ⊞ₑ r) = EMatrix.ofMatrix₂ (l.asMatrix₂ ⊞ r.asMatrix₂)

def WeightedNetKAT.RPol.E𝒪_lambda {F : Type} [Listed F] {N 𝒮 : Type} [Semiring 𝒮] [KStar 𝒮] [Listed N] (p : RPol 𝒮) : EMatrix Pk[F,N] Pk[F,N] (EMatrix (S p) Unit 𝒮)

Equations

• One or more equations did not get rendered due to their size.
• WeightedNetKAT.RPol.Drop.E𝒪_lambda = 0
• wnk_rpol {skip}.E𝒪_lambda = EMatrix.ofFn fun (α β : Li[Pk[F,N]]) => if α = β then EMatrix.ofFn fun (x : Li[WeightedNetKAT.S wnk_rpol {skip}]) => 1 else 0
• wnk_rpol {@test ~γ}.E𝒪_lambda = EMatrix.ofFn fun (α β : Li[Pk[F,N]]) => if α = β ∧ ↑β = Listed.encode γ then EMatrix.ofFn fun (x : Li[WeightedNetKAT.S wnk_rpol {@test ~γ}]) => 1 else 0
• wnk_rpol {@mod ~π}.E𝒪_lambda = EMatrix.ofFn fun (x β : Li[Pk[F,N]]) => if ↑β = Listed.encode π then EMatrix.ofFn fun (x : Li[WeightedNetKAT.S wnk_rpol {@mod ~π}]) => 1 else 0
• wnk_rpol {dup}.E𝒪_lambda = EMatrix.ofFn fun (α β : Li[Pk[F,N]]) => if α = β then WeightedNetKAT.Eη₂ (Sum.inr ()) () else 0
• wnk_rpol {~w ⨀ ~p₁}.E𝒪_lambda = EMatrix.ofFn fun (α β : Li[Pk[F,N]]) => p₁.E𝒪_lambda.getN α β
• wnk_rpol {~p₁ ⨁ ~p₂}.E𝒪_lambda = EMatrix.ofFn fun (α β : Li[Pk[F,N]]) => E𝒪_lambda[p₁.E𝒪_lambda.getN α β,p₂.E𝒪_lambda.getN α β]

def WeightedNetKAT.RPol.E𝒪_heart {F : Type} [Listed F] {N 𝒮 : Type} [Semiring 𝒮] [KStar 𝒮] [Listed N] [DecidableEq N] (p₁ : RPol 𝒮) : EMatrix Pk[F,N] Pk[F,N] 𝒮

Equations

• p₁.E𝒪_heart = KStar.kstar (WeightedNetKAT.Eι p₁ ⊠ₑ p₁.E𝒪_lambda)

theorem WeightedNetKAT.RPol.E𝒪_lambda_iter {F : Type} [Listed F] {N 𝒮 : Type} [Semiring 𝒮] [KStar 𝒮] [Listed N] [DecidableEq N] (p₁ : RPol 𝒮) : wnk_rpol {~p₁*}.E𝒪_lambda = EMatrix.ofFn fun (α β : Li[Pk[F,N]]) => E𝒪_lambda[∑ γ : Li[Pk[F,N]], MulOpposite.op (p₁.E𝒪_heart.asNMatrix γ β) • p₁.E𝒪_lambda.asNMatrix α γ,EMatrix.ofFn fun (x x_1 : Li[Unit]) => p₁.E𝒪_heart.asNMatrix α β]

@[simp]

theorem WeightedNetKAT.RPol.EMatrix.asMatrix_one {X : Type u_1} {α : Type u_2} [Listed X] [DecidableEq X] [Zero α] [One α] : EMatrix.asMatrix 1 = 1

@[simp]

theorem WeightedNetKAT.RPol.Eι_eq_ι {F : Type} [Listed F] {N 𝒮 : Type} [Semiring 𝒮] {p : RPol 𝒮} : Eι p = EMatrix.ofMatrix p.ι

theorem WeightedNetKAT.RPol.E𝒪_heart_eq_𝒪_heart {F : Type} [Listed F] {N 𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [KStar 𝒮] [DecidableEq F] [Listed N] [DecidableEq N] [LawfulKStar (NMatrix (Listed.size Pk[F,N]) (Listed.size Pk[F,N]) 𝒮)] {p : RPol 𝒮} (h : p.E𝒪_lambda = EMatrix.ofMatrix₂ p.𝒪) : p.E𝒪_heart = EMatrix.ofMatrix p.𝒪_heart

theorem EMatrix.apply_encodeFin {m : Type u_1} {n : Type u_2} {α : Type u_3} [Listed m] [Listed n] {M : NMatrix (Listed.size m) (Listed.size n) α} {i : m} {j : n} : M i j = M (Listed.encodeFin i) (Listed.encodeFin j)

@[simp]

theorem WeightedNetKAT.RPol.E𝒪_lambda_eq_𝒪 {F : Type} [Listed F] {N 𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [KStar 𝒮] [DecidableEq F] [Listed N] [DecidableEq N] [LawfulKStar (NMatrix (Listed.size Pk[F,N]) (Listed.size Pk[F,N]) 𝒮)] {p : RPol 𝒮} : p.E𝒪_lambda = EMatrix.ofMatrix₂ p.𝒪

def WeightedNetKAT.RPol.ι_aux {F : Type} [Listed F] {N 𝒮 : Type} [Semiring 𝒮] (p : RPol 𝒮) : Matrix Unit (S p) 𝒮

Equations

• p.ι_aux = (WeightedNetKAT.Eι p).asMatrix

def WeightedNetKAT.RPol.𝒪_aux {F : Type} [Listed F] {N 𝒮 : Type} [Semiring 𝒮] [KStar 𝒮] [Listed N] (p : RPol 𝒮) : Matrix Pk[F,N] Pk[F,N] (Matrix (S p) Unit 𝒮)

Equations

• p.𝒪_aux = p.E𝒪_lambda.asMatrix₂

def WeightedNetKAT.RPol.Eδ_delta {F : Type} [Listed F] {N 𝒮 : Type} [Semiring 𝒮] [KStar 𝒮] [Listed N] [DecidableEq N] (p : RPol 𝒮) : EMatrix Pk[F,N] Pk[F,N] (EMatrix (S p) (S p) 𝒮)

Equations

• One or more equations did not get rendered due to their size.
• WeightedNetKAT.RPol.Drop.Eδ_delta = EMatrix.ofFn fun (x x_1 : Li[Pk[F,N]]) => 0
• wnk_rpol {skip}.Eδ_delta = EMatrix.ofFn fun (x x_1 : Li[Pk[F,N]]) => 0
• wnk_rpol {@test ~pk}.Eδ_delta = EMatrix.ofFn fun (x x_1 : Li[Pk[F,N]]) => 0
• wnk_rpol {@mod ~pk}.Eδ_delta = EMatrix.ofFn fun (x x_1 : Li[Pk[F,N]]) => 0
• wnk_rpol {~w ⨀ ~p₁}.Eδ_delta = p₁.Eδ_delta
• wnk_rpol {~p₁ ⨁ ~p₂}.Eδ_delta = EMatrix.ofFn fun (α β : Li[Pk[F,N]]) => Eδ_delta[[p₁.Eδ_delta.getN α β,0],[0,p₂.Eδ_delta.getN α β]]

@[simp]

theorem WeightedNetKAT.RPol.Eδ_delta_eq_δ {F : Type} [Listed F] {N 𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [KStar 𝒮] [DecidableEq F] [Listed N] [DecidableEq N] [LawfulKStar (NMatrix (Listed.size Pk[F,N]) (Listed.size Pk[F,N]) 𝒮)] {p : RPol 𝒮} : p.Eδ_delta = EMatrix.ofMatrix₂ p.δ

def WeightedNetKAT.RPol.δ_aux {F : Type} [Listed F] {N 𝒮 : Type} [Semiring 𝒮] [KStar 𝒮] [Listed N] [DecidableEq N] (p : RPol 𝒮) : Matrix Pk[F,N] Pk[F,N] (Matrix (S p) (S p) 𝒮)

Equations

• p.δ_aux = p.Eδ_delta.asMatrix₂

def WeightedNetKAT.RPol.ewnka {F : Type} [Listed F] {N 𝒮 : Type} [Semiring 𝒮] [KStar 𝒮] [Listed N] [DecidableEq N] (p : RPol 𝒮) : EWNKA[F,N,𝒮,S p]

Equations

• p.ewnka = { ι := WeightedNetKAT.Eι p, δ := p.Eδ_delta, 𝒪 := p.E𝒪_lambda }

def WeightedNetKAT.WNKA.toEWNKA {F : Type} [Listed F] {N 𝒮 : Type} [Semiring 𝒮] [Listed N] {Q : Type} [Listed Q] (𝔄 : WNKA[F,N,𝒮,Q]) : EWNKA[F,N,𝒮,Q]

Equations

• 𝔄.toEWNKA = { ι := EMatrix.ofMatrix 𝔄.ι, δ := EMatrix.ofMatrix₂ 𝔄.δ, 𝒪 := EMatrix.ofMatrix₂ 𝔄.𝒪 }

def WeightedNetKAT.EWNKA.toWNKA {F : Type} [Listed F] {N 𝒮 : Type} [Semiring 𝒮] [Listed N] {Q : Type} [Listed Q] (𝔈 : EWNKA[F,N,𝒮,Q]) : WNKA[F,N,𝒮,Q]

Equations

• 𝔈.toWNKA = { ι := 𝔈.ι.asMatrix, δ := 𝔈.δ.asMatrix₂, 𝒪 := 𝔈.𝒪.asMatrix₂ }

@[simp]

theorem WeightedNetKAT.WNKA.toWNKA_toEWNKA {F : Type} [Listed F] {N 𝒮 : Type} [Semiring 𝒮] [Listed N] {Q : Type} [Listed Q] (𝔄 : WNKA[F,N,𝒮,Q]) : 𝔄.toEWNKA.toWNKA = 𝔄

@[simp]

theorem WeightedNetKAT.EWNKA.toEWNKA_toWNKA {F : Type} [Listed F] {N 𝒮 : Type} [Semiring 𝒮] [Listed N] {Q : Type} [Listed Q] (𝔈 : EWNKA[F,N,𝒮,Q]) : 𝔈.toWNKA.toEWNKA = 𝔈

@[simp]

theorem WeightedNetKAT.RPol.wnka_toEWNKA {F : Type} [Listed F] {N 𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [Listed N] [DecidableEq F] [DecidableEq N] [KStar 𝒮] [LawfulKStar 𝒮] [KStarIter 𝒮] [MulLeftMono 𝒮] [MulRightMono 𝒮] [OmegaContinuousNonUnitalSemiring 𝒮] (p : RPol 𝒮) : p.wnka.toEWNKA = p.ewnka

@[simp]

theorem WeightedNetKAT.RPol.ewnka_toWNKA {F : Type} [Listed F] {N 𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [Listed N] [DecidableEq F] [DecidableEq N] [KStar 𝒮] [LawfulKStar 𝒮] [KStarIter 𝒮] [MulLeftMono 𝒮] [MulRightMono 𝒮] [OmegaContinuousNonUnitalSemiring 𝒮] (p : RPol 𝒮) : p.ewnka.toWNKA = p.wnka

def WeightedNetKAT.RPol.wnka_fast {F : Type} [Listed F] {N 𝒮 : Type} [Semiring 𝒮] [Listed N] [DecidableEq N] [KStar 𝒮] (p : RPol 𝒮) : WNKA[F,N,𝒮,S p]

Equations

• p.wnka_fast = p.ewnka.toWNKA

@[simp]

def WeightedNetKAT.EWNKA.toEWNKA_ι_apply {F : Type} [Listed F] {N 𝒮 : Type} [Semiring 𝒮] [Listed N] {Q : Type} [Listed Q] (𝔈 : EWNKA[F,N,𝒮,Q]) {α : Unit} {β : Q} : 𝔈.toWNKA.ι α β = 𝔈.ι α β

Equations

• ⋯ = ⋯

@[simp]

def WeightedNetKAT.EWNKA.toEWNKA_δ_apply {F : Type} [Listed F] {N 𝒮 : Type} [Semiring 𝒮] [Listed N] {Q : Type} [Listed Q] (𝔈 : EWNKA[F,N,𝒮,Q]) {α β : Pk[F,N]} : 𝔈.toWNKA.δ α β = (𝔈.δ α β).asMatrix

Equations

• ⋯ = ⋯

@[simp]

def WeightedNetKAT.EWNKA.toEWNKA_𝒪_apply {F : Type} [Listed F] {N 𝒮 : Type} [Semiring 𝒮] [Listed N] {Q : Type} [Listed Q] (𝔈 : EWNKA[F,N,𝒮,Q]) {α β : Pk[F,N]} : 𝔈.toWNKA.𝒪 α β = (𝔈.𝒪 α β).asMatrix

Equations

• ⋯ = ⋯

def WeightedNetKAT.«termLi[_]» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def WeightedNetKAT.EWNKA.sem {F : Type} [Listed F] {N 𝒮 : Type} [Semiring 𝒮] [Listed N] {Q : Type} [Listed Q] [DecidableEq N] (𝒜 : EWNKA[F,N,𝒮,Q]) : GS F N →c 𝒮

Equations

• One or more equations did not get rendered due to their size.

structure WeightedNetKAT.EWNKA.Precompute {F : Type} [Listed F] {N 𝒮 : Type} [Semiring 𝒮] [Listed N] {Q : Type} [Listed Q] (𝔈 : EWNKA[F,N,𝒮,Q]) : Type

Stores partial computation of the weight of a trace.

We want to compute the prefix as little as possible, and reuse it the final computation with 𝒪. This structure turned out to be crucial for performance, as Lean would push the computation of the prefix into the lambda where the final β was given, leading it to recomputing the prefix for every final packet.

This gives roughly a |Pk[F,N]| times speed up.

• m : EMatrix Unit Q 𝒮
• γ : Pk[F,N]

@[inline, specialize #[]]

def WeightedNetKAT.EWNKA.Precompute.finish {F : Type} [Listed F] {N 𝒮 : Type} [Semiring 𝒮] [Listed N] {Q : Type} [Listed Q] {𝔈 : EWNKA[F,N,𝒮,Q]} (p : 𝔈.Precompute) (β : Pk[F,N]) : 𝒮

Equations

• p.finish β = (p.m * 𝔈.𝒪 p.γ β) () ()

@[noinline, specialize #[]]

def WeightedNetKAT.EWNKA.semArray_aux {F : Type} [Listed F] {N 𝒮 : Type} [Semiring 𝒮] [Listed N] {Q : Type} [Listed Q] (𝒜 : EWNKA[F,N,𝒮,Q]) (α_xs : Array Pk[F,N]) (h : 0 < α_xs.size) : 𝒜.Precompute

Equations

• One or more equations did not get rendered due to their size.

@[inline, specialize #[]]

def WeightedNetKAT.EWNKA.semArray {F : Type} [Listed F] {N 𝒮 : Type} [Semiring 𝒮] [Listed N] {Q : Type} [Listed Q] (𝒜 : EWNKA[F,N,𝒮,Q]) (α_xs : Array Pk[F,N]) (h : 0 < α_xs.size) : 𝒜.Precompute

Equations

• 𝒜.semArray α_xs h = 𝒜.semArray_aux α_xs h

theorem WeightedNetKAT.EWNKA.semArray_eq_sem {F : Type} [Listed F] {N 𝒮 : Type} [Semiring 𝒮] [Listed N] {Q : Type} [Listed Q] [DecidableEq N] {𝔈 : EWNKA[F,N,𝒮,Q]} {α_xs : Array Pk[F,N]} {β : Pk[F,N]} (h : 0 < α_xs.size) : (𝔈.semArray α_xs h).finish β = 𝔈.sem (α_xs.toList.head ⋯, α_xs.toList.tail, β)

theorem WeightedNetKAT.RPol.ewnka_sem_eq_wnka_sem {F : Type} [Listed F] {N 𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [Listed N] [DecidableEq F] [DecidableEq N] [KStar 𝒮] [LawfulKStar 𝒮] [KStarIter 𝒮] [MulLeftMono 𝒮] [MulRightMono 𝒮] [OmegaContinuousNonUnitalSemiring 𝒮] (p : RPol 𝒮) : p.ewnka.sem = 𝒜⟦~p⟧