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=bfb7fbf61e86114e49cb3671503e8307a4582342;hp=3a9adc231262f58a9bfc5da65783cf790b4e9a89;hpb=59cce4c27057cff97d9b4311a379c3107c5ee9a3;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 3a9adc231..4796ec10b 100644 --- a/helm/software/matita/library/nat/generic_iter_p.ma +++ b/helm/software/matita/library/nat/generic_iter_p.ma @@ -12,8 +12,7 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/nat/generic_iter_p". - +include "nat/div_and_mod_diseq.ma". include "nat/primes.ma". include "nat/ord.ma". @@ -47,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. @@ -59,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. @@ -205,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. @@ -667,9 +704,38 @@ elim n ] qed. - -(* da spostare *) - +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 @@ -708,23 +774,6 @@ elim (le_to_or_lt_eq O ? (le_O_n m)) ] qed. -(* lemmino da postare *) -theorem lt_times_to_lt_div: \forall i,n,m. i < n*m \to i/m < n. -intros. -cut (O < m) - [apply (lt_times_n_to_lt m) - [assumption - |apply (le_to_lt_to_lt ? i) - [rewrite > (div_mod i m) in \vdash (? ? %). - apply le_plus_n_r. - assumption - |assumption - ] - ] - |apply (lt_times_to_lt_O ? ? ? H) - ] -qed. - theorem iter_p_gen_knm: \forall A:Type. \forall baseA: A. @@ -1522,7 +1571,10 @@ apply (trans_eq ? ? [ assumption | assumption ] - | rewrite > H14. + | unfold ha. + unfold ha12. + unfold ha22. + rewrite > H14. rewrite > H13. apply sym_eq. apply div_mod. @@ -1569,18 +1621,23 @@ apply (trans_eq ? ? rewrite > Hcut. assumption ] - | rewrite > Hcut1. + | unfold ha. + unfold ha12. + rewrite > Hcut1. rewrite > Hcut. assumption ] - | rewrite > Hcut1. + | 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) ) - [ apply (lt_plus_r). + [ unfold ha. + apply (lt_plus_r). assumption | rewrite > sym_plus. rewrite > (sym_times (h11 i j) m1). @@ -1631,7 +1688,79 @@ apply (trans_eq ? ? ] 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