WeightedNetKAT.Reduction

source

theorem Finset.filterMap_insert {α β : Type} [DecidableEq α] [DecidableEq β] (f : α → Option β) (hf : ∀ (a a' : α), ∀ b ∈ f a, b ∈ f a' → a = a') (a : α) (s : Finset α) :

filterMap f (insert a s) hf = match f a with | some x => insert x (filterMap f s hf) | none => filterMap f s hf

source

theorem Finset.sum_filterMap {ι κ M : Type} [AddCommMonoid M] [DecidableEq ι] [DecidableEq κ] (s : Finset ι) (e : ι → Option κ) (he : ∀ (a a' : ι), ∀ b ∈ e a, b ∈ e a' → a = a') (f : κ → M) :

∑ x ∈ filterMap e s he, f x = ∑ x ∈ s, match e x with | some y => f y | none => 0

source

@[implicit_reducible]

instance WeightedNetKAT.instOneCountsuppOfCountable {𝒮 : Type} [Semiring 𝒮] {X : Type} [Countable X] :

One (X →c 𝒮)

Equations

WeightedNetKAT.instOneCountsuppOfCountable = { one := { toFun := 1, countable := ⋯ } }

source

@[simp]

theorem WeightedNetKAT.Countsupp.one_apply {𝒮 : Type} [Semiring 𝒮] {X : Type} [Countable X] {x : X} :

1 x = 1

source

@[simp]

theorem WeightedNetKAT.Countsupp.zero_bind {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] {X : Type} [Countable X] [Encodable X] {g : X → X →c 𝒮} :

Countsupp.bind 0 g = 0

source

@[simp]

theorem WeightedNetKAT.Countsupp.one_bind {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] {X : Type} [Countable X] [Encodable X] {g : X → X →c 𝒮} :

Countsupp.bind 1 g = ω∑ (x : X), g x

source

@[irreducible]

noncomputable def WeightedNetKAT.RPol.sem {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] {F : Type} [DecidableEq F] [Listed F] {N : Type} [DecidableEq N] (p : RPol 𝒮) :

Pk[F,N] × List Pk[F,N] → Pk[F,N] × List Pk[F,N] →c 𝒮

Equations

WeightedNetKAT.RPol.Drop.sem = 0
wnk_rpol {skip }.sem = WeightedNetKAT.η
wnk_rpol {@test ~t}.sem = fun (x : Pk[F,N] × List Pk[F,N]) => match x with | (π, h) => if π = t then WeightedNetKAT.η (π, h) else 0
wnk_rpol {@mod ~t}.sem = fun (x : Pk[F,N] × List Pk[F,N]) => match x with | (fst, h) => WeightedNetKAT.η (t, h)
wnk_rpol {dup }.sem = fun (x : Pk[F,N] × List Pk[F,N]) => match x with | (π, h) => WeightedNetKAT.η (π, π :: h)
wnk_rpol {~p_2; ~q}.sem = fun (h : Pk[F,N] × List Pk[F,N]) => (p_2.sem h).bind q.sem
wnk_rpol {~w ⨀ ~p_2}.sem = fun (h : Pk[F,N] × List Pk[F,N]) => w * p_2.sem h
wnk_rpol {~p_2 ⨁ ~q}.sem = fun (h : Pk[F,N] × List Pk[F,N]) => p_2.sem h + q.sem h
wnk_rpol {~p_2*}.sem = fun (h : Pk[F,N] × List Pk[F,N]) => ω∑ (n : ℕ), (p_2 ^ n).sem h

Instances For

source

theorem WeightedNetKAT.RPol.seq_of_prefix {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] {F : Type} [DecidableEq F] [Listed F] {N : Type} [DecidableEq N] {p : RPol 𝒮} {h₀ h₁ : Pk[F,N] × List Pk[F,N]} (h : (p.sem h₀) h₁ ≠ 0) :

h₀.2 <:+ h₁.2

source

@[implicit_reducible]

instance WeightedNetKAT.RPol.instZero {𝒮 F : Type} [Listed F] {N : Type} :

Zero (RPol 𝒮)

Equations

WeightedNetKAT.RPol.instZero = { zero := WeightedNetKAT.RPol.Drop }

source

@[implicit_reducible]

instance WeightedNetKAT.instAddRPol {𝒮 F : Type} [Listed F] {N : Type} :

Add (RPol 𝒮)

Equations

WeightedNetKAT.instAddRPol = { add := WeightedNetKAT.RPol.Add }

source

@[simp]

theorem WeightedNetKAT.RPol.add_def {𝒮 F : Type} [Listed F] {N : Type} (p q : RPol 𝒮) :

p + q = wnk_rpol {~p ⨁ ~q}

source

@[simp]

theorem WeightedNetKAT.RPol.instAdd_sem {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] {F : Type} [DecidableEq F] [Listed F] {N : Type} [DecidableEq N] (p q : RPol 𝒮) :

(p + q).sem = p.sem + q.sem

source

@[simp]

theorem WeightedNetKAT.RPol.instZero_sem {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] {F : Type} [DecidableEq F] [Listed F] {N : Type} [DecidableEq N] :

sem 0 = 0

source

def WeightedNetKAT.Pol.toRPol {𝒮 F : Type} [DecidableEq F] [Listed F] {N : Type} [DecidableEq N] [Listed N] (p : Pol[F,N,𝒮]) :

RPol 𝒮

Equations

(WeightedNetKAT.Pol.Filter t).toRPol = (Array.filterMap (fun (α : Pk[F,N]) => if t.test α then some wnk_rpol {@test ~α} else none) Listed.array).sum
wnk_pol {~f ← ~n}.toRPol = (Array.map (fun (α : Pk[F,N]) => wnk_rpol {@test ~α; @mod ~α[f ↦ n]}) Listed.array).sum
wnk_pol {dup }.toRPol = wnk_rpol {dup }
wnk_pol {~p_2; ~q}.toRPol = wnk_rpol {~p_2.toRPol; ~q.toRPol}
wnk_pol {~w ⨀ ~p_2}.toRPol = wnk_rpol {~w ⨀ ~p_2.toRPol}
wnk_pol {~p_2 ⨁ ~q}.toRPol = wnk_rpol {~p_2.toRPol ⨁ ~q.toRPol}
wnk_pol {~p_2*}.toRPol = wnk_rpol {~p_2.toRPol*}

Instances For

source

theorem WeightedNetKAT.Pol.filter_toRol_sem_eq_sum {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] {F : Type} [DecidableEq F] [Listed F] {N : Type} [DecidableEq N] [Listed N] (t : Pred[F,N]) :

(Filter t).toRPol.sem = ∑ α : Pk[F,N], if t.test α then wnk_rpol {@test ~α}.sem else 0

source

theorem WeightedNetKAT.Pol.assign_toRol_sem_eq_sum {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] {F : Type} [DecidableEq F] [Listed F] {N : Type} [DecidableEq N] [Listed N] (f : F) (v : N) :

wnk_pol {~f ← ~v}.toRPol.sem = ∑ α : Pk[F,N], wnk_rpol {@test ~α; @mod ~α[f ↦ v]}.sem

source

theorem WeightedNetKAT.Pol.toRol_sem_eq_sem {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] {F : Type} [DecidableEq F] [Listed F] {N : Type} [DecidableEq N] [Listed N] (p : Pol[F,N,𝒮]) :

p.toRPol.sem = p.sem