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 \cap 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 \cup 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).
  constructor; try apply L.
  apply dual_laws, kar_BKA.
  intros. simpl in ×.
  rewrite capC. apply inj_cap.

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