Module rs_definitions

Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div choice fintype.
Require Import finfun finset ssralg perm zmodp seqmatrixCR advf_type.
Require Import Recdef invmx.

Set Implicit Arguments.
Unset Strict Implicit.
Import Prenex Implicits.





Section definitions.

Local Open Scope ring_scope.


Definition compijCvd (vf:vectorfield)(M: matZ2) :=
  all [pred p| compij p.1 p.2 M == true] vf.



Section matrices.

Fixpoint getcol (c:nat)(s: matZ2) :=
match s with
|nil => nil
|a::b => ((nth false a c)::nil) ++ (getcol c b)
end.


Definition vectorZeros n := nseq n false.

Definition matrizZeros m n := nseq m (vectorZeros n).









End matrices.


Section vectors.



Section seqcvd.





Definition getlastE (k:nat)(ord: orders):= filter [pred s | last 0%N s == k] ord.



Fixpoint following l k (s:seqZ2):=
match s with
|nil=> false
|a::b => if ((l >= k) && (a!= false)) then true else (following (l+1)%N k b)
end.



Fixpoint firstElem1 k (s:seqZ2):nat:=
match s with
|nil => 0%N
|a::b => match k with
          |0 => if (a!=false) then 0%N else (1%N + (firstElem1 0 b))%N
          |S p => (1%N + (firstElem1 (k.-1) b))%N
          end
end.


Functional Scheme firstElem1_ind := Induction for firstElem1 Sort Prop.


Fixpoint getk (k:nat)(ss: matZ2):=
match ss with
|nil => 0%N
|a::b => if ((following 0 0 a)== false) then (getk (k+1) b) else k
end.


End seqcvd.


Local Close Scope ring_scope.


Definition verifyLength (m n a b: nat):= ((0<=a) && (a<m) && (0<=b) && (b<n)).


Definition canAddCvd (m n a b: nat)(vf: vectorfield):=
 (((a \in (getfirstElemseq vf))== false) && ((b \in (getsndElemseq vf))== false)
     && (verifyLength m n a b)).


Definition addcvd (a b: nat)(vf:vectorfield):= ((a, b)::nil) ++ vf.



Definition nocycles_order (i j:nat)(ord: order):=
match ord with
|nil => true
|a::b => if ((i \in (a::b))==false)
  then true
  else if ((j \in (a::b))==false)
                     then true
                     else if ((index i (a::b)) < (index j (a::b)))
                          then true
                          else false
end.

Fixpoint canAddOrder (i j:nat)(ords:orders):=
match ords with
|nil => if (i!=j)
           then true
           else false
|a::b => if (i!=j)
            then if ((nocycles_order i j a) == true)
  then (canAddOrder i j b)
  else false
            else false
end.


Fixpoint nocycles_concat_order (l1:order) (l2:orders) :=
match l1, l2 with
|_, nil => true
|nil, _ => true
|a::b, c::d => if uniq (c ++ (a::b))
                    then (nocycles_concat_order l1 d)
                    else false
end.


Fixpoint nocycles_concat_orders (l1 l2:orders) :=
match l1, l2 with
|nil, _ => true
|a::b ,nil => true
|a::b, c::d => if (nocycles_concat_order a (c::d))
                  then (nocycles_concat_orders b (c::d))
                  else false
end.



Definition canAOrder (i j:nat) (s: orders) :=
match s with
|nil => true
|a::b => let getl := (getlastE i (a::b)) in
          let getf := (getfirstE j (a::b)) in
          if ((getf == nil) || (getl == nil))
          then true
          else (nocycles_concat_orders (getf)(getl))
end.



Definition addOrder_order (i j:nat)(r:order):=
match r with
|nil => nil
|a::b => if (i == (last 0%N (a::b)))
           then if (j == (head 0%N (a::b)))
                  then nil
                  else (((a::b) ++ (j::nil))::nil)
           else if (j == (head 0%N (a::b)))
                  then (((i::nil)++(a::b))::nil)
                  else nil
end.

Fixpoint addOrder_orders (i j : nat)(ords: orders):=
match ords with
|nil => nil
|a::b => (a::nil)++ if (i!=j)
                      then (addOrder_order i j a) ++ (addOrder_orders i j b)
                      else nil
end.





