Require Export MatrixInvAM.
Require Export MatrixInvGE.
Require Import ExtrOcamlBasic ExtrOcamlNatInt MyExtrOCamlR.

Generalizable Variable A Aadd Azero Aopp Amul Aone Ainv.

Module test_inv_ocaml.
  Module AM := MinvMoreAM FieldElementTypeR.
  Module GE := MinvMoreGE FieldElementTypeR.

  Import AM.
  Definition minvtblebAM {n} := @minvtbleb n.
  Definition minvoAM {n} := @minvo n.
  Definition minvAM {n} := @minv n.
  Definition minvListAM {n} := @minvList n.

  Import GE.
  Definition minvtblebGE {n} := @minvtbleb n.
  Definition minvoGE {n} := @minvo n.
  Definition minvGE {n} := @minv n.
  Definition minvListGE {n} := @minvList n.


End test_inv_ocaml.

Module usage_AM_Qc.
  Module AM := MinvMoreAM FieldElementTypeQc.
  Import AM.
  Import AMNotations.

  Section ex1.
    Let M : smat 3 := l2m 0 (Q2Qc_dlist [[1;3;1];[2;1;1];[2;2;1]]%Q).
    Let N : smat 3 := l2m 0 (Q2Qc_dlist [[-1;-1;2];[0;-1;1];[2;4;-5]]%Q).

  End ex1.

  Section ex2.
    Let C : smat 2 := l2m 0 (Q2Qc_dlist [[1;2];[3;4]]%Q).
    Let b : vec 2 := l2v 0 (Q2Qc_list [5;6]%Q).


  End ex2.
End usage_AM_Qc.

Module usage_GE_Qc.
  Module GE := MinvMoreGE FieldElementTypeQc.
  Import GE.
  Import GENotations.

  Section ex1.
    Let M : smat 3 := l2m 0 (Q2Qc_dlist [[1;3;1];[2;1;1];[2;2;1]]%Q).
    Let N : smat 3 := l2m 0 (Q2Qc_dlist [[-1;-1;2];[0;-1;1];[2;4;-5]]%Q).

  End ex1.

  Section ex2.
    Let C : smat 2 := l2m 0 (Q2Qc_dlist [[1;2];[3;4]]%Q).
    Let b : vec 2 := l2v 0 (Q2Qc_list [5;6]%Q).

  End ex2.
End usage_GE_Qc.

