X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Fgeneric_iter_p.ma;h=4796ec10b2e14c1829daefba403a11b34e98e38d;hb=b771a37f83637be22d9b3f1254a6a0f15dc49612;hp=7c972e76f8b1de14aaf4e69f9aea1809cdf5653b;hpb=d5afc8f8891d0020f5804eb2322fc0d1c8c60702;p=helm.git diff --git a/helm/software/matita/library/nat/generic_iter_p.ma b/helm/software/matita/library/nat/generic_iter_p.ma index 7c972e76f..4796ec10b 100644 --- a/helm/software/matita/library/nat/generic_iter_p.ma +++ b/helm/software/matita/library/nat/generic_iter_p.ma @@ -12,13 +12,10 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/nat/generic_iter_p.ma". - +include "nat/div_and_mod_diseq.ma". include "nat/primes.ma". include "nat/ord.ma". - - (*a generic definition of summatory indexed over natural numbers: * n:N is the advanced end in the range of the sommatory * p: N -> bool is a predicate. if (p i) = true, then (g i) is summed, else it isn't @@ -27,6 +24,7 @@ include "nat/ord.ma". * baseA (of type A) is the neutral element of A for plusA operation * plusA: A -> A -> A is the sum over elements in A. *) + let rec iter_p_gen (n:nat) (p: nat \to bool) (A:Type) (g: nat \to A) (baseA: A) (plusA: A \to A \to A) \def match n with @@ -48,8 +46,6 @@ rewrite > H. reflexivity. qed. - - theorem false_to_iter_p_gen_Sn: \forall n:nat. \forall p:nat \to bool. \forall A:Type. \forall g:nat \to A. \forall baseA:A. \forall plusA: A \to A \to A. @@ -60,7 +56,6 @@ rewrite > H. reflexivity. qed. - theorem eq_iter_p_gen: \forall p1,p2:nat \to bool. \forall A:Type. \forall g1,g2: nat \to A. \forall baseA: A. \forall plusA: A \to A \to A. \forall n:nat. @@ -206,6 +201,47 @@ elim H ] qed. +(* a therem slightly more general than the previous one *) +theorem or_false_eq_baseA_to_eq_iter_p_gen: \forall A:Type. \forall n,m:nat.\forall p:nat \to bool. +\forall g: nat \to A. \forall baseA:A. \forall plusA: A \to A \to A. +(\forall a. plusA baseA a = a) \to +n \le m \to (\forall i:nat. n \le i \to i < m \to p i = false \lor g i = baseA) +\to iter_p_gen m p A g baseA plusA = iter_p_gen n p A g baseA plusA. +intros 9. +elim H1 +[reflexivity +|apply (bool_elim ? (p n1));intro + [elim (H4 n1) + [apply False_ind. + apply not_eq_true_false. + rewrite < H5. + rewrite < H6. + reflexivity + |rewrite > true_to_iter_p_gen_Sn + [rewrite > H6. + rewrite > H. + apply H3.intros. + apply H4 + [assumption + |apply le_S.assumption + ] + |assumption + ] + |assumption + |apply le_n + ] + |rewrite > false_to_iter_p_gen_Sn + [apply H3.intros. + apply H4 + [assumption + |apply le_S.assumption + ] + |assumption + ] + ] +] +qed. + theorem iter_p_gen2 : \forall n,m:nat. \forall p1,p2:nat \to bool. @@ -288,7 +324,6 @@ elim n ] qed. - theorem iter_p_gen2': \forall n,m:nat. \forall p1: nat \to bool. @@ -472,7 +507,7 @@ elim n ] qed. - +(* invariance under permutation; single sum *) theorem eq_iter_p_gen_gh: \forall A:Type. \forall baseA: A. @@ -490,7 +525,7 @@ theorem eq_iter_p_gen_gh: (\forall j. j < n1 \to p2 j = true \to h1 j < n) \to iter_p_gen n p1 A (\lambda x.g(h x)) baseA plusA = -iter_p_gen n1 (\lambda x.p2 x) A g baseA plusA. +iter_p_gen n1 p2 A g baseA plusA. intros 10. elim n [ generalize in match H8. @@ -669,8 +704,38 @@ elim n ] qed. - - +theorem eq_iter_p_gen_pred: +\forall A:Type. +\forall baseA: A. +\forall plusA: A \to A \to A. +\forall n,p,g. +p O = true \to +(symmetric A plusA) \to (associative A plusA) \to (\forall a:A.(plusA a baseA) = a) \to +iter_p_gen (S n) (\lambda i.p (pred i)) A (\lambda i.g(pred i)) baseA plusA = +plusA (iter_p_gen n p A g baseA plusA) (g O). +intros. +elim n + [rewrite > true_to_iter_p_gen_Sn + [simplify.apply H1 + |assumption + ] + |apply (bool_elim ? (p n1));intro + [rewrite > true_to_iter_p_gen_Sn + [rewrite > true_to_iter_p_gen_Sn in ⊢ (? ? ? %) + [rewrite > H2 in ⊢ (? ? ? %). + apply eq_f.assumption + |assumption + ] + |assumption + ] + |rewrite > false_to_iter_p_gen_Sn + [rewrite > false_to_iter_p_gen_Sn in ⊢ (? ? ? %);assumption + |assumption + ] + ] + ] +qed. + definition p_ord_times \def \lambda p,m,x. match p_ord x p with @@ -698,6 +763,123 @@ apply mod_plus_times. assumption. qed. +lemma lt_times_to_lt_O: \forall i,n,m:nat. i < n*m \to O < m. +intros. +elim (le_to_or_lt_eq O ? (le_O_n m)) + [assumption + |apply False_ind. + rewrite < H1 in H. + rewrite < times_n_O in H. + apply (not_le_Sn_O ? H) + ] +qed. + +theorem iter_p_gen_knm: +\forall A:Type. +\forall baseA: A. +\forall plusA: A \to A \to A. +(symmetric A plusA) \to +(associative A plusA) \to +(\forall a:A.(plusA a baseA) = a)\to +\forall g: nat \to A. +\forall h2:nat \to nat \to nat. +\forall h11,h12:nat \to nat. +\forall k,n,m. +\forall p1,p21:nat \to bool. +\forall p22:nat \to nat \to bool. +(\forall x. x < k \to p1 x = true \to +p21 (h11 x) = true \land p22 (h11 x) (h12 x) = true +\land h2 (h11 x) (h12 x) = x +\land (h11 x) < n \land (h12 x) < m) \to +(\forall i,j. i < n \to j < m \to p21 i = true \to p22 i j = true \to +p1 (h2 i j) = true \land +h11 (h2 i j) = i \land h12 (h2 i j) = j +\land h2 i j < k) \to +iter_p_gen k p1 A g baseA plusA = +iter_p_gen n p21 A (\lambda x:nat.iter_p_gen m (p22 x) A (\lambda y. g (h2 x y)) baseA plusA) baseA plusA. +intros. +rewrite < (iter_p_gen2' n m p21 p22 ? ? ? ? H H1 H2). +apply sym_eq. +apply (eq_iter_p_gen_gh A baseA plusA H H1 H2 g ? (\lambda x.(h11 x)*m+(h12 x))) + [intros. + elim (H4 (i/m) (i \mod m));clear H4 + [elim H7.clear H7. + elim H4.clear H4. + assumption + |apply (lt_times_to_lt_div ? ? ? H5) + |apply lt_mod_m_m. + apply (lt_times_to_lt_O ? ? ? H5) + |apply (andb_true_true ? ? H6) + |apply (andb_true_true_r ? ? H6) + ] + |intros. + elim (H4 (i/m) (i \mod m));clear H4 + [elim H7.clear H7. + elim H4.clear H4. + rewrite > H10. + rewrite > H9. + apply sym_eq. + apply div_mod. + apply (lt_times_to_lt_O ? ? ? H5) + |apply (lt_times_to_lt_div ? ? ? H5) + |apply lt_mod_m_m. + apply (lt_times_to_lt_O ? ? ? H5) + |apply (andb_true_true ? ? H6) + |apply (andb_true_true_r ? ? H6) + ] + |intros. + elim (H4 (i/m) (i \mod m));clear H4 + [elim H7.clear H7. + elim H4.clear H4. + assumption + |apply (lt_times_to_lt_div ? ? ? H5) + |apply lt_mod_m_m. + apply (lt_times_to_lt_O ? ? ? H5) + |apply (andb_true_true ? ? H6) + |apply (andb_true_true_r ? ? H6) + ] + |intros. + elim (H3 j H5 H6). + elim H7.clear H7. + elim H9.clear H9. + elim H7.clear H7. + rewrite > div_plus_times + [rewrite > mod_plus_times + [rewrite > H9. + rewrite > H12. + reflexivity. + |assumption + ] + |assumption + ] + |intros. + elim (H3 j H5 H6). + elim H7.clear H7. + elim H9.clear H9. + elim H7.clear H7. + rewrite > div_plus_times + [rewrite > mod_plus_times + [assumption + |assumption + ] + |assumption + ] + |intros. + elim (H3 j H5 H6). + elim H7.clear H7. + elim H9.clear H9. + elim H7.clear H7. + apply (lt_to_le_to_lt ? ((h11 j)*m+m)) + [apply monotonic_lt_plus_r. + assumption + |rewrite > sym_plus. + change with ((S (h11 j)*m) \le n*m). + apply monotonic_le_times_l. + assumption + ] + ] +qed. + theorem iter_p_gen_divides: \forall A:Type. \forall baseA: A. @@ -1009,4 +1191,576 @@ elim n ] qed. +(* old version - proved without theorem iter_p_gen_knm +theorem iter_p_gen_2_eq: +\forall A:Type. +\forall baseA: A. +\forall plusA: A \to A \to A. +(symmetric A plusA) \to +(associative A plusA) \to +(\forall a:A.(plusA a baseA) = a)\to +\forall g: nat \to nat \to A. +\forall h11,h12,h21,h22: nat \to nat \to nat. +\forall n1,m1,n2,m2. +\forall p11,p21:nat \to bool. +\forall p12,p22:nat \to nat \to bool. +(\forall i,j. i < n2 \to j < m2 \to p21 i = true \to p22 i j = true \to +p11 (h11 i j) = true \land p12 (h11 i j) (h12 i j) = true +\land h21 (h11 i j) (h12 i j) = i \land h22 (h11 i j) (h12 i j) = j +\land h11 i j < n1 \land h12 i j < m1) \to +(\forall i,j. i < n1 \to j < m1 \to p11 i = true \to p12 i j = true \to +p21 (h21 i j) = true \land p22 (h21 i j) (h22 i j) = true +\land h11 (h21 i j) (h22 i j) = i \land h12 (h21 i j) (h22 i j) = j +\land (h21 i j) < n2 \land (h22 i j) < m2) \to +iter_p_gen n1 p11 A + (\lambda x:nat .iter_p_gen m1 (p12 x) A (\lambda y. g x y) baseA plusA) + baseA plusA = +iter_p_gen n2 p21 A + (\lambda x:nat .iter_p_gen m2 (p22 x) A (\lambda y. g (h11 x y) (h12 x y)) baseA plusA ) + baseA plusA. +intros. +rewrite < (iter_p_gen2' ? ? ? ? ? ? ? ? H H1 H2). +rewrite < (iter_p_gen2' ? ? ? ? ? ? ? ? H H1 H2). +apply sym_eq. +letin h := (\lambda x.(h11 (x/m2) (x\mod m2))*m1 + (h12 (x/m2) (x\mod m2))). +letin h1 := (\lambda x.(h21 (x/m1) (x\mod m1))*m2 + (h22 (x/m1) (x\mod m1))). +apply (trans_eq ? ? + (iter_p_gen (n2*m2) (\lambda x:nat.p21 (x/m2)\land p22 (x/m2) (x\mod m2)) A + (\lambda x:nat.g ((h x)/m1) ((h x)\mod m1)) baseA plusA )) + [clear h.clear h1. + apply eq_iter_p_gen1 + [intros.reflexivity + |intros. + cut (O < m2) + [cut (x/m2 < n2) + [cut (x \mod m2 < m2) + [elim (and_true ? ? H6). + elim (H3 ? ? Hcut1 Hcut2 H7 H8). + elim H9.clear H9. + elim H11.clear H11. + elim H9.clear H9. + elim H11.clear H11. + apply eq_f2 + [apply sym_eq. + apply div_plus_times. + assumption + | apply sym_eq. + apply mod_plus_times. + assumption + ] + |apply lt_mod_m_m. + assumption + ] + |apply (lt_times_n_to_lt m2) + [assumption + |apply (le_to_lt_to_lt ? x) + [apply (eq_plus_to_le ? ? (x \mod m2)). + apply div_mod. + assumption + |assumption + ] + ] + ] + |apply not_le_to_lt.unfold.intro. + generalize in match H5. + apply (le_n_O_elim ? H7). + rewrite < times_n_O. + apply le_to_not_lt. + apply le_O_n + ] + ] + |apply (eq_iter_p_gen_gh ? ? ? H H1 H2 ? h h1);intros + [cut (O < m2) + [cut (i/m2 < n2) + [cut (i \mod m2 < m2) + [elim (and_true ? ? H6). + elim (H3 ? ? Hcut1 Hcut2 H7 H8). + elim H9.clear H9. + elim H11.clear H11. + elim H9.clear H9. + elim H11.clear H11. + cut ((h11 (i/m2) (i\mod m2)*m1+h12 (i/m2) (i\mod m2))/m1 = + h11 (i/m2) (i\mod m2)) + [cut ((h11 (i/m2) (i\mod m2)*m1+h12 (i/m2) (i\mod m2))\mod m1 = + h12 (i/m2) (i\mod m2)) + [rewrite > Hcut3. + rewrite > Hcut4. + rewrite > H9. + rewrite > H15. + reflexivity + |apply mod_plus_times. + assumption + ] + |apply div_plus_times. + assumption + ] + |apply lt_mod_m_m. + assumption + ] + |apply (lt_times_n_to_lt m2) + [assumption + |apply (le_to_lt_to_lt ? i) + [apply (eq_plus_to_le ? ? (i \mod m2)). + apply div_mod. + assumption + |assumption + ] + ] + ] + |apply not_le_to_lt.unfold.intro. + generalize in match H5. + apply (le_n_O_elim ? H7). + rewrite < times_n_O. + apply le_to_not_lt. + apply le_O_n + ] + |cut (O < m2) + [cut (i/m2 < n2) + [cut (i \mod m2 < m2) + [elim (and_true ? ? H6). + elim (H3 ? ? Hcut1 Hcut2 H7 H8). + elim H9.clear H9. + elim H11.clear H11. + elim H9.clear H9. + elim H11.clear H11. + cut ((h11 (i/m2) (i\mod m2)*m1+h12 (i/m2) (i\mod m2))/m1 = + h11 (i/m2) (i\mod m2)) + [cut ((h11 (i/m2) (i\mod m2)*m1+h12 (i/m2) (i\mod m2))\mod m1 = + h12 (i/m2) (i\mod m2)) + [rewrite > Hcut3. + rewrite > Hcut4. + rewrite > H13. + rewrite > H14. + apply sym_eq. + apply div_mod. + assumption + |apply mod_plus_times. + assumption + ] + |apply div_plus_times. + assumption + ] + |apply lt_mod_m_m. + assumption + ] + |apply (lt_times_n_to_lt m2) + [assumption + |apply (le_to_lt_to_lt ? i) + [apply (eq_plus_to_le ? ? (i \mod m2)). + apply div_mod. + assumption + |assumption + ] + ] + ] + |apply not_le_to_lt.unfold.intro. + generalize in match H5. + apply (le_n_O_elim ? H7). + rewrite < times_n_O. + apply le_to_not_lt. + apply le_O_n + ] + |cut (O < m2) + [cut (i/m2 < n2) + [cut (i \mod m2 < m2) + [elim (and_true ? ? H6). + elim (H3 ? ? Hcut1 Hcut2 H7 H8). + elim H9.clear H9. + elim H11.clear H11. + elim H9.clear H9. + elim H11.clear H11. + apply lt_times_plus_times + [assumption|assumption] + |apply lt_mod_m_m. + assumption + ] + |apply (lt_times_n_to_lt m2) + [assumption + |apply (le_to_lt_to_lt ? i) + [apply (eq_plus_to_le ? ? (i \mod m2)). + apply div_mod. + assumption + |assumption + ] + ] + ] + |apply not_le_to_lt.unfold.intro. + generalize in match H5. + apply (le_n_O_elim ? H7). + rewrite < times_n_O. + apply le_to_not_lt. + apply le_O_n + ] + |cut (O < m1) + [cut (j/m1 < n1) + [cut (j \mod m1 < m1) + [elim (and_true ? ? H6). + elim (H4 ? ? Hcut1 Hcut2 H7 H8). + elim H9.clear H9. + elim H11.clear H11. + elim H9.clear H9. + elim H11.clear H11. + cut ((h21 (j/m1) (j\mod m1)*m2+h22 (j/m1) (j\mod m1))/m2 = + h21 (j/m1) (j\mod m1)) + [cut ((h21 (j/m1) (j\mod m1)*m2+h22 (j/m1) (j\mod m1))\mod m2 = + h22 (j/m1) (j\mod m1)) + [rewrite > Hcut3. + rewrite > Hcut4. + rewrite > H9. + rewrite > H15. + reflexivity + |apply mod_plus_times. + assumption + ] + |apply div_plus_times. + assumption + ] + |apply lt_mod_m_m. + assumption + ] + |apply (lt_times_n_to_lt m1) + [assumption + |apply (le_to_lt_to_lt ? j) + [apply (eq_plus_to_le ? ? (j \mod m1)). + apply div_mod. + assumption + |assumption + ] + ] + ] + |apply not_le_to_lt.unfold.intro. + generalize in match H5. + apply (le_n_O_elim ? H7). + rewrite < times_n_O. + apply le_to_not_lt. + apply le_O_n + ] + |cut (O < m1) + [cut (j/m1 < n1) + [cut (j \mod m1 < m1) + [elim (and_true ? ? H6). + elim (H4 ? ? Hcut1 Hcut2 H7 H8). + elim H9.clear H9. + elim H11.clear H11. + elim H9.clear H9. + elim H11.clear H11. + cut ((h21 (j/m1) (j\mod m1)*m2+h22 (j/m1) (j\mod m1))/m2 = + h21 (j/m1) (j\mod m1)) + [cut ((h21 (j/m1) (j\mod m1)*m2+h22 (j/m1) (j\mod m1))\mod m2 = + h22 (j/m1) (j\mod m1)) + [rewrite > Hcut3. + rewrite > Hcut4. + rewrite > H13. + rewrite > H14. + apply sym_eq. + apply div_mod. + assumption + |apply mod_plus_times. + assumption + ] + |apply div_plus_times. + assumption + ] + |apply lt_mod_m_m. + assumption + ] + |apply (lt_times_n_to_lt m1) + [assumption + |apply (le_to_lt_to_lt ? j) + [apply (eq_plus_to_le ? ? (j \mod m1)). + apply div_mod. + assumption + |assumption + ] + ] + ] + |apply not_le_to_lt.unfold.intro. + generalize in match H5. + apply (le_n_O_elim ? H7). + rewrite < times_n_O. + apply le_to_not_lt. + apply le_O_n + ] + |cut (O < m1) + [cut (j/m1 < n1) + [cut (j \mod m1 < m1) + [elim (and_true ? ? H6). + elim (H4 ? ? Hcut1 Hcut2 H7 H8). + elim H9.clear H9. + elim H11.clear H11. + elim H9.clear H9. + elim H11.clear H11. + apply (lt_times_plus_times ? ? ? m2) + [assumption|assumption] + |apply lt_mod_m_m. + assumption + ] + |apply (lt_times_n_to_lt m1) + [assumption + |apply (le_to_lt_to_lt ? j) + [apply (eq_plus_to_le ? ? (j \mod m1)). + apply div_mod. + assumption + |assumption + ] + ] + ] + |apply not_le_to_lt.unfold.intro. + generalize in match H5. + apply (le_n_O_elim ? H7). + rewrite < times_n_O. + apply le_to_not_lt. + apply le_O_n + ] + ] + ] +qed.*) + + +theorem iter_p_gen_2_eq: +\forall A:Type. +\forall baseA: A. +\forall plusA: A \to A \to A. +(symmetric A plusA) \to +(associative A plusA) \to +(\forall a:A.(plusA a baseA) = a)\to +\forall g: nat \to nat \to A. +\forall h11,h12,h21,h22: nat \to nat \to nat. +\forall n1,m1,n2,m2. +\forall p11,p21:nat \to bool. +\forall p12,p22:nat \to nat \to bool. +(\forall i,j. i < n2 \to j < m2 \to p21 i = true \to p22 i j = true \to +p11 (h11 i j) = true \land p12 (h11 i j) (h12 i j) = true +\land h21 (h11 i j) (h12 i j) = i \land h22 (h11 i j) (h12 i j) = j +\land h11 i j < n1 \land h12 i j < m1) \to +(\forall i,j. i < n1 \to j < m1 \to p11 i = true \to p12 i j = true \to +p21 (h21 i j) = true \land p22 (h21 i j) (h22 i j) = true +\land h11 (h21 i j) (h22 i j) = i \land h12 (h21 i j) (h22 i j) = j +\land (h21 i j) < n2 \land (h22 i j) < m2) \to +iter_p_gen n1 p11 A + (\lambda x:nat .iter_p_gen m1 (p12 x) A (\lambda y. g x y) baseA plusA) + baseA plusA = +iter_p_gen n2 p21 A + (\lambda x:nat .iter_p_gen m2 (p22 x) A (\lambda y. g (h11 x y) (h12 x y)) baseA plusA ) + baseA plusA. + +intros. +rewrite < (iter_p_gen2' ? ? ? ? ? ? ? ? H H1 H2). +letin ha:= (\lambda x,y.(((h11 x y)*m1) + (h12 x y))). +letin ha12:= (\lambda x.(h21 (x/m1) (x \mod m1))). +letin ha22:= (\lambda x.(h22 (x/m1) (x \mod m1))). + +apply (trans_eq ? ? +(iter_p_gen n2 p21 A (\lambda x:nat. iter_p_gen m2 (p22 x) A + (\lambda y:nat.(g (((h11 x y)*m1+(h12 x y))/m1) (((h11 x y)*m1+(h12 x y))\mod m1))) baseA plusA ) baseA plusA)) +[ + apply (iter_p_gen_knm A baseA plusA H H1 H2 (\lambda e. (g (e/m1) (e \mod m1))) ha ha12 ha22);intros + [ elim (and_true ? ? H6). + cut(O \lt m1) + [ cut(x/m1 < n1) + [ cut((x \mod m1) < m1) + [ elim (H4 ? ? Hcut1 Hcut2 H7 H8). + elim H9.clear H9. + elim H11.clear H11. + elim H9.clear H9. + elim H11.clear H11. + split + [ split + [ split + [ split + [ assumption + | assumption + ] + | unfold ha. + unfold ha12. + unfold ha22. + rewrite > H14. + rewrite > H13. + apply sym_eq. + apply div_mod. + assumption + ] + | assumption + ] + | assumption + ] + | apply lt_mod_m_m. + assumption + ] + | apply (lt_times_n_to_lt m1) + [ assumption + | apply (le_to_lt_to_lt ? x) + [ apply (eq_plus_to_le ? ? (x \mod m1)). + apply div_mod. + assumption + | assumption + ] + ] + ] + | apply not_le_to_lt.unfold.intro. + generalize in match H5. + apply (le_n_O_elim ? H9). + rewrite < times_n_O. + apply le_to_not_lt. + apply le_O_n. + ] + | elim (H3 ? ? H5 H6 H7 H8). + elim H9.clear H9. + elim H11.clear H11. + elim H9.clear H9. + elim H11.clear H11. + cut(((h11 i j)*m1 + (h12 i j))/m1 = (h11 i j)) + [ cut(((h11 i j)*m1 + (h12 i j)) \mod m1 = (h12 i j)) + [ split + [ split + [ split + [ apply true_to_true_to_andb_true + [ rewrite > Hcut. + assumption + | rewrite > Hcut1. + rewrite > Hcut. + assumption + ] + | unfold ha. + unfold ha12. + rewrite > Hcut1. + rewrite > Hcut. + assumption + ] + | unfold ha. + unfold ha22. + rewrite > Hcut1. + rewrite > Hcut. + assumption + ] + | cut(O \lt m1) + [ cut(O \lt n1) + [ apply (lt_to_le_to_lt ? ((h11 i j)*m1 + m1) ) + [ unfold ha. + apply (lt_plus_r). + assumption + | rewrite > sym_plus. + rewrite > (sym_times (h11 i j) m1). + rewrite > times_n_Sm. + rewrite > sym_times. + apply (le_times_l). + assumption + ] + | apply not_le_to_lt.unfold.intro. + generalize in match H12. + apply (le_n_O_elim ? H11). + apply le_to_not_lt. + apply le_O_n + ] + | apply not_le_to_lt.unfold.intro. + generalize in match H10. + apply (le_n_O_elim ? H11). + apply le_to_not_lt. + apply le_O_n + ] + ] + | rewrite > (mod_plus_times m1 (h11 i j) (h12 i j)). + reflexivity. + assumption + ] + | rewrite > (div_plus_times m1 (h11 i j) (h12 i j)). + reflexivity. + assumption + ] + ] +| apply (eq_iter_p_gen1) + [ intros. reflexivity + | intros. + apply (eq_iter_p_gen1) + [ intros. reflexivity + | intros. + rewrite > (div_plus_times) + [ rewrite > (mod_plus_times) + [ reflexivity + | elim (H3 x x1 H5 H7 H6 H8). + assumption + ] + | elim (H3 x x1 H5 H7 H6 H8). + assumption + ] + ] + ] +] +qed. +theorem iter_p_gen_iter_p_gen: +\forall A:Type. +\forall baseA: A. +\forall plusA: A \to A \to A. +(symmetric A plusA) \to +(associative A plusA) \to +(\forall a:A.(plusA a baseA) = a)\to +\forall g: nat \to nat \to A. +\forall n,m. +\forall p11,p21:nat \to bool. +\forall p12,p22:nat \to nat \to bool. +(\forall x,y. x < n \to y < m \to + (p11 x \land p12 x y) = (p21 y \land p22 y x)) \to +iter_p_gen n p11 A + (\lambda x:nat.iter_p_gen m (p12 x) A (\lambda y. g x y) baseA plusA) + baseA plusA = +iter_p_gen m p21 A + (\lambda y:nat.iter_p_gen n (p22 y) A (\lambda x. g x y) baseA plusA ) + baseA plusA. +intros. +apply (iter_p_gen_2_eq A baseA plusA H H1 H2 (\lambda x,y. g x y) (\lambda x,y.y) (\lambda x,y.x) (\lambda x,y.y) (\lambda x,y.x) + n m m n p11 p21 p12 p22) + [intros.split + [split + [split + [split + [split + [apply (andb_true_true ? (p12 j i)). + rewrite > H3 + [rewrite > H6.rewrite > H7.reflexivity + |assumption + |assumption + ] + |apply (andb_true_true_r (p11 j)). + rewrite > H3 + [rewrite > H6.rewrite > H7.reflexivity + |assumption + |assumption + ] + ] + |reflexivity + ] + |reflexivity + ] + |assumption + ] + |assumption + ] + |intros.split + [split + [split + [split + [split + [apply (andb_true_true ? (p22 j i)). + rewrite < H3 + [rewrite > H6.rewrite > H7.reflexivity + |assumption + |assumption + ] + |apply (andb_true_true_r (p21 j)). + rewrite < H3 + [rewrite > H6.rewrite > H7.reflexivity + |assumption + |assumption + ] + ] + |reflexivity + ] + |reflexivity + ] + |assumption + ] + |assumption + ] + ] +qed. \ No newline at end of file