Function addOrder_concat (ords: orders * orders){measure (fun ords => ((size (fst ords)) + (size (snd ords)))%N)}:orders:=
match (fst ords), (snd ords) with
| nil , _ => nil
| _ , nil => nil
|a::nil, c::d => ((c++a)::nil) ++ (addOrder_concat ((a::nil), d))
|a::b, c::nil => ((c++a)::nil) ++ (addOrder_concat (b,(c::nil)))
|a::b , c::d => ((c++a)::nil) ++ (addOrder_concat ((a::nil), d)) ++ (addOrder_concat (b, (c::d)))
end.




Local Open Scope ring_scope.

Fixpoint addOrders (i k:nat)(s:seqZ2)(ords: orders):=
match s, ords with
|nil, _ => ords
|a::nil, nil => if ((a!= false) && (i!=k))
                   then (i::k::nil)::nil
                   else nil
|a::nil, _ => let getf := (getfirstE k ords) in
                 let getl := (getlastE i ords) in
                 if ((a!=false) && (i!=k))
                      then if ((getf == nil) || (getl == nil))
                             then ((i::k::nil)::nil ) ++ (addOrder_orders i k ords)
                             else ((i::k::nil)::nil ) ++(addOrder_orders i k ords)++(addOrder_concat (getf, getl))
                   else ords
|a::b, nil => if ((a != false) && (i != k))
   then addOrders i (k+1) b ((i::k::nil)::nil)
  else addOrders i (k+1) b nil
|a::b, _ => let getf := (getfirstE k ords) in
                 let getl := (getlastE i ords) in
                 if ((a != false) && (i != k))
                      then (addOrders i (k+1) b (((i::k::nil)::nil) ++ (addOrder_orders i k ords) ++ (addOrder_concat (getf, getl))))
    else addOrders i (k+1) b ords
end.

Functional Scheme addOrders_ind := Induction for addOrders Sort Prop.


Fixpoint canAddOrders (i k:nat)(s:seqZ2)(ord: orders) :=
match s, ord with
|nil, _ => true
|a::b, nil => if ((i!=k) && (a != false))
               then (canAddOrders i (k+1) b ((i::k::nil)::nil))
               else (canAddOrders i (k+1) b nil)
|a::b, c::d => if ((i!=k) &&(a!= false))
                   then if ((canAddOrder i k (c::d)) && (canAOrder i k (c::d)))
   then (canAddOrders i (k+1) b (((i::k::nil)::nil) ++ (addOrder_orders i k (c::d))
                                 ++ (addOrder_concat ((getfirstE k ord), (getlastE i ord)))))
          else false
   else (canAddOrders i (k+1) b (c::d))
end.
  

Functional Scheme canAddOrders_ind := Induction for canAddOrders Sort Prop.
       


Fixpoint genDvfOrders (it:nat)(i j:nat) (mm:matZ2) (mm1:matZ2) (vf:vectorfield) (ords:orders):=
match it with
0 => (nil, nil)
|S p => if ((longmn (size mm)(getfirstElemseq vf))&& (longmn (size (nth nil mm 0))(getsndElemseq vf)) &&
 (uniq (getfirstElemseq vf)) && (uniq (getsndElemseq vf)) && (norep ords) && (compijCvd vf mm))
   then
match mm1, vf, ords with
|nil , _ , _ => (vf, ords)
|a::nil , _ , nil => let k:= (firstElem1 j a) in
                        let colk1:= (getcol k mm) in
                             if (k < size a)
    then if ((canAddCvd (size mm) (size (nth nil mm 0)) i k vf) == true)
         then if ((canAddOrders i 0 colk1 nil) == true)
                                                 then ((vf ++ ((i, k)::nil)), (addOrders i 0 colk1 nil))
                                             else (genDvfOrders p i (j+1) mm (a::nil) vf nil)
     else (genDvfOrders p i (j+1) mm (a::nil) vf nil)
    else (vf, nil)
|a::nil ,_,e::f => let k := (firstElem1 j a) in
               let colk1 := (getcol k mm) in
                             if (k < size a)
    then if ((canAddCvd (size mm) (size (nth nil mm 0)) i k vf) == true)
     then if ((canAddOrders i 0 colk1 (e::f)) == true)
            then (vf ++((i, k)::nil), (addOrders i 0 colk1 (e::f)))
      else (genDvfOrders p i (j+1) mm (a::nil) vf (e::f))
     else (genDvfOrders p i (j+1) mm (a::nil) vf (e::f))
    else (vf, (e::f))
