Library ATBR.MxFunctors

Require Import Common.
Require Import Classes.
Require Import Monoid.
Require Import SemiLattice.
Require Import SemiRing.
Require Import KleeneAlgebra.
Require Import MxGraph.
Require Import MxSemiLattice.
Require Import MxSemiRing.
Require Import MxKleeneAlgebra.

Require Import Functors.


Transparent equal.

Section Defs.

  Context {G1: Graph} {G2: Graph}
  {SLo1: SemiLattice_Ops G1} {SLo2: SemiLattice_Ops G2}
  {Mo1: Monoid_Ops G1} {Mo2: Monoid_Ops G2}
  {So1: Star_Op G1} {So2: Star_Op G2}.

  Variable F: functor G1 G2.
  Variable A: @T G1.

  Notation MG1 := (@mx_Graph G1 A).
  Notation MG2 := (@mx_Graph G2 (fT F A)).

  Definition mxF: functor MG1 MG2 :=
    @Build_functor MG1 MG2
    (fun n => n)
    (fun n m M => box n m (fun i j => F _ _ (!M i j))).

  Global Instance mxgraph_functor {HF: graph_functor F}: graph_functor mxF.

  Global Instance mxsemilattice_functor {HF: semilattice_functor F}: semilattice_functor mxF.

  Global Instance mxsemiring_functor {SL1: SemiLattice G1} {SL2: SemiLattice G2}
    {HF: semiring_functor F}: semiring_functor mxF.

  Lemma functor_mx_blocks:
    forall x y n m a b c d,
      mxF _ _ (@mx_blocks _ A x y n m a b c d) ==
      mx_blocks (mxF _ _ a) (mxF _ _ b) (mxF _ _ c) (mxF _ _ d).

  Lemma functor_mx_sub:
    forall n' m' x y n m M,
      mxF _ _ (@mx_sub _ A n' m' x y n m M) =
      mx_sub x y n m (mxF _ _ M).

  Lemma functor_mx_of_scal:
    forall a,
      mxF _ _ (mx_of_scal a) =
      mx_of_scal (F _ _ a).

  Lemma functor_mx_to_scal:
    forall M,
      F _ _ (mx_to_scal M) =
      mx_to_scal (mxF _ _ M).

  Global Instance mxkleene_functor {KA1: KleeneAlgebra G1} {KA2: KleeneAlgebra G2}
    {HF: kleene_functor F}: kleene_functor mxF.

End Defs.