# Library ATBR.MxGraph

Basic definitions for matrices: definition of their Graph

Require Import Common.
Require Import Classes.
Require Import Graph.
Require List.
Require Force.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Section Defs.

Context {G: Graph}.
Variable A: T.
Notation X := (X A A).

n and m are phantom types, a matrix is a function from two nat to X
Inductive MX (n m: nat) :=
box: (nat nat X) MX n m.

Definition get n m (M: MX n m) := let (f) := M in f.

matrix equality is bounded pointwise equality

Definition mx_equal n m: relation (MX n m) :=
fun M N i j, i<n j<m get M i j == get N i j.

matrix Graph, equality is bounded pointwise equality
Program Instance mx_Graph: Graph := {
T := nat;
X := MX;
equal := mx_equal }.
Next Obligation.
split; repeat intro; simpl in ×.
reflexivity.
symmetry; auto.
transitivity (get y i j); auto.
Qed.

Lemma mx_equal': n m (M N: @Classes.X mx_Graph n m)
(H: i j, i<n j<m get M i j == get N i j), M == N.
Proof (fun _ _ _ _ HH).

Definition mx_equal_at p q n m n' m' (M : MX n m) (N : MX n' m') :=
i j, i < p j < q get M i j == get N i j.

Lemma mx_equal_at_equal n m (M N: @Classes.X mx_Graph n m) : mx_equal_at n m M N M == N.
Proof. intros. unfold mx_equal_at. intuition. Qed.
End Defs.

Notation MX_ A n m := (@X (mx_Graph A) (n%nat:nat) (m%nat:nat)) (only parsing).
Notation mx_equal_ A n m := (@equal (mx_Graph A) (n%nat:nat) (m%nat:nat)) (only parsing).

Notation "! M" := (get M) (at level 0) : A_scope.
Notation "M == [ n , m ] N" := (@equal (mx_Graph _) n m M N) (at level 80) : A_scope.

Lemma plus_minus : m n, S (m+n)-n = S m.
Proof. intros. omega. Qed.
Global Opaque minus.

Lemma lt_n_1 n: ¬ (S n<1)%nat.
Proof. omega. Qed.

case analysis on block matrix acesses
Ltac destruct_blocks :=
unfold mx_equal; intros; simpl;
rewrite ? plus_minus;
repeat match goal with
| |- context[S ?i - ?n] ⇒ case_eq (S i - n); intros
end.

tactic to pointwise check matrix equality
Ltac mx_intros i j Hi Hj :=
apply mx_equal'; intros i j Hi Hj;
match type of Hi with
| i < 0%natelim (lt_n_O _ Hi)
| i < 1%natdestruct i; [clear Hi | elim (lt_n_1 Hi)]
| _idtac
end;
match type of Hj with
| j < 0%natelim (lt_n_O _ Hj)
| j < 1%natdestruct j; [clear Hj | elim (lt_n_1 Hj)]
| _idtac
end.

Transparent equal.

Section Props.

Context {G: Graph}.
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_equal_compat n m: M N: MX n m,
M == N
i j i' j', i<n j<m i=i' j=j' !M i j == !N i' j'.
Proof. intros; subst; auto. Qed.

Definition mx_force n m (M: MX n m): MX n m := box n m (Force.id2 n m !M).
Definition mx_print n m (M: MX n m) := Force.print2 n m !M.
Definition mx_noprint n m (M: MX n m) := let _ := mx_force M in (n,m).

Lemma mx_force_id n m (M: MX n m): mx_force M == M.
Proof. repeat intro; unfold mx_force. simpl. rewrite Force.id2_id by assumption. reflexivity. Qed.

Global Instance mx_force_compat n m: Proper (mx_equal n m ==> mx_equal n m) (@mx_force n m).
Proof. intros M N H. rewrite 2 mx_force_id. assumption. Qed.

Global Instance box_compat n m:
Proper (pointwise_relation nat (pointwise_relation nat (equal A A)) ==> mx_equal n m) (box n m).
Proof. intros. intros f g H. mx_intros i j Hi Hj. apply H. Qed.

sub-matrix
Definition mx_sub n' m' x y n m (M: MX n' m') : MX n m
:= box n m (fun i j!M (x+i) (y+j))%nat.

special case of block matrices
Section Subs.
Variables x y n m: nat.
Section Def.
Variable M: MX (x+n) (y+m).
Definition mx_sub00 := mx_sub 0 0 x y M.
Definition mx_sub01 := mx_sub 0 y x m M.
Definition mx_sub10 := mx_sub x 0 n y M.
Definition mx_sub11 := mx_sub x y n m M.
End Def.
Global Instance mx_sub00_compat: Proper (mx_equal (x+n) (y+m) ==> mx_equal x y) mx_sub00.
Proof. repeat intro. simpl. apply H; auto with omega. Qed.
Global Instance mx_sub01_compat: Proper (mx_equal (x+n) (y+m) ==> mx_equal x m) mx_sub01.
Proof. repeat intro. simpl. apply H; auto with omega. Qed.
Global Instance mx_sub10_compat: Proper (mx_equal (x+n) (y+m) ==> mx_equal n y) mx_sub10.
Proof. repeat intro. simpl. apply H; auto with omega. Qed.
Global Instance mx_sub11_compat: Proper (mx_equal (x+n) (y+m) ==> mx_equal n m) mx_sub11.
Proof. repeat intro. simpl. apply H; auto with omega. Qed.
End Subs.

Section Blocks.

Variables x y n m: nat.

block matrix
Definition mx_blocks
(M: MX x y)
(N: MX x m)
(P: MX n y)
(Q: MX n m): MX (x+n) (y+m)
:= box _ _
(fun i j
match S i-x, S j-y with
| O, O!M i j
| S i, O!P i j
| O, S j!N i j
| S i, S j!Q i j
end).

