(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/nat/gcd".
-
include "nat/primes.ma".
include "nat/lt_arith.ma".
theorem divides_mod_to_divides: \forall p,m,n:nat. O < n \to
p \divides (m \mod n) \to p \divides n \to p \divides m.
intros.elim H1.elim H2.
-apply (witness p m ((n1*(m / n))+n2)).
+apply (witness p m ((n2*(m / n))+n1)).
rewrite > distr_times_plus.
rewrite < H3.
rewrite < assoc_times.
theorem divides_gcd_nm: \forall n,m.
gcd n m \divides m \land gcd n m \divides n.
intros.
-(*CSC: simplify simplifies too much because of a redex in gcd *)
change with
(match leb n m with
[ true \Rightarrow
qed.
theorem symmetric_gcd: symmetric nat gcd.
-(*CSC: bug here: unfold symmetric does not work *)
change with
(\forall n,m:nat. gcd n m = gcd m n).
intros.
generalize in match H1.
rewrite > H3.
intro.
-cut (O < n2)
- [elim (gcd_times_SO_to_gcd_SO n n n2 ? ? H4)
- [cut (gcd n (n*n2) = n)
+cut (O < n1)
+ [elim (gcd_times_SO_to_gcd_SO n n n1 ? ? H4)
+ [cut (gcd n (n*n1) = n)
[apply (lt_to_not_eq (S O) n)
[assumption|rewrite < H4.assumption]
|apply gcd_n_times_nm.assumption
|apply (trans_lt ? (S O))[apply le_n|assumption]
|assumption
]
- |elim (le_to_or_lt_eq O n2 (le_O_n n2));
+ |elim (le_to_or_lt_eq O n1 (le_O_n n1));
[assumption
|apply False_ind.
apply (le_to_not_lt n (S O))
apply divides_to_le
[rewrite > H4.apply lt_O_S
|apply divides_d_gcd
- [apply (witness ? ? n2).reflexivity
+ [apply (witness ? ? n1).reflexivity
|apply divides_n_n
]
]
apply le_to_or_lt_eq.apply le_O_n.
qed.
+(* primes and divides *)
theorem divides_times_to_divides: \forall n,p,q:nat.prime n \to n \divides p*q \to
n \divides p \lor n \divides q.
intros.
|right.
cut (\exists a,b. a*n - b*p = (S O) \lor b*p - a*n = (S O))
[elim Hcut1.elim H3.elim H4
- [(* first case *)
- rewrite > (times_n_SO q).rewrite < H5.
+ [rewrite > (times_n_SO q).rewrite < H5.
rewrite > distr_times_minus.
+ elim H1.
+ autobatch by witness;
+ (*
rewrite > (sym_times q (a1*p)).
rewrite > (assoc_times a1).
- elim H1.
- (*
- rewrite > H6.
- applyS (witness n (n*(q*a-a1*n2)) (q*a-a1*n2))
- reflexivity. *);
- applyS (witness n ? ? (refl_eq ? ?)) (* timeout=50 *).
- (*
+ applyS (witness n ? ? (refl_eq ? ?)).
rewrite < (sym_times n).rewrite < assoc_times.
rewrite > (sym_times q).rewrite > assoc_times.
rewrite < (assoc_times a1).rewrite < (sym_times n).
|(* second case *)
rewrite > (times_n_SO q).rewrite < H5.
rewrite > distr_times_minus.
+ elim H1. autobatch by witness;
+ (*
rewrite > (sym_times q (a1*p)).
rewrite > (assoc_times a1).
- elim H1.rewrite > H6.
+ rewrite > H6.
+ applyS (witness n ? ? (refl_eq ? ?)).
rewrite < sym_times.rewrite > assoc_times.
rewrite < (assoc_times q).
rewrite < (sym_times n).
rewrite < distr_times_minus.
- apply (witness ? ? (n2*a1-q*a)).reflexivity
+ apply (witness ? ? (n1*a1-q*a)).reflexivity
+ *)
](* end second case *)
|rewrite < (prime_to_gcd_SO n p)
[apply eq_minus_gcd|assumption|assumption
]
qed.
+theorem divides_exp_to_divides:
+\forall p,n,m:nat. prime p \to
+p \divides n \sup m \to p \divides n.
+intros 3.elim m.simplify in H1.
+apply (transitive_divides p (S O)).assumption.
+apply divides_SO_n.
+cut (p \divides n \lor p \divides n \sup n1).
+elim Hcut.assumption.
+apply H.assumption.assumption.
+apply divides_times_to_divides.assumption.
+exact H2.
+qed.
+
+theorem divides_exp_to_eq:
+\forall p,q,m:nat. prime p \to prime q \to
+p \divides q \sup m \to p = q.
+intros.
+unfold prime in H1.
+elim H1.apply H4.
+apply (divides_exp_to_divides p q m).
+assumption.assumption.
+unfold prime in H.elim H.assumption.
+qed.
+
theorem eq_gcd_times_SO: \forall m,n,p:nat. O < n \to O < p \to
gcd m n = (S O) \to gcd m p = (S O) \to gcd m (n*p) = (S O).
intros.
|cut (\exists a,b. a*n - b*m = (S O) \lor b*m - a*n = (S O))
[elim Hcut1.elim H4.elim H5
[(* first case *)
+ elim H2.
rewrite > (times_n_SO p).rewrite < H6.
rewrite > distr_times_minus.
- rewrite > (sym_times p (a1*m)).
- rewrite > (assoc_times a1).
+ autobatch by witness, divides_minus.
+ |(* second case *)
elim H2.
- applyS (witness n ? ? (refl_eq ? ?)) (* timeout=50 *).
- |(* second case *)
rewrite > (times_n_SO p).rewrite < H6.
rewrite > distr_times_minus.
- rewrite > (sym_times p (a1*m)).
- rewrite > (assoc_times a1).
- elim H2.
- applyS (witness n ? ? (refl_eq ? ?)).
+ autobatch by witness, divides_minus.
](* end second case *)
|rewrite < H1.apply eq_minus_gcd.
]
|apply (decidable_divides n p).
assumption.
]
+qed.
+
+(*
+theorem divides_to_divides_times1: \forall p,q,n. prime p \to prime q \to p \neq q \to
+divides p n \to divides q n \to divides (p*q) n.
+intros.elim H3.
+rewrite > H5 in H4.
+elim (divides_times_to_divides ? ? ? H1 H4)
+ [elim H.apply False_ind.
+ apply H2.apply sym_eq.apply H8
+ [assumption
+ |apply prime_to_lt_SO.assumption
+ ]
+ |elim H6.
+ apply (witness ? ? n1).
+ rewrite > assoc_times.
+ rewrite < H7.assumption
+ ]
+qed.
+*)
+
+theorem divides_to_divides_times: \forall p,q,n. prime p \to p \ndivides q \to
+divides p n \to divides q n \to divides (p*q) n.
+intros.elim H3.
+rewrite > H4 in H2.
+elim (divides_times_to_divides ? ? ? H H2)
+ [apply False_ind.apply H1.assumption
+ |elim H5.
+ autobatch by transitive_divides, H5, reflexive_divides,divides_times.
+ (*
+ apply (witness ? ? n2).
+ rewrite > sym_times in ⊢ (? ? ? (? % ?)).
+ rewrite > assoc_times.
+ autobatch.
+ (*rewrite < H6.assumption*)
+ *)
+ ]
qed.
\ No newline at end of file