X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Flibrary%2Fnat%2Ford.ma;h=ba08a0dcf5ba21536cb4830f10c22e88b5eac00a;hb=f0a11927dd1519e748d2eb6ecaaa4d035693d442;hp=24874c08af2fd10d2e3286f01e388940f3390d51;hpb=7f2444c2670cadafddd8785b687ef312158376b0;p=helm.git

diff --git a/matita/library/nat/ord.ma b/matita/library/nat/ord.ma
index 24874c08a..ba08a0dcf 100644
--- a/matita/library/nat/ord.ma
+++ b/matita/library/nat/ord.ma
@@ -12,12 +12,12 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/log".
+set "baseuri" "cic:/matita/nat/ord".
 
 include "datatypes/constructors.ma".
 include "nat/exp.ma".
-include "nat/lt_arith.ma".
-include "nat/primes.ma".
+include "nat/gcd.ma".
+include "nat/relevant_equations.ma". (* required by auto paramod *)
 
 (* this definition of log is based on pairs, with a remainder *)
 
@@ -38,34 +38,14 @@ theorem p_ord_aux_to_Prop: \forall p,n,m. O < m \to
   match p_ord_aux p n m with
   [ (pair q r) \Rightarrow n = m \sup q *r ].
 intro.
-elim p.
-change with 
-match (
-match n \mod m with
-  [ O \Rightarrow pair nat nat O n
-  | (S a) \Rightarrow pair nat nat O n] )
-with
-  [ (pair q r) \Rightarrow n = m \sup q * r ].
+elim p.simplify.
 apply (nat_case (n \mod m)).
 simplify.apply plus_n_O.
 intros.
