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 rs_admissible advf_type.
Require Import Recdef.
Set Implicit Arguments.
Unset Strict Implicit.
Import Prenex Implicits.
Section proofs_conditions_of_matrixReorder.
Section diagonal1.
Fixpoint schema_nth_dvf (
k:
nat)(
dvf:
vectorfield):=
match dvf with
|
nil =>
dvf
|
a::
b =>
schema_nth_dvf (
k-1)
b
end.
Functional Scheme schema_nth_dvf_ind:=
Induction for schema_nth_dvf Sort Prop.
Lemma ij_kget (
i j k:
nat)(
dvf:
vectorfield):
(
i,
j) \
in dvf ->
uniq (
getfirstElemseq dvf) ->
uniq (
getsndElemseq dvf)->
k =
index i (
getfirstElemseq dvf) ->
k =
index j (
getsndElemseq dvf).
Proof.
functional induction (schema_nth_dvf k dvf); try by done.
rewrite /= => HH H1 H2.
move: (andP H1)(andP H2) => [H11 H3] [H21 H4].
move: HH; rewrite inE; move/orP=>[H5|H5].
move: (eqP H5)=> <-; by have ->: (i==i); last by have ->: (j == j).
have ->: (_x.1 == i) = false.
case H7:((_x.1 == i)); last by done.
move: (inl_infstl H5) => H8.
by move: H11; rewrite (eqP H7) H8.
have ->: (_x.2 == j)= false.
case H7:((_x.2 == j)); last by done.
move: (inl_insndl H5)=> H8.
by move: H21; rewrite (eqP H7) H8.
move => H8.
have H9:(k - 1 = index i (getfirstElemseq b)); first by rewrite H8 subn1 /=.
move: (IHv H5 H3 H4 H9).
move:H8; case H10: k=>[|k1]; first by done.
by rewrite /= => ->; rewrite subn1 /= => ->.
Qed.
Lemma exists_ijdvf (
i:
nat)(
dvf:
vectorfield):
i \
in (
getfirstElemseq dvf) ->
exists j:
nat, (
i,
j) \
in dvf.
Proof.
elim H1: dvf=>[|d1 d2]; first by done.
move=> HI; rewrite inE; move/orP=>[H2|H2].
exists d1.2; rewrite inE; apply/orP; left.
by move: (eqP H2) => ->; rewrite (surjective_pairing d1).
move: (HI H2); intros (j, H4).
by exists j; rewrite inE H4 Bool.orb_true_r.
Qed.
Lemma diagonalis1_gen dvf M ords:
Vecfieldadm M dvf ords ->
(
forall k, 0 <=
k < (
size dvf) ->
compij k k (
reorderM_dvf dvf M) =
true).
Proof.
rewrite /reorderM_dvf (sizedvf_getfirst dvf) => H1 k H4.
move: (andP H4)=>[H41 H42].
move: (mem_nth 0 H42)=> H6.
move:H1; rewrite /Vecfieldadm.
move=> [H10 H11]; move:H11 =>[_ H13]; move:H13 =>[H7 H13]; move:H13 =>[H15 H13]; move:H13 =>[H16 _].
move: (index_uniq 0 H4 H7) => H8.
move: (exists_ijdvf H6); intros (j, H61).
move: H8; move/eqP; rewrite eq_sym => H8.
move: (inl_infstl H61) => H31.
move: (inl_insndl H61)=> H5.
have H71: (k == index j (getsndElemseq dvf)); first by apply/eqP; apply:(ij_kget H61 H7 H15 (eqP H8)).
move: (H16 (nth 0 (getfirstElemseq dvf) k) j H61) => H81.
move: (inl_infilll (size M) H31) => H20.
move: (inl_infilll (size (head [::] M)) H5) => H21.
move: (ijdvf_Mij1 M H21 H20).
have H22: (k == (index (nth 0 (getfirstElemseq dvf) k)
(fill (getfirstElemseq dvf) (size M)))); first by rewrite /fill index_cat H31 H8.
have H23: (k == (index j (fill (getsndElemseq dvf) (size (head [::] M))))).
by rewrite /fill index_cat H5 H71.
by rewrite -(eqP H22) -(eqP H23) H81 => <-.
Qed.
End diagonal1.
Section zerosonDiagonal.
Lemma nthj_nthi (
s:
nat)(
dvfo:
vectorfield):
s <
size (
getsndElemseq dvfo) ->
let b := (
nth 0 (
getsndElemseq dvfo)
s)
in
let a:= (
nth 0 (
getfirstElemseq dvfo)
s)
in
b \
in (
getsndElemseq dvfo) -> (
a,
b) \
in dvfo.
Proof.
functional induction (schema_nth_dvf s dvfo); first by rewrite in_nil.
case H1: k=>[|k1]; first by move => _ _; rewrite inE (surjective_pairing _x); apply/orP; left.
rewrite inE; rewrite H1 /= in IHv.
rewrite /= -(addn1 k1) -(addn1 (size (getsndElemseq b))) ltn_add2r => H3.
move/orP=>[H2|H2];last first.
rewrite inE; apply/orP; right.
by move: IHv; rewrite subn1 /= => IHv; apply: (IHv H3 H2).
move: (mem_nth 0 H3) => H4.
move: IHv; rewrite subn1 /= => IHv; move: (IHv H3 H4)=> H5.
by rewrite inE; apply/orP; right.
Qed.
Fixpoint ispath ir ii ords:=
match ords with
|
nil =>
false
|
a::
b =>
if ((
ir \
in a) && (
ii \
in a)&& (
head 0%
N a ==
ir))
then true
else ispath ir ii b
end.
Lemma ispath_exists ir ii ords :
ispath ir ii ords ->
exists p:
seq nat, (
p \
in ords) && (
ir \
in p) && (
ii \
in p) && (
head 0%
N p ==
ir).
Proof.
elim H: ords =>[|o1 o2]; first by done.
move=> H1; rewrite /= -/ispath.
case H2: ((ir \in o1) && (ii \in o1) && (head 0%N o1 == ir)).
move => _; exists o1; rewrite inE; by have -> //: (o1 == o1).
move=> H3; move: (H1 H3); intros (p, H4); exists p; rewrite inE; move: H4.
by case:(p \in o2); first by rewrite Bool.orb_true_r.
Qed.
Lemma innorepfalse_gen (
ii:
nat)(
p:
seq nat)
ords:
norep ords -> (
ii::
p) \
in ords ->
ii\
in p ->
false.
Proof.
elim H1:ords=>[|o1 o2]; first by done.
move=> HI /=; move/andP=>[H2 H3].
rewrite inE; move/orP=>[H41| H42]; first by move=> H5; move:H2; rewrite -(eqP H41) /= H5.
have H6: (norep o2); first by case H6: o2; rewrite /norep -H6.
by apply: (HI H6).
Qed.
Lemma uniq_nthdif r s (
l:
seq nat): 0 <=
s -> 0 <=
r ->
r <
s ->
s <
size l ->
r <
size l ->
uniq l ->
nth 0
l s!=
nth 0
l r.
Proof.
case H:(nth 0 l s!= nth 0 l r); first by done.
move:H; move/eqP => H1 H8 H9 H10 H2 H3 H4.
move: H1; move/eqP.
move: (nth_uniq 0 H2 H3 H4) => ->.
case H11: s =>[|s1]; first by move: H10; rewrite H11.
case H12: r =>[|r1]; first by move: H9; rewrite H12.
rewrite /= => H13; move: H10; rewrite H11 H12.
by move: (eqP H13)=> ->; rewrite ltnn.
Qed.
Lemma lengthmax_exist (
ir n:
nat)
ords:
0 <
n ->
glMax ir ords =
n ->
(
exists s, (
s \
in ords) && (
head 0
s ==
ir) && (
size s ==
n)).
Proof.
elim ords =>[|o1 o2]; first by rewrite /glMax //= => H1 H2; move:H1; rewrite H2 ltnn.
rewrite /glMax /=.
case H2:(head 0 o1 == ir); last first.
move=> HI H1 H3; move: (HI H1 H3).
intros (s, H); move:(andP H)=>[H4 H5]; move:(andP H4) =>[H7 H6].
by exists s; rewrite inE H7 H5 H6 !Bool.andb_true_r Bool.orb_true_r.
move=> HI H1; rewrite /= {1}/maxn.
case H3:(maxn 0 (size o1) < lengthMax1 (getfirstE ir o2)).
move=> H4; move: (HI H1 H4).
intros (s, H); move:(andP H)=>[H41 H5]; move:(andP H41) =>[H7 H6].
by exists s; rewrite inE H7 H5 H6 //= !Bool.andb_true_r Bool.orb_true_r.
rewrite /maxn; case H4:(0 < size o1); last by move=> H5; move:H1; rewrite H5 ltnn.
by move/eqP => H5; exists o1; rewrite /= H2 H5 inE !Bool.andb_true_r; apply/orP; left.
Qed.
Lemma ltn_leq_trans a b c :
a <
b ->
b <=
c ->
a <
c.
Proof.
move => H1.
rewrite leq_eqVlt; move/orP => [H2 | H2].
by rewrite -(eqP H2).
by apply : (ltn_trans H1 H2).
Qed.
Lemma lengthmax_size (
ii n:
nat)
s ords:
size s =
n -> (
ii::
s)\
in ords ->
n <
glMax ii ords.
Proof.
elim H: ords =>[|o1 o2]; first by done.
move=> H1 H2; rewrite inE; move/orP=>[H3|H3].
move: (eqP H3) => <-.
rewrite /glMax /=.
have ->: ii == ii. by apply/eqP.
rewrite /=. move : (leq_maxl (maxn 0 (size s).+1) (lengthMax1 (getfirstE ii o2))).
rewrite H2 /=.
by apply : leq_ltn_trans.
move: (H1 H2 H3); rewrite /glMax /=.
case H4:(head 0 o1 == ii); last by done.
rewrite /= -/lengthMax1.
move : (leq_maxr (maxn 0 (size o1)) (lengthMax1 (getfirstE ii o2))) => H5 H6.
by move : (ltn_leq_trans H6 H5).
Qed.
Lemma length_a_b a b ords:
norep ords ->
(
forall (
a :
nat_eqType) (
b :
nat) (
s :
seq nat_eqType) (
p :
seq nat),
a ::
s \
in ords ->
last 0
s =
b ->
b ::
p \
in ords -> (
a ::
s) ++
p \
in ords) ->
(
a::
b::
nil)\
in ords ->
glMax a ords >
glMax b ords.
Proof.
move=> H1 H2 H3.
case H4:(glMax b ords)=>[|n1]; last first.
move:(lengthmax_exist (ltn0Sn n1) H4).
intros (s, H); move:(andP H)=>[H5 H6]; move:(andP H5)=>[H7 H8].
case H9: s=>[|s1 s2]; first by move:H6; rewrite H9.
rewrite H9 in H6 H7 H8.
have H10:(last 0 [::b] = s1); first by rewrite /=; move:H8; rewrite /head; move/eqP => ->.
move:(@H2 a s1 [::b] s2 H3 H10 H7).
rewrite cat_cons cat1s; move: H10; rewrite /= => -> H11.
by move:(lengthmax_size (eqP H6) H11).
move: H1 H3 H4 H2; elim H5: ords =>[|o1 o2]; first by done.
rewrite -H5 => H1 H2 H3 H4 H6.
case H7: (size [::b]) => [|nn]; first by done.
by move:(lengthmax_size H7 H3); apply: (ltn_trans (ltn0Sn nn)).
Qed.
Lemma nth_fill n s1 s:
s <
size s1 ->
nth 0
s1 s =
nth 0 (
fill s1 n)
s.
Proof.
by rewrite /fill nth_cat => ->.
Qed.
Lemma onDiagonal0_gen (
n:
nat)(
M:
matZ2)(
dvfo:
vectorfield)
ords:
let n :=
size dvfo in
Vecfieldadm M dvfo ords ->
(
forall (
r s:
nat), (0<=
r<
n) && (0<=
s <
n) && (
r <
s) ->
compij r s (
reorderM_dvf dvfo M ) =
false).
Proof.
rewrite /reorderM_dvf /Vecfieldadm.
move=> [HH1 HH2]; move:HH2 =>[HH2 HH3]; move:HH3 =>[HH3 HH4]; move:HH4 =>[HH4 HH5];
move:HH5 =>[HH5 HH6]; move:HH6 =>[HH6 HH7]; move:HH7 =>[HH7 HH8];
move:HH8 =>[HH8 HH9].
move=> r s; move/andP => [H3 H4]; move: (andP H3) =>[H5 H6].
have H7: M!=[::].
case H71: M=>[|m1 m2]; last by done.
move:HH1; rewrite H71 /=.
case H8:((getfirstElemseq dvfo))=>[|t s1 ]; last by case h:t.
move: H8 H5; by case H9: dvfo=>[|v1 v2]; first by case h:r.
move:(andP H5)=>[_ h52]; move:(andP H6)=>[_ h62].
move:H5 H6; rewrite {1}sizedvf_getfirst sizedvf_getsnd=> H8 H9.
have H20:(r < size (fill (getfirstElemseq dvfo) (size M))).
rewrite /fill size_cat; move:(andP H8)=>[_ H82].
case hh:(size (filter [pred i | i \notin getfirstElemseq dvfo] (iota 0 (size M))))=>[|n1].
by rewrite addn0.
have hh1:(size (getfirstElemseq dvfo) < size (getfirstElemseq dvfo) + n1.+1).
by rewrite -{1}(addn0 (size (getfirstElemseq dvfo))) ltn_add2l.
apply:(ltn_trans H82 hh1).
have H21:(s < size (fill (getsndElemseq dvfo) (size (head [::] M)))).
rewrite /fill size_cat; move:(andP H9)=>[_ H82].
case hh:(size (filter [pred i | i \notin getsndElemseq dvfo] (iota 0 (size (head [::] M)))))=>[|n1].
by rewrite addn0.
have hh1:(size (getsndElemseq dvfo) < size (getsndElemseq dvfo) + n1.+1).
by rewrite -{1}(addn0 (size (getsndElemseq dvfo))) ltn_add2l.
apply:(ltn_trans H82 hh1).
have H24: (uniq (fill (getfirstElemseq dvfo) (size M))).
rewrite /fill.
have hh: (uniq (iota 0 (size M))); first by rewrite iota_uniq.
move: (filter_uniq [pred i | i \notin getfirstElemseq dvfo] hh).
rewrite cat_uniq HH3 Bool.andb_true_l => ->; rewrite Bool.andb_true_r.
apply/hasPn.
move=> x; rewrite inE mem_filter; move/andP=>[h1 h2].
by move: h1; rewrite /=.
have H25: (uniq (fill (getsndElemseq dvfo) (size (head [::] M)))).
rewrite /fill.
have hh: (uniq (iota 0 (size (head [::] M)))); first by rewrite iota_uniq.
move: (filter_uniq [pred i | i \notin getsndElemseq dvfo] hh).
rewrite cat_uniq HH4 Bool.andb_true_l => ->; rewrite Bool.andb_true_r.
apply/hasPn.
move=> x; rewrite inE mem_filter; move/andP=>[h1 h2].
by move: h1; rewrite /=.
rewrite (compijrsM1 M H20 H21 H24 H25); apply/eqP.
set ir:= nth 0 (fill (getfirstElemseq dvfo)(size M)) r.
set ii:= (nth 0 (fill (getfirstElemseq dvfo) (size M)) s).
case H12: (compij ir (nth 0%N (fill (getsndElemseq dvfo)(size (head [::] M))) s) M == false); first by done.
move: (andP H8)(andP H9)=>[H81 H82] [H91 H92].
move: (mem_nth 0 H92)=> H15; move:(nthj_nthi H92 H15) => H16; move: (inl_infstl H16) => H17.
move: H12; move/eqP; move/eqP => H12.
move: H92; rewrite -(sizedvf_getsnd dvfo) (sizedvf_getfirst dvfo) => H201.
move: (uniq_nthdif H91 H81 H4 H201 H82 HH3)=> H34.
move: (nth_fill (size M) H82); rewrite -/ir => HH11.
move: (andP H9)=>[_ H92].
move: (nth_fill (size M) H201); rewrite -/ii => HH12.
move: (nth_fill (size (head [::] M)) H92); rewrite -/ii => HH13.
rewrite HH12 HH13 in H16 H34.
rewrite HH11 in H34.
move: (HH8 ii (nth 0 (fill (getsndElemseq dvfo)(size (head [::] M)))s) ir H16 H34 H12) => H244.
case H18: (ispath ir ii ords).
move: (ispath_exists H18); intros (p, H19).
move: (andP H19)=> [H191 H251]; move: (andP H191)=> [H1911 H193]; move: (andP H1911) => [H195 _].
move:H193 H195; case H26: p =>[|p1 p2]; first by done.
move: (eqP H251); rewrite H26 /= => -> H195 H196.
have H27:(last 0 [::ir] = ir); first by done.
move:(HH9 ii ir [::ir] p2 H244 H27 H196) => H28.
apply:(innorepfalse_gen HH6 H28 H195).
move: (length_a_b HH6 HH9 H244) => H41.
have H42: ((r < size dvfo) && (s < size dvfo) && (r< s)); first by rewrite h52 h62 H4.
move: (lengthmax_gen HH7 H42) => H43.
rewrite -HH11 -HH12 in H41.
by move: (leq_ltn_trans H43 H41); rewrite ltnn.
Qed.
End zerosonDiagonal.
End proofs_conditions_of_matrixReorder.
Section proofs_genDvfOrders_M.
Lemma diagonalis1_dvford (
dvf:
vectorfield)
m n (
M:
matZ2):
is_matrix m n M ->
let dvf :=
dvford M in
(
forall k, 0 <=
k < (
size dvf) ->
compij k k (
reorderM_dvf dvf M) =
true).
Proof.
rewrite /reorderM_dvf.
by move=> H1; apply: (diagonalis1_gen (dvfordisVecfieldadm H1)).
Qed.
Lemma onDiagonal0_dvford m1 n1 (
M:
matZ2)(
dvfo:
vectorfield):
is_matrix m1 n1 M ->
let dvfo :=
dvford M in
let n :=
size dvfo in
(
forall (
r s:
nat), (0<=
r<
n) && (0<=
s <
n) && (
r <
s) ->
compij r s (
reorderM_dvf dvfo M) =
false).
Proof.
rewrite /reorderM_dvf.
by move=> H1; apply: (onDiagonal0_gen (size (dvford M)) (dvfordisVecfieldadm H1)).
Qed.
End proofs_genDvfOrders_M.