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_reducible]

instance instKStarProgram : KStar Program

Equations

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

@[instance_reducible]

instance instKStarRelProp : KStar RelProp

Equations

• instKStarRelProp = { kstar := RelProp.star }

@[instance_reducible]

instance instAddRelProp : Add RelProp

Equations

• instAddRelProp = { add := RelProp.union }

@[instance_reducible]

instance instAddSemigroupRelProp : AddSemigroup RelProp

Equations

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

@[instance_reducible]

instance instZeroRelProp : Zero RelProp

Equations

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

@[instance_reducible]

instance instAddZeroClassRelProp : AddZeroClass RelProp

Equations

• instAddZeroClassRelProp = { toZero := instZeroRelProp, toAdd := instAddRelProp, zero_add := instAddZeroClassRelProp._proof_1, add_zero := instAddZeroClassRelProp._proof_2 }

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_reducible]

instance RelProp.addMonoid : AddMonoid RelProp

Equations

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

@[instance_reducible]

instance RelProp.mul : Mul RelProp

Equations

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

@[instance_reducible]

instance instMulZeroClassRelProp : MulZeroClass RelProp

Equations

• instMulZeroClassRelProp = { toMul := RelProp.mul, toZero := instZeroRelProp, zero_mul := instMulZeroClassRelProp._proof_1, mul_zero := instMulZeroClassRelProp._proof_2 }

@[instance_reducible]

instance instDistribRelProp : Distrib RelProp

Equations

• instDistribRelProp = { toMul := RelProp.mul, toAdd := instAddRelProp, left_distrib := instDistribRelProp._proof_1, right_distrib := instDistribRelProp._proof_2 }

@[instance_reducible]

instance instAddCommMonoidRelProp : AddCommMonoid RelProp

Equations

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

@[instance_reducible]

instance instNonUnitalNonAssocSemiringRelProp : NonUnitalNonAssocSemiring RelProp

Equations

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

@[instance_reducible]

instance instNonUnitalSemiringRelProp : NonUnitalSemiring RelProp

Equations

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

@[instance_reducible]

instance RelProp.instOne : One RelProp

Equations

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

@[instance_reducible]

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_1

theorem relImp_congr {α₁ β₁ α₂ β₂ : Program} (hα : α₁ ≈ α₂) (hβ : β₁ ≈ β₂) : relImp α₁ β₁ ↔ relImp α₂ β₂

relImp only depends on the equivalence classes of its arguments.

def RelProp.lt : RelProp → RelProp → Prop

Equations

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

@[instance_reducible]

instance RelProp.instLE : LE RelProp

Equations

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

@[instance_reducible]

instance RelProp.instPreorder : Preorder RelProp

Equations

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

@[instance_reducible]

instance RelProp.partialOrder : PartialOrder RelProp

Equations

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

@[instance_reducible]

instance RelProp.semilatticeSup : SemilatticeSup RelProp

Equations

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

@[instance_reducible]

instance RelProp.idemSemiring : IdemSemiring RelProp

Equations

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

@[instance_reducible]

instance RelProp.kleeneAlgebra : KleeneAlgebra RelProp

Equations

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