Require Import Common.
Require Import Classes.
Require Import DecideKleeneAlgebra.
Set Implicit Arguments.
Unset Printing Implicit Defensive.

Bind Scope SA_scope with X.

Class SKA_Ops (G: Graph) := {
  dot: ∀ A B C, X A B → X B C → X A C;
  one: ∀ A, X A A;
  plus: ∀ A B, X A B → X A B → X A B;
  star: ∀ A, X A A → X A A;
  leq: ∀ 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:>
    ∀ A B C, Proper (equal A B ==> equal B C ==> equal A C) (dot A B C);
  plus_compat:>
    ∀ A B, Proper (equal A B ==> equal A B ==> equal A B) (plus A B);
  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 A B), x×1 == 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;
  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;
  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 <== c → a#×c <== c;
  star_destruct_right: ∀ 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: ∀ x y, R x y → oequal (Some x) (Some y)
  | oe_none: oequal None None.
  Hypothesis HR: Equivalence R.
  Lemma oequal_equivalence: Equivalence oequal.
  Proof.
    constructor.
     intros [x|]; constructor. reflexivity.
     intros x y [x' y' H|]; constructor. symmetry. assumption.
     intros x y z [x' y' H|] H'; trivial.
      inversion_clear H'. constructor. rewrite H. assumption.
  Qed.
End oe.

Unset Strict Implicit.

Section F.
  Context G Ops `{@StrictKleeneAlgebra G Ops}.

  Instance oGraph: Graph := {
    T := T;
    X A B := option (X A B);
    equal A B := oequal (equal A B)
  }.
  Proof.
    intros. apply oequal_equivalence, G.
  Defined.

  Definition inj A B (x: @X G A B): @X oGraph A B := Some x.
  Lemma faithful: ∀ A B (x y: X A B), inj x == inj y → x == y.
  Proof.
    intros A B x y Hxy. inversion_clear Hxy. assumption.
  Qed.

  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.
  Proof.
    constructor; intros.
     intros _ _ [x x' Hx|] _ _ [y y' Hy|]; simpl; constructor.
      apply dot_compat; assumption.
     destruct x; try constructor.
      destruct y; try constructor.
       destruct z; constructor. apply dot_assoc.
     destruct x; simpl; constructor. apply dot_neutral_left.
     destruct x; simpl; constructor. apply dot_neutral_right.
  Qed.

  Instance oSemiLattice: SemiLattice oGraph.
  Proof.
    constructor; intros.
     intros _ _ [x x' Hx|] _ _ [y y' Hy|]; simpl; constructor; trivial.
      apply plus_compat; assumption.
     destruct x; simpl; constructor. reflexivity.
     destruct x; simpl; constructor. apply plus_idem.
     destruct x; destruct y; destruct z; simpl; constructor; try reflexivity.
      apply plus_assoc.
     destruct x; destruct y; simpl; constructor; try reflexivity.
      apply plus_com.
  Qed.

  Instance oIdemSemiRing: IdemSemiRing oGraph.
  Proof.
    constructor; eauto with typeclass_instances; intros.
     destruct x; reflexivity.
     destruct x; destruct y; destruct z; simpl; constructor; try reflexivity.
      apply dot_distr_left.
     destruct x; destruct y; destruct z; simpl; constructor; try reflexivity.
      apply dot_distr_right.
  Qed.

  Global Instance oKleeneAlgebra: KleeneAlgebra oGraph.
  Proof.
    constructor; eauto with typeclass_instances.
     intros A [a|]; simpl; constructor; try reflexivity.
      apply star_make_left.
     intros A B [a|] [c|] Hac; simpl in *; try constructor.
      apply star_destruct_left. inversion_clear Hac. assumption.
      rewrite dot_neutral_left. apply plus_idem.
     intros A B [a|] [c|] Hac; simpl in *; try constructor.
      apply star_destruct_right. inversion_clear Hac. assumption.
      rewrite dot_neutral_right. apply plus_idem.
  Qed.
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.