Module triangular_rs

Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div choice fintype.
Require Import finfun finset ssralg perm zmodp seqmatrixCR.
Require Import rs_definitions aux_lemmas advf_type advf_ord_triangular triangular.
Require Import Recdef matrix rs_admissible boolF2 cssralg rs_dvf.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Open Local Scope ring_scope.



Section Triangular_ulsubseqmx.


Lemma compij_M_ulsubseqmx M k: forall i j, i < k -> j < k ->
  compij i j M = compij i j (take k M).

Lemma compij_M_ulsubseqmx2 M k: forall i j, i < k -> j < k ->
  k <= size M ->compij i j M = compij i j (map (take k) M).



Lemma compij_M_ulsubseqmx1 M k: forall i j, i < k -> j < k ->
  k <= size M -> compij i j M = compij i j (ulsubseqmx k k M).



Lemma size_dvf_reorderM dvfo M:
size dvfo <= size (reorderM_dvf dvfo M).



Lemma diagonalis1_ulsubseqmx dvf M ords:
  let n:= size dvf in
  Vecfieldadm M dvf ords ->
  (forall k, k < n ->
   compij k k (ulsubseqmx n n (reorderM_dvf dvf M)) = true).


Lemma diagonalis1_ulsubseqmx_dvford (dvf:vectorfield) m1 n1 (M:matZ2):
is_matrix m1 n1 M ->
let dvf := dvford M in
let n:= size dvf in
  (forall k, 0 <= k < (size dvf) ->
   compij k k (ulsubseqmx n n (reorderM_dvf dvf M)) = true).




Lemma onDiagonal0_ulsubseqmx (M:matZ2)(dvfo:vectorfield) ords:
  let n := size dvfo in
  Vecfieldadm M dvfo ords ->
  (forall (r s:nat), (r< n) && (s < n) && (r < s) ->
    compij r s (ulsubseqmx n n (reorderM_dvf dvfo M)) = false).


Lemma onDiagonal0_ulsubseqmx_dvford (n:nat)(M:matZ2)(dvfo:vectorfield):
  is_matrix n n M ->
let dvfo := dvford M in
  let n := size dvfo in
  (forall (r s:nat), (r< n) && (s < n) && (r < s) ->
    compij r s (ulsubseqmx n n (reorderM_dvf dvfo M)) = false).



End Triangular_ulsubseqmx.



Section triangular_seq_ulsubseq.

Definition lower_triangular_seq n (M:matZ2) :=
  (forall k, k < (n+1) -> (compij k k M) = true) /\
  (forall r s, (r < (n+1)) && (0 <= s < (n+1)) && (r < s) -> (compij r s M) = false).


Lemma lower_triangular_seq_ulsubseqmx_rs M dvf ords:
  let n:= ((size dvf)%N)%N in
  0 < n ->
  Vecfieldadm M dvf ords ->
  lower_triangular_seq (size dvf - 1) (ulsubseqmx n n (reorderM_dvf dvf M)).


End triangular_seq_ulsubseq.



Section triangular_ulsubseq.

Lemma eq_nat_of_ord_eq_ord n (i j:'I_n) : (nat_of_ord i)==(nat_of_ord j) -> i==j.


Lemma lower_triangular_seqE : forall n (M:'M_(n+1)),
   lower_triangular_seq n (seqmx_of_mx bool_cunitRingType M) <-> (lower_triangular M).


Section identity_lemmas.



Variables m n : nat.

Local Open Scope ring_scope.


Definition boolseqtoF2 (s : seq bool) :=
map (fun i => if (i == false) then 0:'F_2 else 1:'F_2) s.


Definition mx_of_seqmx (M:seqmatrix bool_cunitRingType) :=
  \matrix_(i < m, j < n) nth (0:'F_2) (boolseqtoF2 (rowseqmx M i)) j.



Lemma trans_mx_of_seqmx (M : seqmatrix bool_cunitRingType) :
  [/\ m = size M & forall i, i < m -> size (rowseqmx M i) = n] -> forall (i : 'I_m) (j:'I_n),
  M i j = trans (mx_of_seqmx M i j).


Lemma seqmx_of_mx_mx_of_seqmx: forall (M : seqmatrix bool_cunitRingType),
  [/\ m = size M & forall i, i < m -> size (rowseqmx M i) = n] ->
   (@seqmx_of_mx _ bool_cunitRingType m n (mx_of_seqmx M)) = M.


End identity_lemmas.




Lemma lower_triangular_ulsubseqmx_rs M dvf ords:
  let n:= ((size dvf)%N - 1%N)%N in
  dvf!=[::] ->
  Vecfieldadm M dvf ords ->
  lower_triangular (mx_of_seqmx (n+1) (n+1) (ulsubseqmx (n+1) (n+1) (reorderM_dvf dvf M))).

Lemma lower_triangular_det_1 M dvf ords:
  let n:= ((size dvf)%N - 1%N)%N in
  let A:= (mx_of_seqmx (n+1) (n+1) (ulsubseqmx (n+1) (n+1) (reorderM_dvf dvf M))) in
  dvf!= [::] ->
  Vecfieldadm M dvf ords -> \det A = 1.


End triangular_ulsubseq.