A discrete instance (TODO.md, discrete sorts)

The generic development needs a σ-finite reference measure per sort and nothing else, so discrete sorts under counting measure fit as they are: there a density is a probability mass function. This module is a minimal instance with two sorts, int (ℤ) and bool, both under counting measure:

operation	inv = false	inv = true	log-weight
add	x + q	x - q	0
xor	x ^^ q	(itself)	0

and the conditioners mul and parity, which have no semi-inverse. Every leaf is a bijection of a countable type, which preserves counting measure (measurePreserving_count). The examples at the end are integer and binary additive couplings (as in integer discrete flows); their densities are pmfs by Prog.density.

Sorts

inductive RoleFlow.Discrete.DS : Type

The sorts: integers and booleans, each under counting measure.

• int : DS
• bool : DS

@[implicit_reducible]

instance RoleFlow.Discrete.instDecidableEqDS : DecidableEq DS

Equations

• RoleFlow.Discrete.instDecidableEqDS x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def RoleFlow.Discrete.instReprDS.repr : DS → ℕ → Std.Format

Equations

• RoleFlow.Discrete.instReprDS.repr RoleFlow.Discrete.DS.int prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "RoleFlow.Discrete.DS.int")).group prec✝
• RoleFlow.Discrete.instReprDS.repr RoleFlow.Discrete.DS.bool prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "RoleFlow.Discrete.DS.bool")).group prec✝

@[implicit_reducible]

instance RoleFlow.Discrete.instReprDS : Repr DS

Equations

• RoleFlow.Discrete.instReprDS = { reprPrec := RoleFlow.Discrete.instReprDS.repr }

@[reducible, inline]

abbrev RoleFlow.Discrete.DS.X : DS → Type

The space of a sort.

Equations

• RoleFlow.Discrete.DS.int.X = ℤ
• RoleFlow.Discrete.DS.bool.X = Bool

@[implicit_reducible]

instance RoleFlow.Discrete.instMeasurableSpaceX (s : DS) : MeasurableSpace s.X

Equations

• RoleFlow.Discrete.instMeasurableSpaceX s = ⊤

instance RoleFlow.Discrete.instMeasurableSingletonClassX (s : DS) : MeasurableSingletonClass s.X

instance RoleFlow.Discrete.instCountableX (s : DS) : Countable s.X

@[implicit_reducible]

noncomputable instance RoleFlow.Discrete.instSortsDS : Sorts DS

Equations

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

instance RoleFlow.Discrete.instMeasurableSingletonClassXDS (s : DS) : MeasurableSingletonClass (X s)

instance RoleFlow.Discrete.instCountableXDS (s : DS) : Countable (X s)

theorem RoleFlow.Discrete.measurePreserving_count {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] (e : α ≃ α) (he : Measurable ⇑e) : MeasureTheory.MeasurePreserving (⇑e) MeasureTheory.Measure.count MeasureTheory.Measure.count

A bijection of a countable type preserves counting measure.

Operations

inductive RoleFlow.Discrete.DOp : List DS → List DS → Type

• add (inv : Bool := false) : DOp [DS.int, DS.int] [DS.int]

  x + q; x - q if inv.

• xor : DOp [DS.bool, DS.bool] [DS.bool]

  x ^^ q, its own semi-inverse.

• mul : DOp [DS.int, DS.int] [DS.int]
• parity : DOp [DS.int] [DS.bool]

@[reducible, inline]

abbrev RoleFlow.Discrete.si1 {a b c : DS} (o : DOp [c, b] [a]) : SemiInv DOp [a, b] [c]

A semi-inverse solving the first argument from the result and the second argument.

Equations

• RoleFlow.Discrete.si1 o = { cs := [a], ps := [b], split := ⋯, cs_ne := ⋯, op := o }

def RoleFlow.Discrete.DOp.inv {as bs : List DS} : DOp as bs → Option (SemiInv DOp as bs)

Equations

• (RoleFlow.Discrete.DOp.add inv).inv = some (RoleFlow.Discrete.si1 (RoleFlow.Discrete.DOp.add !inv))
• RoleFlow.Discrete.DOp.xor.inv = some (RoleFlow.Discrete.si1 RoleFlow.Discrete.DOp.xor)
• x✝.inv = none

def RoleFlow.Discrete.discSig : Sig DS

Equations

• RoleFlow.Discrete.discSig = { Op := RoleFlow.Discrete.DOp, bs_ne := @RoleFlow.Discrete.discSig._proof_1, inv := fun {as bs : List RoleFlow.Discrete.DS} => RoleFlow.Discrete.DOp.inv }

The model

@[reducible, inline]

noncomputable abbrev RoleFlow.Discrete.one {a : DS} (x : X a) : Val [a]

Equations

• RoleFlow.Discrete.one x = RoleFlow.Val.cons x RoleFlow.Val.nil

def RoleFlow.Discrete.toZ (x : X DS.int) : ℤ

The integer operations, at the type of the sort.

Equations

• RoleFlow.Discrete.toZ x = x

def RoleFlow.Discrete.toB (x : X DS.bool) : Bool

Equations

• RoleFlow.Discrete.toB x = x

