FinMatrix.Matrix.MatrixGauss_test

Require Import MatrixGauss.
Require Import QcExt RExt.

Section test.
  Open Scope nat_scope.

  Let M : smat nat 3 := l2m 0 [[1;0;0];[0;1;0];[0;0;1]].
  Notation getPivot := (@getPivot nat 0).

End test.

Section test.
  Import QcExt.
  Notation elimDown := (@elimDown _ Qcplus 0 Qcopp Qcmult _).

  Let M : smat Qc 3 := l2m 0 (dlistQ2Qc [[1;2;3];[4;5;6];[7;8;9]]%Q).
End test.

Section test.

  Import QcExt.
  Notation getPivot := (getPivot (Azero:=0)).
  Notation toREF := (@toREF _ Qcplus 0 Qcopp Qcmult Qcinv _).
  Notation elimDown := (@elimDown _ Qcplus 0 Qcopp Qcmult _).
  Notation rowOps2mat := (@rowOps2mat _ Qcplus 0 Qcmult 1 _).
  Notation mmul := (@mmul _ Qcplus 0 Qcmult).
  Infix "*" := mmul : mat_scope.

  Let M : smat Qc 3 := l2m 0 (dlistQ2Qc [[0;-2;1];[3;0;-2];[-2;3;0]]%Q).
  Let M1 : smat Qc 3 := l2m 0 (dlistQ2Qc [[1;0;-2/3];[0;1;-1/2];[0;0;1]]%Q).
  Let E1 : smat Qc 3 := l2m 0 (dlistQ2Qc [[0;1/3;0];[-1/2;0;0];[9;4;6]]%Q).

  Goal match toREF M 3 with
       | Some (l1',M1') => m2l (rowOps2mat l1') = m2l E1
                          /\ m2l M1' = m2l M1
       | _ => False
       end.
  Proof.
    cbv; split; list_eq; f_equal; apply proof_irrelevance.
  Qed.

  Goal (E1 * M)%M = M1.
  Proof. apply m2l_inj. cbv. list_eq; f_equal. Qed.

End test.

Section test.

  Import QcExt.
  Notation elimUp := (@elimUp _ Qcplus 0 Qcopp Qcmult _).

  Let M : smat Qc 3 := l2m 0 (dlistQ2Qc [[1;2;3];[4;5;6];[7;8;1]]%Q).
End test.

Section test.
  Import QcExt.
  Open Scope mat_scope.

  Notation smat n := (smat Qc n).
  Notation mat1 := (@mat1 _ 0 1).
  Notation mmul := (@mmul _ Qcplus 0 Qcmult).
  Infix "*" := mmul : mat_scope.
  Notation toREF := (@toREF _ Qcplus 0 Qcopp Qcmult Qcinv).
  Notation toRREF := (@toRREF _ Qcplus 0 Qcopp Qcmult).
  Notation elimUp := (@elimUp _ Qcplus 0 Qcopp Qcmult).
  Notation rowOps2mat := (@rowOps2mat _ Qcplus 0 Qcmult 1).
  Notation rowOps2matInv := (@rowOps2matInv _ Qcplus 0 Qcopp Qcmult 1 Qcinv).


  Let M0 : smat 3 := l2m 0 (dlistQ2Qc [[0;-2;1];[3;0;-2];[-2;3;0]]%Q).
  Let N0 : smat 3 := l2m 0 (dlistQ2Qc [[6;3;4];[4;2;3];[9;4;6]]%Q).

  Goal M0 * N0 = mat1. Proof. meq. Qed.
  Goal N0 * M0 = mat1. Proof. meq. Qed.

  Let l1 := match toREF M0 3 with Some (l1,M1) => l1 | _ => [] end.
  Let T1 : smat 3 := rowOps2mat l1.
  Let M1 : smat 3 := match toREF M0 3 with Some (l1,M1) => M1 | _ => mat1 end.

  Let l2 := fst (toRREF M1 3).
  Let T2 : smat 3 := rowOps2mat l2.
  Let M2 : smat 3 := snd (toRREF M1 3).

  Goal M2 = mat1. Proof. meq; f_equal; apply proof_irrelevance. Qed.

  Goal T2 * T1 = N0. Proof. meq; f_equal; apply proof_irrelevance. Qed.


  Goal rowOps2matInv l1 * M1 = M0. Proof. meq; f_equal; apply proof_irrelevance. Qed.

  Goal rowOps2matInv l2 = M1. Proof. meq; f_equal; apply proof_irrelevance. Qed.

  Goal rowOps2matInv l1 * rowOps2matInv l2 = M0.
  Proof. meq; f_equal; apply proof_irrelevance. Qed.

  Goal rowOps2matInv (l2 ++ l1) = M0.
  Proof. meq; f_equal; apply proof_irrelevance. Qed.

End test.