Global Instance mx_blocks_compat:
Proper (
mx_equal x y ==>
mx_equal x m ==>
mx_equal n y ==>
mx_equal n m ==>
mx_equal (x+n) (y+m))
mx_blocks.
Proof.
repeat intro. destruct_blocks; auto with omega.
Qed.

Lemma mx_decompose_blocks :
M: MX (x+n) (y+m),
M ==
mx_blocks
(mx_sub00 M)
(mx_sub01 M)
(mx_sub10 M)
(mx_sub11 M).
Proof.
simpl; intros. destruct_blocks; auto with omega.
Qed.

Section Proj.

Variables (a: MX x y) (b: MX x m) (c: MX n y) (d: MX n m).

Lemma mx_block_00: mx_sub00 (mx_blocks a b c d) == a.
Proof.
simpl. intros. destruct_blocks; reflexivity || omega_false.
Qed.

Lemma mx_block_01: mx_sub01 (mx_blocks a b c d) == b.
Proof.
simpl. intros. destruct_blocks; omega_false || auto with compat omega.
Qed.

Lemma mx_block_10: mx_sub10 (mx_blocks a b c d) == c.
Proof.
simpl. intros. destruct_blocks; omega_false || auto with compat omega.
Qed.

Lemma mx_block_11: mx_sub11 (mx_blocks a b c d) == d.
Proof.
simpl. intros. destruct_blocks; omega_false || auto with compat omega.
Qed.

End Proj.

Lemma mx_blocks_equal: (a a': MX x y) b b' c c' (d d': MX n m),
mx_blocks a b c d == mx_blocks a' b' c' d'
a==a' b==b' c==c' d==d'.
Proof.
intros.
rewrite <- (mx_block_11 a b c d) at 1.
rewrite <- (mx_block_10 a b c d) at 1.
rewrite <- (mx_block_01 a b c d) at 1.
rewrite <- (mx_block_00 a b c d) at 1.
rewrite H.
rewrite mx_block_00, mx_block_01, mx_block_10, mx_block_11.
repeat split; reflexivity.
Qed.

End Blocks.

Lemma mx_blocks_degenerate_00 (a: MX 1 1) b c (d: MX 0 0):
(mx_blocks a b c d: MX 1 1) == a.
Proof.
intros [|] [|] Hi Hj; try omega_false. reflexivity.
Qed.

Lemma mx_blocks_degenerate_11 n m (a: MX 0 0) b c (d: MX n m):
(mx_blocks a b c d: MX n m) == d.
Proof.
mx_intros i j Hi Hj. reflexivity.
Qed.

conversions from and to scalars
Definition mx_of_scal (x: X A A): MX 1 1 := box 1 1 (fun _ _x).
Definition mx_to_scal (M: MX 1 1): X A A := !M O O.

Global Instance mx_of_scal_compat:
Proper (equal A A ==> mx_equal 1 1) mx_of_scal.
Proof. repeat intro. simpl. trivial. Qed.

Global Instance mx_to_scal_compat:
Proper (mx_equal 1 1 ==> equal A A) mx_to_scal.
Proof. repeat intro. simpl. apply H; auto. Qed.

Lemma mx_to_scal_from_scal (M: MX 1 1):
M == mx_of_scal (mx_to_scal M).
Proof. mx_intros i j Hi Hj. reflexivity. Qed.

Lemma Meq_to_eq: a b, mx_of_scal a == mx_of_scal b a == b.
Proof.
intros a b H. apply (H O O); auto.
Qed.

Lemma eq_to_Meq: a b, mx_to_scal a == mx_to_scal b a == b.
Proof.
intros a b H. mx_intros i j Hi Hj. apply H.
Qed.

transposition
Definition mx_transpose n m (M : MX n m): MX m n := box m n (fun i j!M j i).

Global Instance mx_transpose_compat n m:
Proper (mx_equal n m ==> mx_equal m n) (@mx_transpose n m).
Proof. repeat intro. simpl. apply H; trivial. Qed.

Lemma mx_transpose_blocks x y n m (a: MX x y) b c (d: MX n m):
mx_transpose (mx_blocks a b c d)
== mx_blocks (mx_transpose a) (mx_transpose c) (mx_transpose b) (mx_transpose d).
Proof.
repeat intro. simpl. destruct_blocks; reflexivity.
Qed.

End Props.

Hint Extern 1 (mx_equal_ _ _ _ _ _) ⇒ apply mx_sub00_compat: compat algebra.
Hint Extern 1 (mx_equal_ _ _ _ _ _) ⇒ apply mx_sub01_compat: compat algebra.
Hint Extern 1 (mx_equal_ _ _ _ _ _) ⇒ apply mx_sub10_compat: compat algebra.
Hint Extern 1 (mx_equal_ _ _ _ _ _) ⇒ apply mx_sub11_compat: compat algebra.
Hint Extern 1 (mx_equal_ _ _ _ _ _) ⇒ apply mx_transpose_compat: compat algebra.
Hint Extern 1 (mx_equal_ _ _ _ _ _) ⇒ apply mx_force_compat: compat algebra.
Hint Extern 4 (mx_equal_ _ _ _ _ _) ⇒ apply mx_blocks_compat: compat algebra.
Hint Extern 1 (mx_equal_ _ _ _ _ _) ⇒ apply mx_of_scal_compat: compat algebra.
Hint Extern 1 (equal _ _ _ _) ⇒ apply mx_to_scal_compat: compat algebra.
Hint Extern 5 (equal _ _ _ _) ⇒ apply mx_equal_compat : compat algebra.