Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div choice fintype.
Require Import finset zmodp ssralg rs_definitions aux_lemmas advf_type.
Set Implicit Arguments.
Unset Strict Implicit.
Import Prenex Implicits.
Section rs_properties_dvf_ordered.
Section rs_prop1.
Section rs_prop11.
Lemma longmn_catfirst (
m:
nat)(
vf vf1:
vectorfield):
((
longmn m (
getfirstElemseq (
vf ++
vf1)))) = (((
longmn m (
getfirstElemseq vf))) && ((
longmn m (
getfirstElemseq vf1)))).
Proof.
elim: vf=> [|t s HI]; first by done.
by rewrite /=; case: (t.1 < m).
Qed.
Lemma aux_propsizef a b m1 m2 :
longmn (
size (
a ::
b))
(
getfirstElemseq
(
genDvfOrders (
size (
a ::
b) *
size a).+1
m2 m2 (
a ::
b)
m1 [::] [::]).1).
Proof.
Lemma propSizef (
ss:
matZ2) : (
longmn (
size ss) (
getfirstElemseq (
genDvf ss))).
Proof.
elim H:
ss=> [|
a b HI];
first by done.
rewrite /
genDvf !
addn1.
have H1:
ss =
ss;
first by done.
case HH:(
prop_cat(
genDvfOrders (
size (
a ::
b) *
size a).+1 0 0 (
a ::
b) (
a ::
b) [::] [::]).2);
last by done.
move:
HH=>
_.
set m1:= (
a::
b);
rewrite {-4}/
m1.
by apply :
aux_propsizef.
Qed.
Lemma propSizef_ord (
ss:
matZ2):
longmn (
size ss) (
getfirstElemseq (
dvford ss)).
Proof.
End rs_prop11.
Section rs_prop12.
Lemma longmn_catsnd (
n:
nat)(
vf vf1:
vectorfield):
((
longmn n (
getsndElemseq (
vf ++
vf1)))) = (((
longmn n (
getsndElemseq vf))) && ((
longmn n (
getsndElemseq vf1)))).
Proof.
elim: vf=> [|t s HI]; first by done.
by rewrite /=; case: (t.2 < n).
Qed.
Lemma propSizes_aux r a b m n m1 m2 :
r <
size (
a ::
b) ->
is_matrix m n (
a ::
b) ->
longmn (
size (
nth [::] (
a ::
b)
r))
(
getsndElemseq
(
genDvfOrders (
size (
a ::
b) *
size a).+1
m2 m2 (
a ::
b)
m1 [::] [::]).1).
Proof.
Lemma propSizes m n (
ss:
matZ2)
r :
r <
size ss ->
is_matrix m n ss -> (
longmn (
size (
nth nil ss r)) (
getsndElemseq (
genDvf ss))).
Proof.
elim H:
ss=> [|
a b HI];
first by done.
rewrite /
genDvf !
addn1.
have H1:
ss =
ss;
first by done.
case HH:(
prop_cat(
genDvfOrders (
size (
a ::
b) *
size a).+1 0 0 (
a ::
b) (
a ::
b) [::] [::]).2);
last by done.
move:
HH=>
_.
set m1:= (
a::
b);
rewrite {-6}/
m1.
by apply :
propSizes_aux.
Qed.
Lemma propSizes_ord m n (
ss:
matZ2) :
ss!=[::] ->
is_matrix m n ss ->
(
longmn (
size (
nth nil ss 0)) (
getsndElemseq (
dvford ss))).
Proof.
End rs_prop12.
End rs_prop1.
Section rs_prop2.
Open Local Scope ring_scope.
Lemma compij_in (
i j:
nat)(
vf:
vectorfield)(
ss:
matZ2):
(
i,
j) \
in vf ->
compijCvd vf ss -> (
compij i j ss =
true).
Proof.
elim HH:
vf=>[|
v1 v2 HI];
first by done.
rewrite inE;
move/
orP=> [
H1 |
H2].
move:(
eqP H1) => <- /=.
by move/
andP =>[
H2 _];
move:(
eqP H2).
by move/
andP=>[
_ H4];
apply: (
HI H2 H4).
Qed.
Lemma pairs (
i j i0 j0:
nat): (
i,
j)== (
i0,
j0) -> (
i==
i0)/\ (
j ==
j0).
Proof.
Lemma or_Z2ring (
a: '
F_2): ((
a == 0) \/ (
a== 1)).
Proof.
have H3: 0 \
in '
F_2;
first by done.
have H5: #|'
F_2| = 2;
first by rewrite card_ord.
apply/
orP.
case H6: ((
a == 0) || (
a == 1));
first by done.
case H7:((
a == 0));
first by rewrite H7 in H6.
move:
H6;
rewrite H7 Bool.orb_false_l =>
H8.
have H9: (
a \
in '
F_2);
first by rewrite inE.
have H10: #|'
F_2| = #|[
set x in '
F_2]|;
first by rewrite cardsE.
have H11: #|[
set x in '
F_2]| >= 3.
move: (
cardsD1 a [
set x in '
F_2]);
rewrite inE H9.
move: (
cardsD1 (0:'
F_2) ([
set x in '
F_2] :\
a)).
have: (0 \
in [
set x in '
F_2] :\
a) =
true.
apply/
setD1P;
move:
H7;
move/
eqP =>
H14.
have: (0 !=
a);
first by apply/
eqP=>
H15;
move:
H14;
rewrite H15.
by move=> ->;
rewrite inE H3.
move=>
H14 H11 H12;
rewrite H14 in H11;
rewrite H12 H11.
move: (
cardsD1 (1:'
F_2) (([
set x in '
F_2] :\
a) :\ (0:'
F_2))) =>
H13.
have H15: ((1 \
in ([
set x in '
F_2] :\
a) :\ (0:'
F_2))).
apply/
setD1P;
apply/
andP;
rewrite Bool.andb_true_l.
move:
H7;
move/
eqP =>
H141;
apply/
setD1P.
have ->: ( 1 !=
a);
first by apply/
eqP=>
H15;
move:
H8;
rewrite H15;
move/
eqP.
by apply/
andP;
rewrite inE.
by move:
H13;
rewrite H15 => ->.
by move:
H11;
rewrite -
H10 H5.
Qed.
Lemma or_bool (
a:
bool): ((
a ==
false) \/ (
a==
true)).
Proof.
Lemma z2_neq0_eq1 (
a: '
F_2) :
a!= 0 -> (
a = 1).
Proof.
move/
eqP=>
H1;
apply/
eqP.
case H: (
a == 1);
first by done.
move:
H;
move/
eqP =>
H2.
by move: (
or_Z2ring a)=>[
H3|
H3];
move:
H3;
move/
eqP =>
H3;
move:
H1;
rewrite H3.
Qed.
Lemma bool_neq0_eq1 (
a:
bool) :
a!=
false -> (
a =
true).
Proof.
move/
eqP=>
H1;
apply/
eqP.
case H: (
a ==
true);
first by done.
move:
H;
move/
eqP =>
H2.
by move: (
or_bool a)=>[
H3|
H3];
move:
H3;
move/
eqP =>
H3;
move:
H1;
rewrite H3.
Qed.
Lemma z2_eq0_neq1 (
a: '
F_2): (
a = 0) -> (
a != 1).
Proof.
case H: (
a != 1);
first by done.
by move:
H;
move/
eqP => ->.
Qed.
Lemma bool_eq0_neq1 (
a:
bool): (
a =
false) -> (
a !=
true).
Proof.
case H: (
a !=
true);
first by done.
by move:
H;
move/
eqP => ->.
Qed.
Fixpoint schema_firstElem1 k (
s:
seqZ2)
n :
nat:=
match s with
|
nil => 0%
N
|
a::
b =>
match k with
|0 =>
if (
a!=
false)
then 0%
N else (1%
N + (
schema_firstElem1 0
b (
n - 1)))%
N
|
S p => (1%
N + (
schema_firstElem1 (
k.-1)
b (
n - 1)))%
N
end
end.
Functional Scheme schema_firstElem1_ind :=
Induction for schema_firstElem1 Sort Prop.
Lemma firstElem1_nth (
k l j:
nat)(
a:
seqZ2):
k <
size a ->
k = (
firstElem1 j a) ->
nth false a k =
true.
Proof.
functional induction (schema_firstElem1 j a k); first by done.
by move=> _ -> /=; rewrite e1 /=; apply: (bool_neq0_eq1 e1).
move=> H1 H2.
case hh: n=>[|n1]; first by move:H2; rewrite hh /firstElem1 e1.
have H3: n!=0%N; first by rewrite hh.
have H5: (n-1 < n); first by rewrite hh subn1 /=.
have H6:(n-1 < size b).
move: H1; rewrite /= leq_eqVlt; move/orP=>[H7|H8].
move: H7; move/eqP; rewrite -addn1 -(addn1 (size b)).
move/eqP; rewrite eqn_add2r; move/eqP => H4.
by move: H5; rewrite H4.
move: H8; rewrite -(addn1 n) -(addn1 (size b)).
rewrite ltn_add2r; apply: (ltn_trans H5).
have H7:((n%N - 1)%N = firstElem1 0 b).
by rewrite H2 /firstElem1 -/firstElem1 e1 add1n subn1 /=.
by move: (IHn H6 H7); rewrite hh subn1 /=.
move=> H1 H2.
have H7:((n - 1)%N = firstElem1 _x.+1.-1 b).
by rewrite H2 /firstElem1 -/firstElem1 add1n subn1 /=.
case hh: n=>[|n1]; first by move:H2; rewrite hh /firstElem1.
have H3: n!=0%N; first by rewrite hh.
have H5: (n-1 < n); first by rewrite hh subn1 /=.
have H6:(n-1 < size b).
move: H1; rewrite /= leq_eqVlt; move/orP=>[H71|H8].
move: H71; move/eqP; rewrite -addn1 -(addn1 (size b)).
move/eqP; rewrite eqn_add2r; move/eqP => H4.
by move: H5; rewrite H4.
move: H8; rewrite -(addn1 n) -(addn1 (size b)).
rewrite ltn_add2r; apply: (ltn_trans H5).
by move: (IHn H6 H7); rewrite hh subn1 /=.
Qed.
Lemma v_in_genDvfOrders (
p i j x y:
nat)(
M1 M2:
matZ2)(
vf:
vectorfield)(
ord:
orders):
((
x,
y) \
in (
genDvfOrders p i j M1 M2 vf ord).1) -> (
x,
y) \
in vf \/
x >=
i.
Proof.
functional induction (genDvfOrders p i j M1 M2 vf ord); try by rewrite /=.
by rewrite /= => -> ; apply/orP => /=.
rewrite mem_cat; move/orP=>[H1|H2]; first by rewrite H1; apply/orP.
move: H2; rewrite inE =>H1; move: (pairs H1)=>[H2 H3].
by move:(eqP H2) => ->; right.
by rewrite /= => ->; apply/orP.
rewrite mem_cat; move/orP=>[H1|H2]; first by rewrite H1; apply/orP.
move: H2; rewrite inE =>H1; move: (pairs H1)=>[H2 H3].
by move:(eqP H2) => ->; right.
by rewrite /= => ->; apply/orP.
move => H1; move:(IHp0 H1); move => [H2|H2].
move:H2; rewrite /addcvd mem_cat; move/orP=>[H4 |H4]; last by rewrite H4; apply/orP.
move: H4; rewrite inE =>H11; move: (pairs H11) =>[H2 H31].
by move:(eqP H2) => ->; right.
move: (leqnSn i); rewrite -addn1 => H3.
by move: (leq_trans H3 H2) => ->; apply/orP; rewrite Bool.orb_true_r.
move => H1; move:(IHp0 H1) =>[H2|H2]; first by rewrite H2; apply/orP.
move: (leqnSn i); rewrite -addn1 => H3.
move: (leq_trans H3 H2); first by move=> ->; apply/orP; rewrite Bool.orb_true_r.
move => H1; move:(IHp0 H1); move => [H2|H2].
move:H2; rewrite /addcvd mem_cat; move/orP=>[H4 |H4]; last by rewrite H4; apply/orP.
move: H4; rewrite inE =>H11; move: (pairs H11) =>[H2 H31].
by move:(eqP H2) => ->; right.
move: (leqnSn i); rewrite -addn1 => H3.
by move: (leq_trans H3 H2) => ->; apply/orP; rewrite Bool.orb_true_r.
move => H1; move:(IHp0 H1) =>[H2|H2]; first by rewrite H2; apply/orP.
move: (leqnSn i); rewrite -addn1 => H3.
move: (leq_trans H3 H2); first by move=> ->; apply/orP; rewrite Bool.orb_true_r.
Qed.
Lemma compijsub (
k1 k2:
nat)(
a:
seqZ2)(
s:
matZ2):
k1 > 0 ->
compij k1 k2 (
a::
s) =
compij k1.-1
k2 s.
Proof.
move=> H; rewrite /compij.
have: ((nth [::] (a :: s) k1) =(nth [::] s (k1.-1))); last by move=> ->.
case H1: k1=>[|k]; first by move:H; rewrite H1.
case H2: k=>[|kk]; first by rewrite H2 in H1; move:H; rewrite H1.
by rewrite /=; case: s.
Qed.
Lemma firstElem1_compij (
j kk:
nat)(
a:
seqZ2)(
x:
matZ2):
kk <
size a ->
kk == (
firstElem1 j a) ->
compij 0
kk (
a::
x) =
true.
Proof.
move=> H1.
set k:= (firstElem1 j a); move/eqP => H2.
have H3: (k = firstElem1 j a); first by done.
rewrite H2 H3 /compij.
move: (subn_eq0 1 1); rewrite /=.
rewrite -H3 -H2; rewrite -H2 in H3.
by move: (firstElem1_nth kk H1 H3).
Qed.
Fixpoint schemaGenDvfOrders_a (
it i j a1 :
nat)(
mm:
matZ2)(
ss :
matZ2)(
vf:
vectorfield)(
rest:
orders):=
match it with
0 =>
it
|
S p =>
if ((
longmn (
size mm)(
getfirstElemseq vf))&& (
longmn (
size (
nth nil mm 0))(
getsndElemseq vf)) &&
(
uniq (
getfirstElemseq vf)) && (
uniq (
getsndElemseq vf)) &&(
norep rest) && (
compijCvd vf mm))
then
match ss,
vf,
rest with
|
nil,
_ ,
_ =>
it
|
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 it
else (
schemaGenDvfOrders_a p i (
j+1)
a1 mm (
a::
nil)
vf nil)
else (
schemaGenDvfOrders_a p i (
j+1)
a1 mm (
a::
nil)
vf nil)
else it
|
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 it
else (
schemaGenDvfOrders_a p i (
j+1)
a1 mm (
a::
nil)
vf (
e::
f))
else (
schemaGenDvfOrders_a p i (
j+1)
a1 mm (
a::
nil)
vf (
e::
f))
else it
|
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 (
schemaGenDvfOrders_a p (
i+1) 0 (
a1.-1)
mm b (
addcvd i k vf) (
addOrders i 0
colk1 nil))
else (
schemaGenDvfOrders_a p i (
j+1)
a1 mm (
a::
b)
vf nil)
else (
schemaGenDvfOrders_a p i (
j+1)
a1 mm (
a::
b)
vf nil)
else (
schemaGenDvfOrders_a p (
i+1) 0 (
a1.-1)
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 (
schemaGenDvfOrders_a p (
i+1) 0 (
a1.-1)
mm b (
addcvd i k vf) (
addOrders i 0
colk1 ((
e::
f))))
else (
schemaGenDvfOrders_a p i (
j+1)
a1 mm (
a::
b)
vf (
e::
f))
else (
schemaGenDvfOrders_a p i (
j+1)
a1 mm (
a::
b)
vf (
e::
f))
else (
schemaGenDvfOrders_a p (
i+1) 0 (
a1 -1)
mm (
b)
vf (
e::
f))
end
else it
end.
Functional Scheme schemaGenDvfOrders_a_ind :=
Induction for schemaGenDvfOrders_a Sort Prop.
Close Local Scope ring_scope.
Lemma compij0_notinDvf (
p i j kk a:
nat)(
M1 M2:
matZ2)(
vf:
vectorfield)(
ord:
orders):
(
forall k2,
compij (
i +
a)
k2 M1 =
compij a k2 M2)
->
compij (
i +
a)
kk M1 ==
false ->
((
i +
a,
kk) \
in (
genDvfOrders p i j M1 M2 vf ord).1)=
false.
Proof.
move=> H.
functional induction (schemaGenDvfOrders_a p i j a M1 M2 vf ord); try done; try by rewrite /= e0.
rewrite /= e0.
case H2: ((i + a1, kk) \in vf); last by done.
move:(andP e0) =>[H3 H4]; move/eqP=> HH.
by move: (compij_in H2 H4); move/eqP=>H5; move: (bool_eq0_neq1 HH); rewrite H5.
rewrite /genDvfOrders e0 e4 e5 e6 mem_cat=> HH.
case H11: (((i + a1, kk) \in vf)).
move:e0; move/andP=>[H3 H4].
move: (compij_in H11 H4); move/eqP=> H5.
by move: (bool_eq0_neq1 (eqP HH)); rewrite H5.
rewrite Bool.orb_false_l.
case H2: (((i + a1, kk) \in [:: (i, firstElem1 j a)])); last by done.
move:H2; rewrite inE => H2; move: (pairs H2) =>[H3 H4].
move: HH; rewrite (H kk).
move: e0; move/andP=>[e0 H5]; move: e0; move/andP=>[e0 H6]; move: e0; move/andP=>[e0 H7];
move: e0; move/andP=>[e0 H8]; move: e0; move/andP=>[e0 H9].
rewrite -(eqP H4) in e5.
rewrite -(eqP H4) in e4.
move: (firstElem1_compij [::] e4 H4); move/eqP=> H13; move/eqP=> H14.
by move: H3 H14; rewrite -{2}(addn0 i) eqn_add2l; move/eqP => ->; rewrite (eqP H13).
by rewrite /= e6 e4 e5 e0; apply: IHn.
by rewrite /= e4 e5 e0; apply: IHn.
rewrite /genDvfOrders e0 e4 /= => H1.
case H2:(((i + a1, kk) \in vf)); last by done.
move:e0; move/andP=>[H3 H4]; move: (compij_in H2 H4); move/eqP=>H411.
by move:H1; move/eqP =>H51; move: (bool_eq0_neq1 H51); rewrite H411.
rewrite /genDvfOrders e0 e7 e5 e6 mem_cat=> HH.
case H11: (((i + a1, kk) \in vf)).
move:e0; move/andP=>[H3 H4].
move: (compij_in H11 H4); move/eqP=> H5.
by move: (bool_eq0_neq1 (eqP HH)); rewrite H5.
rewrite Bool.orb_false_l.
case H2: (((i + a1, kk) \in [:: (i, firstElem1 j a)])); last by done.
move:H2; rewrite inE => H2; move: (pairs H2) =>[H3 H4].
move: HH; rewrite (H kk).
move: e0; move/andP=>[e0 H5]; move: e0; move/andP=>[e0 H6]; move: e0; move/andP=>[e0 H7];
move: e0; move/andP=>[e0 H8]; move: e0; move/andP=>[e0 H9].
rewrite -(eqP H4) in e6.
rewrite -(eqP H4) in e5.
move: (firstElem1_compij [::] e5 H4); move/eqP=> H13; move/eqP=> H14.
by move: H3 H14; rewrite -{2}(addn0 i) eqn_add2l; move/eqP => ->; rewrite (eqP H13).
by rewrite /= e5 e6 e7 e0; apply: IHn.
by rewrite /= e5 e6 e0; apply: IHn.
rewrite /genDvfOrders e0 e5 /= => H1.
case H2:(((i + a1, kk) \in vf)); last by done.
move:e0; move/andP=>[H3 H4]; move: (compij_in H2 H4); move/eqP=>H411.
by move:H1; move/eqP =>H51; move: (bool_eq0_neq1 H51); rewrite H411.
rewrite /= e0 e6 e4 e5 -/genDvfOrders.
move: e0; move/andP=>[e0 H7];
move: e0; move/andP=>[e0 H8]; move: e0; move/andP=>[e0 H9]; move: e0; move/andP=>[e0 H10];
move: e0; move/andP=>[e0 H11].
case H1: a1 =>[|a11].
rewrite addn0.
case H3:(((i, kk) \in (genDvfOrders p (i + 1) 0 mm (_x :: _x0)
(addcvd i (firstElem1 j a) vf)
(addOrders i 0 (getcol (firstElem1 j a) mm) [::])).1)); last by done.
move: (v_in_genDvfOrders H3) =>[H4|H4].
move:H4; rewrite /addcvd.
rewrite mem_cat; move/orP=>[H61|H61].
move:H61; rewrite inE =>H61; move: (pairs H61) =>[H71 H81]; move: (eqP H71).
rewrite -(eqP H81) in e4.
move: (firstElem1_compij [::] e4 H81); move/eqP=> H13; move/eqP=> H14.
rewrite H1 addn0 in H.
rewrite (H kk).
by move: H13; rewrite /compij /=; move/eqP => ->.
by move: (compij_in H61 H7) => ->.
by move:H4; rewrite addn1 /= ltnn.
have H12:((i + 1 + a1.-1) = i + a1); first by rewrite H1 /= -(addn1 a11)(addnC a11) -addnA.
rewrite -H1 . rewrite -H12.
have H13: (forall k2 : nat,
compij (i + 1 + a1.-1) k2 mm = compij a1.-1 k2 (_x :: _x0)); last by apply:(IHn H13).
have H13: (a1 > 0); first by rewrite H1 /=.
move=> k2; rewrite H12 (H k2).
by move: (compijsub k2 a (_x::_x0) H13).
by rewrite /= e6 e4 e5 e0; apply: IHn.
by rewrite /= e4 e5 e0; apply: IHn.
rewrite /= e0 e4 -/genDvfOrders.
move: e0; move/andP=>[e0 H7];
move: e0; move/andP=>[e0 H8]; move: e0; move/andP=>[e0 H9]; move: e0; move/andP=>[e0 H10];
move: e0; move/andP=>[e0 H11].
case H1: a1 =>[|a11].
rewrite addn0 => H2.
case H3:(((i, kk) \in (genDvfOrders p (i + 1) 0 mm (_x :: _x0) vf [::]).1)); last by done.
move: (v_in_genDvfOrders H3) =>[H4|H4].
by move: (compij_in H4 H7); move/eqP=>H12; move: (bool_eq0_neq1 (eqP H2)); rewrite H12.
by move: H4; rewrite leqNgt addn1 /= ltnSn.
rewrite -H1.
have H2: ((i + 1 + a1.-1) = (i + a1)); first by rewrite H1 /= -(addn1 a11)(addnC a11) -addnA.
rewrite H2 in IHn => H12.
have H13: ((forall k2 : nat, compij (i + a1) k2 mm = compij a1.-1 k2 (_x :: _x0))); last by apply:(IHn H13 H12).
have H13: (a1 > 0); first by rewrite H1 /=.
move=> k2; move: (compijsub k2 a (_x::_x0) H13) => H14.
rewrite -H14; apply: (H k2).
rewrite /= e0 e6 e7 e5 -/genDvfOrders.
move: e0; move/andP=>[e0 H7];
move: e0; move/andP=>[e0 H8]; move: e0; move/andP=>[e0 H9]; move: e0; move/andP=>[e0 H10];
move: e0; move/andP=>[e0 H11].
case H1: a1 =>[|a11].
rewrite addn0.
case H3:(((i, kk) \in (genDvfOrders p (i + 1) 0 mm (_x :: _x0)
(addcvd i (firstElem1 j a) vf)
(addOrders i 0 (getcol (firstElem1 j a) mm) (e3 :: f))).1)); last by done.
move: (v_in_genDvfOrders H3) =>[H4|H4].
move:H4; rewrite /addcvd.
rewrite mem_cat; move/orP=>[H61|H61].
move:H61; rewrite inE =>H61; move: (pairs H61) =>[H71 H81]; move: (eqP H71).
rewrite -(eqP H81) in e5.
move: (firstElem1_compij [::] e5 H81); move/eqP=> H13; move/eqP=> H14.
rewrite H1 addn0 in H.
rewrite (H kk).
by move: H13; rewrite /compij /=; move/eqP => ->.
by move: (compij_in H61 H7) => ->.
by move:H4; rewrite addn1 /= ltnn.
have H12:((i + 1 + a1.-1) = i + a1); first by rewrite H1 /= -(addn1 a11)(addnC a11) -addnA.
rewrite -H1 . rewrite -H12.
have H13: (forall k2 : nat,
compij (i + 1 + a1.-1) k2 mm = compij a1.-1 k2 (_x :: _x0)); last by apply:(IHn H13).
have H13: (a1 > 0); first by rewrite H1 /=.
move=> k2; rewrite H12 (H k2).
by move: (compijsub k2 a (_x::_x0) H13).
by rewrite /= e5 e6 e7 e0; apply: IHn.
by rewrite /= e5 e6 e0; apply: IHn.
rewrite /= e0 e5 -/genDvfOrders.
move: e0; move/andP=>[e0 H7];
move: e0; move/andP=>[e0 H8]; move: e0; move/andP=>[e0 H9]; move: e0; move/andP=>[e0 H10];
move: e0; move/andP=>[e0 H11].
case H1: a1 =>[|a11].
rewrite addn0 => H2.
case H3:(((i, kk) \in (genDvfOrders p (i + 1) 0 mm (_x :: _x0) vf (e3 :: f)).1)); last by done.
move: (v_in_genDvfOrders H3) =>[H4|H4].
by move: (compij_in H4 H7); move/eqP=>H12; move: (bool_eq0_neq1 (eqP H2)); rewrite H12.
by move: H4; rewrite leqNgt addn1 /= ltnSn.
rewrite -H1.
have H2: ((i + 1 + (a1 -1)) = (i + a1)); first by rewrite subn1 H1 /= -(addn1 a11)(addnC a11) -addnA.
rewrite H2 in IHn => H12.
have H13: ((forall k2 : nat, compij (i + a1) k2 mm = compij (a1 - 1) k2 (_x :: _x0))); last by apply:(IHn H13 H12).
have H13: (a1 > 0); first by rewrite H1 /=.
move=> k2; move: (compijsub k2 a (_x::_x0) H13) => H14.
rewrite subn1 -H14; apply: (H k2).
Qed.
Fixpoint schemaGenDvfOrders_ab (
it i j a1 b1 k1:
nat)(
mm:
matZ2)(
ss :
matZ2)(
vf:
vectorfield)(
rest:
orders):=
match it with
0 =>
it
|
S p =>
if ((
longmn (
size mm)(
getfirstElemseq vf))&& (
longmn (
size (
nth nil mm 0))(
getsndElemseq vf)) &&
(
uniq (
getfirstElemseq vf)) && (
uniq (
getsndElemseq vf)) &&(
norep rest) && (
compijCvd vf mm))
then
match ss,
vf,
rest with
|
nil,
_ ,
_ =>
it
|
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 it
else (
schemaGenDvfOrders_ab p i (
j+1)
a1 (
b1.-1)
k1 mm (
a::
nil)
vf nil)
else (
schemaGenDvfOrders_ab p i (
j+1)
a1 (
b1.-1)
k1 mm (
a::
nil)
vf nil)
else it
|
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 it
else (
schemaGenDvfOrders_ab p i (
j+1)
a1 (
b1.-1)
k1 mm (
a::
nil)
vf (
e::
f))
else (
schemaGenDvfOrders_ab p i (
j+1)
a1 (
b1.-1)
k1 mm (
a::
nil)
vf (
e::
f))
else it
|
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 (
schemaGenDvfOrders_ab p (
i+1) 0 (
a1.-1)(
j +
b1) (
k1-1)
mm b (
addcvd i k vf) (
addOrders i 0
colk1 nil))
else (
schemaGenDvfOrders_ab p i (
j+1)
a1 (
b1.-1)
k1 mm (
a::
b)
vf nil)
else (
schemaGenDvfOrders_ab p i (
j+1)
a1 (
b1.-1 )
k1 mm (
a::
b)
vf nil)
else (
schemaGenDvfOrders_ab p (
i+1) 0 (
a1.-1) (
j +
b1) (
k1-1)
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 (
schemaGenDvfOrders_ab p (
i+1) 0 (
a1.-1) (
j +
b1) (
k1-1)
mm b (
addcvd i k vf) (
addOrders i 0
colk1 ((
e::
f))))
else (
schemaGenDvfOrders_ab p i (
j+1)
a1 (
b1.-1)
k1 mm (
a::
b)
vf (
e::
f))
else (
schemaGenDvfOrders_ab p i (
j+1)
a1 (
b1.-1)
k1 mm (
a::
b)
vf (
e::
f))
else (
schemaGenDvfOrders_ab p (
i+1) 0 (
a1 -1)(
j +
b1) (
k1-1)
mm (
b)
vf (
e::
f))
end
else it
end.
Functional Scheme schemaGenDvfOrders_ab_ind :=
Induction for schemaGenDvfOrders_ab Sort Prop.
Lemma inDvf_compij1 (
p i j a b k1 :
nat) (
M1 M2:
matZ2)(
vf:
vectorfield)(
ord:
orders):
(
forall k2,
compij (
i +
a)
k2 M1 =
compij a k2 M2) ->
((
i +
a ,
j +
b) \
in (
genDvfOrders p i j M1 M2 vf ord).1)
->
compij (
i +
a ) (
j +
b)
M1 =
true.
Proof.
move=> H.
functional induction (schemaGenDvfOrders_ab p i j a b k1 M1 M2 vf ord); try done; try by rewrite /= e0.
rewrite /= e0; move: (andP e0) =>[H4 H2] H3.
apply:(compij_in H3 H2).
rewrite /genDvfOrders e0 e4 e6 e5 -/genDvfOrders mem_cat.
move/orP=>[H2|H3]; first by move:(andP e0) =>[H21 H31]; apply: (compij_in H2 H31).
move: H3; rewrite inE => H3; move: (pairs H3)=> [H21 H31].
move:H21; move/eqP=> H21; move:H31; move/eqP=>H31.
move:e0; move/andP=>[e0 H9];
move:e0; move/andP=>[e0 H10]; move:e0; move/andP=>[e0 H11]; move:e0; move/andP=>[e0 H12];
move:e0; move/andP=>[e0 H13].
move: (H (j + b1)).
case H14: a1=>[|a11].
move: H21; rewrite H14 addn0 => _ ->.
rewrite -H31 in e4.
by move:H31; move/eqP=>H31; rewrite (firstElem1_compij ([::]) e4 H31).
rewrite H31 -H14.
move: H21; rewrite -{2}(addn0 i); move/eqP; rewrite eqn_add2l; move/eqP => ->.
rewrite addn0 => ->.
rewrite -H31 in e4.
move:H31; move/eqP=>H31.
by move: (firstElem1_compij ([::]) e4 H31); rewrite (eqP H31).
rewrite /= e4 e6 e5 e0 -/genDvfOrders.
case H1: b1=>[|b2]; last first.
move: (IHn H).
have H2: (j + 1 + b1.-1)= (j + b1); last by rewrite -H1 H2; apply => ->.
by rewrite H1 /= -addnA addnC.
rewrite addn0 => H2.
case H3: ((compij (i + a1) j mm)== true); first by move:(eqP H3) => ->.
move:H3; move/eqP; move/eqP =>H3.
move: (or_bool (compij (i + a1) (j) mm))=>[H41|H42]; last by move:H3; rewrite (eqP H42); move/eqP.
have H5: (j - 1 < j + 1); first by case H12: j=>[|j1]; last by rewrite subn1 addn1.
by move: (compij0_notinDvf p (j+1) vf [::] H H41); rewrite H2.
rewrite /= e4 e5 e0 -/genDvfOrders.
case H1: b1=>[|b2]; last first.
move: (IHn H).
have H2: (j + 1 + b1.-1)= (j + b1); last by rewrite -H1 H2; apply => ->.
by rewrite H1 /= -addnA addnC.
rewrite addn0 => H2.
case H3: ((compij (i + a1) j mm)== true); first by move:(eqP H3) => ->.
move:H3; move/eqP; move/eqP =>H3.
move: (or_bool (compij (i + a1) (j) mm))=>[H41|H42]; last by move:H3; rewrite (eqP H42); move/eqP.
have H5: (j - 1 < j + 1); first by case H12: j=>[|j1]; last by rewrite subn1 addn1.
by move: (compij0_notinDvf p (j+1) vf [::] H H41); rewrite H2.
rewrite /= e0 e4; move: (andP e0) =>[H4 H2] H3.
apply:(compij_in H3 H2).
rewrite /genDvfOrders e0 e5 e6 e7 -/genDvfOrders mem_cat.
move/orP=>[H2|H3]; first by move:(andP e0) =>[H21 H31]; apply: (compij_in H2 H31).
move: H3; rewrite inE => H3; move: (pairs H3)=> [H21 H31].
move:H21; move/eqP=> H21; move:H31; move/eqP=>H31.
move:e0; move/andP=>[e0 H9];
move:e0; move/andP=>[e0 H10]; move:e0; move/andP=>[e0 H11]; move:e0; move/andP=>[e0 H12];
move:e0; move/andP=>[e0 H13].
move: (H (j + b1)).
case H14: a1=>[|a11].
move: H21; rewrite H14 addn0 => _ ->.
rewrite -H31 in e5.
by move:H31; move/eqP=>H31; rewrite (firstElem1_compij ([::]) e5 H31).
rewrite H31 -H14.
move: H21; rewrite -{2}(addn0 i); move/eqP; rewrite eqn_add2l; move/eqP => ->.
rewrite addn0 => ->.
rewrite -H31 in e5.
move:H31; move/eqP=>H31.
by move: (firstElem1_compij ([::]) e5 H31); rewrite (eqP H31).
rewrite /= e5 e6 e7 e0 -/genDvfOrders.
case H1: b1=>[|b2]; last first.
move: (IHn H).
have H2: (j + 1 + b1.-1)= (j + b1); last by rewrite -H1 H2; apply => ->.
by rewrite H1 /= -addnA addnC.
rewrite addn0 => H2.
case H3: ((compij (i + a1) j mm)== true); first by move:(eqP H3) => ->.
move:H3; move/eqP; move/eqP =>H3.
move: (or_bool (compij (i + a1) (j) mm))=>[H41|H42]; last by move:H3; rewrite (eqP H42); move/eqP.
have H5: (j - 1 < j + 1); first by case H12: j=>[|j1]; last by rewrite subn1 addn1.
by move: (compij0_notinDvf p (j+1) vf (e3::f) H H41); rewrite H2.
rewrite /= e6 e5 e0 -/genDvfOrders.
case H1: b1=>[|b2]; last first.
move: (IHn H).
have H2: (j + 1 + b1.-1)= (j + b1); last by rewrite -H1 H2; apply => ->.
by rewrite H1 /= -addnA addnC.
rewrite addn0 => H2.
case H3: ((compij (i + a1) j mm)== true); first by move:(eqP H3) => ->.
move:H3; move/eqP; move/eqP =>H3.
move: (or_bool (compij (i + a1) (j) mm))=>[H41|H42]; last by move:H3; rewrite (eqP H42); move/eqP.
have H5: (j - 1 < j + 1); first by case H12: j=>[|j1]; last by rewrite subn1 addn1.
by move: (compij0_notinDvf p (j+1) vf (e3::f) H H41); rewrite H2.
rewrite /= e0 e5 /=; move: (andP e0) =>[H4 H2] H3.
apply:(compij_in H3 H2).
rewrite /= e5 e4 e6 e0 -/genDvfOrders.
rewrite add0n in IHn.
case H2: a1=>[|a2].
rewrite addn0 => H3; move: (v_in_genDvfOrders H3) => [H4| H4].
move:H4; rewrite /addcvd inE; move/orP=>[H6|H6].
rewrite H2 addn0 in H.
rewrite (H (j+b1)).
move: (pairs H6) =>[H7 H8]; move:H7.
rewrite -(eqP H8) in e4.
by rewrite (firstElem1_compij (_x::_x0) e4 H8).
move:(andP e0) => [H7 H8]; apply: (compij_in H6 H8).
by move: H4; rewrite addn1 ltnn.
rewrite -H2.
have HH1:((i + 1 + a1.-1) = (i + a1)); first by rewrite -subn1 H2 /= -addnA add1n subn1 /=.
rewrite HH1 in IHn.
have H6: ((forall k2 : nat, compij (i + a1) k2 mm = compij a1.-1 k2 (_x :: _x0))); last by apply: (IHn H6).
move=> k2; move: (H k2)=> ->.
have: (0 < a1); last by move=>H7; apply: (compijsub k2 a (_x::_x0) H7).
by rewrite H2 .
rewrite /= e4 e6 e5 e0 -/genDvfOrders.
case H1: b1=>[|b2]; last first.
move: (IHn H).
have H2: (j + 1 + b1.-1)= (j + b1); last by rewrite -H1 H2; apply => ->.
by rewrite H1 /= -addnA addnC.
rewrite addn0 => H2.
case H3: ((compij (i + a1) j mm)== true); first by move:(eqP H3) => ->.
move:H3; move/eqP; move/eqP =>H3.
move: (or_bool (compij (i + a1) (j) mm))=>[H41|H42]; last by move:H3; rewrite (eqP H42); move/eqP.
have H5: (j - 1 < j + 1); first by case H12: j=>[|j1]; last by rewrite subn1 addn1.
by move: (compij0_notinDvf p (j+1) vf [::] H H41); rewrite H2.
rewrite /= e4 e5 e0 -/genDvfOrders.
case H1: b1=>[|b2]; last first.
move: (IHn H).
have H2: (j + 1 + b1.-1)= (j + b1); last by rewrite -H1 H2; apply => ->.
by rewrite H1 /= -addnA addnC.
rewrite addn0 => H2.
case H3: ((compij (i + a1) j mm)== true); first by move:(eqP H3) => ->.
move:H3; move/eqP; move/eqP =>H3.
move: (or_bool (compij (i + a1) (j) mm))=>[H41|H42]; last by move:H3; rewrite (eqP H42); move/eqP.
have H5: (j - 1 < j + 1); first by case H12: j=>[|j1]; last by rewrite subn1 addn1.
by move: (compij0_notinDvf p (j+1) vf [::] H H41); rewrite H2.
rewrite /= e4 e0 -/genDvfOrders.
case H2: a1=>[|a2].
rewrite addn0 => H3; move: (v_in_genDvfOrders H3)=> [H4| H4].
move: (andP e0) =>[H7 H8]; apply: (compij_in H4 H8).
move:H4; rewrite addn1 /=.
case H4: i=>[|i1]; first by done.
by rewrite ltnn.
rewrite -H2 addn1 => H4.
rewrite add0n in IHn.
have H5:( (i + 1 + (a1.-1)) = i + a1); first by rewrite -subn1 H2 /= -addnA add1n subn1 /=.
rewrite -H5 in H4.
rewrite -(addn1 i) in H4.
have H6: (forall k2 : nat, compij (i + 1 + (a1.-1)) k2 mm = compij (a1.-1) k2 (_x :: _x0)); last first.
rewrite -H5; apply: (IHn H6 H4).
rewrite H5.
have H13: (0 < a1); first by rewrite H2.
move=> k2; rewrite (H k2).
by move: (compijsub k2 a (_x::_x0) H13).
rewrite /= e6 e7 e5 e0 -/genDvfOrders.
rewrite add0n in IHn.
case H2: a1=>[|a2].
rewrite addn0 => H3; move: (v_in_genDvfOrders H3) => [H4| H4].
move:H4; rewrite /addcvd inE; move/orP=>[H6|H6].
rewrite H2 addn0 in H.
rewrite (H (j+b1)).
move: (pairs H6) =>[H7 H8]; move:H7.
rewrite -(eqP H8) in e5.
by rewrite (firstElem1_compij (_x::_x0) e5 H8).
move:(andP e0) => [H7 H8]; apply: (compij_in H6 H8).
by move: H4; rewrite addn1 ltnn.
rewrite -H2.
have HH1:((i + 1 + a1.-1) = (i + a1)); first by rewrite -subn1 H2 /= -addnA add1n subn1 /=.
rewrite HH1 in IHn.
have H6: ((forall k2 : nat, compij (i + a1) k2 mm = compij a1.-1 k2 (_x :: _x0))); last by apply: (IHn H6).
move=> k2; move: (H k2)=> ->.
have: (0 < a1); last by move=>H7; apply: (compijsub k2 a (_x::_x0) H7).
by rewrite H2 .
rewrite /= e5 e6 e7 e0 -/genDvfOrders.
case H1: b1=>[|b2]; last first.
move: (IHn H).
have H2: (j + 1 + b1.-1)= (j + b1); last by rewrite -H1 H2; apply => ->.
by rewrite H1 /= -addnA addnC.
rewrite addn0 => H2.
case H3: ((compij (i + a1) j mm)== true); first by move:(eqP H3) => ->.
move:H3; move/eqP; move/eqP =>H3.
move: (or_bool (compij (i + a1) (j) mm))=>[H41|H42]; last by move:H3; rewrite (eqP H42); move/eqP.
have H5: (j - 1 < j + 1); first by case H12: j=>[|j1]; last by rewrite subn1 addn1.
by move: (compij0_notinDvf p (j+1) vf (e3::f) H H41); rewrite H2.
rewrite /= e6 e5 e0 -/genDvfOrders.
case H1: b1=>[|b2]; last first.
move: (IHn H).
have H2: (j + 1 + b1.-1)= (j + b1); last by rewrite -H1 H2; apply => ->.
by rewrite H1 /= -addnA addnC.
rewrite addn0 => H2.
case H3: ((compij (i + a1) j mm)== true); first by move:(eqP H3) => ->.
move:H3; move/eqP; move/eqP =>H3.
move: (or_bool (compij (i + a1) (j) mm))=>[H41|H42]; last by move:H3; rewrite (eqP H42); move/eqP.
have H5: (j - 1 < j + 1); first by case H12: j=>[|j1]; last by rewrite subn1 addn1.
by move: (compij0_notinDvf p (j+1) vf (e3::f) H H41); rewrite H2.
rewrite /= e5 e0 -/genDvfOrders.
case H2: a1=>[|a2].
rewrite addn0 => H3; move: (v_in_genDvfOrders H3)=> [H4| H4].
move: (andP e0) =>[H7 H8]; apply: (compij_in H4 H8).
move:H4; rewrite addn1 /=.
case H4: i=>[|i1]; first by done.
by rewrite ltnn.
rewrite -H2 addn1 => H4.
rewrite add0n in IHn.
have H5:( (i + 1 + (a1 - 1)) = i + a1); first by rewrite H2 /= -addnA add1n subn1 /=.
rewrite -H5 in H4.
rewrite -(addn1 i) in H4.
have H6: (forall k2 : nat, compij (i + 1 + (a1 - 1)) k2 mm = compij (a1 - 1) k2 (_x :: _x0)); last first.
rewrite -H5; apply: (IHn H6 H4).
rewrite H5.
have H13: (0 < a1); first by rewrite H2.
move=> k2; rewrite (H k2).
by move: (compijsub k2 a (_x::_x0) H13); rewrite subn1.
Qed.
Lemma v_in_genDvf_Mv1 (
ss:
matZ2):
(
forall i j:
nat, ((
i,
j) \
in (
genDvf ss)) ->
compij i j ss =
true).
Proof.
move=> i j; rewrite /genDvf.
case H1: ss=>[|s1 s2]; first by done.
case HH:(prop_cat (genDvfOrders (size (s1 :: s2) * size s1 +1) 0 0 (s1 :: s2) (s1 :: s2) [::] [::]).2); last by rewrite in_nil.
move: HH=> _.
case H3:((size (s1 :: s2) * size (nth [::] (s1 :: s2) 0) + 1))=>[|n]; first by done.
move=> H4.
move: (v_in_genDvfOrders H4) =>[H6|H6]; first by move: H6; rewrite in_nil.
have H7: (forall k2 : nat, compij i k2 (s1 :: s2) = compij i k2 (s1 :: s2)); first by move=> k2.
move: (@inDvf_compij1 (n.+1) 0 0 i j 0 (s1::s2) (s1 :: s2) [::] [::]).
rewrite !add0n => H11.
by apply : (H11 H7 H4).
Qed.
Lemma v_in_genDvf_Mv1_ord (
ss:
matZ2):
(
forall i j:
nat, ((
i,
j) \
in (
dvford ss)) ->
compij i j ss =
true).
Proof.
move: (@v_in_genDvf_Mv1 ss) => H i j H1.
apply:(H i j (indvford_genDvf H1)).
Qed.
End rs_prop2.
Section rs_prop3.
Section rs_prop31.
Lemma norepfst_aux a b m1 m2 :
uniq
(
getfirstElemseq
(
genDvfOrders (
size (
a ::
b) *
size a).+1
m2 m2 (
a ::
b)
m1 [::] [::]).1).
Proof.
functional induction (genDvfOrders (((size (a::b))*(size a)).+1) m2 m2 (a::b) m1 [::] [::]);
try done; try apply: (IHp H1).
by move: e0; move/andP =>[H2 H4]; move: H2; move/andP => [H2 H3]; move: H2;
move/andP=>[H21 H22]; move: H21; move/andP=>[H21 H23]; move: H21; move/andP=>[H21 H24].
move: (andP e0) =>[H2 H4]; move: (andP H2) => [H31 H3]; move: (andP H31)=>[H21 H22];
move: (andP H21)=>[H211 H23]; move: H23.
rewrite /getfirstElemseq map_cat cat_uniq => ->.
move:e5; rewrite /canAddCvd.
case H41: (((i \in getfirstElemseq vf) == false) &&
((firstElem1 j a0 \in getsndElemseq vf) == false) &&
verifyLength (size mm) (size (nth [::] mm 0)) i (firstElem1 j a0)); last by done.
move: (andP H41) => [H43 H42] _; move: (andP H43) =>[H411 H412].
by move: H411; rewrite /=; move/eqP => ->.
by move: e0; move/andP =>[H2 H4]; move: H2; move/andP => [H2 H3]; move: H2;
move/andP=>[H21 H22]; move: H21; move/andP=>[H21 H23]; move: H21; move/andP=>[H211 H213].
move: (andP e0) =>[H2 H4]; move: (andP H2) => [H31 H3]; move: (andP H31)=>[H21 H22];
move: (andP H21)=>[H211 H23]; move: (andP H211)=>[H212 H231]; move: H212.
rewrite /getfirstElemseq map_cat cat_uniq.
move:e6; rewrite /canAddCvd.
case H41: (((i \in getfirstElemseq vf) == false) &&
((firstElem1 j a0 \in getsndElemseq vf) == false) &&
verifyLength (size mm) (size (nth [::] mm 0)) i (firstElem1 j a0)); last by move/eqP.
move: (andP H41) => [H43 H42] _; move: (andP H43) =>[H411 H412].
rewrite H23 /=. rewrite Bool.orb_false_r.
move: (eqP H411); rewrite /=.
by rewrite /getfirstElemseq Bool.andb_true_r /= => ->.
by move: e0; move/andP =>[H2 H4]; move: H2; move/andP => [H2 H3]; move: H2;
move/andP=>[H21 H22]; move: H21; move/andP=>[H21 H23];move: H21; move/andP=>[H222 H232].
Qed.
Lemma norepfst (
ss:
matZ2) : (
uniq (
getfirstElemseq (
genDvf ss))).
Proof.
elim H: ss=> [|a b HI]; try by done.
rewrite /genDvf !addn1.
have H1: ss = ss; first by done.
case HH:(prop_cat (genDvfOrders (size (a :: b) * size a).+1 0 0 (a :: b) (a :: b) [::] [::]).2); last by done.
move: HH=> _.
set m1:= (a::b); rewrite {-3}/m1.
by apply: norepfst_aux.
Qed.
Lemma norepfst_ord (
ss:
matZ2) : (
uniq (
getfirstElemseq (
dvford ss))).
Proof.
rewrite /=; move: (perm_insert_sort_fst glMax (genOrders ss)(genDvf ss))=> H1.
move: (perm_eq_uniq H1) => <-.
by apply: norepfst.
Qed.
End rs_prop31.
Section rs_prop32.
Lemma norepsnd_aux a b m1 m2:
uniq
(
getsndElemseq
(
genDvfOrders (
size (
a ::
b) *
size a).+1
m2 m2 (
a ::
b)
m1 [::] [::]).1).
Proof.
functional induction (genDvfOrders (((size (a::b))*(size a)).+1) m2 m2 (a::b)
m1 [::] [::]); try done; try apply: (IHp H1).
by move: (andP e0) =>[H2 _]; move: (andP H2) => [H31 _]; move: (andP H31)=>[H30 H22]; move: (andP H30)=>[H301 H221].
move: (andP e0) =>[H2 _]; move: (andP H2) => [H31 _]; move: (andP H31)=>[H30 H22].
move: H22.
rewrite /getsndElemseq map_cat cat_uniq => ->; move:e5; rewrite /canAddCvd.
case H4: (((i \in getfirstElemseq vf) == false) &&
((firstElem1 j a0 \in getsndElemseq vf) == false) &&
verifyLength (size mm) (size (nth [::] mm 0)) i (firstElem1 j a0)); last by done.
move: (andP H4) => [H41 _] _; move: (andP H41) =>[H411 H412].
by move: H412; rewrite /=; move/eqP => ->.
by move: (andP e0) =>[H2 _]; move: (andP H2) => [H31 _]; move: (andP H31)=>[H30 H22]; move: (andP H30)=>[H301 H221].
move: (andP e0) =>[H2 _]; move: (andP H2) => [H31 _]; move: (andP H31)=>[H30 H22].
move: H22.
rewrite /getsndElemseq map_cat cat_uniq => ->; move:e6; rewrite /canAddCvd.
case H4: (((i \in getfirstElemseq vf) == false) &&
((firstElem1 j a0 \in getsndElemseq vf) == false) &&
verifyLength (size mm) (size (nth [::] mm 0)) i (firstElem1 j a0)); last by done.
move: (andP H4) => [H41 _] _; move: (andP H41) =>[H411 H412].
by move: H412; rewrite /=; move/eqP => ->.
by move: (andP e0) =>[H2 _]; move: (andP H2) => [H31 _]; move: (andP H31)=>[H30 H22]; move: (andP H30)=>[H301 H221].
Qed.
Lemma norepsnd (
ss:
matZ2): (
uniq (
getsndElemseq (
genDvf ss))).
Proof.
elim H: ss=> [|a b HI]; try by done.
rewrite /genDvf !addn1.
have H1: ss = ss; first by done.
case HH:(prop_cat (genDvfOrders (size (a :: b) * size a).+1 0 0 (a :: b) (a :: b) [::] [::]).2); last by done.
move: HH=> _.
set m1:= (a::b); rewrite {-3}/m1.
by apply : norepsnd_aux.
Qed.
Lemma norepsnd_ord (
ss:
matZ2): (
uniq (
getsndElemseq (
dvford ss))).
Proof.
rewrite /=; move: (perm_insert_sort_snd glMax (genOrders ss)(genDvf ss))=> H1.
move: (perm_eq_uniq H1) => <-.
by apply: norepsnd.
Qed.
End rs_prop32.
End rs_prop3.
Section rs_ordered.
Lemma ordered_dvfg M:
let dvf := (
dvford M)
in
let ords:= (
genOrders M)
in
ordered glMax dvf ords.
Proof.
by apply:(ordered_insert_sort glMax (genDvf M) (genOrders M)).
Qed.
End rs_ordered.
End rs_properties_dvf_ordered.