Require Import MatrixInvAM QExt QcExt.

Module MinvAM_Qc := MinvAM FieldElementTypeQc.

Section inv_Qc.
  Import MinvAM_Qc.

  Section ex1.

    Let d1 := Q2Qc_dlist [[1;3;1];[2;1;1];[2;2;1]]%Q.
    Let d2 := Q2Qc_dlist [[-1;-1;2];[0;-1;1];[2;4;-5]]%Q.



    Goal minvList 3 d1 = d2.
    Proof.
      cbv.
      auto.

    Qed.
  End ex1.

End inv_Qc.

Section inv_Q.

  Import MinvAM_Qc.
  Open Scope Q_scope.

  Definition minvtblebListQ (n : nat) (d : dlist Q) : bool :=
    minvtblebList n (Q2Qc_dlist d).

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

  Section ex2.

    Let d1 := [[1;3;1];[2;1;1];[2;2;1]].
    Let d2 := [[-1;-1;2];[0;-1;1];[2;4;-5]].


    Goal minvListQ 3 d1 = d2.
    Proof. cbv. auto. Qed.

    Goal 1 == Qmake 2 2.
    Proof. cbv. auto. Qed.

    Goal 1 <> Qmake 2 2.
    Proof. cbv. intros. easy. Qed.

    Let d2' : dlist Q := [[-1;-1;2];[0;-1;Qmake 2 2];[2;4;-5]].

    Goal minvListQ 3 d1 <> d2'.
    Proof. cbv. intro. inv H. Qed.

    Infix "==" := (dlistSetoidEq Qeq).
    Goal minvListQ 3 d1 == d2.
    Proof. Local Opaque Qeq. cbv. repeat constructor. Qed.
  End ex2.

  Section ex3.
    Let d1 : dlist Q :=
      [[1;2;3;4;5;6;7;8];
       [2;4;5;6;7;8;9;1];
       [3;5;7;6;8;4;2;1];
       [4;5;7;6;9;8;3;2];
       [5;4;3;7;9;6;8;1];
       [6;5;3;4;7;8;9;2];
       [7;8;6;5;9;2;1;3];
       [8;9;6;3;4;5;2;1]].







    Open Scope Qc_scope.
    Let M : smat _ 8 := l2m 0 (Q2Qc_dlist d1).

    Let M1 := @minv 8 (l2m 0 (Q2Qc_dlist d1)).

    Goal ~(Qmake 41846 50943 == Qmake 23 28).
    Proof.
      intro. cbv in H.       easy.
    Qed.

  End ex3.

  Section ex4.
    Let d1 :=
          [[0.8001;0.5797;0.0760;0.9448;0.3897;0.0598;0.7317;0.1835];
           [0.4314;0.5499;0.2399;0.4909;0.2417;0.2348;0.6477;0.3685];
           [0.9106;0.1450;0.1233;0.4893;0.4039;0.3532;0.4509;0.6256];
           [0.1818;0.8530;0.1839;0.3377;0.0965;0.8212;0.5470;0.7802];
           [0.2638;0.6221;0.2400;0.9001;0.1320;0.0154;0.2963;0.0811];
           [0.1455;0.3510;0.4173;0.3692;0.9421;0.0430;0.7447;0.9294];
           [0.1361;0.5132;0.0497;0.1112;0.9561;0.1690;0.1890;0.7757];
           [0.8693;0.4018;0.9027;0.7803;0.5752;0.6491;0.6868;0.4868]].

  End ex4.

End inv_Q.

Section solveEq_cramerRule_Qc.
  Import MinvAM_Qc.

  Let M1 : smat _ 2 := l2m 0 (Q2Qc_dlist [[1;2];[3;4]]%Q).
  Let b1 : vec 2 := l2v 0 (Q2Qc_list [5;6]%Q).

  Let M2 : smat _ 5 :=
        l2m 0 (Q2Qc_dlist
                 [[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]]%Q).
  Let b2 : vec 5 := l2v 0 (Q2Qc_list [1;2;3;5;4]%Q).
End solveEq_cramerRule_Qc.

Module usage_AM_Qc.
  Module AM := MinvAM FieldElementTypeQc.
  Import AM.

  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_AM_Q.
  Module AM := MinvAM FieldElementTypeQc.
  Import AM.

  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.