Library RelationAlgebra.kat

kat: Kleene algebra with tests

We define here the class of Kleene algebra with tests, as a two sorted structure

Require Export kleene.
Set Implicit Arguments.

KAT operations

A Kleene algebra with tests is composed of a Kleene algebra (kar, i.e., (X,dot,pls,one,zer,str)), a Boolean algebra of tests (tst, i.e., (T,cap,cup,top,bot,neg)), and an injection from tests to Kleene elements.

Since we work with typed structures, the Kleene algebra is a category, and we actually have a family of Boolean algebras, for each square homset (X n n).

Class ops := mk_ops {
  kar: monoid.ops;
  tst: ob kar → lattice.ops;
  inj: ∀ {n}, tst n → kar n n
}.
Coercion kar : ops >-> monoid.ops.

we use [p] to denote the injection of the test p into the Kleene algebra

Notation " [ p ] " := (inj p): ra_terms.

KAT laws

The Kleene algebra should be a Kleene algebra (with bottom element), the Boolean algebras should be a Boolean lattice, and the injection should be a morphism of idempotent semirings, i.e, map (leq,weq,cap,cup,top,bot) into (leq,weq,dot,pls,one,zer)

Class laws (X: ops) := {
  kar_BKA:> monoid.laws BKA kar;
  tst_BL:> ∀ n, lattice.laws BL (tst n);
  mor_inj: ∀ n, morphism BSL (@inj X n);
  inj_top: ∀ n, [top ] ≡ one n;
  inj_cap: ∀ n (p q: tst n), [p ⊓ q ] ≡ [p ] ⋅ [q ]
}.

Basic properties of KAT

Section s.
Context `{L: laws}.
Variable n: ob X.

Global Instance inj_leq: Proper (leq ==> leq) (@inj X n).
Proof. apply mor_inj. Qed.

Global Instance inj_weq: Proper (weq ==> weq) (@inj X n).
Proof. apply mor_inj. Qed.

Lemma inj_bot: [bot ] ≡ zer n n.
Proof. now apply mor_inj. Qed.

Lemma inj_cup (p q: tst n): [p ⊔ q ] ≡ [p ] + [q ].
Proof. now apply mor_inj. Qed.

Lemma str_inj (p: tst n): [p ]^* ≡ 1.
Proof. apply antisym. now rewrite leq_xt, inj_top, str1. apply str_refl. Qed.

End s.

dual KAT, for duality reasoning

Definition dual (X: ops) := {|
  kar := dual kar;
  tst := tst;
  inj := @inj X |}.

Lemma dual_laws X (L: laws X): laws (dual X).
Proof.
  constructor; try apply L.
  apply dual_laws, kar_BKA.
  intros. simpl in ×.
  rewrite capC. apply inj_cap.
Qed.

Lemma dualize {P: ops → Prop} (L: ∀ X, laws X → P X) {X} {H: laws X}: P (dual X).
Proof. eapply L. now apply dual_laws. Qed.

Ltac dual x := apply (dualize x).