PDL programs form a Kleene Algebra

This file provides RelProp.kleeneAlgebra. It shows that the semantic quotient of PDL Programs as RelProps forms a KleeneAlgebra.

instance instKStarProgram : KStar Program

Equations

• instKStarProgram = { kstar := fun (α : Program) => ∗α }

instance instKStarRelProp : KStar RelProp

Equations

• instKStarRelProp = { kstar := RelProp.star }

instance instAddRelProp : Add RelProp

Equations

• instAddRelProp = { add := RelProp.union }

instance instAddSemigroupRelProp : AddSemigroup RelProp

Equations

• instAddSemigroupRelProp = { toAdd := instAddRelProp, add_assoc := instAddSemigroupRelProp._proof_2 }

instance instZeroRelProp : Zero RelProp

Equations

• instZeroRelProp = { zero := ⟦?'⊥⟧ }

instance instAddZeroClassRelProp : AddZeroClass RelProp

Equations

• instAddZeroClassRelProp = { toZero := instZeroRelProp, toAdd := instAddRelProp, zero_add := instAddZeroClassRelProp._proof_3, add_zero := instAddZeroClassRelProp._proof_4 }

def Program.Repeat : ℕ → Program → Program

Equations

• Program.Repeat 0 x✝ = (?'⊥)
• Program.Repeat n.succ x✝ = (x✝;'Program.Repeat n x✝)

def RelProp.Repeat : ℕ → RelProp → RelProp

Equations

• RelProp.Repeat 0 x✝ = 0
• RelProp.Repeat n.succ x✝ = RelProp.Repeat n x✝ + x✝

instance RelProp.addMonoid : AddMonoid RelProp

Equations

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

instance RelProp.mul : Mul RelProp

Equations

• RelProp.mul = { mul := RelProp.sequence }

instance instMulZeroClassRelProp : MulZeroClass RelProp

Equations

• instMulZeroClassRelProp = { toMul := RelProp.mul, toZero := instZeroRelProp, zero_mul := instMulZeroClassRelProp._proof_7, mul_zero := instMulZeroClassRelProp._proof_8 }

instance instDistribRelProp : Distrib RelProp

Equations

• instDistribRelProp = { toMul := RelProp.mul, toAdd := instAddRelProp, left_distrib := instDistribRelProp._proof_9, right_distrib := instDistribRelProp._proof_10 }

instance instAddCommMonoidRelProp : AddCommMonoid RelProp

Equations

• instAddCommMonoidRelProp = { toAddMonoid := RelProp.addMonoid, add_comm := instAddCommMonoidRelProp._proof_11 }

instance instNonUnitalNonAssocSemiringRelProp : NonUnitalNonAssocSemiring RelProp

Equations

• instNonUnitalNonAssocSemiringRelProp = { toAddCommMonoid := instAddCommMonoidRelProp, toMul := RelProp.mul, left_distrib := ⋯, right_distrib := ⋯, zero_mul := ⋯, mul_zero := ⋯ }

instance instNonUnitalSemiringRelProp : NonUnitalSemiring RelProp

Equations

• instNonUnitalSemiringRelProp = { toNonUnitalNonAssocSemiring := instNonUnitalNonAssocSemiringRelProp, mul_assoc := instNonUnitalSemiringRelProp._proof_12 }

instance RelProp.instOne : One RelProp

Equations

• RelProp.instOne = { one := ⟦?'⊤⟧ }

instance RelProp.semiring : Semiring RelProp

Equations

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

def relImp (α β : Program) : Prop

Equations

• relImp α β = ∀ (W : Type) (M : KripkeModel W) (v w : W), relate M α v w → relate M β v w

def relImp_strict (α β : Program) : Prop

Equations

• relImp_strict α β = ((∀ (W : Type) (M : KripkeModel W) (v w : W), relate M α v w → relate M β v w) ∧ ¬∀ (W : Type) (M : KripkeModel W) (v w : W), relate M β v w → relate M α v w)

def RelProp.le : RelProp → RelProp → Prop

Equations

• RelProp.le = Quotient.lift₂ relImp RelProp.le._proof_21

def RelProp.lt : RelProp → RelProp → Prop

Equations

• RelProp.lt = Quotient.lift₂ relImp_strict RelProp.lt._proof_22

instance RelProp.instLE : LE RelProp

Equations

• RelProp.instLE = { le := RelProp.le }

instance RelProp.instPreorder : Preorder RelProp

Equations

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

instance RelProp.partialOrder : PartialOrder RelProp

Equations

• RelProp.partialOrder = { toPreorder := RelProp.instPreorder, le_antisymm := RelProp.partialOrder._proof_26 }

instance RelProp.semilatticeSup : SemilatticeSup RelProp

Equations

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

instance RelProp.idemSemiring : IdemSemiring RelProp

Equations

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

instance RelProp.kleeneAlgebra : KleeneAlgebra RelProp

Equations

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