(**************************************************************************)
(*  This is part of ATBR, it is distributed under the terms of the        *)
(*         GNU Lesser General Public License version 3                    *)
(*              (see file LICENSE for more details)                       *)
(*                                                                        *)
(*       Copyright 2009-2011: Thomas Braibant, Damien Pous.               *)
(**************************************************************************)

Require Import Common.

(* RMK: we do not separate operators (equal) from axioms
   (equal_equivalence) for this base class. This is to be able to add
   reflexivity as a trivial hint, and symmetry as an immediate
   one. This might change in the future, if the semantics of hints for
   lemmas with maximally inserted implicit arguments changes. 
   *)

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

(*Arguments equal : simpl never.*)

Set Implicit Arguments.

Bind Scope A_scope with X.

Section Ops.

  Context (G: Graph).

  Class Monoid_Ops := {
    dot: forall A B C, X A B -> X B C -> X A C;
    one: forall A, X A A
  }.

  Class SemiLattice_Ops := {
    plus: forall A B, X A B -> X A B -> X A B;
    zero: forall A B, X A B;
    leq: forall A B: T, relation (X A B) := fun A B x y => equal A B (plus A B x y) y
  }.

  Class Star_Op := {
    star: forall A, X A A -> X A A
  }.

  Class Converse_Op := {
    conv: forall A B, X A B -> X B A
  }.

End Ops.

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 Implicit Arguments. *)
Unset Strict Implicit.

Section Structures.

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

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

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

  Class IdemSemiRing := {
    ISR_Monoid :> Monoid;
    ISR_SemiLattice :> SemiLattice;
    dot_ann_left: forall A B C (x: X B C), zero A B * x == 0;
    dot_ann_right: forall A B C (x: X C B), x * zero B A == 0;
    dot_distr_left: forall A B C (x y: X A B) (z: X B C), (x+y)*z == x*z + y*z;
    dot_distr_right: forall 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: forall A (a:X A A), 1 + a#*a == a#;
    star_destruct_left: forall A B (a: X A A) (c: X A B), a*c <== c -> a#*c <== c;
    star_destruct_right: forall A B (a: X A A) (c: X B A), c*a <== c -> c*a# <== c
  }.

  (* TODO: introduce an intermediate ConverseMonoid class *)

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

    conv_compat:> forall A B, Proper (equal A B ==> equal B A) (conv A B);
    conv_invol: forall A B (x: X A B), x`` == x;
    conv_dot: forall A B C (x: X A B) (y: X B C), (x*y)` == y`*x`;
    conv_plus: forall A B (x y: X A B), (x+y)` == y`+x`;
    dot_ann_left_c: forall A B C (x: X B C), zero A B * x == 0;
    dot_distr_left_c: forall 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: forall A (a:X A A), 1 + a#*a == a#;
    star_destruct_left_c: forall A B (a: X A A) (c: X A B), a*c <== c -> a#*c <== c
  }.

End Structures.

Arguments Monoid G {Mo}.
Arguments SemiLattice G {SLo}.
Arguments IdemSemiRing G {Mo SLo}, G Mo SLo.
Arguments ConverseIdemSemiRing G {Mo} {SLo} {Co}.
Arguments KleeneAlgebra G {Mo} {SLo} {Ko}.
Arguments ConverseIdemSemiRing G {Mo} {SLo} {Co}.
Arguments ConverseKleeneAlgebra G {Mo} {SLo} {Ko} {Co}.

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

  Program 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
  }.
  Obligation 1.
    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.