|a::b, _, nil => let k := (firstElem1 j a) in
                    let colk1 := (getcol k mm) in
                    if (k < size a)
               then if ((canAddCvd (size mm)(size (nth nil mm 0)) i k vf) == true)
           then if ((canAddOrders i 0 colk1 nil) == true)
                              then (genDvfOrders p (i+1) 0 mm b (addcvd i k vf) (addOrders i 0 colk1 nil))
                             else (genDvfOrders p i (j+1) mm (a::b) vf nil)
                       else (genDvfOrders p i (j+1) mm (a::b) vf nil)
  else (genDvfOrders p (i+1) 0 mm (b) vf nil)
|a::b, _, e::f => let k := (firstElem1 j a) in
              let colk1 := (getcol k mm) in
                  if (k < size a)
           then if ((canAddCvd (size mm) (size (nth nil mm 0)) i k vf) ==true)
              then if ((canAddOrders i 0 colk1 (e::f)) == true)
             then (genDvfOrders p (i+1) 0 mm b (addcvd i k vf) (addOrders i 0 colk1 ((e::f))))
           else (genDvfOrders p i (j+1) mm (a::b) vf (e::f))
               else (genDvfOrders p i (j+1) mm (a::b) vf (e::f))
               else (genDvfOrders p (i+1) 0 mm (b) vf (e::f))
end
else (nil, nil)
end.


Functional Scheme genDvfOrders_ind := Induction for genDvfOrders Sort Prop.



End vectors.




Section genDvfOrd.


Definition genDvf (ss: matZ2):=
match ss with
|nil => nil
|a::b => let dvforders:= (genDvfOrders ((size ss)*(size a)+1) 0 0 (a::b) (a::b) nil nil) in
           if (prop_cat dvforders.2) then (dvforders.1) else nil

end.



Definition genOrders (ss: matZ2):=
match ss with
|nil => nil
|a::b => let ords:= (snd (genDvfOrders ((size ss)*(size a)+1) 0 0 (a::b) (a::b) nil nil)) in
            if (prop_cat ords) then ords else nil
end.

End genDvfOrd.

Close Scope ring_scope.



Section matrix_reduced.



Section REORDERDVF.


Definition insert_sort_g (ord:orders)(s : seq (nat * nat)) := insert_sort glMax s ord.


Definition dvford (ss:matZ2):= insert_sort_g (genOrders ss)(genDvf ss).


End REORDERDVF.




Section REORDERMATRIX.

Definition fill s n:= s ++ (filter [pred i | i \notin s] (iota 0 n)).


Definition take_rows_s (s:seq nat) (M: matZ2):= map (nth nil M) s.


Definition take_row_s (s:seq nat)(l:seq bool):=
  map (nth false l) s.



Definition take_columns_s (s:seq nat) (M: matZ2):=
  map (take_row_s s) M.


Definition reorderM (s1 s2: seq nat)(M: matZ2):=
  (take_columns_s s2 (take_rows_s s1 M)).


Definition reorderM_dvf (dvf:vectorfield)(M: matZ2):=
  reorderM (fill (getfirstElemseq dvf) (size M))
     (fill (getsndElemseq dvf) (size (head [::] M))) M.



End REORDERMATRIX.



Section GETMATRIXREDUCED.

Variable m1:nat.
Variable m: matZ2.

Definition epsilonseq := ulsubseqmx m1 m1 m.
Definition betaseq := drsubseqmx m1 m1 m.
Definition phiseq := ursubseqmx m1 m1 m.
Definition psiseq := dlsubseqmx m1 m1 m.

Definition getMatrixReduced :=
match m with
|nil => nil
|a::b => let lm := (size (a::b)) in
         let n := (size a) in
          if ((m1 == lm) || (m1 == n))
            then nil
            else subseqmx betaseq (mulseqmx m1 (n - m1) (mulseqmx m1 m1 psiseq
         (cfast_invmx m1 epsilonseq)) phiseq)
end.



Definition getMatrixReduced_2 :=
match m with
|nil => nil
|a::b => let lm := (size (a::b)) in
         let n := (size a) in
          if ((m1 == lm) || (m1 == n))
            then nil
            else if (@const_seqmx _ Z2 (lm - m1) m1 false) == phiseq
                 then betaseq
                 else
subseqmx betaseq (mulseqmx (lm - m1) m1 (mulseqmx m1 m1 psiseq
         (cfast_invmx m1 epsilonseq)) phiseq)
end.


End GETMATRIXREDUCED.



Definition matrixReduced (m:matZ2) :=
match m with
|nil => nil
|_ => let cvd := dvford m in
      getMatrixReduced (size cvd) (reorderM_dvf cvd m)
end.


End matrix_reduced.




End definitions.