Library ATBR.MxSemiRing

Require Import Common.
Require Import Classes.
Require Import Graph.
Require Import Monoid.
Require Import SemiLattice.
Require Import SemiRing.
Require Import MxGraph.
Require Import MxSemiLattice.
Require Import BoolView.


Transparent equal.

Section Defs.

  Context `{ISR: IdemSemiRing}.
  Variable A: T.
  Notation MX n m := (MX_ A n m).
  Notation mx_equal n m := (mx_equal_ A n m) (only parsing).

  Definition mx_dot n m p (M: MX n m) (N: MX m p): MX n p :=
    box n p (fun i j => sum 0 m (fun k => !M i k * !N k j)).
  Definition mx_one n: MX n n :=
    box n n (fun i j => if eq_nat_bool i j then 1 else 0).

  Global Instance mx_Monoid_Ops: Monoid_Ops (mx_Graph A) := {
    dot := mx_dot;
    one := mx_one }.

  Definition mx_bool n m (f: nat -> nat -> bool): MX n m :=
    box n m (fun i j => xif (f i j) 1 0).

  Lemma mx_dot_assoc n m p o (M: MX n m) (N: MX m p) (P: MX p o): M*(N*P) == (M*N)*P.

  Lemma mx_dot_neutral_left n m (M: MX n m): 1 * M == M.

  Lemma mx_dot_neutral_right n m (M: MX m n): M * 1 == M.

  Global Instance mx_Monoid: Monoid (mx_Graph A) := {
    dot_assoc := mx_dot_assoc;
    dot_neutral_left := mx_dot_neutral_left;
    dot_neutral_right := mx_dot_neutral_right
  }.

  Global Instance mx_SemiRing: IdemSemiRing (mx_Graph A).

End Defs.

Notation mx_dot_ A := (@dot (mx_Graph A) (mx_Monoid_Ops A)) (only parsing).
Notation mx_one_ A := (@one (mx_Graph A) (mx_Monoid_Ops A)) (only parsing).


Section Props1.

  Context `{M: Monoid}.
  Variable A: T.
  Notation MX n m := (MX_ A n m).
  Notation mx_equal n m := (mx_equal_ A n m) (only parsing).

  Definition dot_scal_right n m (M: MX n m) (v: X A A): MX n m :=
    box n m (fun i j => !M i j * v).

  Definition dot_scal_left n m (v: X A A) (M: MX n m): MX n m :=
    box n m (fun i j => v * !M i j).

  Global Instance dot_scal_right_compat n m:
  Proper (mx_equal n m ==> equal A A ==> mx_equal n m) (@dot_scal_right n m).

  Global Instance dot_scal_left_compat n m:
  Proper (equal A A ==> mx_equal n m ==> mx_equal n m) (@dot_scal_left n m).

End Props1.

Infix "'*" := dot_scal_left (at level 40): A_scope.
Infix "*'" := dot_scal_right (at level 40): A_scope.

Hint Extern 2 (mx_equal_ _ _ _ _ _) => apply dot_scal_left_compat: compat algebra.
Hint Extern 2 (mx_equal_ _ _ _ _ _) => apply dot_scal_right_compat: compat algebra.

Section Props2.

  Context `{ISR: IdemSemiRing}.
  Variable A: T.
  Notation MX n m := (MX_ A n m).
  Notation mx_equal n m := (mx_equal_ A n m) (only parsing).

  Lemma mx_blocks_dot n m n' m' p p': forall
    (a : MX n m )
    (b : MX n m')
    (c : MX n' m )
    (d : MX n' m')
    (a': MX m p )
    (b': MX m p')
    (c': MX m' p )
    (d': MX m' p'),
    mx_blocks a b c d * mx_blocks a' b' c' d'
    == mx_blocks
    (a * a' + b * c')
    (a * b' + b * d')
    (c * a' + d * c')
    (c * b' + d * d').

  Lemma mx_blocks_one x n :
    1 == @mx_blocks _ A x x n n 1 0 0 1.

  Lemma dot_scal_left_is_dot n (M: MX 1 n) x:
    x '* M == mx_of_scal x * M.

  Lemma dot_scal_left_one n m (M: MX n m): 1 '* M == M.

  Lemma dot_scal_left_zero n m x: x '* (0: MX n m) == 0.

  Lemma dot_scal_left_dot n m p (M: MX n m) (P: MX m p) x:
    (x '* M) * P == x '* (M * P).

  Lemma dot_scal_left_blocks n m p q
    (N: MX n p)
    (M: MX n q)
    (P: MX m p)
    (Q: MX m q) x:
    x '* mx_blocks N M P Q
    == mx_blocks (x '* N) (x '* M) (x '* P) (x '* Q).

  Lemma dot_scal_right_is_dot n x (M: MX 1 n):
    x '* M == mx_of_scal x * M.

  Lemma dot_scal_right_one n m (M: MX n m): M *' 1 == M.

  Lemma dot_scal_right_zero n m x: (0: MX n m) *' x == 0.

  Lemma dot_scal_right_dot n m p (M: MX n m) (P: MX m p) x:
    M * (P *' x) == (M * P) *' x.

  Lemma dot_scal_right_blocks n m p q
    (N: MX n p)
    (M: MX n q)
    (P: MX m p)
    (Q: MX m q) x:
    mx_blocks N M P Q *' x
    == mx_blocks (N *' x) (M *' x) (P *' x) (Q *' x).

  Lemma mx_of_scal_dot: forall a b: X A A,
                        mx_of_scal a * mx_of_scal b == mx_of_scal (a*b).

  Lemma mx_of_scal_one: 1 == mx_of_scal (one A).

  Lemma mx_to_scal_dot: forall a b: MX 1 1,
                        mx_to_scal a * mx_to_scal b == mx_to_scal (a*b).

  Lemma mx_to_scal_one: one A == mx_to_scal 1.

  Lemma mx_point_dot n m o i j k: forall a b: X A A, j < m ->
    mx_point n m i j a * mx_point m o j k b == mx_point n o i k (a*b).

  Lemma mx_point_dot_zero n m o i j j' k: forall a b: X A A, j<>j' ->
    mx_point n m i j a * mx_point m o j' k b == 0.

  Lemma mx_point_one_left n m p i j: forall M: MX m p, j < m ->
    mx_point n m i j 1 * M == box n p (fun s t => xif (eq_nat_bool i s) (!M j t) 0).

  Lemma mx_point_center n m p q i j (M: MX n m) (N: MX p q):
    i < m -> j < p ->
    M * mx_point m p i j 1 * N == box n q (fun s t => !M s i * !N j t).

End Props2.