# Library ATBR.Classes

This module defines all classes of our algebraic hierarchy

Require Import Common.

# Graph : base class of the hierarchy

a multigraph with indexed equalities on vertices.

Class Graph := {
T: Type;
X: TTType;
equal: A B, relation (X A B);
equal_:> A B, Equivalence (equal A B)
}.
Global Opaque equal.

Set Implicit Arguments.

Bind Scope A_scope with X.

Section Ops.

# Operations

All operations are parametrised by the Graph base-class
Context (G: Graph).

Class Monoid_Ops := {
dot: A B C, X A BX B CX A C;
one: A, X A A
}.

Class SemiLattice_Ops := {
plus: A B, X A BX A BX A B;
zero: A B, X A B;
leq: A B: T, relation (X A B) := fun A B x yequal A B (plus A B x y) y
}.

Class Star_Op := {
star: A, X A AX A A
}.

Class Converse_Op := {
conv: A B, X A BX B A
}.

End Ops.

Notations for operations
Notation "x == y" := (equal _ _ x y) (at level 70): A_scope.
Notation "x <== y" := (leq _ _ x y) (at level 70): A_scope.
Notation "x * y" := (dot _ _ _ x y) (at level 40, left associativity): A_scope.
Notation "x + y" := (plus _ _ x y) (at level 50, left associativity): A_scope.
Notation "x #" := (star _ x) (at level 15, left associativity): A_scope.
Notation "x `" := (conv _ _ x) (at level 15, left associativity): A_scope.
Notation "1" := (one _): A_scope.
Notation "0" := (zero _ _): A_scope.

Open Scope A_scope.
Delimit Scope A_scope with A.

Unset Strict Implicit.

Section Structures.

# Structures

All structures are parametrised by both the Graph base-class and the corresponding operations.

Context {G: Graph}.
Context {Mo: Monoid_Ops G} {SLo: SemiLattice_Ops G} {Ko: Star_Op G} {Co: Converse_Op G}.

Class Monoid := {
dot_compat:> A B C, Proper (equal A B ==> equal B C ==> equal A C) (dot A B C);
dot_assoc: A B C D (x: X A B) y (z: X C D), x*(y×z) == (x×y)*z;
dot_neutral_left: A B (x: X A B), 1×x == x;
dot_neutral_right: A B (x: X B A), x×1 == x
}.

Class SemiLattice := {
plus_compat:> A B, Proper (equal A B ==> equal A B ==> equal A B) (plus A B);
plus_neutral_left: A B (x: X A B), 0+x == x;
plus_idem: A B (x: X A B), x+x == x;
plus_assoc: A B (x y z: X A B), x+(y+z) == (x+y)+z;
plus_com: A B (x y: X A B), x+y == y+x
}.

Class IdemSemiRing := {
ISR_Monoid :> Monoid;
ISR_SemiLattice :> SemiLattice;
dot_ann_left: A B C (x: X B C), zero A B × x == 0;
dot_ann_right: A B C (x: X C B), x × zero B A == 0;
dot_distr_left: A B C (x y: X A B) (z: X B C), (x+y)*z == x×z + y×z;
dot_distr_right: A B C (x y: X B A) (z: X C B), z*(x+y) == z×x + z×y
}.

Class KleeneAlgebra := {
KA_ISR :> IdemSemiRing;
star_make_left: A (a:X A A), 1 + a#×a == a#;
star_destruct_left: A B (a: X A A) (c: X A B), a×c <== ca#×c <== c;
star_destruct_right: A B (a: X A A) (c: X B A), c×a <== cc×a# <== c
}.

Once we add the converse operation, we no longer need some axioms from Monoid/SemiRing/KA. This is why we do not use direct inheritance

