Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div choice fintype.
Require Import finfun finset ssralg perm zmodp seqmatrixCR rs_definitions advf_type.
Require Import Recdef.
Set Implicit Arguments.
Unset Strict Implicit.
Import Prenex Implicits.
Section ordered_proofs.
Variable f:
nat ->
orders ->
nat.
Lemma sizedvf_getfirst (
dvf:
vectorfield):
size dvf =
size (
getfirstElemseq dvf).
Proof.
by elim H: dvf; last by rewrite /= => ->.
Qed.
Lemma sizedvf_getsnd (
dvf:
vectorfield):
size dvf =
size (
getsndElemseq dvf).
Proof.
by elim H: dvf; last by rewrite /= => ->.
Qed.
Fixpoint schemaseqnatm (
v:
seq(
nat*
nat))(
m:
nat):=
match v with
|
nil => 0
|
v1::
v2=> (
schemaseqnatm v2 (
m -1))
end.
Functional Scheme schemaseqnatm_ind:=
Induction for schemaseqnatm Sort Prop.
Lemma head_ordered_insert_sort_m x s m ords:
m <
size (
getfirstElemseq (
x::
s)) ->
ordered f (
x::
s)
ords ->
f (
fst x)
ords >=
f (
nth 0 (
getfirstElemseq (
x::
s))
m)
ords.
Proof.
functional induction (schemaseqnatm s m); first by case: m.
move=> H1 H2.
have H3: (ordered f (x :: v2) ords).
case H3: v2=>[|v21 v22]; first by done.
move: H2; rewrite H3 /=; move/andP =>[ H4 H5]; move: (andP H5)=>[h6 ->].
by move: (leq_trans h6 H4) => ->.
case H: m=>[|m1]; first by done.
case H5: m1 =>[|m2]; first by move: H2; move/andP =>[-> _].
have H11: (m - 1 < size (getfirstElemseq (x :: v2))); first by move:H1; rewrite H H5.
move: (IHn H11 H3)=> H4.
case H6: v2=>[|v21 v22]; first by move:H1; rewrite H H5 H6.
by move:H4; rewrite H H5 H6 subn1 => ->.
Qed.
Fixpoint schemanthmp (
v:
seq(
nat*
nat))(
m p:
nat):=
match v with
|
nil => 0
|
a::
b => (
schemanthmp b (
m -1)(
p-1))
end.
Functional Scheme schemanthmp_ind:=
Induction for schemanthmp Sort Prop.
Lemma lengthmax_gen m p dvfo ords:
let n :=
size dvfo in
ordered f dvfo ords ->
(
m <
n) && (
p <
n) &&(
m <
p) ->
f (
nth 0 (
getfirstElemseq dvfo)
m)
ords >=
f (
nth 0 (
getfirstElemseq dvfo)
p)
ords.
Proof.
functional induction (schemanthmp dvfo m p); first by done.
move=> H1; move/andP=>[H2 H3]; move: (andP H2)=>[H5 H4].
case H6: p =>[|p1]; first by move:H3; rewrite H6.
case H7: m=>[|m1].
move:H4; rewrite H6 sizedvf_getfirst => H8; apply: (head_ordered_insert_sort_m H8 H1).
have H8: (ordered f b ords); first by move: H1; by case H8: b; last by move/andP =>[_ H10].
have H9: ((m - 1 < size b) && (p - 1 < size b) && (m - 1 < p - 1)).
by move:H4 H5 H3; rewrite /= H6 H7 !subn1 /= !ltnS => -> -> ->.
by move:(IHn H8 H9); rewrite H6 H7 !subn1.
Qed.
End ordered_proofs.
Section perm.
Variable f:
nat ->
orders ->
nat.
Lemma nth_perm_in (
a:
nat)
l l1 :
a \
in l ->
perm_eq l l1 ->
a \
in l1.
Proof.
move=> h1 h2; move: (perm_eq_mem h2)=> h3.
by move: (h3 a) h1 => ->.
Qed.
Lemma perm_insert n (
ord:
orders)(
s:
seq (
nat *
nat)) :
perm_eq (
n::
s) (
insert f n s ord).
Proof.
functional induction (insert f n s ord); try by done.
rewrite -cat1s -{1}(cat1s a).
have H1 : perm_eq ([:: n] ++ [:: a] ++ b) ([:: a] ++ [:: n] ++ b).
by rewrite !catA perm_cat2r perm_catC.
have H2 : perm_eq ([:: a] ++ [:: n] ++ b) (a:: insert f n b ord); last by apply : perm_eq_trans H1 H2.
by rewrite -(cat1s a (insert f n b ord)) perm_cat2l cat1s.
Qed.
Lemma perm_insert_sort ord (
s:
seq (
nat *
nat)):
perm_eq s (
insert_sort f s ord).
Proof.
elim H: s =>[|s1 s2]; first by done.
rewrite /= -/insert_sort => H1.
case H2 : (insert_sort f s2 ord) => [|t s3].
rewrite H2 in H1.
have -> : s2 = nil; first by move : (perm_eq_size H1); rewrite /=; apply (size0nil).
by rewrite perm_eq_refl.
have H4 : perm_eq (s1::s2) (s1::insert_sort f s2 ord); first by rewrite perm_cons.
have H5 : perm_eq (s1::insert_sort f s2 ord) (s1::(t::s3)); first by rewrite -H2.
have H6 : perm_eq (s1::s2) (s1::(t::s3)); first by apply : perm_eq_trans H4 H5.
have H7 : perm_eq (s1::(t::s3)) (insert f s1 (t::s3) ord); first by apply : perm_insert.
by apply : perm_eq_trans H6 H7.
Qed.
Lemma perm_insert_fst n (
ord:
orders)(
s:
seq (
nat *
nat)) :
perm_eq (
getfirstElemseq (
n::
s)) (
getfirstElemseq (
insert f n s ord)).
Proof.
functional induction (insert f n s ord); try by done.
rewrite -cat1s -{1}(cat1s a).
have H1 : perm_eq (getfirstElemseq([:: n] ++ [:: a] ++ b)) (getfirstElemseq([:: a] ++ [:: n] ++ b)).
by rewrite !cat1s /= -cat1s -(cat1s a.1) perm_catCA.
have H2 : perm_eq (getfirstElemseq ([:: a] ++ [:: n] ++ b)) (getfirstElemseq (a:: insert f n b ord));
last by apply : perm_eq_trans H1 H2.
by rewrite cat1s /= perm_cons; apply: IHl.
Qed.
Lemma perm_insert_sort_fst (
ord:
orders)(
s:
seq (
nat *
nat)):
perm_eq (
getfirstElemseq s) (
getfirstElemseq (
insert_sort f s ord)).
Proof.
elim H: s =>[|s1 s2]; first by done.
move=> H1; rewrite /= -/insert_sort.
case H2 : (insert_sort f s2 ord) => [|t s3].
rewrite /insert; rewrite H2 in H1.
have -> : s2 = nil; last by rewrite perm_eq_refl.
move : (perm_eq_size H1) => H3.
move: (size0nil H3); by case H4: s2.
have H4 : perm_eq (getfirstElemseq (s1::s2)) (getfirstElemseq(s1::insert_sort f s2 ord));
first by rewrite perm_cons.
have H5 : perm_eq (getfirstElemseq (s1::insert_sort f s2 ord)) (getfirstElemseq (s1::(t::s3)));
first by rewrite -H2.
have H6 : perm_eq (getfirstElemseq (s1::s2)) (getfirstElemseq (s1::(t::s3)));
first by apply: perm_eq_trans H4 H5.
have H7 : perm_eq (getfirstElemseq (s1::(t::s3))) (getfirstElemseq (insert f s1 (t::s3) ord));
first by apply : perm_insert_fst.
by apply : perm_eq_trans H6 H7.
Qed.
Lemma perm_insert_snd n (
ord:
orders)(
s:
seq (
nat *
nat)) :
perm_eq (
getsndElemseq (
n::
s)) (
getsndElemseq (
insert f n s ord)).
Proof.
functional induction (insert f n s ord); try by done.
rewrite -cat1s -{1}(cat1s a).
have H1 : perm_eq (getsndElemseq([:: n] ++ [:: a] ++ b)) (getsndElemseq([:: a] ++ [:: n] ++ b)).
by rewrite !cat1s /= -cat1s -(cat1s a.2) perm_catCA.
have H2 : perm_eq (getsndElemseq ([:: a] ++ [:: n] ++ b)) (getsndElemseq (a:: insert f n b ord));
last by apply : perm_eq_trans H1 H2.
by rewrite cat1s /= perm_cons; apply: IHl.
Qed.
Lemma perm_insert_sort_snd (
ord:
orders)(
s:
seq (
nat *
nat)):
perm_eq (
getsndElemseq s) (
getsndElemseq (
insert_sort f s ord)).
Proof.
elim H: s =>[|s1 s2]; first by done.
move=> H1; rewrite /= -/insert_sort.
case H2 : (insert_sort f s2 ord) => [|t s3].
rewrite /insert; rewrite H2 in H1.
have -> : s2 = nil; last by rewrite perm_eq_refl.
move : (perm_eq_size H1) => H3.
move: (size0nil H3); by case H4: s2.
have H4 : perm_eq (getsndElemseq (s1::s2)) (getsndElemseq(s1::insert_sort f s2 ord));
first by rewrite perm_cons.
have H5 : perm_eq (getsndElemseq (s1::insert_sort f s2 ord)) (getsndElemseq (s1::(t::s3)));
first by rewrite -H2.
have H6 : perm_eq (getsndElemseq (s1::s2)) (getsndElemseq (s1::(t::s3)));
first by apply: perm_eq_trans H4 H5.
have H7 : perm_eq (getsndElemseq (s1::(t::s3))) (getsndElemseq (insert f s1 (t::s3) ord));
first by apply : perm_insert_snd.
by apply : perm_eq_trans H6 H7.
Qed.
End perm.
Section indvford_genDvf.
Lemma indvford_genDvf x M:
x\
in dvford M ->
x \
in genDvf M.
Proof.
move: ((perm_insert_sort glMax (genOrders M) (genDvf M))) =>H2 H3.
move: (perm_eq_mem H2) => H4.
by move: (H4 x) H3 => ->.
Qed.
Lemma ingenDvf_dvford x M :
x \
in genDvf M ->
x \
in dvford M.
Proof.
move: ((perm_insert_sort glMax (genOrders M) (genDvf M))) =>H2 H3.
move: (perm_eq_mem H2) => H4.
by move: (H4 x) H3 => ->.
Qed.
End indvford_genDvf.
Section reorderR.
Lemma reorderR_ij s (
M:
matZ2)
i j:
i \
in s ->
compij i j M =
compij (
index i s)
j (
take_rows_s s M).
Proof.
rewrite /take_rows_s /compij /= => H4.
have ->:((nth [::] M i) = (nth [::] (map (nth [::] M) s) (index i s))); last by done.
rewrite (nth_map 0%N); first by rewrite (nth_index).
move: (index_size i s)=> H3.
by move: H4; rewrite -index_mem.
Qed.
End reorderR.
Section reorderC.
Lemma reorderC_ij s (
M:
matZ2)
i j:
i <
size M ->
j \
in s ->
compij i j M =
compij i (
index j s) (
take_columns_s s M).
Proof.
move=> H2 H4.
by rewrite /take_columns_s /compij /= (nth_map nil) ?(nth_map 0%N) ?(nth_index) ?index_mem.
Qed.
End reorderC.
Section reorderM.
Lemma inl_infstl (
x1 x2:
nat)(
l:
vectorfield):
(
x1,
x2)\
in l ->
x1 \
in (
getfirstElemseq l).
Proof.
elim H: l =>[|l1 l2]; first by rewrite in_nil.
move=> H1; rewrite inE;rewrite /= inE; move/orP=>[H2|H2].
move: H2; rewrite (surjective_pairing l1) xpair_eqE; move/andP=>[H2 _].
by apply/orP; left.
by apply/orP; right; move: (H1 H2).
Qed.
Lemma inl_insndl (
x1 x2:
nat)(
l:
vectorfield):
(
x1,
x2)\
in l ->
x2 \
in (
getsndElemseq l).
Proof.
Proof.
elim H: l =>[|l1 l2]; first by rewrite in_nil.
move=> H1; rewrite inE;rewrite /= inE; move/orP=>[H2|H2].
move: H2; rewrite (surjective_pairing l1) xpair_eqE; move/andP=>[_ H3].
by apply/orP; left.
by apply/orP; right; move: (H1 H2).
Qed.
Lemma inl_infilll (
x1 n:
nat)(
l:
seq nat):
x1 \
in l ->
x1 \
in (
fill l n).
Proof.
by rewrite /fill => H; rewrite mem_cat; apply/orP; left.
Qed.
Lemma reorderR_noempty (
M:
matZ2)(
l:
seq nat):
M !=[::]->
l!=[::] ->
take_rows_s l M != [::].
Proof.
by case H1: M=>[|m1 m2]; last by case H2: l=>[|l1 l2].
Qed.
Lemma reorderC_noempty (
M:
matZ2)(
l:
seq nat):
M !=[::]->
l!=[::] ->
take_columns_s l M != [::].
Proof.
by case H1: M=>[|m1 m2]; last by case H2: l=>[|l1 l2].
Qed.
Lemma ijdvf_Mij1 s1 s2 (
M:
matZ2)
i j:
j \
in s2 ->
i \
in s1 ->
compij i j M =
compij (
index i s1) (
index j s2) (
reorderM s1 s2 M).
Proof.
move=> H6 H7.
rewrite (reorderR_ij M j H7).
have H8:((index i s1) < size (take_rows_s s1 M)); first by rewrite size_map index_mem.
by rewrite (reorderC_ij H8 H6).
Qed.
End reorderM.
Section reorderM_nth.
Lemma compijrsM1 s1 s2 (
M:
matZ2)
i j:
i <
size s1 ->
j <
size s2 ->
uniq s1 ->
uniq s2 ->
compij i j (
reorderM s1 s2 M) =
compij (
nth 0
s1 i) (
nth 0
s2 j)
M.
Proof.
move=> H10 H11 H8 H9.
have H6: (nth 0 s1 i) \in s1; first by apply: (mem_nth 0 H10).
have H7: (nth 0 s2 j) \in s2; first by apply: (mem_nth 0 H11).
by rewrite (ijdvf_Mij1 M H7 H6) (index_uniq 0 H10 H8) (index_uniq 0 H11 H9).
Qed.
End reorderM_nth.