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