def WeightedNetKAT.Pred.compute {𝒮 : Type} [Semiring 𝒮] [DecidableEq 𝒮] {F : Type} [Listed F] [DecidableEq F] {N : Type} [DecidableEq N] (p : Pred[F,N]) : Pk[F,N] × List Pk[F,N] → Pk[F,N] × List Pk[F,N] →₀ 𝒮

Equations

• p.compute (π, h) = if p.test π then Finsupp.η' (π, h) else 0

@[irreducible]

def WeightedNetKAT.Pol.compute {𝒮 : Type} [Semiring 𝒮] [PartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [DecidableEq 𝒮] {F : Type} [Listed F] [DecidableEq F] {N : Type} [DecidableEq N] (p : Pol[F,N,𝒮]) (n : ℕ) : Pk[F,N] × List Pk[F,N] → Pk[F,N] × List Pk[F,N] →₀ 𝒮

Equations

• (WeightedNetKAT.Pol.Filter t).compute n = t.compute
• wnk_pol {~f ← ~n_1}.compute n = fun (x : Pk[F,N] × List Pk[F,N]) => match x with | (π, h) => Finsupp.η' (π[f ↦ n_1], h)
• wnk_pol {dup}.compute n = fun (x : Pk[F,N] × List Pk[F,N]) => match x with | (π, h) => Finsupp.η' (π, π :: h)
• wnk_pol {~p_2; ~q}.compute n = fun (h : Pk[F,N] × List Pk[F,N]) => (p_2.compute n h).bind (q.compute n)
• wnk_pol {~w ⨀ ~p_2}.compute n = fun (h : Pk[F,N] × List Pk[F,N]) => w * p_2.compute n h
• wnk_pol {~p_2 ⨁ ~q}.compute n = fun (h : Pk[F,N] × List Pk[F,N]) => p_2.compute n h + q.compute n h
• wnk_pol {~p_2*}.compute n = fun (h : Pk[F,N] × List Pk[F,N]) => ∑ i ∈ Finset.range n, (p_2 ^ i).compute n h

def Finset.toList' {α : Type} [Encodable α] [DecidableEq α] (s : Finset α) : List α

Equations

• s.toList' = Quotient.rep s.val

def Finsupp.pretty {X 𝒮 : Type} [Semiring 𝒮] [DecidableEq 𝒮] [DecidableEq X] (m : X →₀ 𝒮) : Finset (X × 𝒮)

Equations

• m.pretty = Finset.image (fun (s : X) => (s, m s)) m.support

@[implicit_reducible]

unsafe instance 𝒞.repr {X 𝒮 : Type} [Semiring 𝒮] [DecidableEq 𝒮] [DecidableEq X] [Repr X] [Repr 𝒮] : Repr (X →₀ 𝒮)

Equations

• 𝒞.repr = { reprPrec := fun (m : X →₀ 𝒮) (n : ℕ) => reprPrec m.pretty n }

def Finsupp.to𝒲 {𝒮 : Type} [Semiring 𝒮] {F : Type} [Listed F] {N : Type} (m : Pk[F,N] × List Pk[F,N] →₀ 𝒮) : Pk[F,N] × List Pk[F,N] →c 𝒮

Equations

• m.to𝒲 = { toFun := m.toFun, countable := ⋯ }

@[simp]

def Finsupp.to𝒲_apply {𝒮 : Type} [Semiring 𝒮] {F : Type} [Listed F] {N : Type} (m : Pk[F,N] × List Pk[F,N] →₀ 𝒮) (x : Pk[F,N] × List Pk[F,N]) : m.to𝒲 x = m x

Equations

• ⋯ = ⋯

@[simp]

def Finsupp.to𝒲_eq_zero {𝒮 : Type} [Semiring 𝒮] {F : Type} [Listed F] {N : Type} (m : Pk[F,N] × List Pk[F,N] →₀ 𝒮) : m.to𝒲 = 0 ↔ m = 0

Equations

• ⋯ = ⋯

@[implicit_reducible]

noncomputable instance instFintypeElemProdPkListSupportTo𝒲 {𝒮 : Type} [Semiring 𝒮] {F : Type} [Listed F] {N : Type} (m : Pk[F,N] × List Pk[F,N] →₀ 𝒮) : Fintype ↑m.to𝒲.support

Equations

• instFintypeElemProdPkListSupportTo𝒲 m = Set.Finite.fintype ⋯

@[simp]

theorem 𝒲.bind_of_𝒞' {𝒮 : Type} [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [Semiring 𝒮] [IsPositiveOrderedAddMonoid 𝒮] {F : Type} [Listed F] [DecidableEq F] {N : Type} [DecidableEq N] [Listed N] (m : Pk[F,N] × List Pk[F,N] →₀ 𝒮) (f : Pk[F,N] × List Pk[F,N] → Pk[F,N] × List Pk[F,N] →c 𝒮) : (m.to𝒲.bind fun (h : Pk[F,N] × List Pk[F,N]) => f h) = ∑ h ∈ m.support, { toFun := fun (h' : Pk[F,N] × List Pk[F,N]) => m h * (f h) h', countable := ⋯ }

theorem 𝒲.η_eq_η' {𝒮 : Type} [Semiring 𝒮] [DecidableEq 𝒮] {F : Type} [Listed F] [DecidableEq F] {N : Type} [DecidableEq N] (x : Pk[F,N] × List Pk[F,N]) : WeightedNetKAT.η x = (Finsupp.η' x).to𝒲

@[simp]

theorem 𝒲.bind_of_𝒞 {𝒮 : Type} [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [Semiring 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [DecidableEq 𝒮] {F : Type} [Listed F] [DecidableEq F] {N : Type} [DecidableEq N] [Listed N] (m : Pk[F,N] × List Pk[F,N] →₀ 𝒮) (f : Pk[F,N] × List Pk[F,N] → Pk[F,N] × List Pk[F,N] →₀ 𝒮) : (m.to𝒲.bind fun (h : Pk[F,N] × List Pk[F,N]) => (f h).to𝒲) = (m.bind f).to𝒲

theorem 𝒲.η_bind {𝒮 : Type} [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [Semiring 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [DecidableEq 𝒮] {F : Type} [Listed F] [DecidableEq F] {N : Type} [DecidableEq N] [Listed N] (x : Pk[F,N] × List Pk[F,N]) (f : Pk[F,N] × List Pk[F,N] → Pk[F,N] × List Pk[F,N] →c 𝒮) : (WeightedNetKAT.η x).bind f = { toFun := fun (h : Pk[F,N] × List Pk[F,N]) => (WeightedNetKAT.η x) x * (f x) h, countable := ⋯ }

theorem WeightedNetKAT.Pred.compute_eq_sem_n {𝒮 : Type} [Semiring 𝒮] [DecidableEq 𝒮] {F : Type} [Listed F] [DecidableEq F] {N : Type} [DecidableEq N] (p : Pred[F,N]) : p.sem = fun (h : Pk[F,N] × List Pk[F,N]) => (p.compute h).to𝒲

theorem WeightedNetKAT.Pol.compute_eq_sem_n {𝒮 : Type} [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [Semiring 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [DecidableEq 𝒮] {F : Type} [Listed F] [DecidableEq F] {N : Type} [DecidableEq N] [Listed N] (p : Pol[F,N,𝒮]) (n : ℕ) : p.sem_n n = fun (h : Pk[F,N] × List Pk[F,N]) => (p.compute n h).to𝒲