Require Export QcExt.
Require Export MatrixModule.

Include (NormedOrderedFieldMatrixTheory NormedOrderedFieldElementTypeQc).

Open Scope Q_scope.
Open Scope Qc_scope.
Open Scope vec_scope.
Open Scope mat_scope.

Definition cramerRuleListQ (n : nat) (lC : dlist Q) (lb : list Q) : list Q :=
  let lC' := dmap Q2Qc lC in
  let lb' := map Q2Qc lb in
  let lx' := cramerRuleList n lC' lb' in
  map Qc2Q lx'.

Lemma cramerRuleListQ_spec : forall (n : nat) (lC : dlist Q) (lb : list Q),
    map Q2Qc (cramerRuleListQ n lC lb) = cramerRuleList n (dmap Q2Qc lC) (map Q2Qc lb).
Proof.
  intros. unfold cramerRuleListQ. rewrite map_map.
  apply ListExt.map_id. intros. apply Q2Qc_Qc2Q.
Qed.

Definition solveEqListGEQ (n : nat) (lC : dlist Q) (lb : list Q) : list Q :=
  let lC' := dmap Q2Qc lC in
  let lb' := map Q2Qc lb in
  let lx' := solveEqListGE n lC' lb' in
  map Qc2Q lx'.

Lemma solveEqListGEQ_spec : forall (n : nat) (lC : dlist Q) (lb : list Q),
    map Q2Qc (solveEqListGEQ n lC lb) = solveEqListGE n (dmap Q2Qc lC) (map Q2Qc lb).
Proof.
  intros. unfold solveEqListGEQ. rewrite map_map.
  apply ListExt.map_id. intros. apply Q2Qc_Qc2Q.
Qed.

Definition solveEqListAMQ (n : nat) (lC : dlist Q) (lb : list Q) : list Q :=
  let lC' := dmap Q2Qc lC in
  let lb' := map Q2Qc lb in
  let lx' := solveEqListAM n lC' lb' in
  map Qc2Q lx'.

Lemma solveEqListAMQ_spec : forall (n : nat) (lC : dlist Q) (lb : list Q),
    map Q2Qc (solveEqListAMQ n lC lb) = solveEqListAM n (dmap Q2Qc lC) (map Q2Qc lb).
Proof.
  intros. unfold solveEqListAMQ. rewrite map_map.
  apply ListExt.map_id. intros. apply Q2Qc_Qc2Q.
Qed.

Notation solveEqListQ := solveEqListGEQ.

Section test.

  Notation v2l v := (Qc2Q_list (v2l v)).
  Notation m2l M := (Qc2Q_dlist (m2l M)).

  Open Scope vec_scope.

  Let u := @l2v 3 (Q2Qc_list [1; 2; 3]%Q).
  Let v := @l2v 3 (Q2Qc_list [2; 1; 0]%Q).

  Open Scope mat_scope.

  Let M := @l2m 3 3 (Q2Qc_dlist [[1;-3;-2];[-2;1;-4];[-1;4;-1]]%Q).

  Open Scope Q_scope.

  Let C := [[1;2];[3;4]].
  Let b := [5;6].
End test.