Library ATBR.MxKleeneAlgebra
Properties of matrices over a Kleene algebra (in particular, they form a typed Kleene algebra)
Require Import Common.
Require Import Classes.
Require Import Graph.
Require Import Monoid.
Require Import SemiLattice.
Require Import SemiRing.
Require Import KleeneAlgebra.
Require Import MxGraph.
Require Import MxSemiLattice.
Require Import MxSemiRing.
Section PreDefs.
Local Transparent equal.
Context `{KA: KleeneAlgebra}.
Variable A: T.
Notation mx_equal n m := (mx_equal_ A n m) (only parsing).
Notation mx_leq n m := (mx_leq_ A n m) (only parsing).
Notation MX n m := (@X (mx_Graph A) (n%nat) (m%nat)).
Notation X := (@X G A A).
Notation SMX n := (MX n n).
block construction of the star operation over matrices
Definition star_build x n (sx: SMX x -> SMX x) (sn: SMX n -> SMX n) (M: SMX (x+n)): SMX (x+n) :=
let a := mx_sub00 M in
let b := mx_sub01 M in
let c := mx_sub10 M in
let d := mx_sub11 M in
let e := sn d in
let be:= b*e in
let ec:= e*c in
let f := sx (a + be*c) in
let fbe := f*be in
let ecf := ec*f in
mx_blocks f fbe ecf (e + ecf*be).
let a := mx_sub00 M in
let b := mx_sub01 M in
let c := mx_sub10 M in
let d := mx_sub11 M in
let e := sn d in
let be:= b*e in
let ec:= e*c in
let f := sx (a + be*c) in
let fbe := f*be in
let ecf := ec*f in
mx_blocks f fbe ecf (e + ecf*be).
recursive construction
Fixpoint star_rec n: SMX n -> SMX n :=
match n with
| 0 => fun M => M
| S n => fun M =>
star_build (fun a => mx_of_scal (mx_to_scal a #)) (@star_rec n) M
end.
Definition mx_star_block x n := star_build (@star_rec x) (@star_rec n).
Definition prop_star_make_left n f := forall M: SMX n, 1 + f M * M == f M.
match n with
| 0 => fun M => M
| S n => fun M =>
star_build (fun a => mx_of_scal (mx_to_scal a #)) (@star_rec n) M
end.
Definition mx_star_block x n := star_build (@star_rec x) (@star_rec n).
Definition prop_star_make_left n f := forall M: SMX n, 1 + f M * M == f M.
below, we prove that the operation we constructed is actually the star operation over matrices
Lemma build_star_make_left x n sx sn:
prop_star_make_left sx ->
prop_star_make_left sn ->
prop_star_make_left (@star_build x n sx sn).
Lemma decomp_dot_leq_left x n m (a: SMX x) b c (d: SMX n) (Y: MX (x+n) m):
mx_blocks a b c d * Y <== Y <->
let z := mx_sub01 (y:=0) Y in
let y := mx_sub11 (y:=0) Y in
a*z <== z /\ b*y <== z /\ c*z <== y /\ d*y <== y.
Definition prop_star_destruct_left n f :=
forall m (M: SMX n) (Y: MX n m),
M * Y <== Y -> f M * Y <== Y.
Lemma build_star_destruct_left x n sx sn:
prop_star_destruct_left sx ->
prop_star_destruct_left sn ->
prop_star_destruct_left (@star_build x n sx sn).
Lemma decomp_dot_leq_right x n m (a: SMX x) b c (d: SMX n) (Y: MX m (x+n)):
Y * mx_blocks a b c d <== Y <->
let y := mx_sub10 (x:= 0) Y in
let z := mx_sub11 (x:= 0) (y:=x) Y in
y * a <== y /\ z * c <== y /\
y * b <== z /\ z * d <== z.
Definition prop_star_destruct_right n f :=
forall m (M: SMX n) (Y: MX m n),
Y * M <== Y -> Y * f M <== Y.
Lemma build_star_destruct_right x n sx sn:
prop_star_destruct_right sx ->
prop_star_destruct_right sn ->
prop_star_destruct_right (@star_build x n sx sn).
End PreDefs.
Section Defs.
Context `{KA: KleeneAlgebra}.
Variable A: T.
Notation mx_equal n m := (mx_equal_ A n m) (only parsing).
Notation mx_leq n m := (mx_leq_ A n m) (only parsing).
Notation X := (@X G A A).
Notation MX n m := (MX_ A n m).
Notation SMX n := (MX_ A n n).
Global Instance mx_Star_Op: Star_Op (mx_Graph A) := { star n := @star_rec _ _ _ _ _ _ }.
Lemma mx_star_compat n (M N: MX n n): M==N -> M# == N# .
Lemma mx_star_make_left n: forall M: MX n n, 1 + M# * M == M#.
Opaque one dot plus. Transparent one dot plus.
Lemma mx_star_block_make_left x n: forall M: MX (x+n) (x+n),
1 + mx_star_block M * M == mx_star_block M.
Lemma mx_star_destruct_left: forall n m (M: MX n n) (Y: MX n m), M*Y <== Y -> M#*Y <== Y.
Opaque one dot plus leq. Transparent one dot plus leq.
Lemma mx_star_block_destruct_left: forall x n m (M: MX (x+n) (x+n)) (Y: MX (x+n) m),
M * Y <== Y -> mx_star_block M * Y <== Y.
Lemma mx_star_destruct_right: forall n m (M: MX n n) (Y: MX m n), Y*M <== Y -> Y*M# <== Y.
Opaque one dot plus leq. Transparent one dot plus leq.
Global Instance mx_KleeneAlgebra: KleeneAlgebra (mx_Graph A).
additional properties of block matrices
Lemma mx_blocks_star': forall x n (M: MX (x+n) (x+n)), M# == mx_star_block M.
Lemma mx_blocks_star: forall x n (a: MX x x) (b: MX x n) (c: MX n x) (d: MX n n),
let e := d# in
let be:= b*e in
let ec:= e*c in
let f := (a + be*c)# in
let fbe := f*be in
let ecf := ec*f in
(mx_blocks a b c d)# == mx_blocks f fbe ecf (e + ecf*be).
Lemma mx_blocks_star_trigonal n m (M: MX n n) (N: MX m m) (P: MX n m):
(mx_blocks M P 0 N)# == mx_blocks (M#) (M# * P * N#) 0 (N#).
Lemma mx_blocks_star_diagonal n m (M: MX n n) (N: MX m m) :
(mx_blocks M 0 0 N)# == mx_blocks (M#) 0 0 (N#).
Lemma mx_to_scal_star (a: MX 1 1): mx_to_scal (a #) == (mx_to_scal a) #.
Lemma mx_of_scal_star (a: X): mx_of_scal (a #) == (mx_of_scal a) #.
End Defs.