Library ATBR.StrictKleeneAlgebra

Require Import Common.
Require Import Classes.
Require Import DecideKleeneAlgebra.

Class SKA_Ops (G: Graph) := {
  dot: forall A B C, X A B -> X B C -> X A C;
  one: forall A, X A A;
  plus: forall A B, X A B -> X A B -> X A B;
  star: forall A, X A A -> X A A;
  leq: forall A B: T, relation (X A B) := fun A B x y => equal A B (plus A B x y) y
}.

Notation "x == y" := (equal _ _ x y) (at level 70): SA_scope.
Notation "x <== y" := (leq _ _ x y) (at level 70): SA_scope.
Notation "x * y" := (dot _ _ _ x y) (at level 40, left associativity): SA_scope.
Notation "x + y" := (plus _ _ x y) (at level 50, left associativity): SA_scope.
Notation "x #" := (star _ x) (at level 15, left associativity): SA_scope.
Notation "1" := (one _): SA_scope.

Close Scope A_scope.
Open Scope SA_scope.
Delimit Scope SA_scope with SA.

Class StrictKleeneAlgebra {G: Graph} {Ops: SKA_Ops G} := {
  dot_compat:>
    forall A B C, Proper (equal A B ==> equal B C ==> equal A C) (dot A B C);
  plus_compat:>
    forall A B, Proper (equal A B ==> equal A B ==> equal A B) (plus A B);
  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 A B), x*1 == 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;
  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;
  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
}.
Implicit Arguments StrictKleeneAlgebra [[Ops]].

Section oe.
  Variable A: Type.
  Variable R: relation A.
  Inductive oequal: relation (option A) :=
  | oe_some: forall x y, R x y -> oequal (Some x) (Some y)
  | oe_none: oequal None None.
  Hypothesis HR: Equivalence R.
  Lemma oequal_equivalence: Equivalence oequal.
End oe.

Section F.
  Context `{StrictKleeneAlgebra}.

  Instance oGraph: Graph := {
    T := T;
    X A B := option (X A B);
    equal A B := oequal (equal A B)
  }.

  Definition inj A B (x: X A B): @X oGraph A B := Some x.
  Lemma faithful: forall A B (x y: X A B), inj x == inj y -> x == y.

  Global Instance oMonoid_Ops: Monoid_Ops oGraph := {
    dot A B C x y :=
      match x,y with
        | Some x, Some y => Some (x*y)
        | _,_ => None
      end;
    one A := Some 1
  }.

  Global Instance oSemiLattice_Ops: SemiLattice_Ops oGraph := {
    plus A B x y :=
      match x,y with
        | None,y => y
        | x,None => x
        | Some x, Some y => Some (x+y)
      end;
    zero A B := None
  }.

  Global Instance oStar_Op: Star_Op oGraph := {
    star A x :=
      match x with
        | None => Some 1
        | Some x => Some (x#)
      end
  }.

  Instance oMonoid: Monoid oGraph.

  Instance oSemiLattice: SemiLattice oGraph.

  Instance oIdemSemiRing: IdemSemiRing oGraph.

  Global Instance oKleeneAlgebra: KleeneAlgebra oGraph.
End F.

Ltac skleene_reflexivity :=
  
  let rec parse t :=
    match t with
      | @dot ?G ?O ?A ?B ?C ?x ?y =>
        let x := parse x in
        let y := parse y in
          constr:(@Classes.dot (@oGraph G) (@oMonoid_Ops G O) A B C x y)
      | @one ?G ?O ?A =>
          constr:(@Classes.one (@oGraph G) (@oMonoid_Ops G O) A)
      | @plus ?G ?O ?A ?B ?x ?y =>
        let x := parse x in
        let y := parse y in
          constr:(@Classes.plus (@oGraph G) (@oSemiLattice_Ops G O) A B x y)
      | @star ?G ?O ?A ?x =>
        let x := parse x in
          constr:(@Classes.star (@oGraph G) (@oStar_Op G O) A x)
      | _ => constr:(inj t)
    end
  in
  unfold leq;
  lazymatch goal with
    | |- @equal ?G ?A ?B ?x ?y =>
      let x := parse x in
      let y := parse y in
        apply faithful; change (@equal (@oGraph G) A B x y); kleene_reflexivity
  end.