X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Ford.ma;h=c45bfe701df66faeb665c9296c2e31690f609ff6;hb=e1f0bb910f75b8b21f2c5e394ebb4c5a63ef4945;hp=e9353ba5b31af9903f2c8270025773c8b2c6e7fe;hpb=68a2f8d0a8c34cb7ea0438c7db9222a853a38826;p=helm.git diff --git a/helm/software/matita/library/nat/ord.ma b/helm/software/matita/library/nat/ord.ma index e9353ba5b..c45bfe701 100644 --- a/helm/software/matita/library/nat/ord.ma +++ b/helm/software/matita/library/nat/ord.ma @@ -17,8 +17,7 @@ set "baseuri" "cic:/matita/nat/ord". include "datatypes/constructors.ma". include "nat/exp.ma". include "nat/gcd.ma". - -(* this definition of log is based on pairs, with a remainder *) +include "nat/relevant_equations.ma". (* required by auto paramod *) let rec p_ord_aux p n m \def match n \mod m with @@ -167,7 +166,7 @@ apply p_ord_exp apply le_times_l. assumption. apply le_times_r.assumption. - alias id "not_eq_to_le_to_lt" = "cic:/matita/algebra/finite_groups/not_eq_to_le_to_lt.con". +alias id "not_eq_to_le_to_lt" = "cic:/matita/algebra/finite_groups/not_eq_to_le_to_lt.con". apply not_eq_to_le_to_lt. unfold.intro.apply H1. rewrite < H3. @@ -212,8 +211,8 @@ unfold.intro. elim (divides_times_to_divides ? ? ? H H9). apply (absurd ? ? H10 H5). apply (absurd ? ? H10 H7). -rewrite > H6. -rewrite > H8. +(* rewrite > H6. +rewrite > H8. *) auto paramodulation. unfold prime in H. elim H. assumption. qed. @@ -239,4 +238,173 @@ apply le_to_not_lt. apply divides_to_le.unfold.apply le_n.assumption. rewrite < times_n_SO. apply exp_n_SO. +qed. + +theorem divides_to_p_ord: \forall p,a,b,c,d,n,m:nat. +O < n \to O < m \to prime p +\to divides n m \to p_ord n p = pair ? ? a b \to +p_ord m p = pair ? ? c d \to divides b d \land a \le c. +intros. +cut (S O < p) + [lapply (p_ord_to_exp1 ? ? ? ? Hcut H H4). + lapply (p_ord_to_exp1 ? ? ? ? Hcut H1 H5). + elim Hletin. clear Hletin. + elim Hletin1. clear Hletin1. + rewrite > H9 in H3. + split + [apply (gcd_SO_to_divides_times_to_divides (exp p c)) + [elim (le_to_or_lt_eq ? ? (le_O_n b)) + [assumption + |apply False_ind. + apply (lt_to_not_eq O ? H). + rewrite > H7. + rewrite < H10. + auto + ] + |elim c + [rewrite > sym_gcd. + apply gcd_SO_n + |simplify. + apply eq_gcd_times_SO + [apply lt_to_le.assumption + |apply lt_O_exp.apply lt_to_le.assumption + |rewrite > sym_gcd. + (* hint non trova prime_to_gcd_SO e + auto non chiude il goal *) + apply prime_to_gcd_SO + [assumption|assumption] + |assumption + ] + ] + |apply (trans_divides ? n) + [apply (witness ? ? (exp p a)). + rewrite > sym_times. + assumption + |assumption + ] + ] + |apply (le_exp_to_le p) + [assumption + |apply divides_to_le + [apply lt_O_exp.apply lt_to_le.assumption + |apply (gcd_SO_to_divides_times_to_divides d) + [apply lt_O_exp.apply lt_to_le.assumption + |elim a + [apply gcd_SO_n + |simplify.rewrite < sym_gcd. + apply eq_gcd_times_SO + [apply lt_to_le.assumption + |apply lt_O_exp.apply lt_to_le.assumption + |rewrite > sym_gcd. + (* hint non trova prime_to_gcd_SO e + auto non chiude il goal *) + apply prime_to_gcd_SO + [assumption|assumption] + |rewrite > sym_gcd. assumption + ] + ] + |apply (trans_divides ? n) + [apply (witness ? ? b).assumption + |rewrite > sym_times.assumption + ] + ] + ] + ] + ] + |elim H2.assumption + ] +qed. + +definition ord :nat \to nat \to nat \def +\lambda n,p. fst ? ? (p_ord n p). + +definition ord_rem :nat \to nat \to nat \def +\lambda n,p. snd ? ? (p_ord n p). + +theorem divides_to_ord: \forall p,n,m:nat. +O < n \to O < m \to prime p +\to divides n m +\to divides (ord_rem n p) (ord_rem m p) \land (ord n p) \le (ord m p). +intros. +apply (divides_to_p_ord p ? ? ? ? n m H H1 H2 H3) + [unfold ord.unfold ord_rem.apply eq_pair_fst_snd + |unfold ord.unfold ord_rem.apply eq_pair_fst_snd + ] +qed. + +theorem divides_to_divides_ord_rem: \forall p,n,m:nat. +O < n \to O < m \to prime p \to divides n m \to +divides (ord_rem n p) (ord_rem m p). +intros. +elim (divides_to_ord p n m H H1 H2 H3).assumption. +qed. + +theorem divides_to_le_ord: \forall p,n,m:nat. +O < n \to O < m \to prime p \to divides n m \to +(ord n p) \le (ord m p). +intros. +elim (divides_to_ord p n m H H1 H2 H3).assumption. +qed. + +theorem exp_ord: \forall p,n. (S O) \lt p +\to O \lt n \to n = p \sup (ord n p) * (ord_rem n p). +intros. +elim (p_ord_to_exp1 p n (ord n p) (ord_rem n p)) + [assumption + |assumption + |assumption + |unfold ord.unfold ord_rem. + apply eq_pair_fst_snd + ] +qed. + +theorem divides_ord_rem: \forall p,n. (S O) < p \to O < n +\to divides (ord_rem n p) n. +intros. +apply (witness ? ? (p \sup (ord n p))). +rewrite > sym_times. +apply exp_ord[assumption|assumption] +qed. + +theorem lt_O_ord_rem: \forall p,n. (S O) < p \to O < n \to O < ord_rem n p. +intros. +elim (le_to_or_lt_eq O (ord_rem n p)) + [assumption + |apply False_ind. + apply (lt_to_not_eq ? ? H1). + lapply (divides_ord_rem ? ? H H1). + rewrite < H2 in Hletin. + elim Hletin. + rewrite > H3. + reflexivity + |apply le_O_n + ] +qed. + +(* p_ord_inv is the inverse of ord *) +definition p_ord_inv \def +\lambda p,m,x. + match p_ord x p with + [pair q r \Rightarrow r*m+q]. + +theorem eq_p_ord_inv: \forall p,m,x. +p_ord_inv p m x = (ord_rem x p)*m+(ord x p). +intros.unfold p_ord_inv. unfold ord_rem. +unfold ord. +elim (p_ord x p). +reflexivity. +qed. + +theorem div_p_ord_inv: +\forall p,m,x. ord x p < m \to p_ord_inv p m x / m = ord_rem x p. +intros.rewrite > eq_p_ord_inv. +apply div_plus_times. +assumption. +qed. + +theorem mod_p_ord_inv: +\forall p,m,x. ord x p < m \to p_ord_inv p m x \mod m = ord x p. +intros.rewrite > eq_p_ord_inv. +apply mod_plus_times. +assumption. qed. \ No newline at end of file