Empty types not in Prop and empty types elimination handled correctly.

[helm.git] / matita / library_auto / auto / nat / fermat_little_theorem.ma

diff --git a/matita/library_auto/auto/nat/fermat_little_theorem.ma b/matita/library_auto/auto/nat/fermat_little_theorem.ma
index df8aff7275aba39992d550388fbc02340af046b1..a04adaad8fa686679b773166690756d5d7bf5278 100644 (file)
--- a/matita/library_auto/auto/nat/fermat_little_theorem.ma
+++ b/matita/library_auto/auto/nat/fermat_little_theorem.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/library_auto/nat/fermat_little_theorem".
+set "baseuri" "cic:/matita/library_autobatch/nat/fermat_little_theorem".
 
 include "auto/nat/exp.ma".
 include "auto/nat/gcd.ma".
@@ -25,7 +25,7 @@ unfold permut.
 split
 [ intros.
   unfold S_mod.
-  auto
+  autobatch
   (*apply le_S_S_to_le.
   change with ((S i) \mod (S n) < S n).
   apply lt_mod_m_m.
@@ -44,29 +44,27 @@ split
             [ (* i < n, j< n *)
               rewrite < mod_S
               [ rewrite < mod_S
-                [ (*qui auto non chiude il goal, chiuso invece dalla tattica
+                [ (*qui autobatch non chiude il goal, chiuso invece dalla tattica
                    * apply H2
                    *)
                   apply H2                
-                | auto
+                | autobatch
                   (*unfold lt.
                   apply le_S_S.
                   apply le_O_n*)
                 | rewrite > lt_to_eq_mod;
-                    auto(*unfold lt;apply le_S_S;assumption*)                  
+                    unfold lt;autobatch.(*apply le_S_S;assumption*)                  
                 ]
-              | auto
+              | autobatch
                 (*unfold lt.
                 apply le_S_S.
                 apply le_O_n*)              
               | rewrite > lt_to_eq_mod
-                [ auto
-                  (*unfold lt.
-                  apply le_S_S.
+                [ unfold lt.autobatch
+                  (*apply le_S_S.
                   assumption*)
-                | auto
-                  (*unfold lt.
-                  apply le_S_S.
+                | unfold lt.autobatch
+                  (*apply le_S_S.
                   assumption*)
                 ]
               ]
@@ -80,16 +78,14 @@ split
               [ rewrite < H4 in \vdash (? ? ? (? %?)).
                 rewrite < mod_S
                 [ assumption
-                | auto
-                  (*unfold lt.
-                  apply le_S_S.
+                | unfold lt.autobatch
+                  (*apply le_S_S.
                   apply le_O_n*)
                 | rewrite > lt_to_eq_mod;
-                    auto;(*unfold lt;apply le_S_S;assumption*)                
+                    unfold lt;autobatch;(*apply le_S_S;assumption*)                
                 ]
-              | auto
-                (*unfold lt.
-                apply le_S_S.
+              | unfold lt.autobatch
+                (*apply le_S_S.
                 apply le_O_n*)
               ]
             ]
@@ -101,41 +97,37 @@ split
               [ rewrite < H3 in \vdash (? ? (? %?) ?).
                 rewrite < mod_S
                 [ assumption
-                | auto
-                  (*unfold lt.
-                  apply le_S_S.
+                | unfold lt.autobatch
+                  (*apply le_S_S.
                   apply le_O_n*)
                 | rewrite > lt_to_eq_mod;
-                    auto(*unfold lt;apply le_S_S;assumption*)                  
+                    unfold lt;autobatch(*apply le_S_S;assumption*)                  
                 ]
-              | auto
-                (*unfold lt.
-                apply le_S_S.
+              | unfold lt.autobatch
+                (*apply le_S_S.
                 apply le_O_n*)
               ]
             |(* i = n, j= n*)
-              auto
+              autobatch
               (*rewrite > H3.
               rewrite > H4.
               reflexivity*)
             ]
           ]
-        | auto
+        | autobatch
           (*apply le_to_or_lt_eq.
           assumption*)
         ]
-      | auto
+      | autobatch
         (*apply le_to_or_lt_eq.
         assumption*)
       ]                  
-    | auto
-      (*unfold lt.
-      apply le_S_S.
+    | unfold lt.autobatch
+      (*apply le_S_S.
       assumption*)
     ]
-  | auto
-    (*unfold lt.
-    apply le_S_S.
+  | unfold lt.autobatch
+    (*apply le_S_S.
     assumption*)
   ]
 ]
@@ -163,7 +155,7 @@ elim n
   [ unfold prime in H.
     elim H.
     assumption
-  | auto
+  | autobatch
     (*apply divides_to_le.
     unfold lt.
     apply le_n.
@@ -175,7 +167,7 @@ elim n
   [ elim Hcut
     [ apply (lt_to_not_le (S n1) p)
       [ assumption
-      | auto
+      | autobatch
         (*apply divides_to_le
         [ unfold lt.
           apply le_S_S.
@@ -183,7 +175,7 @@ elim n
         | assumption
         ]*)
       ]
-    | auto
+    | autobatch
       (*apply H1
       [ apply (trans_lt ? (S n1))
         [ unfold lt. 
@@ -193,7 +185,7 @@ elim n
       | assumption
       ]*)
     ]
-  | auto
+  | autobatch
     (*apply divides_times_to_divides;
       assumption*)
   ]
@@ -212,7 +204,7 @@ split
     apply lt_mod_m_m.
     unfold prime in H.
     elim H.
-    auto
+    autobatch
     (*unfold lt.
     apply (trans_le ? (S (S O)))
     [ apply le_n_Sn
@@ -222,7 +214,7 @@ split
     [ apply le_n
     | unfold prime in H.
       elim H.
-      auto
+      autobatch
       (*apply (trans_lt ? (S O))
       [ unfold lt.
         apply le_n
@@ -238,7 +230,7 @@ split
     absurd (j-i \lt p)
     [ unfold lt.
       rewrite > (S_pred p)
-      [ auto
+      [ autobatch
         (*apply le_S_S.
         apply le_plus_to_minus.
         apply (trans_le ? (pred p))
@@ -246,9 +238,8 @@ split
         | rewrite > sym_plus.
           apply le_plus_n
         ]*)
-      | auto
-        (*unfold prime in H.
-        elim H.
+      | unfold prime in H. elim H. autobatch.
+        (*
         apply (trans_lt ? (S O))
         [ unfold lt.
           apply le_n
@@ -257,14 +248,13 @@ split
       ]
     | apply (le_to_not_lt p (j-i)).
       apply divides_to_le
-      [ auto
-        (*unfold lt.
-        apply le_SO_minus.
+      [ unfold lt.autobatch
+        (*apply le_SO_minus.
         assumption*)
       | cut (divides p a \lor divides p (j-i))
         [ elim Hcut
           [ apply False_ind.
-            auto
+            autobatch
             (*apply H1.
             assumption*)
           | assumption
@@ -273,15 +263,13 @@ split
           [ assumption
           | rewrite > distr_times_minus.
             apply eq_mod_to_divides
-            [ auto
-              (*unfold prime in H.                        
-              elim H.
-              apply (trans_lt ? (S O))
+            [ unfold prime in H.elim H.autobatch
+              (*apply (trans_lt ? (S O))
               [ unfold lt.
                 apply le_n
               | assumption
               ]*)
-            | auto
+            | autobatch
               (*apply sym_eq.
               apply H4*)
             ]
@@ -290,7 +278,7 @@ split
       ]
     ]
   |(* i = j *)
-    auto
+    autobatch
     (*intro. 
     assumption*)
   | (* j < i *)
@@ -298,7 +286,7 @@ split
     absurd (i-j \lt p)
     [ unfold lt.
       rewrite > (S_pred p)
-      [ auto
+      [ autobatch
         (*apply le_S_S.
         apply le_plus_to_minus.
         apply (trans_le ? (pred p))
@@ -306,9 +294,8 @@ split
         | rewrite > sym_plus.
           apply le_plus_n
         ]*)
-      | auto
-        (*unfold prime in H.
-        elim H.
+      | unfold prime in H.elim H.autobatch.
+        (*
         apply (trans_lt ? (S O))
         [ unfold lt.
           apply le_n
@@ -317,14 +304,13 @@ split
       ]
     | apply (le_to_not_lt p (i-j)).
       apply divides_to_le
-      [ auto
-        (*unfold lt.
-        apply le_SO_minus.
+      [ unfold lt.autobatch
+        (*apply le_SO_minus.
         assumption*)
       | cut (divides p a \lor divides p (i-j))
         [ elim Hcut
           [ apply False_ind.
-            auto
+            autobatch
             (*apply H1.
             assumption*)
           | assumption
@@ -333,9 +319,8 @@ split
           [ assumption
           | rewrite > distr_times_minus.
             apply eq_mod_to_divides
-            [ auto
-              (*unfold prime in H.
-              elim H.
+            [ unfold prime in H.elim H.autobatch.
+              (*
               apply (trans_lt ? (S O))
               [ unfold lt.
                 apply le_n
@@ -359,7 +344,7 @@ cut (O < a)
   [ cut (O < pred p)
     [ apply divides_to_congruent
       [ assumption
-      | auto
+      | autobatch
         (*change with (O < exp a (pred p)).
         apply lt_O_exp.
         assumption*)
@@ -369,7 +354,7 @@ cut (O < a)
           | apply False_ind.
             apply (prime_to_not_divides_fact p H (pred p))
             [ unfold lt.
-              auto
+              autobatch
               (*rewrite < (S_pred ? Hcut1).
               apply le_n*)
             | assumption
@@ -397,25 +382,25 @@ cut (O < a)
                   rewrite < eq_map_iter_i_pi.
                   apply (permut_to_eq_map_iter_i ? ? ? ? ? (λm.m))
                   [ apply assoc_times
-                  | (*NB qui auto non chiude il goal, chiuso invece dalla sola
+                  | (*NB qui autobatch non chiude il goal, chiuso invece dalla sola
                      ( tattica apply sys_times
                      *)
                     apply sym_times
                   | rewrite < plus_n_Sm.
                     rewrite < plus_n_O.
                     rewrite < (S_pred ? Hcut2).
-                    auto
+                    autobatch
                     (*apply permut_mod
                     [ assumption
                     | assumption
                     ]*)
                   | intros.
                     cut (m=O)
-                    [ auto
+                    [ autobatch
                       (*rewrite > Hcut3.
                       rewrite < times_n_O.
                       apply mod_O_n.*)
-                    | auto
+                    | autobatch
                       (*apply sym_eq.
                       apply le_n_O_to_eq.
                       apply le_S_S_to_le.
@@ -437,7 +422,7 @@ cut (O < a)
     ]
   | unfold prime in H.
     elim H.
-    auto
+    autobatch
     (*apply (trans_lt ? (S O))
     [ unfold lt.
       apply le_n
@@ -450,11 +435,11 @@ cut (O < a)
     | apply False_ind.
       apply H1.
       rewrite < H2.
-      auto
+      autobatch
       (*apply (witness ? ? O).
       apply times_n_O*)
     ]
-  | auto
+  | autobatch
     (*apply le_to_or_lt_eq.
     apply le_O_n*)
   ]