Class ConverseIdemSemiRing := {
CISR_SL :> SemiLattice;
dot_compat_c: A B C, Proper (equal A B ==> equal B C ==> equal A C) (dot A B C);
dot_assoc_c: A B C D (x: X A B) y (z: X C D), x*(y×z) == (x×y)*z;
dot_neutral_left_c: A B (x: X A B), 1×x == x;

conv_compat:> A B, Proper (equal A B ==> equal B A) (conv A B);
conv_invol: A B (x: X A B), x`` == x;
conv_dot: A B C (x: X A B) (y: X B C), (x×y)` == y`×x`;
conv_plus: A B (x y: X A B), (x+y)` == y`+x`;
dot_ann_left_c: A B C (x: X B C), zero A B × x == 0;
dot_distr_left_c: A B C (x y: X A B) (z: X B C), (x+y)*z == x×z + y×z
}.

Class ConverseKleeneAlgebra := {
CKA_CISR :> ConverseIdemSemiRing;
star_make_left_c: A (a:X A A), 1 + a#×a == a#;
star_destruct_left_c: A B (a: X A A) (c: X A B), a×c <== ca#×c <== c
}.

End Structures.

we want to keep the graph explicit, for better readability, (but we still want the graph to be maximally implicit in projections like dot_assoc.
Implicit Arguments Monoid [[Mo]].
Implicit Arguments SemiLattice [[SLo]].
Implicit Arguments IdemSemiRing [[Mo] [SLo]].
Implicit Arguments ConverseIdemSemiRing [[Mo] [SLo] [Co]].
Implicit Arguments KleeneAlgebra [[Mo] [SLo] [Ko]].
Implicit Arguments ConverseIdemSemiRing [[Mo] [SLo] [Co]].
Implicit Arguments ConverseKleeneAlgebra [[Mo] [SLo] [Co] [Ko]].

# Dual structures

These structures are obtained by reversing all arrows; they make it possible to factorise several proofs, by symmetry.

Module Dual. Section Protect.

Local Transparent equal.

Context (G: Graph).
Context {Mo: Monoid_Ops G} {SLo: SemiLattice_Ops G} {Ko: Star_Op G} {Co: Converse_Op G}.

Instance Graph: Graph := {
T := T;
X A B := X B A;
equal A B := equal B A;
equal_ A B := equal_ B A
}.

Instance Monoid_Ops: Monoid_Ops Graph := {
dot A B C x y := @dot _ Mo C B A y x;
one := @one _ Mo
}.

Instance SemiLattice_Ops: SemiLattice_Ops Graph := {
plus A B := @plus _ SLo B A;
zero A B := @zero _ SLo B A
}.

Instance Star_Op: Star_Op Graph := {
star := @star _ Ko
}.

Instance Converse_Op: Converse_Op Graph := {
conv A B := @conv _ Co B A
}.

Instance Monoid {M: Monoid G}: Monoid Graph := {
dot_neutral_left := @dot_neutral_right _ _ M;
dot_neutral_right := @dot_neutral_left _ _ M;
dot_compat A B C x x' Hx y y' Hy := @dot_compat _ _ M C B A _ _ Hy _ _ Hx
}.
Proof.
intros. symmetry. simpl. apply dot_assoc.
Defined.

Instance SemiLattice {SL: SemiLattice G}: SemiLattice Graph := {
plus_com A B := @plus_com _ _ SL B A;
plus_idem A B := @plus_idem _ _ SL B A;
plus_assoc A B := @plus_assoc _ _ SL B A;
plus_compat A B := @plus_compat _ _ SL B A;
plus_neutral_left A B := @plus_neutral_left _ _ SL B A
}.

Instance IdemSemiRing {ISR: IdemSemiRing G}: IdemSemiRing Graph.
Proof.
intros.
constructor.
exact Monoid.
exact SemiLattice.
exact (@dot_ann_right _ _ _ ISR).
exact (@dot_ann_left _ _ _ ISR).
exact (@dot_distr_right _ _ _ ISR).
exact (@dot_distr_left _ _ _ ISR).
Defined.

End Protect. End Dual.