def RoleFlow.Discrete.zadd (x q : X DS.int) : X DS.int

Equations

• RoleFlow.Discrete.zadd x q = RoleFlow.Discrete.toZ x + RoleFlow.Discrete.toZ q

def RoleFlow.Discrete.zsub (x q : X DS.int) : X DS.int

Equations

• RoleFlow.Discrete.zsub x q = RoleFlow.Discrete.toZ x - RoleFlow.Discrete.toZ q

def RoleFlow.Discrete.zmul (x q : X DS.int) : X DS.int

Equations

• RoleFlow.Discrete.zmul x q = RoleFlow.Discrete.toZ x * RoleFlow.Discrete.toZ q

def RoleFlow.Discrete.bxor (x q : X DS.bool) : X DS.bool

Equations

• RoleFlow.Discrete.bxor x q = (RoleFlow.Discrete.toB x ^^ RoleFlow.Discrete.toB q)

def RoleFlow.Discrete.zpar (x : X DS.int) : X DS.bool

Equations

• RoleFlow.Discrete.zpar x = decide (RoleFlow.Discrete.toZ x % 2 = 1)

noncomputable def RoleFlow.Discrete.semOp {as bs : List DS} : DOp as bs → Val as → Val bs

Equations

• One or more equations did not get rendered due to their size.
• RoleFlow.Discrete.semOp RoleFlow.Discrete.DOp.parity = fun (v : RoleFlow.Val [RoleFlow.Discrete.DS.int]) => RoleFlow.Discrete.one (RoleFlow.Discrete.zpar v.head)

theorem RoleFlow.Discrete.measurable_val {Γ : List DS} {Y : Type u_1} [MeasurableSpace Y] (f : Val Γ → Y) : Measurable f

On a discrete sort, a measurable map is any map.

theorem RoleFlow.Discrete.eq_one {a : DS} (v : Val [a]) : one v.head = v

theorem RoleFlow.Discrete.left1 {a b c : DS} {o : DOp [a, b] [c]} {o' : DOp [c, b] [a]} (F : X a → X b → X c) (G : X c → X b → X a) (hF : ∀ (v : Val [a, b]), semOp o v = one (F v.head v.tail.head)) (hG : ∀ (v : Val [c, b]), semOp o' v = one (G v.head v.tail.head)) (h : ∀ (x : X a) (q : X b), G (F x q) q = x) (c✝ : Val (si1 o').cs) (p : Val (si1 o').ps) : semOp (si1 o').op ((semOp o ((si1 o').glue c✝ p)).append p) = c✝

The left law of an operation that consumes its first argument.

theorem RoleFlow.Discrete.leaf1 {a b : DS} {o : DOp [a, b] [a]} (F : X a → X b → X a) (hF : ∀ (v : Val [a, b]), semOp o v = one (F v.head v.tail.head)) (e : X b → X a ≃ X a) (he : ∀ (q : X b) (x : X a), (e q) x = F x q) (p : Val [b]) : Cov (vol [a]) (vol [a]) (fun (c : Val [a]) => semOp o (Val.cast ⋯ (c.append p))) fun (x : Val [a]) => expw 0

A leaf of weight 1 from a bijection of the consumed argument at each parameter.

@[reducible, inline]

abbrev RoleFlow.Discrete.LeftLaw {as bs : List DS} (o : DOp as bs) (si : SemiInv DOp as bs) : Prop

The left law of o with the semi-inverse si.

Equations

• RoleFlow.Discrete.LeftLaw o si = ∀ (c : RoleFlow.Val si.cs) (p : RoleFlow.Val si.ps), RoleFlow.Discrete.semOp si.op ((RoleFlow.Discrete.semOp o (si.glue c p)).append p) = c

theorem RoleFlow.Discrete.left_add (inv : Bool) : LeftLaw (DOp.add inv) (si1 (DOp.add !inv))

theorem RoleFlow.Discrete.left_xor : LeftLaw DOp.xor (si1 DOp.xor)

def RoleFlow.Discrete.xorEquiv (q : X DS.bool) : X DS.bool ≃ X DS.bool

· ^^ q as a bijection.

Equations

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

noncomputable def RoleFlow.Discrete.discModel : ModelInv discSig

Equations

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

Examples

def RoleFlow.Discrete.ln {as bs : List DS} (o : DOp as bs) (args : List ℕ) : Line discSig

Equations

• RoleFlow.Discrete.ln o args = { as := as, bs := bs, op := o, args := args }

def RoleFlow.Discrete.intCoupling : Prog discSig

Integer additive coupling: θ : int (0), x₁ x₂ : int (1, 2); t = mul(θ, x₁) (3), y = add(x₂, t) (4); returns (x₁, y).

Equations

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

def RoleFlow.Discrete.boolCoupling : Prog discSig

Binary coupling across sorts: x : int (0), b : bool (1); p = parity(x) (2), c = xor(b, p) (3); returns (x, c).

Equations

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

theorem RoleFlow.Discrete.intCoupling_typed : intCoupling.Typed [Role.cond, Role.spine]

theorem RoleFlow.Discrete.boolCoupling_typed : boolCoupling.Typed [Role.cond, Role.spine]