# Library RelationAlgebra.kat

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

# KAT operations

Class ops := mk_ops {

kar: monoid.ops;

tst: ob kar → lattice.ops;

inj: ∀ {n}, tst n → kar n n

}.

Coercion kar: ops >-> monoid.ops.

kar: monoid.ops;

tst: ob kar → lattice.ops;

inj: ∀ {n}, tst n → kar n n

}.

Coercion kar: ops >-> monoid.ops.

# KAT laws

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]

}.

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.

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).