(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/library_auto/nat/ord".
+set "baseuri" "cic:/matita/library_autobatch/nat/ord".
include "datatypes/constructors.ma".
include "auto/nat/exp.ma".
include "auto/nat/gcd.ma".
-include "auto/nat/relevant_equations.ma". (* required by auto paramod *)
+include "auto/nat/relevant_equations.ma". (* required by autobatch paramod *)
(* this definition of log is based on pairs, with a remainder *)
[ rewrite > (plus_n_O (m*(n1 / m))).
rewrite < H2.
rewrite > sym_times.
- auto
+ autobatch
(*rewrite < div_mod
[ reflexivity
| assumption
rewrite < plus_n_O.
apply (nat_case p)
[ simplify.
- elim (n \mod m);auto
+ elim (n \mod m);autobatch
(*[ simplify.
reflexivity
| simplify.
cut (O < n \mod m \lor O = n \mod m)
[ elim Hcut
[ apply (lt_O_n_elim (n \mod m) H3).
- intros.auto
+ intros.autobatch
(*simplify.
reflexivity*)
- | apply False_ind.auto
+ | apply False_ind.autobatch
(*apply H1.
apply sym_eq.
assumption*)
]
- | auto
+ | autobatch
(*apply le_to_or_lt_eq.
apply le_O_n*)
]
fold simplify (m \sup (S n1)).
cut ((m \sup (S n1) *n) / m = m \sup n1 *n)
[ rewrite > Hcut1.
- rewrite > (H2 m1);auto
+ rewrite > (H2 m1);autobatch
(*[ simplify.
reflexivity
| apply le_S_S_to_le.
| (* mod_exp = O *)
apply divides_to_mod_O
[ assumption
- | simplify.auto
+ | simplify.autobatch
(*rewrite > assoc_times.
apply (witness ? ? (m \sup n1 *n)).
reflexivity*)
[ (pair q r) \Rightarrow r \mod m \neq O].
intro.
elim p
-[ absurd (O < n);auto
+[ absurd (O < n);autobatch
(*[ assumption
| apply le_to_not_lt.
assumption
elim (p_ord_aux n (n1 / m) m).
apply H5
[ assumption
- | auto
+ | autobatch
(*apply eq_mod_O_to_lt_O_div
[ apply (trans_lt ? (S O))
[ unfold lt.
| assumption
| assumption
]*)
- | apply le_S_S_to_le.auto
+ | apply le_S_S_to_le.autobatch
(*apply (trans_le ? n1)
[ change with (n1 / m < n1).
apply lt_div_n_m_n;assumption
]*)
]
| intros.
- simplify.auto
+ simplify.autobatch
(*rewrite > H4.
unfold Not.
intro.
[ assumption
| unfold.
intro.
- auto
+ autobatch
(*apply H1.
apply mod_O_to_divides
[ assumption
]*)
| apply (trans_le ? (p \sup q))
[ cut ((S O) \lt p)
- [ auto
+ [ autobatch
(*elim q
[ simplify.
apply le_n_Sn
| apply not_eq_to_le_to_lt
[ unfold.
intro.
- auto
+ autobatch
(*apply H1.
rewrite < H3.
apply (witness ? r r ?).
change with (O \lt r).
apply not_eq_to_le_to_lt
[ unfold.
- intro.auto
+ intro.autobatch
(*apply H1.rewrite < H3.
apply (witness ? ? O ?).rewrite < times_n_O.
reflexivity*)
unfold p_ord in H2.
split
[ unfold.intro.
- apply (p_ord_aux_to_not_mod_O n n p q r);auto
+ apply (p_ord_aux_to_not_mod_O n n p q r);autobatch
(*[ assumption
| assumption
| apply le_n
| assumption
]
]*)
-| apply (p_ord_aux_to_exp n);auto
+| apply (p_ord_aux_to_exp n);autobatch
(*[ apply (trans_lt ? (S O))
[ unfold.
apply le_n
[ elim (p_ord_to_exp1 ? ? ? ? Hcut H1 H3).
elim (p_ord_to_exp1 ? ? ? ? Hcut H2 H4).
apply p_ord_exp1
- [ auto
+ [ autobatch
(*apply (trans_lt ? (S O))
[ unfold.
apply le_n
]*)
| unfold.
intro.
- elim (divides_times_to_divides ? ? ? H H9);auto
+ elim (divides_times_to_divides ? ? ? H H9);autobatch
(*[ apply (absurd ? ? H10 H5)
| apply (absurd ? ? H10 H7)
]*)
| (* rewrite > H6.
rewrite > H8. *)
- auto paramodulation
+ autobatch paramodulation
]
| unfold prime in H.
elim H.
\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);auto.
+(fst ? ? (p_ord b p)) (snd ? ? (p_ord b p)) H H1 H2);autobatch.
(*[ simplify.
reflexivity
| apply eq_pair_fst_snd
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
-[ auto
+[ autobatch
(*apply (trans_lt ? (S O))
[ unfold.
apply le_n
]*)
| unfold.
intro.
- apply (absurd ? ? H).auto
+ apply (absurd ? ? H).autobatch
(*apply le_to_not_lt.
apply divides_to_le
[ unfold.
apply le_n
| assumption
]*)
-| auto
+| autobatch
(*rewrite < times_n_SO.
apply exp_n_SO*)
]