X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Ford.ma;h=340e33a865fb809d8beb35e632f4e129fa2bd0dc;hb=071bb57c99e38a52d2606f7aca47bf56cdeaff53;hp=159e8613b30ea600c9477a21ca277911823a9b74;hpb=6423f1b6e3056883016598e454c55cab1004dfd2;p=helm.git

diff --git a/helm/software/matita/library/nat/ord.ma b/helm/software/matita/library/nat/ord.ma
index 159e8613b..340e33a86 100644
--- a/helm/software/matita/library/nat/ord.ma
+++ b/helm/software/matita/library/nat/ord.ma
@@ -16,8 +16,8 @@ set "baseuri" "cic:/matita/nat/ord".
 
 include "datatypes/constructors.ma".
 include "nat/exp.ma".
-include "nat/gcd.ma".
-include "nat/relevant_equations.ma". (* required by auto paramod *)
+include "nat/nth_prime.ma".
+include "nat/relevant_equations.ma". (* required by autobatch paramod *)
 
 let rec p_ord_aux p n m \def
   match n \mod m with
@@ -166,8 +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".
-apply not_eq_to_le_to_lt.
+  apply not_eq_to_le_to_lt.
   unfold.intro.apply H1.
   rewrite < H3.
   apply (witness ? r r ?).simplify.apply plus_n_O.
@@ -213,7 +212,7 @@ apply (absurd ? ? H10 H5).
 apply (absurd ? ? H10 H7).
 (* rewrite > H6.
 rewrite > H8. *)
-auto paramodulation.
+autobatch paramodulation.
 unfold prime in H. elim H. assumption.
 qed.
 
@@ -240,65 +239,7 @@ rewrite < times_n_SO.
 apply exp_n_SO.
 qed.
 
-(* spostare *)
-theorem le_plus_to_le: 
-\forall a,n,m. a + n \le a + m \to n \le m.
-intro.
-elim a
-  [assumption
-  |apply H.
-   apply le_S_S_to_le.assumption
-  ]
-qed.
-  
-theorem le_times_to_le: 
-\forall a,n,m. O < a \to a * n \le a * m \to n \le m.
-intro.
-apply nat_elim2;intros
-  [apply le_O_n
-  |apply False_ind.
-   rewrite < times_n_O in H1.
-   generalize in match H1.
-   apply (lt_O_n_elim ? H).
-   intros.
-   simplify in H2.
-   apply (le_to_not_lt ? ? H2).
-   apply lt_O_S
-  |apply le_S_S.
-   apply H
-    [assumption
-    |rewrite < times_n_Sm in H2.
-     rewrite < times_n_Sm in H2.
-     apply (le_plus_to_le a).
-     assumption
-    ]
-  ]
-qed.
-
-theorem le_exp_to_le: 
-\forall a,n,m. S O < a \to exp a n \le exp a m \to n \le m.
-intro.
-apply nat_elim2;intros
-  [apply le_O_n
-  |apply False_ind.
-   apply (le_to_not_lt ? ? H1).
-   simplify.
-   rewrite > times_n_SO.
-   apply lt_to_le_to_lt_times
-    [assumption
-    |apply lt_O_exp.apply lt_to_le.assumption
-    |apply lt_O_exp.apply lt_to_le.assumption
-    ]
-  |simplify in H2.
-   apply le_S_S.
-   apply H
-    [assumption
-    |apply (le_times_to_le a)
-      [apply lt_to_le.assumption|assumption]
-    ]
-  ]
-qed.
-
+(* p_ord and divides *)
 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
@@ -318,7 +259,7 @@ cut (S O < p)
          apply (lt_to_not_eq O ? H).
          rewrite > H7.
          rewrite < H10.
-         auto
+         autobatch
         ]
       |elim c
         [rewrite > sym_gcd.
@@ -329,7 +270,7 @@ cut (S O < p)
           |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 *)
+              autobatch non chiude il goal *)
            apply prime_to_gcd_SO
             [assumption|assumption]
           |assumption
@@ -356,7 +297,7 @@ cut (S O < p)
               |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 *)
+                 autobatch non chiude il goal *)
                apply prime_to_gcd_SO
                 [assumption|assumption]
               |rewrite > sym_gcd. assumption
@@ -372,7 +313,55 @@ cut (S O < p)
     ]
   |elim H2.assumption
   ]
-qed.     
+qed.    
+
+(* p_ord and primes *)
+theorem not_divides_to_p_ord_O: \forall n,i.
+Not (divides (nth_prime i) n) \to p_ord n (nth_prime i) = 
+pair nat nat O n.
+intros.
+apply p_ord_exp1
+  [apply lt_O_nth_prime_n
+  |assumption
+  |autobatch
+  ]
+qed.
+
+theorem p_ord_O_to_not_divides: \forall n,i,r.
+O < n \to
+p_ord n (nth_prime i) = pair nat nat O r 
+\to Not (divides (nth_prime i) n).
+intros.
+lapply (p_ord_to_exp1 ? ? ? ? ? ? H1)
+  [apply lt_SO_nth_prime_n
+  |assumption
+  |elim Hletin.
+   simplify in H3.
+   rewrite > H3.
+   rewrite < plus_n_O.
+   assumption
+  ]
+qed.
+
+theorem p_ord_to_not_eq_O : \forall n,p,q,r.
+  (S O) < n \to
+  p_ord n (nth_prime p) = pair nat nat q r \to
+  Not (r=O).
+intros.
+unfold.intro.
+cut (O < n)
+  [lapply (p_ord_to_exp1 ? ? ? ? ? ? H1)
+    [apply lt_SO_nth_prime_n.
+    |assumption
+    |elim Hletin.
+     apply (lt_to_not_eq ? ? Hcut).
+     rewrite > H4.
+     rewrite > H2.
+     apply times_n_O
+    ]
+  |apply (trans_lt ? (S O))[apply lt_O_S|assumption]
+  ]
+qed.
 
 definition ord :nat \to nat \to nat \def
 \lambda n,p. fst ? ? (p_ord n p).
@@ -439,3 +428,31 @@ elim (le_to_or_lt_eq O (ord_rem n p))
   |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.