-simplify.apply plus_n_O. 
-change with 
-match (
-match n1 \mod m with
-  [ O \Rightarrow 
-     match (p_ord_aux n (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 = m \sup q * r].
+simplify.apply plus_n_O.
+simplify. 
 apply (nat_case1 (n1 \mod m)).intro.
-change with 
-match (
- match (p_ord_aux n (n1 / m) m) with
-   [ (pair q r) \Rightarrow pair nat nat (S q) r])
-with
-  [ (pair q r) \Rightarrow n1 = m \sup q * r].
+simplify.
 generalize in match (H (n1 / m) m).
 elim (p_ord_aux n (n1 / m) m).
 simplify.
@@ -88,6 +68,7 @@ rewrite > H1.
 apply p_ord_aux_to_Prop.
 assumption.
 qed.
+
 (* questo va spostato in primes1.ma *)
 theorem p_ord_exp: \forall n,m,i. O < m \to n \mod m \neq O \to
 \forall p. i \le p \to p_ord_aux p (m \sup i * n) m = pair nat nat i n.
@@ -96,20 +77,10 @@ elim i.
 simplify.
 rewrite < plus_n_O.
 apply (nat_case p).
-change with
- (match n \mod m with
-  [ O \Rightarrow pair nat nat O n
-  | (S a) \Rightarrow pair nat nat O n]
-  = pair nat nat O n).
+simplify.
 elim (n \mod m).simplify.reflexivity.simplify.reflexivity.
 intro.
-change with
- (match n \mod m with
-  [ O \Rightarrow 
-       match (p_ord_aux m1 (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).
+simplify.
 cut (O < n \mod m \lor O = n \mod m).
 elim Hcut.apply (lt_O_n_elim (n \mod m) H3).
 intros. simplify.reflexivity.
@@ -119,25 +90,16 @@ 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 ((m \sup (S n1) *n) \mod m) with
-  [ O \Rightarrow 
-       match (p_ord_aux m1 ((m \sup (S n1) *n) / m) m) with
-       [ (pair q r) \Rightarrow pair nat nat (S q) r]
-  | (S a) \Rightarrow pair nat nat O (m \sup (S n1) *n)]
-  = pair nat nat (S n1) n).
+simplify. fold simplify (m \sup (S n1)).
 cut (((m \sup (S n1)*n) \mod m) = O).
 rewrite > Hcut.
-change with
-(match (p_ord_aux m1 ((m \sup (S n1)*n) / m) m) with
-       [ (pair q r) \Rightarrow pair nat nat (S q) r] 
-  = pair nat nat (S n1) n). 
+simplify.fold simplify (m \sup (S n1)).
 cut ((m \sup (S n1) *n) / m = m \sup n1 *n).
 rewrite > Hcut1.
 rewrite > (H2 m1). simplify.reflexivity.
 apply le_S_S_to_le.assumption.
 (* div_exp *)
-change with ((m* m \sup n1 *n) / m = m \sup n1 * n).
+simplify.
 rewrite > assoc_times.
 apply (lt_O_n_elim m H).
 intro.apply div_times.
@@ -153,15 +115,7 @@ theorem p_ord_aux_to_Prop1: \forall p,n,m. (S O) < m \to O < n \to n \le p \to
   [ (pair q r) \Rightarrow r \mod m \neq O].
 intro.elim p.absurd (O < n).assumption.
 apply le_to_not_lt.assumption.
-change with
-match 
-  (match n1 \mod m with
-    [ O \Rightarrow 
-        match (p_ord_aux n(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 r \mod m \neq O].
+simplify.
 apply (nat_case1 (n1 \mod m)).intro.
 generalize in match (H (n1 / m) m).
 elim (p_ord_aux n (n1 / m) m).
@@ -172,8 +126,7 @@ assumption.assumption.assumption.
 apply le_S_S_to_le.
 apply (trans_le ? n1).change with (n1 / m < n1).
 apply lt_div_n_m_n.assumption.assumption.assumption.
-intros.
-change with (n1 \mod m \neq O).
+intros.simplify.
 rewrite > H4.
 unfold Not.intro.
 apply (not_eq_O_S m1).
@@ -190,4 +143,101 @@ rewrite > H3.
 apply p_ord_aux_to_Prop1.
 assumption.assumption.assumption.
 qed.
-  
+
+theorem p_ord_exp1: \forall p,n,q,r. O < p \to \lnot p \divides r \to
+n = p \sup q * r \to p_ord n p = pair nat nat q r.
+intros.unfold p_ord.
+rewrite > H2.
+apply p_ord_exp
+ [assumption
+ |unfold.intro.apply H1.
+  apply mod_O_to_divides[assumption|assumption]
+ |apply (trans_le ? (p \sup q)).
+  cut ((S O) \lt p).
+  elim q.simplify.apply le_n_Sn.
+  simplify.
+  generalize in match H3.
+  apply (nat_case n1).simplify.
+  rewrite < times_n_SO.intro.assumption.
+  intros.
+  apply (trans_le ? (p*(S m))).
+  apply (trans_le ? ((S (S O))*(S m))).
+  simplify.rewrite > plus_n_Sm.
+  rewrite < plus_n_O.
+  apply le_plus_n.
+  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".
+apply not_eq_to_le_to_lt.
+  unfold.intro.apply H1.
+  rewrite < H3.
+  apply (witness ? r r ?).simplify.apply plus_n_O.
+  assumption.
+  rewrite > times_n_SO in \vdash (? % ?).
+  apply le_times_r.
+  change with (O \lt r).
+  apply not_eq_to_le_to_lt.
+  unfold.intro.
+  apply H1.rewrite < H3.
+  apply (witness ? ? O ?).rewrite < times_n_O.reflexivity.
+  apply le_O_n.
+  ]
+qed.
+
+theorem p_ord_to_exp1: \forall p,n,q,r. (S O) \lt p \to O \lt n \to p_ord n p = pair nat nat q r\to 
+\lnot p \divides r \land n = p \sup q * r.
+intros.
+unfold p_ord in H2.
+split.unfold.intro.
+apply (p_ord_aux_to_not_mod_O n n p q r).assumption.assumption.
+apply le_n.symmetry.assumption.
+apply divides_to_mod_O.apply (trans_lt ? (S O)).
+unfold.apply le_n.assumption.assumption.
+apply (p_ord_aux_to_exp n).apply (trans_lt ? (S O)).
+unfold.apply le_n.assumption.symmetry.assumption.
+qed.
+
+theorem p_ord_times: \forall p,a,b,qa,ra,qb,rb. prime p 
+\to O \lt a \to O \lt b 
+\to p_ord a p = pair nat nat qa ra  
+\to p_ord b p = pair nat nat qb rb
+\to p_ord (a*b) p = pair nat nat (qa + qb) (ra*rb).
+intros.
+cut ((S O) \lt p).
+elim (p_ord_to_exp1 ? ? ? ? Hcut H1 H3).
+elim (p_ord_to_exp1 ? ? ? ? Hcut H2 H4).
+apply p_ord_exp1.
+apply (trans_lt ? (S O)).unfold.apply le_n.assumption.
+unfold.intro.
+elim (divides_times_to_divides ? ? ? H H9).
+apply (absurd ? ? H10 H5).
+apply (absurd ? ? H10 H7).
+(* rewrite > H6.
+rewrite > H8. *)
+auto paramodulation library=yes.
+unfold prime in H. elim H. assumption.
+qed.
+
+theorem fst_p_ord_times: \forall p,a,b. prime p 
+\to O \lt a \to O \lt b 
+\to fst ? ? (p_ord (a*b) p) = (fst ? ? (p_ord a p)) + (fst ? ? (p_ord b p)).
+intros.
+rewrite > (p_ord_times p a b (fst ? ? (p_ord a p)) (snd ? ? (p_ord a p))
+(fst ? ? (p_ord b p)) (snd ? ? (p_ord b p)) H H1 H2).
+simplify.reflexivity.
+apply eq_pair_fst_snd.
+apply eq_pair_fst_snd.
+qed.
+
+theorem p_ord_p : \forall p:nat. (S O) \lt p \to p_ord p p = pair ? ? (S O) (S O).
+intros.
+apply p_ord_exp1.
+apply (trans_lt ? (S O)). unfold.apply le_n.assumption.
+unfold.intro.
+apply (absurd ? ? H).
+apply le_to_not_lt.
+apply divides_to_le.unfold.apply le_n.assumption.
+rewrite < times_n_SO.
+apply exp_n_SO.
+qed.
\ No newline at end of file