From d5afc8f8891d0020f5804eb2322fc0d1c8c60702 Mon Sep 17 00:00:00 2001 From: Cristian Armentano Date: Mon, 30 Jul 2007 15:01:31 +0000 Subject: [PATCH] renamed generic_sigma_p.ma to generic_iter_p.ma --- helm/software/matita/library/Z/sigma_p.ma | 32 +- .../matita/library/nat/generic_iter_p.ma | 1012 +++++++++++++++++ .../software/matita/library/nat/iteration2.ma | 35 +- helm/software/matita/library/nat/totient.ma | 4 +- helm/software/matita/library/nat/totient1.ma | 3 - 5 files changed, 1047 insertions(+), 39 deletions(-) create mode 100644 helm/software/matita/library/nat/generic_iter_p.ma diff --git a/helm/software/matita/library/Z/sigma_p.ma b/helm/software/matita/library/Z/sigma_p.ma index a5457c7e2..92b215396 100644 --- a/helm/software/matita/library/Z/sigma_p.ma +++ b/helm/software/matita/library/Z/sigma_p.ma @@ -17,11 +17,11 @@ set "baseuri" "cic:/matita/Z/sigma_p". include "Z/times.ma". include "nat/primes.ma". include "nat/ord.ma". -include "nat/generic_sigma_p.ma". +include "nat/generic_iter_p.ma". -(* sigma_p in Z is a specialization of sigma_p_gen *) +(* sigma_p in Z is a specialization of iter_p_gen *) definition sigma_p: nat \to (nat \to bool) \to (nat \to Z) \to Z \def -\lambda n, p, g. (sigma_p_gen n p Z g OZ Zplus). +\lambda n, p, g. (iter_p_gen n p Z g OZ Zplus). theorem symmetricZPlus: symmetric Z Zplus. change with (\forall a,b:Z. (Zplus a b) = (Zplus b a)). @@ -36,7 +36,7 @@ p n = true \to sigma_p (S n) p g = (g n)+(sigma_p n p g). intros. unfold sigma_p. -apply true_to_sigma_p_Sn_gen. +apply true_to_iter_p_gen_Sn. assumption. qed. @@ -45,7 +45,7 @@ theorem false_to_sigma_p_Sn: p n = false \to sigma_p (S n) p g = sigma_p n p g. intros. unfold sigma_p. -apply false_to_sigma_p_Sn_gen. +apply false_to_iter_p_gen_Sn. assumption. qed. @@ -56,7 +56,7 @@ theorem eq_sigma_p: \forall p1,p2:nat \to bool. sigma_p n p1 g1 = sigma_p n p2 g2. intros. unfold sigma_p. -apply eq_sigma_p_gen; +apply eq_iter_p_gen; assumption. qed. @@ -67,7 +67,7 @@ theorem eq_sigma_p1: \forall p1,p2:nat \to bool. sigma_p n p1 g1 = sigma_p n p2 g2. intros. unfold sigma_p. -apply eq_sigma_p1_gen; +apply eq_iter_p_gen1; assumption. qed. @@ -75,7 +75,7 @@ theorem sigma_p_false: \forall g: nat \to Z.\forall n.sigma_p n (\lambda x.false) g = O. intros. unfold sigma_p. -apply sigma_p_false_gen. +apply iter_p_gen_false. qed. theorem sigma_p_plus: \forall n,k:nat.\forall p:nat \to bool. @@ -84,7 +84,7 @@ sigma_p (k+n) p g = sigma_p k (\lambda x.p (x+n)) (\lambda x.g (x+n)) + sigma_p n p g. intros. unfold sigma_p. -apply (sigma_p_plusA_gen Z n k p g OZ Zplus) +apply (iter_p_gen_plusA Z n k p g OZ Zplus) [ apply symmetricZPlus. | intros. apply cic:/matita/Z/plus/Zplus_z_OZ.con @@ -98,7 +98,7 @@ theorem false_to_eq_sigma_p: \forall n,m:nat.n \le m \to p i = false) \to sigma_p m p g = sigma_p n p g. intros. unfold sigma_p. -apply (false_to_eq_sigma_p_gen); +apply (false_to_eq_iter_p_gen); assumption. qed. @@ -113,7 +113,7 @@ sigma_p n p1 (\lambda x.sigma_p m p2 (g x)). intros. unfold sigma_p. -apply (sigma_p2_gen n m p1 p2 Z g OZ Zplus) +apply (iter_p_gen2 n m p1 p2 Z g OZ Zplus) [ apply symmetricZPlus | apply associative_Zplus | intros. @@ -135,7 +135,7 @@ sigma_p n p1 (\lambda x.sigma_p m (p2 x) (g x)). intros. unfold sigma_p. -apply (sigma_p2_gen' n m p1 p2 Z g OZ Zplus) +apply (iter_p_gen2' n m p1 p2 Z g OZ Zplus) [ apply symmetricZPlus | apply associative_Zplus | intros. @@ -148,7 +148,7 @@ lemma sigma_p_gi: \forall g: nat \to Z. sigma_p n p g = g i + sigma_p n (\lambda x. andb (p x) (notb (eqb x i))) g. intros. unfold sigma_p. -apply (sigma_p_gi_gen) +apply (iter_p_gen_gi) [ apply symmetricZPlus | apply associative_Zplus | intros. @@ -171,7 +171,7 @@ theorem eq_sigma_p_gh: sigma_p n p1 (\lambda x.g(h x)) = sigma_p n1 (\lambda x.p2 x) g. intros. unfold sigma_p. -apply (eq_sigma_p_gh_gen Z OZ Zplus ? ? ? g h h1 n n1 p1 p2) +apply (eq_iter_p_gen_gh Z OZ Zplus ? ? ? g h h1 n n1 p1 p2) [ apply symmetricZPlus | apply associative_Zplus | intros. @@ -273,7 +273,7 @@ sigma_p (S n) (\lambda x.divides_b x n) (\lambda x.sigma_p (S m) (\lambda y.true) (\lambda y.g (x*(exp p y)))). intros. unfold sigma_p. -apply (sigma_p_divides_gen Z OZ Zplus n m p ? ? ? g) +apply (iter_p_gen_divides Z OZ Zplus n m p ? ? ? g) [ assumption | assumption | assumption @@ -289,7 +289,7 @@ qed. lemma Ztimes_sigma_pl: \forall z:Z.\forall n:nat.\forall p. \forall f. z * (sigma_p n p f) = sigma_p n p (\lambda i.z*(f i)). intros. -apply (distributive_times_plus_sigma_p_generic Z Zplus OZ Ztimes n z p f) +apply (distributive_times_plus_iter_p_gen Z Zplus OZ Ztimes n z p f) [ apply symmetricZPlus | apply associative_Zplus | intros. diff --git a/helm/software/matita/library/nat/generic_iter_p.ma b/helm/software/matita/library/nat/generic_iter_p.ma new file mode 100644 index 000000000..7c972e76f --- /dev/null +++ b/helm/software/matita/library/nat/generic_iter_p.ma @@ -0,0 +1,1012 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/nat/generic_iter_p.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 + * A is the type of the elements of the sum. + * g:nat -> A, is the function which associates the nth element of the sum to the nth natural numbers + * 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 + [ O \Rightarrow baseA + | (S k) \Rightarrow + match p k with + [true \Rightarrow (plusA (g k) (iter_p_gen k p A g baseA plusA)) + |false \Rightarrow iter_p_gen k p A g baseA plusA] + ]. + +theorem true_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. +p n = true \to iter_p_gen (S n) p A g baseA plusA = +(plusA (g n) (iter_p_gen n p A g baseA plusA)). +intros. +simplify. +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. +p n = false \to iter_p_gen (S n) p A g baseA plusA = iter_p_gen n p A g baseA plusA. +intros. +simplify. +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. +(\forall x. x < n \to p1 x = p2 x) \to +(\forall x. x < n \to g1 x = g2 x) \to +iter_p_gen n p1 A g1 baseA plusA = iter_p_gen n p2 A g2 baseA plusA. +intros 8. +elim n +[ reflexivity +| apply (bool_elim ? (p1 n1)) + [ intro. + rewrite > (true_to_iter_p_gen_Sn ? ? ? ? ? ? H3). + rewrite > true_to_iter_p_gen_Sn + [ apply eq_f2 + [ apply H2.apply le_n. + | apply H + [ intros.apply H1.apply le_S.assumption + | intros.apply H2.apply le_S.assumption + ] + ] + | rewrite < H3.apply sym_eq.apply H1.apply le_n + ] + | intro. + rewrite > (false_to_iter_p_gen_Sn ? ? ? ? ? ? H3). + rewrite > false_to_iter_p_gen_Sn + [ apply H + [ intros.apply H1.apply le_S.assumption + | intros.apply H2.apply le_S.assumption + ] + | rewrite < H3.apply sym_eq.apply H1.apply le_n + ] + ] +] +qed. + +theorem eq_iter_p_gen1: \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. +(\forall x. x < n \to p1 x = p2 x) \to +(\forall x. x < n \to p1 x = true \to g1 x = g2 x) \to +iter_p_gen n p1 A g1 baseA plusA = iter_p_gen n p2 A g2 baseA plusA. +intros 8. +elim n +[ reflexivity +| apply (bool_elim ? (p1 n1)) + [ intro. + rewrite > (true_to_iter_p_gen_Sn ? ? ? ? ? ? H3). + rewrite > true_to_iter_p_gen_Sn + [ apply eq_f2 + [ apply H2 + [ apply le_n + | assumption + ] + | apply H + [ intros.apply H1.apply le_S.assumption + | intros.apply H2 + [ apply le_S.assumption + | assumption + ] + ] + ] + | rewrite < H3. + apply sym_eq.apply H1.apply le_n + ] + | intro. + rewrite > (false_to_iter_p_gen_Sn ? ? ? ? ? ? H3). + rewrite > false_to_iter_p_gen_Sn + [ apply H + [ intros.apply H1.apply le_S.assumption + | intros.apply H2 + [ apply le_S.assumption + | assumption + ] + ] + | rewrite < H3.apply sym_eq. + apply H1.apply le_n + ] + ] +] +qed. + +theorem iter_p_gen_false: \forall A:Type. \forall g: nat \to A. \forall baseA:A. +\forall plusA: A \to A \to A. \forall n. +iter_p_gen n (\lambda x.false) A g baseA plusA = baseA. +intros. +elim n +[ reflexivity +| simplify. + assumption +] +qed. + +theorem iter_p_gen_plusA: \forall A:Type. \forall n,k:nat.\forall p:nat \to bool. +\forall g: nat \to A. \forall baseA:A. \forall plusA: A \to A \to A. +(symmetric A plusA) \to (\forall a:A. (plusA a baseA) = a) \to (associative A plusA) +\to +iter_p_gen (k + n) p A g baseA plusA += (plusA (iter_p_gen k (\lambda x.p (x+n)) A (\lambda x.g (x+n)) baseA plusA) + (iter_p_gen n p A g baseA plusA)). +intros. + +elim k +[ rewrite < (plus_n_O n). + simplify. + rewrite > H in \vdash (? ? ? %). + rewrite > (H1 ?). + reflexivity +| apply (bool_elim ? (p (n1+n))) + [ intro. + rewrite > (true_to_iter_p_gen_Sn ? ? ? ? ? ? H4). + rewrite > (true_to_iter_p_gen_Sn n1 (\lambda x.p (x+n)) ? ? ? ? H4). + rewrite > (H2 (g (n1 + n)) ? ?). + rewrite < H3. + reflexivity + | intro. + rewrite > (false_to_iter_p_gen_Sn ? ? ? ? ? ? H4). + rewrite > (false_to_iter_p_gen_Sn n1 (\lambda x.p (x+n)) ? ? ? ? H4). + assumption + ] +] +qed. + +theorem false_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. +n \le m \to (\forall i:nat. n \le i \to i < m \to p i = false) +\to iter_p_gen m p A g baseA plusA = iter_p_gen n p A g baseA plusA. +intros 8. +elim H +[ reflexivity +| simplify. + rewrite > H3 + [ simplify. + apply H2. + intros. + apply H3 + [ apply H4 + | apply le_S. + assumption + ] + | assumption + |apply le_n + ] +] +qed. + +theorem iter_p_gen2 : +\forall n,m:nat. +\forall p1,p2:nat \to bool. +\forall A:Type. +\forall g: nat \to nat \to A. +\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 +iter_p_gen (n*m) + (\lambda x.andb (p1 (div x m)) (p2 (mod x m))) + A + (\lambda x.g (div x m) (mod x m)) + baseA + plusA = +iter_p_gen n p1 A + (\lambda x.iter_p_gen m p2 A (g x) baseA plusA) + baseA plusA. +intros. +elim n +[ simplify. + reflexivity +| apply (bool_elim ? (p1 n1)) + [ intro. + rewrite > (true_to_iter_p_gen_Sn ? ? ? ? ? ? H4). + simplify in \vdash (? ? (? % ? ? ? ? ?) ?). + rewrite > iter_p_gen_plusA + [ rewrite < H3. + apply eq_f2 + [ apply eq_iter_p_gen + [ intros. + rewrite > sym_plus. + rewrite > (div_plus_times ? ? ? H5). + rewrite > (mod_plus_times ? ? ? H5). + rewrite > H4. + simplify. + reflexivity + | intros. + rewrite > sym_plus. + rewrite > (div_plus_times ? ? ? H5). + rewrite > (mod_plus_times ? ? ? H5). + rewrite > H4. + simplify.reflexivity. + ] + | reflexivity + ] + | assumption + | assumption + | assumption + ] + | intro. + rewrite > (false_to_iter_p_gen_Sn ? ? ? ? ? ? H4). + simplify in \vdash (? ? (? % ? ? ? ? ?) ?). + rewrite > iter_p_gen_plusA + [ rewrite > H3. + apply (trans_eq ? ? (plusA baseA + (iter_p_gen n1 p1 A (\lambda x:nat.iter_p_gen m p2 A (g x) baseA plusA) baseA plusA ))) + [ apply eq_f2 + [ rewrite > (eq_iter_p_gen ? (\lambda x.false) A ? (\lambda x:nat.g ((x+n1*m)/m) ((x+n1*m)\mod m))) + [ apply iter_p_gen_false + | intros. + rewrite > sym_plus. + rewrite > (div_plus_times ? ? ? H5). + rewrite > (mod_plus_times ? ? ? H5). + rewrite > H4. + simplify.reflexivity + | intros.reflexivity. + ] + | reflexivity + ] + | rewrite < H. + rewrite > H2. + reflexivity. + ] + | assumption + | assumption + | assumption + ] + ] +] +qed. + + +theorem iter_p_gen2': +\forall n,m:nat. +\forall p1: nat \to bool. +\forall p2: nat \to nat \to bool. +\forall A:Type. +\forall g: nat \to nat \to A. +\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 +iter_p_gen (n*m) + (\lambda x.andb (p1 (div x m)) (p2 (div x m)(mod x m))) + A + (\lambda x.g (div x m) (mod x m)) + baseA + plusA = +iter_p_gen n p1 A + (\lambda x.iter_p_gen m (p2 x) A (g x) baseA plusA) + baseA plusA. +intros. +elim n +[ simplify. + reflexivity +| apply (bool_elim ? (p1 n1)) + [ intro. + rewrite > (true_to_iter_p_gen_Sn ? ? ? ? ? ? H4). + simplify in \vdash (? ? (? % ? ? ? ? ?) ?). + rewrite > iter_p_gen_plusA + [ rewrite < H3. + apply eq_f2 + [ apply eq_iter_p_gen + [ intros. + rewrite > sym_plus. + rewrite > (div_plus_times ? ? ? H5). + rewrite > (mod_plus_times ? ? ? H5). + rewrite > H4. + simplify. + reflexivity + | intros. + rewrite > sym_plus. + rewrite > (div_plus_times ? ? ? H5). + rewrite > (mod_plus_times ? ? ? H5). + rewrite > H4. + simplify.reflexivity. + ] + | reflexivity + ] + | assumption + | assumption + | assumption + ] + | intro. + rewrite > (false_to_iter_p_gen_Sn ? ? ? ? ? ? H4). + simplify in \vdash (? ? (? % ? ? ? ? ?) ?). + rewrite > iter_p_gen_plusA + [ rewrite > H3. + apply (trans_eq ? ? (plusA baseA + (iter_p_gen n1 p1 A (\lambda x:nat.iter_p_gen m (p2 x) A (g x) baseA plusA) baseA plusA ))) + [ apply eq_f2 + [ rewrite > (eq_iter_p_gen ? (\lambda x.false) A ? (\lambda x:nat.g ((x+n1*m)/m) ((x+n1*m)\mod m))) + [ apply iter_p_gen_false + | intros. + rewrite > sym_plus. + rewrite > (div_plus_times ? ? ? H5). + rewrite > (mod_plus_times ? ? ? H5). + rewrite > H4. + simplify.reflexivity + | intros.reflexivity. + ] + | reflexivity + ] + | rewrite < H. + rewrite > H2. + reflexivity. + ] + | assumption + | assumption + | assumption + ] + ] +] +qed. + +lemma iter_p_gen_gi: +\forall A:Type. +\forall g: nat \to A. +\forall baseA:A. +\forall plusA: A \to A \to A. +\forall n,i:nat. +\forall p:nat \to bool. +(symmetric A plusA) \to (associative A plusA) \to (\forall a:A.(plusA a baseA) = a) + \to + +i < n \to p i = true \to +(iter_p_gen n p A g baseA plusA) = +(plusA (g i) (iter_p_gen n (\lambda x:nat. andb (p x) (notb (eqb x i))) A g baseA plusA)). +intros 5. +elim n +[ apply False_ind. + apply (not_le_Sn_O i). + assumption +| apply (bool_elim ? (p n1));intro + [ elim (le_to_or_lt_eq i n1) + [ rewrite > true_to_iter_p_gen_Sn + [ rewrite > true_to_iter_p_gen_Sn + [ rewrite < (H2 (g i) ? ?). + rewrite > (H1 (g i) (g n1)). + rewrite > (H2 (g n1) ? ?). + apply eq_f2 + [ reflexivity + | apply H + [ assumption + | assumption + | assumption + | assumption + | assumption + ] + ] + | rewrite > H6.simplify. + change with (notb (eqb n1 i) = notb false). + apply eq_f. + apply not_eq_to_eqb_false. + unfold Not.intro. + apply (lt_to_not_eq ? ? H7). + apply sym_eq.assumption + ] + | assumption + ] + | rewrite > true_to_iter_p_gen_Sn + [ rewrite > H7. + apply eq_f2 + [ reflexivity + | rewrite > false_to_iter_p_gen_Sn + [ apply eq_iter_p_gen + [ intros. + elim (p x) + [ simplify. + change with (notb false = notb (eqb x n1)). + apply eq_f. + apply sym_eq. + apply not_eq_to_eqb_false. + apply (lt_to_not_eq ? ? H8) + | reflexivity + ] + | intros. + reflexivity + ] + | rewrite > H6. + rewrite > (eq_to_eqb_true ? ? (refl_eq ? n1)). + reflexivity + ] + ] + | assumption + ] + | apply le_S_S_to_le. + assumption + ] + | rewrite > false_to_iter_p_gen_Sn + [ elim (le_to_or_lt_eq i n1) + [ rewrite > false_to_iter_p_gen_Sn + [ apply H + [ assumption + | assumption + | assumption + | assumption + | assumption + ] + | rewrite > H6.reflexivity + ] + | apply False_ind. + apply not_eq_true_false. + rewrite < H5. + rewrite > H7. + assumption + | apply le_S_S_to_le. + assumption + ] + | assumption + ] + ] +] +qed. + + +theorem eq_iter_p_gen_gh: +\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 h,h1: nat \to nat. +\forall n,n1:nat. +\forall p1,p2:nat \to bool. +(\forall i. i < n \to p1 i = true \to p2 (h i) = true) \to +(\forall i. i < n \to p1 i = true \to h1 (h i) = i) \to +(\forall i. i < n \to p1 i = true \to h i < n1) \to +(\forall j. j < n1 \to p2 j = true \to p1 (h1 j) = true) \to +(\forall j. j < n1 \to p2 j = true \to h (h1 j) = j) \to +(\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. +intros 10. +elim n +[ generalize in match H8. + elim n1 + [ reflexivity + | apply (bool_elim ? (p2 n2));intro + [ apply False_ind. + apply (not_le_Sn_O (h1 n2)). + apply H10 + [ apply le_n + | assumption + ] + | rewrite > false_to_iter_p_gen_Sn + [ apply H9. + intros. + apply H10 + [ apply le_S. + apply H12 + | assumption + ] + | assumption + ] + ] + ] +| apply (bool_elim ? (p1 n1));intro + [ rewrite > true_to_iter_p_gen_Sn + [ rewrite > (iter_p_gen_gi A g baseA plusA n2 (h n1)) + [ apply eq_f2 + [ reflexivity + | apply H3 + [ intros. + rewrite > H4 + [ simplify. + change with ((\not eqb (h i) (h n1))= \not false). + apply eq_f. + apply not_eq_to_eqb_false. + unfold Not. + intro. + apply (lt_to_not_eq ? ? H11). + rewrite < H5 + [ rewrite < (H5 n1) + [ apply eq_f. + assumption + | apply le_n + | assumption + ] + | apply le_S. + assumption + | assumption + ] + | apply le_S.assumption + | assumption + ] + | intros. + apply H5 + [ apply le_S. + assumption + | assumption + ] + | intros. + apply H6 + [ apply le_S.assumption + | assumption + ] + | intros. + apply H7 + [ assumption + | generalize in match H12. + elim (p2 j) + [ reflexivity + | assumption + ] + ] + | intros. + apply H8 + [ assumption + | generalize in match H12. + elim (p2 j) + [ reflexivity + | assumption + ] + ] + | intros. + elim (le_to_or_lt_eq (h1 j) n1) + [ assumption + | generalize in match H12. + elim (p2 j) + [ simplify in H13. + absurd (j = (h n1)) + [ rewrite < H13. + rewrite > H8 + [ reflexivity + | assumption + | autobatch + ] + | apply eqb_false_to_not_eq. + generalize in match H14. + elim (eqb j (h n1)) + [ apply sym_eq.assumption + | reflexivity + ] + ] + | simplify in H14. + apply False_ind. + apply not_eq_true_false. + apply sym_eq.assumption + ] + | apply le_S_S_to_le. + apply H9 + [ assumption + | generalize in match H12. + elim (p2 j) + [ reflexivity + | assumption + ] + ] + ] + ] + ] + | assumption + | assumption + | assumption + | apply H6 + [ apply le_n + | assumption + ] + | apply H4 + [ apply le_n + | assumption + ] + ] + | assumption + ] + | rewrite > false_to_iter_p_gen_Sn + [ apply H3 + [ intros. + apply H4[apply le_S.assumption|assumption] + | intros. + apply H5[apply le_S.assumption|assumption] + | intros. + apply H6[apply le_S.assumption|assumption] + | intros. + apply H7[assumption|assumption] + | intros. + apply H8[assumption|assumption] + | intros. + elim (le_to_or_lt_eq (h1 j) n1) + [ assumption + | absurd (j = (h n1)) + [ rewrite < H13. + rewrite > H8 + [ reflexivity + | assumption + | assumption + ] + | unfold Not.intro. + apply not_eq_true_false. + rewrite < H10. + rewrite < H13. + rewrite > H7 + [ reflexivity + | assumption + | assumption + ] + ] + | apply le_S_S_to_le. + apply H9 + [ assumption + | assumption + ] + ] + ] + | assumption + ] + ] +] +qed. + + + +definition p_ord_times \def +\lambda p,m,x. + match p_ord x p with + [pair q r \Rightarrow r*m+q]. + +theorem eq_p_ord_times: \forall p,m,x. +p_ord_times p m x = (ord_rem x p)*m+(ord x p). +intros.unfold p_ord_times. unfold ord_rem. +unfold ord. +elim (p_ord x p). +reflexivity. +qed. + +theorem div_p_ord_times: +\forall p,m,x. ord x p < m \to p_ord_times p m x / m = ord_rem x p. +intros.rewrite > eq_p_ord_times. +apply div_plus_times. +assumption. +qed. + +theorem mod_p_ord_times: +\forall p,m,x. ord x p < m \to p_ord_times p m x \mod m = ord x p. +intros.rewrite > eq_p_ord_times. +apply mod_plus_times. +assumption. +qed. + +theorem iter_p_gen_divides: +\forall A:Type. +\forall baseA: A. +\forall plusA: A \to A \to A. +\forall n,m,p:nat.O < n \to prime p \to Not (divides p n) \to +\forall g: nat \to A. +(symmetric A plusA) \to (associative A plusA) \to (\forall a:A.(plusA a baseA) = a) + +\to + +iter_p_gen (S (n*(exp p m))) (\lambda x.divides_b x (n*(exp p m))) A g baseA plusA = +iter_p_gen (S n) (\lambda x.divides_b x n) A + (\lambda x.iter_p_gen (S m) (\lambda y.true) A (\lambda y.g (x*(exp p y))) baseA plusA) baseA plusA. +intros. +cut (O < p) + [rewrite < (iter_p_gen2 ? ? ? ? ? ? ? ? H3 H4 H5). + apply (trans_eq ? ? + (iter_p_gen (S n*S m) (\lambda x:nat.divides_b (x/S m) n) A + (\lambda x:nat.g (x/S m*(p)\sup(x\mod S m))) baseA plusA) ) + [apply sym_eq. + apply (eq_iter_p_gen_gh ? ? ? ? ? ? g ? (p_ord_times p (S m))) + [ assumption + | assumption + | assumption + |intros. + lapply (divides_b_true_to_lt_O ? ? H H7). + apply divides_to_divides_b_true + [rewrite > (times_n_O O). + apply lt_times + [assumption + |apply lt_O_exp.assumption + ] + |apply divides_times + [apply divides_b_true_to_divides.assumption + |apply (witness ? ? (p \sup (m-i \mod (S m)))). + rewrite < exp_plus_times. + apply eq_f. + rewrite > sym_plus. + apply plus_minus_m_m. + autobatch + ] + ] + |intros. + lapply (divides_b_true_to_lt_O ? ? H H7). + unfold p_ord_times. + rewrite > (p_ord_exp1 p ? (i \mod (S m)) (i/S m)) + [change with ((i/S m)*S m+i \mod S m=i). + apply sym_eq. + apply div_mod. + apply lt_O_S + |assumption + |unfold Not.intro. + apply H2. + apply (trans_divides ? (i/ S m)) + [assumption| + apply divides_b_true_to_divides;assumption] + |apply sym_times. + ] + |intros. + apply le_S_S. + apply le_times + [apply le_S_S_to_le. + change with ((i/S m) < S n). + apply (lt_times_to_lt_l m). + apply (le_to_lt_to_lt ? i) + [autobatch|assumption] + |apply le_exp + [assumption + |apply le_S_S_to_le. + apply lt_mod_m_m. + apply lt_O_S + ] + ] + |intros. + cut (ord j p < S m) + [rewrite > div_p_ord_times + [apply divides_to_divides_b_true + [apply lt_O_ord_rem + [elim H1.assumption + |apply (divides_b_true_to_lt_O ? ? ? H7). + rewrite > (times_n_O O). + apply lt_times + [assumption|apply lt_O_exp.assumption] + ] + |cut (n = ord_rem (n*(exp p m)) p) + [rewrite > Hcut2. + apply divides_to_divides_ord_rem + [apply (divides_b_true_to_lt_O ? ? ? H7). + rewrite > (times_n_O O). + apply lt_times + [assumption|apply lt_O_exp.assumption] + |rewrite > (times_n_O O). + apply lt_times + [assumption|apply lt_O_exp.assumption] + |assumption + |apply divides_b_true_to_divides. + assumption + ] + |unfold ord_rem. + rewrite > (p_ord_exp1 p ? m n) + [reflexivity + |assumption + |assumption + |apply sym_times + ] + ] + ] + |assumption + ] + |cut (m = ord (n*(exp p m)) p) + [apply le_S_S. + rewrite > Hcut1. + apply divides_to_le_ord + [apply (divides_b_true_to_lt_O ? ? ? H7). + rewrite > (times_n_O O). + apply lt_times + [assumption|apply lt_O_exp.assumption] + |rewrite > (times_n_O O). + apply lt_times + [assumption|apply lt_O_exp.assumption] + |assumption + |apply divides_b_true_to_divides. + assumption + ] + |unfold ord. + rewrite > (p_ord_exp1 p ? m n) + [reflexivity + |assumption + |assumption + |apply sym_times + ] + ] + ] + |intros. + cut (ord j p < S m) + [rewrite > div_p_ord_times + [rewrite > mod_p_ord_times + [rewrite > sym_times. + apply sym_eq. + apply exp_ord + [elim H1.assumption + |apply (divides_b_true_to_lt_O ? ? ? H7). + rewrite > (times_n_O O). + apply lt_times + [assumption|apply lt_O_exp.assumption] + ] + |cut (m = ord (n*(exp p m)) p) + [apply le_S_S. + rewrite > Hcut2. + apply divides_to_le_ord + [apply (divides_b_true_to_lt_O ? ? ? H7). + rewrite > (times_n_O O). + apply lt_times + [assumption|apply lt_O_exp.assumption] + |rewrite > (times_n_O O). + apply lt_times + [assumption|apply lt_O_exp.assumption] + |assumption + |apply divides_b_true_to_divides. + assumption + ] + |unfold ord. + rewrite > (p_ord_exp1 p ? m n) + [reflexivity + |assumption + |assumption + |apply sym_times + ] + ] + ] + |assumption + ] + |cut (m = ord (n*(exp p m)) p) + [apply le_S_S. + rewrite > Hcut1. + apply divides_to_le_ord + [apply (divides_b_true_to_lt_O ? ? ? H7). + rewrite > (times_n_O O). + apply lt_times + [assumption|apply lt_O_exp.assumption] + |rewrite > (times_n_O O). + apply lt_times + [assumption|apply lt_O_exp.assumption] + |assumption + |apply divides_b_true_to_divides. + assumption + ] + |unfold ord. + rewrite > (p_ord_exp1 p ? m n) + [reflexivity + |assumption + |assumption + |apply sym_times + ] + ] + ] + |intros. + rewrite > eq_p_ord_times. + rewrite > sym_plus. + apply (lt_to_le_to_lt ? (S m +ord_rem j p*S m)) + [apply lt_plus_l. + apply le_S_S. + cut (m = ord (n*(p \sup m)) p) + [rewrite > Hcut1. + apply divides_to_le_ord + [apply (divides_b_true_to_lt_O ? ? ? H7). + rewrite > (times_n_O O). + apply lt_times + [assumption|apply lt_O_exp.assumption] + |rewrite > (times_n_O O). + apply lt_times + [assumption|apply lt_O_exp.assumption] + |assumption + |apply divides_b_true_to_divides. + assumption + ] + |unfold ord. + rewrite > sym_times. + rewrite > (p_ord_exp1 p ? m n) + [reflexivity + |assumption + |assumption + |reflexivity + ] + ] + |change with (S (ord_rem j p)*S m \le S n*S m). + apply le_times_l. + apply le_S_S. + cut (n = ord_rem (n*(p \sup m)) p) + [rewrite > Hcut1. + apply divides_to_le + [apply lt_O_ord_rem + [elim H1.assumption + |rewrite > (times_n_O O). + apply lt_times + [assumption|apply lt_O_exp.assumption] + ] + |apply divides_to_divides_ord_rem + [apply (divides_b_true_to_lt_O ? ? ? H7). + rewrite > (times_n_O O). + apply lt_times + [assumption|apply lt_O_exp.assumption] + |rewrite > (times_n_O O). + apply lt_times + [assumption|apply lt_O_exp.assumption] + |assumption + |apply divides_b_true_to_divides. + assumption + ] + ] + |unfold ord_rem. + rewrite > sym_times. + rewrite > (p_ord_exp1 p ? m n) + [reflexivity + |assumption + |assumption + |reflexivity + ] + ] + ] + ] + |apply eq_iter_p_gen + + [intros. + elim (divides_b (x/S m) n);reflexivity + |intros.reflexivity + ] + ] +|elim H1.apply lt_to_le.assumption +] +qed. + +(*distributive property for iter_p_gen*) +theorem distributive_times_plus_iter_p_gen: \forall A:Type. +\forall plusA: A \to A \to A. \forall basePlusA: A. +\forall timesA: A \to A \to A. +\forall n:nat. \forall k:A. \forall p:nat \to bool. \forall g:nat \to A. +(symmetric A plusA) \to (associative A plusA) \to (\forall a:A.(plusA a basePlusA) = a) \to +(symmetric A timesA) \to (distributive A timesA plusA) \to +(\forall a:A. (timesA a basePlusA) = basePlusA) + + \to + +((timesA k (iter_p_gen n p A g basePlusA plusA)) = + (iter_p_gen n p A (\lambda i:nat.(timesA k (g i))) basePlusA plusA)). +intros. +elim n +[ simplify. + apply H5 +| cut( (p n1) = true \lor (p n1) = false) + [ elim Hcut + [ rewrite > (true_to_iter_p_gen_Sn ? ? ? ? ? ? H7). + rewrite > (true_to_iter_p_gen_Sn ? ? ? ? ? ? H7) in \vdash (? ? ? %). + rewrite > (H4). + rewrite > (H3 k (g n1)). + apply eq_f. + assumption + | rewrite > (false_to_iter_p_gen_Sn ? ? ? ? ? ? H7). + rewrite > (false_to_iter_p_gen_Sn ? ? ? ? ? ? H7) in \vdash (? ? ? %). + assumption + ] + | elim ((p n1)) + [ left. + reflexivity + | right. + reflexivity + ] + ] +] +qed. + + diff --git a/helm/software/matita/library/nat/iteration2.ma b/helm/software/matita/library/nat/iteration2.ma index 4f0238498..3a6bab396 100644 --- a/helm/software/matita/library/nat/iteration2.ma +++ b/helm/software/matita/library/nat/iteration2.ma @@ -16,13 +16,13 @@ set "baseuri" "cic:/matita/nat/iteration2". include "nat/primes.ma". include "nat/ord.ma". -include "nat/generic_sigma_p.ma". +include "nat/generic_iter_p.ma". include "nat/count.ma".(*necessary just to use bool_to_nat and bool_to_nat_andb*) (* sigma_p on nautral numbers is a specialization of sigma_p_gen *) definition sigma_p: nat \to (nat \to bool) \to (nat \to nat) \to nat \def -\lambda n, p, g. (sigma_p_gen n p nat g O plus). +\lambda n, p, g. (iter_p_gen n p nat g O plus). theorem symmetricIntPlus: symmetric nat plus. change with (\forall a,b:nat. (plus a b) = (plus b a)). @@ -40,7 +40,7 @@ p n = true \to sigma_p (S n) p g = (g n)+(sigma_p n p g). intros. unfold sigma_p. -apply true_to_sigma_p_Sn_gen. +apply true_to_iter_p_gen_Sn. assumption. qed. @@ -49,10 +49,9 @@ theorem false_to_sigma_p_Sn: p n = false \to sigma_p (S n) p g = sigma_p n p g. intros. unfold sigma_p. -apply false_to_sigma_p_Sn_gen. +apply false_to_iter_p_gen_Sn. assumption. - -qed. +qed. theorem eq_sigma_p: \forall p1,p2:nat \to bool. \forall g1,g2: nat \to nat.\forall n. @@ -61,7 +60,7 @@ theorem eq_sigma_p: \forall p1,p2:nat \to bool. sigma_p n p1 g1 = sigma_p n p2 g2. intros. unfold sigma_p. -apply eq_sigma_p_gen; +apply eq_iter_p_gen; assumption. qed. @@ -72,7 +71,7 @@ theorem eq_sigma_p1: \forall p1,p2:nat \to bool. sigma_p n p1 g1 = sigma_p n p2 g2. intros. unfold sigma_p. -apply eq_sigma_p1_gen; +apply eq_iter_p_gen1; assumption. qed. @@ -80,7 +79,7 @@ theorem sigma_p_false: \forall g: nat \to nat.\forall n.sigma_p n (\lambda x.false) g = O. intros. unfold sigma_p. -apply sigma_p_false_gen. +apply iter_p_gen_false. qed. theorem sigma_p_plus: \forall n,k:nat.\forall p:nat \to bool. @@ -89,7 +88,7 @@ sigma_p (k+n) p g = sigma_p k (\lambda x.p (x+n)) (\lambda x.g (x+n)) + sigma_p n p g. intros. unfold sigma_p. -apply (sigma_p_plusA_gen nat n k p g O plus) +apply (iter_p_gen_plusA nat n k p g O plus) [ apply symmetricIntPlus. | intros. apply sym_eq. @@ -104,7 +103,7 @@ theorem false_to_eq_sigma_p: \forall n,m:nat.n \le m \to p i = false) \to sigma_p m p g = sigma_p n p g. intros. unfold sigma_p. -apply (false_to_eq_sigma_p_gen); +apply (false_to_eq_iter_p_gen); assumption. qed. @@ -119,7 +118,7 @@ sigma_p n p1 (\lambda x.sigma_p m p2 (g x)). intros. unfold sigma_p. -apply (sigma_p2_gen n m p1 p2 nat g O plus) +apply (iter_p_gen2 n m p1 p2 nat g O plus) [ apply symmetricIntPlus | apply associative_plus | intros. @@ -134,13 +133,13 @@ theorem sigma_p2' : \forall p2:nat \to nat \to bool. \forall g: nat \to nat \to nat. sigma_p (n*m) - (\lambda x.andb (p1 (div x m)) (p2 (div x m) (mod x m))) + (\lambda x.andb (p1 (div x m)) (p2 (div x m) (mod x m))) (\lambda x.g (div x m) (mod x m)) = sigma_p n p1 (\lambda x.sigma_p m (p2 x) (g x)). intros. unfold sigma_p. -apply (sigma_p2_gen' n m p1 p2 nat g O plus) +apply (iter_p_gen2' n m p1 p2 nat g O plus) [ apply symmetricIntPlus | apply associative_plus | intros. @@ -154,7 +153,7 @@ lemma sigma_p_gi: \forall g: nat \to nat. sigma_p n p g = g i + sigma_p n (\lambda x. andb (p x) (notb (eqb x i))) g. intros. unfold sigma_p. -apply (sigma_p_gi_gen) +apply (iter_p_gen_gi) [ apply symmetricIntPlus | apply associative_plus | intros. @@ -177,7 +176,7 @@ theorem eq_sigma_p_gh: sigma_p n p1 (\lambda x.g(h x)) = sigma_p n1 (\lambda x.p2 x) g. intros. unfold sigma_p. -apply (eq_sigma_p_gh_gen nat O plus ? ? ? g h h1 n n1 p1 p2) +apply (eq_iter_p_gen_gh nat O plus ? ? ? g h h1 n n1 p1 p2) [ apply symmetricIntPlus | apply associative_plus | intros. @@ -201,7 +200,7 @@ sigma_p (S n) (\lambda x.divides_b x n) (\lambda x.sigma_p (S m) (\lambda y.true) (\lambda y.g (x*(exp p y)))). intros. unfold sigma_p. -apply (sigma_p_divides_gen nat O plus n m p ? ? ? g) +apply (iter_p_gen_divides nat O plus n m p ? ? ? g) [ assumption | assumption | assumption @@ -216,7 +215,7 @@ qed. theorem distributive_times_plus_sigma_p: \forall n,k:nat. \forall p:nat \to bool. \forall g:nat \to nat. k*(sigma_p n p g) = sigma_p n p (\lambda i:nat.k * (g i)). intros. -apply (distributive_times_plus_sigma_p_generic nat plus O times n k p g) +apply (distributive_times_plus_iter_p_gen nat plus O times n k p g) [ apply symmetricIntPlus | apply associative_plus | intros. diff --git a/helm/software/matita/library/nat/totient.ma b/helm/software/matita/library/nat/totient.ma index 03e2587a8..a86986a81 100644 --- a/helm/software/matita/library/nat/totient.ma +++ b/helm/software/matita/library/nat/totient.ma @@ -24,7 +24,7 @@ include "nat/iteration2.ma". phi (n) is the number of naturals i (less or equal than n) so then gcd (i,n) = 1. (so this definition considers the values i=1,2,...,n) - sigma_p doesn't work ok the value n (but the first value it works on is (pred n)) + sigma_p doesn't work on the value n (but the first value it works on is (pred n)) but works also on 0. That's not a problem, in fact - if n <> 1, gcd (n,0) <>1 and gcd (n,n) = n <> 1. - if n = 1, then Phi(n) = 1, and (totient n), as defined below, returns 1. @@ -134,4 +134,4 @@ apply (nat_case1 n) ] ] ] -qed. \ No newline at end of file +qed. diff --git a/helm/software/matita/library/nat/totient1.ma b/helm/software/matita/library/nat/totient1.ma index feaf1314b..d7483b3b4 100644 --- a/helm/software/matita/library/nat/totient1.ma +++ b/helm/software/matita/library/nat/totient1.ma @@ -96,7 +96,6 @@ cut (O \lt (pred n)) ] qed. - (*3rd*) theorem aux_S_i_mod_n_le_i_div_n: \forall i,n:nat. i < n*n \to (divides_b (i/n) (pred n) \land @@ -413,8 +412,6 @@ cut (O \lt n) ] qed. - - (*6th*) theorem sum_divisor_totient1_aux_6: \forall j,n:nat. -- 2.39.2