Module usage_AM_Q.
  Module AM := MinvMoreAM FieldElementTypeQc.
  Import AM AMNotations.

  Section inv_Q.

    Definition minv {n} (M : mat Q n n) : mat Qc n n :=
      let M : mat Qc n n := mmap Q2Qc M in
      mmap Qc2Q M.

    Definition minvList (n : nat) (dl : dlist Q) : dlist Q :=
      Qc2Q_dlist (minvList n (Q2Qc_dlist dl)).

    Definition cramerRule (n : nat) (C : dlist Q) (b : list Q) : list Q :=
      let C' : smat n := l2m 0 (Q2Qc_dlist C) in
      let b' : vec n := l2v 0 (Q2Qc_list b) in
      let x' : vec n := cramerRule C' b' in
      Qc2Q_list (v2l x').

    Definition solveEq (n : nat) (C : dlist Q) (b : list Q) : list Q :=
      let C' : smat n := l2m 0 (Q2Qc_dlist C) in
      let b' : vec n := l2v 0 (Q2Qc_list b) in
      let x' : vec n := solveEq C' b' in
      Qc2Q_list (v2l x').
  End inv_Q.

  Open Scope Q_scope.

  Section ex1.
    Let M := [[1;3;1];[2;1;1];[2;2;1]].
    Let N := [[-1;-1;2];[0;-1;1];[2;4;-5]].

  End ex1.

  Section ex2.
    Let C := [[1;2];[3;4]].
    Let b := [5;6].


  End ex2.

  Section ex3.
    Let C := [[1;2;3;4;5];
              [2;4;3;5;1];
              [3;1;5;2;4];
              [4;5;2;3;1];
              [5;4;1;2;3]].
    Let b := [1;2;3;5;4].


  End ex3.

  Section ex4.
    Let M :=
          [[0.8147;0.1576;0.6557;0.7060;0.4387;0.2760;0.7513;0.8407;0.3517;0.0759];
           [0.9058;0.9706;0.0357;0.0318;0.3816;0.6797;0.2551;0.2543;0.8308;0.0540];
           [0.1270;0.9572;0.8491;0.2769;0.7655;0.6551;0.5060;0.8143;0.5853;0.5308];
           [0.9134;0.4854;0.9340;0.0462;0.7952;0.1626;0.6991;0.2435;0.5497;0.7792];
           [0.6324;0.8003;0.6787;0.0971;0.1869;0.1190;0.8909;0.9293;0.9172;0.9340];
           [0.0975;0.1419;0.7577;0.8235;0.4898;0.4984;0.9593;0.3500;0.2858;0.1299];
           [0.2785;0.4218;0.7431;0.6948;0.4456;0.9597;0.5472;0.1966;0.7572;0.5688];
           [0.5469;0.9157;0.3922;0.3171;0.6463;0.3404;0.1386;0.2511;0.7537;0.4694];
           [0.9575;0.7922;0.6555;0.9502;0.7094;0.5853;0.1493;0.6160;0.3804;0.0119];
           [0.9649;0.9595;0.1712;0.0344;0.7547;0.2238;0.2575;0.4733;0.5678;0.3371]].

    Let M1 :=
          [[0.81;0.15;0.65;0.70;0.43;0.27;0.75;0.84;0.35;0.07];
           [0.90;0.97;0.03;0.03;0.38;0.67;0.25;0.25;0.83;0.05];
           [0.12;0.95;0.84;0.27;0.76;0.65;0.50;0.81;0.58;0.53];
           [0.91;0.48;0.93;0.04;0.79;0.16;0.69;0.24;0.54;0.77];
           [0.63;0.80;0.67;0.09;0.18;0.11;0.89;0.92;0.91;0.93];
           [0.09;0.14;0.75;0.82;0.48;0.49;0.95;0.35;0.28;0.12];
           [0.27;0.42;0.74;0.69;0.44;0.95;0.54;0.19;0.75;0.56];
           [0.54;0.91;0.39;0.31;0.64;0.34;0.13;0.25;0.75;0.46];
           [0.95;0.79;0.65;0.95;0.70;0.58;0.14;0.61;0.38;0.01];
           [0.96;0.95;0.17;0.03;0.75;0.22;0.25;0.47;0.56;0.33]].
  End ex4.

End usage_AM_Q.

Module usage_GE_Q.
  Module GE := MinvMoreGE FieldElementTypeQc.
  Import GE GENotations.

  Section inv_Q.

    Definition minv {n} (M : mat Q n n) : mat Qc n n :=
      let M : mat Qc n n := mmap Q2Qc M in
      mmap Qc2Q M.

    Definition minvList (n : nat) (dl : dlist Q) : dlist Q :=
      Qc2Q_dlist (minvList n (Q2Qc_dlist dl)).

    Definition solveEq (n : nat) (C : dlist Q) (b : list Q) : list Q :=
      let C' : smat n := l2m 0 (Q2Qc_dlist C) in
      let b' : vec n := l2v 0 (Q2Qc_list b) in
      let x' : vec n := solveEq C' b' in
      Qc2Q_list (v2l x').
  End inv_Q.

  Open Scope Q_scope.

  Section ex1.
  End ex1.

  Section ex2.
    Let C := [[1;2];[3;4]].
    Let b := [5;6].

  End ex2.

  Section ex3.
    Let C := [[1;2;3;4;5];
              [2;4;3;5;1];
              [3;1;5;2;4];
              [4;5;2;3;1];
              [5;4;1;2;3]].
    Let b := [1;2;3;5;4].

  End ex3.

  Section ex4.
    Let M :=
          [[0.8147;0.1576;0.6557;0.7060;0.4387;0.2760;0.7513;0.8407;0.3517;0.0759];
           [0.9058;0.9706;0.0357;0.0318;0.3816;0.6797;0.2551;0.2543;0.8308;0.0540];
           [0.1270;0.9572;0.8491;0.2769;0.7655;0.6551;0.5060;0.8143;0.5853;0.5308];
           [0.9134;0.4854;0.9340;0.0462;0.7952;0.1626;0.6991;0.2435;0.5497;0.7792];
           [0.6324;0.8003;0.6787;0.0971;0.1869;0.1190;0.8909;0.9293;0.9172;0.9340];
           [0.0975;0.1419;0.7577;0.8235;0.4898;0.4984;0.9593;0.3500;0.2858;0.1299];
           [0.2785;0.4218;0.7431;0.6948;0.4456;0.9597;0.5472;0.1966;0.7572;0.5688];
           [0.5469;0.9157;0.3922;0.3171;0.6463;0.3404;0.1386;0.2511;0.7537;0.4694];
           [0.9575;0.7922;0.6555;0.9502;0.7094;0.5853;0.1493;0.6160;0.3804;0.0119];
           [0.9649;0.9595;0.1712;0.0344;0.7547;0.2238;0.2575;0.4733;0.5678;0.3371]].

    Let M1 :=
          [[0.81;0.15;0.65;0.70;0.43;0.27;0.75;0.84;0.35;0.07];
           [0.90;0.97;0.03;0.03;0.38;0.67;0.25;0.25;0.83;0.05];
           [0.12;0.95;0.84;0.27;0.76;0.65;0.50;0.81;0.58;0.53];
           [0.91;0.48;0.93;0.04;0.79;0.16;0.69;0.24;0.54;0.77];
           [0.63;0.80;0.67;0.09;0.18;0.11;0.89;0.92;0.91;0.93];
           [0.09;0.14;0.75;0.82;0.48;0.49;0.95;0.35;0.28;0.12];
           [0.27;0.42;0.74;0.69;0.44;0.95;0.54;0.19;0.75;0.56];
           [0.54;0.91;0.39;0.31;0.64;0.34;0.13;0.25;0.75;0.46];
           [0.95;0.79;0.65;0.95;0.70;0.58;0.14;0.61;0.38;0.01];
           [0.96;0.95;0.17;0.03;0.75;0.22;0.25;0.47;0.56;0.33]].
  End ex4.
End usage_GE_Q.