(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/library_auto/nat/gcd".
+set "baseuri" "cic:/matita/library_autobatch/nat/gcd".
include "auto/nat/primes.ma".
apply sym_eq.
apply plus_to_minus.
rewrite > sym_times.
- auto.
+ autobatch.
(*letin x \def div.
rewrite < (div_mod ? ? H).
reflexivity.*)
rewrite < assoc_times.
rewrite < H4.
rewrite < sym_times.
-auto.
+autobatch.
(*apply div_mod.
assumption.*)
qed.
gcd_aux p m n \divides m \land gcd_aux p m n \divides n.
intro.
elim p
-[ absurd (O < n);auto
+[ absurd (O < n);autobatch
(*[ assumption
| apply le_to_not_lt.
assumption
elim Hcut
[ rewrite > divides_to_divides_b_true
[ simplify.
- auto
+ autobatch
(*split
[ assumption
| apply (witness n1 n1 (S O)).
cut (gcd_aux n n1 (m \mod n1) \divides n1 \land
gcd_aux n n1 (m \mod n1) \divides mod m n1)
[ elim Hcut1.
- auto
+ autobatch width = 4.
(*split
[ apply (divides_mod_to_divides ? ? n1);assumption
| assumption
[ elim Hcut1
[ assumption
| apply False_ind.
- auto
+ autobatch
(*apply H4.
apply mod_O_to_divides
[ assumption
assumption
]*)
]
- | auto
+ | autobatch
(*apply le_to_or_lt_eq.
apply le_O_n*)
]
- | auto
+ | autobatch
(*apply lt_to_le.
apply lt_mod_m_m.
assumption*)
| apply le_S_S_to_le.
- apply (trans_le ? n1);auto
- (*[ auto.change with (m \mod n1 < n1).
+ apply (trans_le ? n1);autobatch
+ (*[ autobatch.change with (m \mod n1 < n1).
apply lt_mod_m_m.
assumption
| assumption
| assumption
]
]
- | auto
+ | autobatch
(*apply (decidable_divides n1 m).
assumption*)
]
[ apply (nat_case1 n)
[ simplify.
intros.
- auto
+ autobatch
(*split
[ apply (witness m m (S O)).
apply times_n_SO
(gcd_aux (S m1) m (S m1) \divides m
\land
gcd_aux (S m1) m (S m1) \divides (S m1)).
- auto
+ autobatch
(*apply divides_gcd_aux_mn
[ unfold lt.
apply le_S_S.
apply (nat_case1 m)
[ simplify.
intros.
- auto
+ autobatch
(*split
[ apply (witness n O O).
apply times_n_O
\land
gcd_aux (S m1) n (S m1) \divides S m1)
[ elim Hcut.
- auto
+ autobatch
(*split;assumption*)
| apply divides_gcd_aux_mn
- [ auto
+ [ autobatch
(*unfold lt.
apply le_S_S.
apply le_O_n*)
intro.
apply H.
rewrite > H1.
- auto
+ autobatch
(*apply (trans_le ? (S n))
[ apply le_n_Sn
| assumption
theorem divides_gcd_n: \forall n,m. gcd n m \divides n.
intros.
-exact (proj2 ? ? (divides_gcd_nm n m)). (*auto non termina la dimostrazione*)
+exact (proj2 ? ? (divides_gcd_nm n m)). (*autobatch non termina la dimostrazione*)
qed.
theorem divides_gcd_m: \forall n,m. gcd n m \divides m.
intros.
-exact (proj1 ? ? (divides_gcd_nm n m)). (*auto non termina la dimostrazione*)
+exact (proj1 ? ? (divides_gcd_nm n m)). (*autobatch non termina la dimostrazione*)
qed.
theorem divides_gcd_aux: \forall p,m,n,d. O < n \to n \le m \to n \le p \to
d \divides m \to d \divides n \to d \divides gcd_aux p m n.
intro.
elim p
-[ absurd (O < n);auto
+[ absurd (O < n);autobatch
(*[ assumption
| apply le_to_not_lt.
assumption
| simplify.
cut (n1 \divides m \lor n1 \ndivides m)
[ elim Hcut.
- rewrite > divides_to_divides_b_true;auto.
+ rewrite > divides_to_divides_b_true;
+ simplify; autobatch.
(*[ simplify.
assumption.
| assumption.
[ elim Hcut1
[ assumption
|
- absurd (n1 \divides m);auto
+ absurd (n1 \divides m);autobatch
(*[ apply mod_O_to_divides
[ assumption.
| apply sym_eq.assumption.
| assumption
]*)
]
- | auto
+ | autobatch
(*apply le_to_or_lt_eq.
apply le_O_n*)
]
- | auto
+ | autobatch
(*apply lt_to_le.
apply lt_mod_m_m.
assumption*)
| apply le_S_S_to_le.
- auto
+ autobatch
(*apply (trans_le ? n1)
[ change with (m \mod n1 < n1).
apply lt_mod_m_m.
| assumption
]*)
| assumption
- | auto
+ | autobatch
(*apply divides_mod;
assumption*)
]
| assumption
| assumption
]
- | auto
+ | autobatch
(*apply (decidable_divides n1 m).
assumption*)
]
| intros.
change with (d \divides gcd_aux (S m1) m (S m1)).
apply divides_gcd_aux
- [ auto
- (*unfold lt.
- apply le_S_S.
+ [ unfold lt.autobatch
+ (*apply le_S_S.
apply le_O_n.*)
| assumption.
- | apply le_n. (*chiude il goal anche con auto*)
+ | apply le_n. (*chiude il goal anche con autobatch*)
| assumption.
| rewrite < H2.
assumption
| intros.
change with (d \divides gcd_aux (S m1) n (S m1)).
apply divides_gcd_aux
- [ auto
- (*unfold lt.
- apply le_S_S.
+ [ unfold lt.autobatch
+ (*apply le_S_S.
apply le_O_n*)
- | auto
+ | autobatch
(*apply lt_to_le.
apply not_le_to_lt.
assumption*)
- | apply le_n (*chiude il goal anche con auto*)
+ | apply le_n (*chiude il goal anche con autobatch*)
| assumption
| rewrite < H2.
assumption
\exists a,b. a*n - b*m = gcd_aux p m n \lor b*m - a*n = gcd_aux p m n.
intro.
elim p
-[ absurd (O < n);auto
+[ absurd (O < n);autobatch
(*[ assumption
| apply le_to_not_lt
assumption.
[ simplify.
apply (ex_intro ? ? (S O)).
apply (ex_intro ? ? O).
- auto
+ autobatch
(*left.
simplify.
rewrite < plus_n_O.
rewrite > distr_times_plus.
rewrite > (sym_times n1).
rewrite > (sym_times n1).
- rewrite > (div_mod m n1) in \vdash (? ? (? % ?) ?);auto
+ rewrite > (div_mod m n1) in \vdash (? ? (? % ?) ?);autobatch
(*[ rewrite > assoc_times.
rewrite < sym_plus.
rewrite > distr_times_plus.
rewrite < eq_minus_minus_minus_plus.
- rewrite < sym_plus.auto.
+ rewrite < sym_plus.autobatch.
rewrite < plus_minus
[ rewrite < minus_n_n.
reflexivity
[ rewrite > distr_times_plus.
rewrite > assoc_times.
rewrite < eq_minus_minus_minus_plus.
- auto
+ autobatch
(*rewrite < sym_plus.
rewrite < plus_minus
[ rewrite < minus_n_n.
[ cut (O \lt m \mod n1 \lor O = m \mod n1)
[ elim Hcut2
[ assumption
- | absurd (n1 \divides m);auto
+ | absurd (n1 \divides m);autobatch
(*[ apply mod_O_to_divides
[ assumption
| symmetry.
| assumption
]*)
]
- | auto
+ | autobatch
(*apply le_to_or_lt_eq.
apply le_O_n*)
]
- | auto
+ | autobatch
(*apply lt_to_le.
apply lt_mod_m_m.
assumption*)
| apply le_S_S_to_le.
- auto
+ autobatch
(*apply (trans_le ? n1)
[ change with (m \mod n1 < n1).
apply lt_mod_m_m.
| assumption
]
]
- | auto
+ | autobatch
(*apply (decidable_divides n1 m).
assumption*)
]
- | auto
+ | autobatch
(*apply (lt_to_le_to_lt ? n1);assumption *)
]
]
intros.
apply (ex_intro ? ? O).
apply (ex_intro ? ? (S O)).
- auto
+ autobatch
(*right.simplify.
rewrite < plus_n_O.
apply sym_eq.
(\exists a,b.
a*(S m1) - b*m = (gcd_aux (S m1) m (S m1))
\lor b*m - a*(S m1) = (gcd_aux (S m1) m (S m1))).
- auto
+ autobatch
(*apply eq_minus_gcd_aux
[ unfold lt.
apply le_S_S.
intros.
apply (ex_intro ? ? (S O)).
apply (ex_intro ? ? O).
- auto
+ autobatch
(*left.simplify.
rewrite < plus_n_O.
apply sym_eq.
b*n - a*(S m1) = (gcd_aux (S m1) n (S m1)))
[ elim Hcut.
elim H2.
- elim H3;apply (ex_intro ? ? a1);auto
+ elim H3;apply (ex_intro ? ? a1);autobatch
(*[ apply (ex_intro ? ? a1).
apply (ex_intro ? ? a).
right.
left.
assumption
]*)
- | apply eq_minus_gcd_aux;auto
+ | apply eq_minus_gcd_aux;autobatch
(*[ unfold lt.
apply le_S_S.
apply le_O_n
- | auto.apply lt_to_le.
+ | autobatch.apply lt_to_le.
apply not_le_to_lt.
assumption
| apply le_n.
(* some properties of gcd *)
theorem gcd_O_n: \forall n:nat. gcd O n = n.
-auto.
+autobatch.
(*intro.simplify.reflexivity.*)
qed.
intros.
cut (O \divides n \land O \divides m)
[ elim Hcut.
- auto
- (*elim H2.
- split
- [ assumption
- | elim H1.
- assumption
- ]*)
+ autobatch size = 7;
+ (*
+ split;
+ [ apply antisymmetric_divides
+ [ apply divides_n_O
+ | assumption
+ ]
+ | apply antisymmetric_divides
+ [ apply divides_n_O
+ | assumption
+ ]
+ ]*)
| rewrite < H.
apply divides_gcd_nm
]
theorem lt_O_gcd:\forall m,n:nat. O < n \to O < gcd m n.
intros.
-auto.
-(*apply (nat_case1 (gcd m n))
-[ intros.
- generalize in match (gcd_O_to_eq_O m n H1).
- intros.
- elim H2.
- rewrite < H4 in \vdash (? ? %).
- assumption
-| intros.
- unfold lt.
- apply le_S_S.
- apply le_O_n
-]*)
+autobatch.
+(*
+apply (divides_to_lt_O (gcd m n) n ? ?);
+ [apply (H).
+ |apply (divides_gcd_m m n).
+ ]
+*)
qed.
theorem gcd_n_n: \forall n.gcd n n = n.
intro.
-auto.
-(*elim n
-[ reflexivity
-| apply le_to_le_to_eq
- [ apply divides_to_le
- [ apply lt_O_S
- | apply divides_gcd_n
- ]
- | apply divides_to_le
- [ apply lt_O_gcd.apply lt_O_S
- | apply divides_d_gcd
- [ apply divides_n_n
- | apply divides_n_n
- ]
+autobatch.
+(*
+apply (antisymmetric_divides (gcd n n) n ? ?);
+ [apply (divides_gcd_n n n).
+ |apply (divides_d_gcd n n n ? ?);
+ [apply (reflexive_divides n).
+ |apply (reflexive_divides n).
]
]
-]*)
+*)
qed.
theorem gcd_SO_to_lt_O: \forall i,n. (S O) < n \to gcd i n = (S O) \to
unfold.
intro.
apply (lt_to_not_eq (S O) n H).
- auto
+ autobatch
(*apply sym_eq.
assumption*)
]
change with
(\forall n,m:nat. gcd n m = gcd m n).
intros.
-auto.
-(*cut (O < (gcd n m) \lor O = (gcd n m))
-[ elim Hcut
- [ cut (O < (gcd m n) \lor O = (gcd m n))
- [ elim Hcut1
- [ apply antisym_le
- [ apply divides_to_le
- [ assumption
- | apply divides_d_gcd
- [ apply divides_gcd_n
- | apply divides_gcd_m
- ]
- ]
- | apply divides_to_le
- [ assumption
- | apply divides_d_gcd
- [ apply divides_gcd_n
- | apply divides_gcd_m
- ]
- ]
- ]
- | rewrite < H1.
- cut (m=O \land n=O)
- [ elim Hcut2.
- rewrite > H2.
- rewrite > H3.
- reflexivity
- | apply gcd_O_to_eq_O.
- apply sym_eq.
- assumption
- ]
- ]
- | apply le_to_or_lt_eq.
- apply le_O_n
+autobatch size = 7.
+(*
+apply (antisymmetric_divides (gcd n m) (gcd m n) ? ?);
+ [apply (divides_d_gcd n m (gcd n m) ? ?);
+ [apply (divides_gcd_n n m).
+ |apply (divides_gcd_m n m).
]
- | rewrite < H.
- cut (n=O \land m=O)
- [ elim Hcut1.
- rewrite > H1.
- rewrite > H2.
- reflexivity
- | apply gcd_O_to_eq_O.apply sym_eq.
- assumption
+ |apply (divides_d_gcd m n (gcd m n) ? ?);
+ [apply (divides_gcd_n m n).
+ |apply (divides_gcd_m m n).
]
]
-| apply le_to_or_lt_eq.
- apply le_O_n
-]*)
+*)
qed.
variant sym_gcd: \forall n,m:nat. gcd n m = gcd m n \def
| intro.
apply divides_to_le
[ apply lt_O_gcd.
- auto
+ autobatch
(*rewrite > (times_n_O O).
apply lt_times
- [ auto.unfold lt.
+ [ autobatch.unfold lt.
apply le_S_S.
apply le_O_n
| assumption
]*)
- | apply divides_d_gcd;auto
+ | apply divides_d_gcd;autobatch
(*[ apply (transitive_divides ? (S m1))
[ apply divides_gcd_m
| apply (witness ? ? p).
intros.
apply antisymmetric_le
[ rewrite < H2.
- auto
+ autobatch
(*apply le_gcd_times.
assumption*)
-| auto
+| autobatch
(*change with (O < gcd m n).
apply lt_O_gcd.
assumption*)
intro.
cut (O < n2)
[ elim (gcd_times_SO_to_gcd_SO n n n2 ? ? H4)
- [ cut (gcd n (n*n2) = n);auto
- (*[ auto.apply (lt_to_not_eq (S O) n)
+ [ cut (gcd n (n*n2) = n);autobatch
+ (*[ autobatch.apply (lt_to_not_eq (S O) n)
[ assumption
| rewrite < H4.
assumption
| apply gcd_n_times_nm.
assumption
]*)
- | auto
+ | autobatch
(*apply (trans_lt ? (S O))
[ apply le_n
| assumption
| apply False_ind.
apply (le_to_not_lt n (S O))
[ rewrite < H4.
- apply divides_to_le;auto
+ apply divides_to_le;autobatch
(*[ rewrite > H4.
apply lt_O_S
| apply divides_d_gcd
theorem gcd_SO_n: \forall n:nat. gcd (S O) n = (S O).
intro.
-auto.
-(*apply antisym_le
-[ apply divides_to_le
- [ unfold lt.
- apply le_n
- | apply divides_gcd_n
- ]
-| cut (O < gcd (S O) n \lor O = gcd (S O) n)
- [ elim Hcut
- [ assumption
- | apply False_ind.
- apply (not_eq_O_S O).
- cut ((S O)=O \land n=O)
- [ elim Hcut1.
- apply sym_eq.
- assumption
- | apply gcd_O_to_eq_O.
- apply sym_eq.
- assumption
- ]
- ]
- | apply le_to_or_lt_eq.
- apply le_O_n
+autobatch.
+(*
+apply (symmetric_eq nat (S O) (gcd (S O) n) ?).
+apply (antisymmetric_divides (S O) (gcd (S O) n) ? ?);
+ [apply (divides_SO_n (gcd (S O) n)).
+ |apply (divides_gcd_n (S O) n).
]
-]*)
+*)
qed.
theorem divides_gcd_mod: \forall m,n:nat. O < n \to
divides (gcd m n) (gcd n (m \mod n)).
intros.
-auto.
+autobatch width = 4.
(*apply divides_d_gcd
[ apply divides_mod
[ assumption
theorem divides_mod_gcd: \forall m,n:nat. O < n \to
divides (gcd n (m \mod n)) (gcd m n) .
intros.
-auto.
+autobatch.
(*apply divides_d_gcd
[ apply divides_gcd_n
| apply (divides_mod_to_divides ? ? n)
theorem gcd_mod: \forall m,n:nat. O < n \to
(gcd n (m \mod n)) = (gcd m n) .
intros.
-auto.
+autobatch.
(*apply antisymmetric_divides
[ apply divides_mod_gcd.
assumption
[ apply not_lt_to_le.unfold Not.unfold lt.
intro.
apply H1.
- rewrite < (H3 (gcd n m));auto
+ rewrite < (H3 (gcd n m));
+ [autobatch|autobatch| unfold lt; autobatch]
(*[ apply divides_gcd_m
| apply divides_gcd_n
| assumption
[ elim Hcut1.
rewrite < H5 in \vdash (? ? %).
assumption
- | auto
+ | autobatch
(*apply gcd_O_to_eq_O.
apply sym_eq.
assumption*)
]
]
- | auto
+ | autobatch
(*apply le_to_or_lt_eq.
apply le_O_n*)
]
rewrite > (sym_times q (a1*p)).
rewrite > (assoc_times a1).
elim H1.
- auto
+ autobatch
(*rewrite > H6.
rewrite < sym_times.rewrite > assoc_times.
rewrite < (assoc_times q).
apply (witness ? ? (n2*a1-q*a)).
reflexivity*)
](* end second case *)
- | rewrite < (prime_to_gcd_SO n p);auto
+ | rewrite < (prime_to_gcd_SO n p);autobatch
(* [ apply eq_minus_gcd
| assumption
| assumption
]
| apply (decidable_divides n p).
apply (trans_lt ? (S O))
- [ auto
+ [ autobatch
(*unfold lt.
apply le_n*)
| unfold prime in H.
change with ((S O) < (S O)).
rewrite < H2 in \vdash (? ? %).
apply (lt_to_le_to_lt ? (smallest_factor (gcd m (n*p))))
- [ auto
+ [ autobatch
(*apply lt_SO_smallest_factor.
assumption*)
- | apply divides_to_le;auto
+ | apply divides_to_le;
+ [ autobatch |
+ apply divides_d_gcd
+ [ assumption
+ | apply (transitive_divides ? (gcd m (n*p)))
+ [ autobatch.
+ | autobatch.
+ ]
+ ]
+ ]
(*[ rewrite > H2.
unfold lt.
apply le_n
apply (lt_to_le_to_lt ? (smallest_factor (gcd m (n*p))))
[ apply lt_SO_smallest_factor.
assumption
- | apply divides_to_le;auto
+ | apply divides_to_le;
+ [ autobatch |
+ apply divides_d_gcd
+ [ assumption
+ | apply (transitive_divides ? (gcd m (n*p)))
+ [ autobatch.
+ | autobatch.
+ ]
+ ]
+ ]
(*[ rewrite > H3.
unfold lt.
apply le_n
]*)
]
]
- | apply divides_times_to_divides;auto
+ | apply divides_times_to_divides;
+ [ autobatch |
+ apply (transitive_divides ? (gcd m (n*p)))
+ [ autobatch.
+ | autobatch.
+ ]
+ ]
+ ]
(*[ apply prime_smallest_factor_n.
assumption
- | auto.apply (transitive_divides ? (gcd m (n*p)))
+ | autobatch.apply (transitive_divides ? (gcd m (n*p)))
[ apply divides_smallest_factor_n.
apply (trans_lt ? (S O))
[ unfold lt.
| apply divides_gcd_m
]
]*)
- ]
-| auto
+| autobatch
(*change with (O < gcd m (n*p)).
apply lt_O_gcd.
rewrite > (times_n_O O).
apply eq_minus_gcd
]
]
-| auto
+| autobatch
(*apply (decidable_divides n p).
assumption.*)
]