(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/library_auto/nat/div_and_mod".
+set "baseuri" "cic:/matita/library_autobatch/nat/div_and_mod".
include "datatypes/constructors.ma".
include "auto/nat/minus.ma".
| (S p) \Rightarrow mod_aux n n p].
interpretation "natural remainder" 'module x y =
- (cic:/matita/library_auto/nat/div_and_mod/mod.con x y).
+ (cic:/matita/library_autobatch/nat/div_and_mod/mod.con x y).
let rec div_aux p m n : nat \def
match (leb m n) with
| (S p) \Rightarrow div_aux n n p].
interpretation "natural divide" 'divide x y =
- (cic:/matita/library_auto/nat/div_and_mod/div.con x y).
+ (cic:/matita/library_autobatch/nat/div_and_mod/div.con x y).
theorem le_mod_aux_m_m:
\forall p,n,m. n \leq p \to (mod_aux p n m) \leq m.
intro.
elim p
[ apply (le_n_O_elim n H (\lambda n.(mod_aux O n m) \leq m)).
- auto
+ autobatch
(*simplify.
apply le_O_n*)
| simplify.
[ assumption
| apply H.
cut (n1 \leq (S n) \to n1-(S m) \leq n)
- [ auto
+ [ autobatch
(*apply Hcut.
assumption*)
- | elim n1;simplify;auto
+ | elim n1;simplify;autobatch
(*[ apply le_O_n.
| apply (trans_le ? n2 n)
[ apply le_minus_m
[ apply False_ind.
apply (not_le_Sn_O O H)
| simplify.
- auto
+ autobatch
(*unfold lt.
apply le_S_S.
apply le_mod_aux_m_m.
(n=(div_aux p n m)*(S m) + (mod_aux p n m)).
intro.
elim p;simplify
-[ elim (leb n m);auto
+[ elim (leb n m);autobatch
(*simplify;apply refl_eq.*)
| apply (leb_elim n1 m);simplify;intro
[ apply refl_eq
elim (H (n1-(S m)) m).
change with (n1=(S m)+(n1-(S m))).
rewrite < sym_plus.
- auto
+ autobatch
(*apply plus_minus_m_m.
change with (m < n1).
apply not_le_to_lt.
unfold Not.
intros.
elim H.
-absurd (le (S r) O);auto.
+absurd (le (S r) O);autobatch.
(*[ rewrite < H1.
assumption
| exact (not_le_Sn_O r).
theorem div_mod_spec_div_mod:
\forall n,m. O < m \to (div_mod_spec n m (n / m) (n \mod m)).
intros.
-auto.
+autobatch.
(*apply div_mod_spec_intro
[ apply lt_mod_m_m.
assumption
| elim Hcut.
assumption
]
- | apply (trans_le ? ((q1-q)*b));auto
+ | apply (trans_le ? ((q1-q)*b));autobatch
(*[ apply le_times_n.
apply le_SO_minus.
exact H6
]
| rewrite < sym_times.
rewrite > distr_times_minus.
- rewrite > plus_minus;auto
+ rewrite > plus_minus;autobatch
(*[ rewrite > sym_times.
rewrite < H5.
rewrite < sym_times.
]*)
]
| (* eq case *)
- auto
+ autobatch
(*intros.
assumption*)
| (* the following case is symmetric *)
| elim Hcut.
assumption
]
- | apply (trans_le ? ((q-q1)*b));auto
+ | apply (trans_le ? ((q-q1)*b));autobatch
(*[ apply le_times_n.
apply le_SO_minus.
exact H6
]
| rewrite < sym_times.
rewrite > distr_times_minus.
- rewrite > plus_minus;auto
+ rewrite > plus_minus;autobatch
(*[ rewrite > sym_times.
rewrite < H3.
rewrite < sym_times.
theorem div_mod_spec_times : \forall n,m:nat.div_mod_spec ((S n)*m) (S n) m O.
intros.
-auto.
+autobatch.
(*constructor 1
[ unfold lt.
apply le_S_S.
(* some properties of div and mod *)
theorem div_times: \forall n,m:nat. ((S n)*m) / (S n) = m.
intros.
-apply (div_mod_spec_to_eq ((S n)*m) (S n) ? ? ? O).
-goal 15. (* ?11 is closed with the following tactics *)
-apply div_mod_spec_div_mod.auto.auto.
+apply (div_mod_spec_to_eq ((S n)*m) (S n) ? ? ? O);
+[2: apply div_mod_spec_div_mod.autobatch.
+| skip
+| autobatch
+]
(*unfold lt.apply le_S_S.apply le_O_n.
apply div_mod_spec_times.*)
qed.
theorem div_n_n: \forall n:nat. O < n \to n / n = S O.
intros.
-apply (div_mod_spec_to_eq n n (n / n) (n \mod n) (S O) O);auto.
+apply (div_mod_spec_to_eq n n (n / n) (n \mod n) (S O) O);autobatch.
(*[ apply div_mod_spec_div_mod.
assumption
| constructor 1
theorem eq_div_O: \forall n,m. n < m \to n / m = O.
intros.
-apply (div_mod_spec_to_eq n m (n/m) (n \mod m) O n);auto.
+apply (div_mod_spec_to_eq n m (n/m) (n \mod m) O n);autobatch.
(*[ apply div_mod_spec_div_mod.
apply (le_to_lt_to_lt O n m)
[ apply le_O_n
theorem mod_n_n: \forall n:nat. O < n \to n \mod n = O.
intros.
-apply (div_mod_spec_to_eq2 n n (n / n) (n \mod n) (S O) O);auto.
+apply (div_mod_spec_to_eq2 n n (n / n) (n \mod n) (S O) O);autobatch.
(*[ apply div_mod_spec_div_mod.
assumption
| constructor 1
((S n) \mod m) = S (n \mod m).
intros.
apply (div_mod_spec_to_eq2 (S n) m ((S n) / m) ((S n) \mod m) (n / m) (S (n \mod m)))
-[ auto
+[ autobatch
(*apply div_mod_spec_div_mod.
assumption*)
| constructor 1
[ assumption
| rewrite < plus_n_Sm.
- auto
+ autobatch
(*apply eq_f.
apply div_mod.
assumption*)
theorem mod_O_n: \forall n:nat.O \mod n = O.
intro.
-elim n;auto.
+elim n;autobatch.
(*simplify;reflexivity*)
qed.
theorem lt_to_eq_mod:\forall n,m:nat. n < m \to n \mod m = n.
intros.
-apply (div_mod_spec_to_eq2 n m (n/m) (n \mod m) O n);auto.
+apply (div_mod_spec_to_eq2 n m (n/m) (n \mod m) O n);autobatch.
(*[ apply div_mod_spec_div_mod.
apply (le_to_lt_to_lt O n m)
[ apply le_O_n
change with (\forall n,p,q:nat.(S n)*p = (S n)*q \to p=q).
intros.
rewrite < (div_times n).
-auto.
+autobatch.
(*rewrite < (div_times n q).
apply eq_f2
[ assumption
intros 4.
apply (lt_O_n_elim n H).
intros.
-auto.
+autobatch.
(*apply (inj_times_r m).
assumption.*)
qed.
theorem injective_times_l: \forall n:nat.injective nat nat (\lambda m:nat.m*(S n)).
simplify.
intros.
-auto.
+autobatch.
(*apply (inj_times_r n x y).
rewrite < sym_times.
rewrite < (sym_times y).
intros 4.
apply (lt_O_n_elim n H).
intros.
-auto.
+autobatch.
(*apply (inj_times_l m).
assumption.*)
qed.