X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2Fnat%2Flog.ma;fp=helm%2Fmatita%2Flibrary%2Fnat%2Flog.ma;h=9f32777b3cda096a75a2bc6d549301ded1c5bc61;hb=da83446deba30fbe32b9bf617d83bd22cc9c9770;hp=0000000000000000000000000000000000000000;hpb=e4384a12ff13352f8f87124f214072446164ed2b;p=helm.git diff --git a/helm/matita/library/nat/log.ma b/helm/matita/library/nat/log.ma new file mode 100644 index 000000000..9f32777b3 --- /dev/null +++ b/helm/matita/library/nat/log.ma @@ -0,0 +1,194 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| A.Asperti, C.Sacerdoti Coen, *) +(* ||A|| E.Tassi, S.Zacchiroli *) +(* \ / *) +(* \ / Matita is distributed under the terms of the *) +(* v GNU Lesser General Public License Version 2.1 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/nat/log". + +include "datatypes/constructors.ma". +include "nat/primes.ma". +include "nat/exp.ma". + +(* this definition of log is based on pairs, with a remainder *) + +let rec plog_aux p n m \def + match (mod n m) with + [ O \Rightarrow + match p with + [ O \Rightarrow pair nat nat O n + | (S p) \Rightarrow + match (plog_aux p (div n m) m) with + [ (pair q r) \Rightarrow pair nat nat (S q) r]] + | (S a) \Rightarrow pair nat nat O n]. + +(* plog n m = if m divides n q times, with remainder r *) +definition plog \def \lambda n,m:nat.plog_aux n n m. + +theorem plog_aux_to_Prop: \forall p,n,m. O < m \to + match plog_aux p n m with + [ (pair q r) \Rightarrow n = (exp m q)*r ]. +intro. +elim p. +change with +match ( +match (mod n m) with + [ O \Rightarrow pair nat nat O n + | (S a) \Rightarrow pair nat nat O n] ) +with + [ (pair q r) \Rightarrow n = (exp m q)*r ]. +apply nat_case (mod n m). +simplify.apply plus_n_O. +intros. +simplify.apply plus_n_O. +change with +match ( +match (mod n1 m) with + [ O \Rightarrow + match (plog_aux n (div n1 m) m) with + [ (pair q r) \Rightarrow pair nat nat (S q) r] + | (S a) \Rightarrow pair nat nat O n1] ) +with + [ (pair q r) \Rightarrow n1 = (exp m q)*r]. +apply nat_case1 (mod n1 m).intro. +change with +match ( + match (plog_aux n (div n1 m) m) with + [ (pair q r) \Rightarrow pair nat nat (S q) r]) +with + [ (pair q r) \Rightarrow n1 = (exp m q)*r]. +generalize in match (H (div n1 m) m). +elim plog_aux n (div n1 m) m. +simplify. +rewrite > assoc_times. +rewrite < H3.rewrite > plus_n_O (m*(div n1 m)). +rewrite < H2. +rewrite > sym_times. +rewrite < div_mod.reflexivity. +intros.simplify.apply plus_n_O. +assumption.assumption. +qed. + +theorem plog_aux_to_exp: \forall p,n,m,q,r. O < m \to + (pair nat nat q r) = plog_aux p n m \to n = (exp m q)*r. +intros. +change with +match (pair nat nat q r) with + [ (pair q r) \Rightarrow n = (exp m q)*r ]. +rewrite > H1. +apply plog_aux_to_Prop. +assumption. +qed. +(* questo va spostato in primes1.ma *) +theorem plog_exp: \forall n,m,i. O < m \to \not (mod n m = O) \to +\forall p. i \le p \to plog_aux p ((exp m i)*n) m = pair nat nat i n. +intros 5. +elim i. +simplify. +rewrite < plus_n_O. +apply nat_case p. +change with + match (mod n m) with + [ O \Rightarrow pair nat nat O n + | (S a) \Rightarrow pair nat nat O n] + = pair nat nat O n. +elim (mod n m).simplify.reflexivity.simplify.reflexivity. +intro. +change with + match (mod n m) with + [ O \Rightarrow + match (plog_aux m1 (div n m) m) with + [ (pair q r) \Rightarrow pair nat nat (S q) r] + | (S a) \Rightarrow pair nat nat O n] + = pair nat nat O n. +cut O < mod n m \lor O = mod n m. +elim Hcut.apply lt_O_n_elim (mod n m) H3. +intros. simplify.reflexivity. +apply False_ind. +apply H1.apply sym_eq.assumption. +apply le_to_or_lt_eq.apply le_O_n. +generalize in match H3. +apply nat_case p.intro.apply False_ind.apply not_le_Sn_O n1 H4. +intros. +change with + match (mod ((exp m (S n1))*n) m) with + [ O \Rightarrow + match (plog_aux m1 (div ((exp m (S n1))*n) m) m) with + [ (pair q r) \Rightarrow pair nat nat (S q) r] + | (S a) \Rightarrow pair nat nat O ((exp m (S n1))*n)] + = pair nat nat (S n1) n. +cut (mod ((exp m (S n1))*n) m) = O. +rewrite > Hcut. +change with +match (plog_aux m1 (div ((exp m (S n1))*n) m) m) with + [ (pair q r) \Rightarrow pair nat nat (S q) r] + = pair nat nat (S n1) n. +cut div ((exp m (S n1))*n) m = (exp m n1)*n. +rewrite > Hcut1. +rewrite > H2 m1. simplify.reflexivity. +(* div_exp *) +change with div (m*(exp m n1)*n) m = (exp m n1)*n. +rewrite > assoc_times. +apply lt_O_n_elim m H. +intro.apply div_times. +(* mod_exp = O *) +apply divides_to_mod_O. +assumption. +simplify.rewrite > assoc_times. +apply witness ? ? ((exp m n1)*n).reflexivity. +apply le_S_S_to_le.assumption. +qed. + +theorem plog_aux_to_Prop1: \forall p,n,m. (S O) < m \to O < n \to n \le p \to + match plog_aux p n m with + [ (pair q r) \Rightarrow \lnot (mod r m = O)]. +intro.elim p.absurd O < n.assumption. +apply le_to_not_lt.assumption. +change with +match + (match (mod n1 m) with + [ O \Rightarrow + match (plog_aux n(div n1 m) m) with + [ (pair q r) \Rightarrow pair nat nat (S q) r] + | (S a) \Rightarrow pair nat nat O n1]) +with + [ (pair q r) \Rightarrow \lnot(mod r m = O)]. +apply nat_case1 (mod n1 m).intro. +generalize in match (H (div n1 m) m). +elim (plog_aux n (div n1 m) m). +apply H5.assumption. +apply eq_mod_O_to_lt_O_div. +apply trans_lt ? (S O).simplify.apply le_n. +assumption.assumption.assumption. +apply le_S_S_to_le. +apply trans_le ? n1.change with div n1 m < n1. +apply lt_div_n_m_n.assumption.assumption.assumption. +intros. +change with (\lnot (mod n1 m = O)). +rewrite > H4. +(* META NOT FOUND !!! +rewrite > sym_eq. *) +simplify.intro. +apply not_eq_O_S m1 ?. +rewrite > H5.reflexivity. +qed. + +theorem plog_aux_to_not_mod_O: \forall p,n,m,q,r. (S O) < m \to O < n \to n \le p \to + pair nat nat q r = plog_aux p n m \to \lnot (mod r m = O). +intros. +change with + match (pair nat nat q r) with + [ (pair q r) \Rightarrow \lnot (mod r m = O)]. +rewrite > H3. +apply plog_aux_to_Prop1. +assumption.assumption.assumption. +qed. +