set "baseuri" "cic:/matita/nat/gcd".
include "nat/primes.ma".
+include "nat/lt_arith.ma".
let rec gcd_aux p m n: nat \def
match divides_b n m with
theorem divides_mod: \forall p,m,n:nat. O < n \to p \divides m \to p \divides n \to
p \divides (m \mod n).
intros.elim H1.elim H2.
-apply (witness ? ? (n2 - n1*(m / n))).
+(* apply (witness ? ? (n2 - n1*(m / n))). *)
+apply witness[|
rewrite > distr_times_minus.
-rewrite < H3.
+rewrite < H3 in \vdash (? ? ? (? % ?)).
rewrite < assoc_times.
-rewrite < H4.
-apply sym_eq.
-apply plus_to_minus.
+rewrite < H4 in \vdash (? ? ? (? ? (? % ?))).
+apply sym_eq.apply plus_to_minus.
rewrite > sym_times.
-apply div_mod.
-assumption.
+letin x \def div.
+rewrite < (div_mod ? ? H).
+reflexivity.
+]
qed.
theorem divides_mod_to_divides: \forall p,m,n:nat. O < n \to
exact (proj1 ? ? (divides_gcd_nm n m)).
qed.
+
+theorem divides_times_gcd_aux: \forall p,m,n,d,c.
+O \lt c \to O < n \to n \le m \to n \le p \to
+d \divides (c*m) \to d \divides (c*n) \to d \divides c*gcd_aux p m n.
+intro.
+elim p
+[ absurd (O < n)
+ [ assumption
+ | apply le_to_not_lt.
+ assumption
+ ]
+| simplify.
+ cut (n1 \divides m \lor n1 \ndivides m)
+ [ elim Hcut
+ [ rewrite > divides_to_divides_b_true
+ [ simplify.
+ assumption
+ | assumption
+ | assumption
+ ]
+ | rewrite > not_divides_to_divides_b_false
+ [ simplify.
+ apply H
+ [ assumption
+ | cut (O \lt m \mod n1 \lor O = m \mod n1)
+ [ elim Hcut1
+ [ assumption
+ | absurd (n1 \divides m)
+ [ apply mod_O_to_divides
+ [ assumption
+ | apply sym_eq.
+ assumption
+ ]
+ | assumption
+ ]
+ ]
+ | apply le_to_or_lt_eq.
+ apply le_O_n
+ ]
+ | apply lt_to_le.
+ apply lt_mod_m_m.
+ assumption
+ | apply le_S_S_to_le.
+ apply (trans_le ? n1)
+ [ change with (m \mod n1 < n1).
+ apply lt_mod_m_m.
+ assumption
+ | assumption
+ ]
+ | assumption
+ | rewrite < times_mod
+ [ rewrite < (sym_times c m).
+ rewrite < (sym_times c n1).
+ apply divides_mod
+ [ rewrite > (S_pred c)
+ [ rewrite > (S_pred n1)
+ [ apply (lt_O_times_S_S)
+ | assumption
+ ]
+ | assumption
+ ]
+ | assumption
+ | assumption
+ ]
+ | assumption
+ | assumption
+ ]
+ ]
+ | assumption
+ | assumption
+ ]
+ ]
+ | apply (decidable_divides n1 m).
+ assumption
+ ]
+]
+qed.
+
+(*a particular case of the previous theorem (setting c=1)*)
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).assumption.apply le_to_not_lt.assumption.
-simplify.
-cut (n1 \divides m \lor n1 \ndivides m).
-elim Hcut.
-rewrite > divides_to_divides_b_true.
-simplify.assumption.
-assumption.assumption.
-rewrite > not_divides_to_divides_b_false.
-simplify.
-apply H.
-cut (O \lt m \mod n1 \lor O = m \mod n1).
-elim Hcut1.assumption.
-absurd (n1 \divides m).apply mod_O_to_divides.
-assumption.apply sym_eq.assumption.assumption.
-apply le_to_or_lt_eq.apply le_O_n.
-apply lt_to_le.
-apply lt_mod_m_m.assumption.
-apply le_S_S_to_le.
-apply (trans_le ? n1).
-change with (m \mod n1 < n1).
-apply lt_mod_m_m.assumption.assumption.
-assumption.
-apply divides_mod.assumption.assumption.assumption.
-assumption.assumption.
-apply (decidable_divides n1 m).assumption.
+intros.
+rewrite > (times_n_SO (gcd_aux p m n)).
+rewrite < (sym_times (S O)).
+apply (divides_times_gcd_aux)
+[ apply (lt_O_S O)
+| assumption
+| assumption
+| assumption
+| rewrite > (sym_times (S O)).
+ rewrite < (times_n_SO m).
+ assumption
+| rewrite > (sym_times (S O)).
+ rewrite < (times_n_SO n).
+ assumption
+]
qed.
-theorem divides_d_gcd: \forall m,n,d.
-d \divides m \to d \divides n \to d \divides gcd n m.
+theorem divides_d_times_gcd: \forall m,n,d,c.
+O \lt c \to d \divides (c*m) \to d \divides (c*n) \to d \divides c*gcd n m.
intros.
-(*CSC: here simplify simplifies too much because of a redex in gcd *)
change with
-(d \divides
+(d \divides c *
match leb n m with
[ true \Rightarrow
match n with
match m with
[ O \Rightarrow n
| (S p) \Rightarrow gcd_aux (S p) n (S p) ]]).
-apply (leb_elim n m).
-apply (nat_case1 n).simplify.intros.assumption.
-intros.
-change with (d \divides gcd_aux (S m1) m (S m1)).
-apply divides_gcd_aux.
-unfold lt.apply le_S_S.apply le_O_n.assumption.apply le_n.assumption.
-rewrite < H2.assumption.
-apply (nat_case1 m).simplify.intros.assumption.
+apply (leb_elim n m)
+[ apply (nat_case1 n)
+ [ simplify.
+ intros.
+ assumption
+ | intros.
+ change with (d \divides c*gcd_aux (S m1) m (S m1)).
+ apply divides_times_gcd_aux
+ [ assumption
+ | unfold lt.
+ apply le_S_S.
+ apply le_O_n
+ | assumption
+ | apply (le_n (S m1))
+ | assumption
+ | rewrite < H3.
+ assumption
+ ]
+ ]
+| apply (nat_case1 m)
+ [ simplify.
+ intros.
+ assumption
+ | intros.
+ change with (d \divides c * gcd_aux (S m1) n (S m1)).
+ apply divides_times_gcd_aux
+ [ unfold lt.
+ change with (O \lt c).
+ assumption
+ | apply lt_O_S
+ | apply lt_to_le.
+ apply not_le_to_lt.
+ assumption
+ | apply (le_n (S m1)).
+ | assumption
+ | rewrite < H3.
+ assumption
+ ]
+ ]
+]
+qed.
+
+(*a particular case of the previous theorem (setting c=1)*)
+theorem divides_d_gcd: \forall m,n,d.
+d \divides m \to d \divides n \to d \divides gcd n m.
intros.
-change with (d \divides gcd_aux (S m1) n (S m1)).
-apply divides_gcd_aux.
-unfold lt.apply le_S_S.apply le_O_n.
-apply lt_to_le.apply not_le_to_lt.assumption.apply le_n.assumption.
-rewrite < H2.assumption.
+rewrite > (times_n_SO (gcd n m)).
+rewrite < (sym_times (S O)).
+apply (divides_d_times_gcd)
+[ apply (lt_O_S O)
+| rewrite > (sym_times (S O)).
+ rewrite < (times_n_SO m).
+ assumption
+| rewrite > (sym_times (S O)).
+ rewrite < (times_n_SO n).
+ assumption
+]
qed.
theorem eq_minus_gcd_aux: \forall p,m,n.O < n \to n \le m \to n \le p \to
\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).assumption.apply le_to_not_lt.assumption.
-cut (O < m).
-cut (n1 \divides m \lor n1 \ndivides m).
-simplify.
-elim Hcut1.
-rewrite > divides_to_divides_b_true.
-simplify.
-apply (ex_intro ? ? (S O)).
-apply (ex_intro ? ? O).
-left.simplify.rewrite < plus_n_O.
-apply sym_eq.apply minus_n_O.
-assumption.assumption.
-rewrite > not_divides_to_divides_b_false.
-change with
-(\exists a,b.
-a*n1 - b*m = gcd_aux n n1 (m \mod n1)
-\lor
-b*m - a*n1 = gcd_aux n n1 (m \mod n1)).
-cut
-(\exists a,b.
-a*(m \mod n1) - b*n1= gcd_aux n n1 (m \mod n1)
-\lor
-b*n1 - a*(m \mod n1) = gcd_aux n n1 (m \mod n1)).
-elim Hcut2.elim H5.elim H6.
-(* first case *)
-rewrite < H7.
-apply (ex_intro ? ? (a1+a*(m / n1))).
-apply (ex_intro ? ? a).
-right.
-rewrite < sym_plus.
-rewrite < (sym_times n1).
-rewrite > distr_times_plus.
-rewrite > (sym_times n1).
-rewrite > (sym_times n1).
-rewrite > (div_mod m n1) in \vdash (? ? (? % ?) ?).
-rewrite > assoc_times.
-rewrite < sym_plus.
-rewrite > distr_times_plus.
-rewrite < eq_minus_minus_minus_plus.
-rewrite < sym_plus.
-rewrite < plus_minus.
-rewrite < minus_n_n.reflexivity.
-apply le_n.
-assumption.
-(* second case *)
-rewrite < H7.
-apply (ex_intro ? ? (a1+a*(m / n1))).
-apply (ex_intro ? ? a).
-left.
-(* clear Hcut2.clear H5.clear H6.clear H. *)
-rewrite > sym_times.
-rewrite > distr_times_plus.
-rewrite > sym_times.
-rewrite > (sym_times n1).
-rewrite > (div_mod m n1) in \vdash (? ? (? ? %) ?).
-rewrite > distr_times_plus.
-rewrite > assoc_times.
-rewrite < eq_minus_minus_minus_plus.
-rewrite < sym_plus.
-rewrite < plus_minus.
-rewrite < minus_n_n.reflexivity.
-apply le_n.
-assumption.
-apply (H n1 (m \mod n1)).
-cut (O \lt m \mod n1 \lor O = m \mod n1).
-elim Hcut2.assumption.
-absurd (n1 \divides m).apply mod_O_to_divides.
-assumption.
-symmetry.assumption.assumption.
-apply le_to_or_lt_eq.apply le_O_n.
-apply lt_to_le.
-apply lt_mod_m_m.assumption.
-apply le_S_S_to_le.
-apply (trans_le ? n1).
-change with (m \mod n1 < n1).
-apply lt_mod_m_m.
-assumption.assumption.assumption.assumption.
-apply (decidable_divides n1 m).assumption.
-apply (lt_to_le_to_lt ? n1).assumption.assumption.
+elim p
+ [absurd (O < n)
+ [assumption
+ |apply le_to_not_lt.assumption
+ ]
+ |cut (O < m)
+ [cut (n1 \divides m \lor n1 \ndivides m)
+ [simplify.
+ elim Hcut1
+ [rewrite > divides_to_divides_b_true
+ [simplify.
+ apply (ex_intro ? ? (S O)).
+ apply (ex_intro ? ? O).
+ left.
+ simplify.
+ rewrite < plus_n_O.
+ apply sym_eq.
+ apply minus_n_O
+ |assumption
+ |assumption
+ ]
+ |rewrite > not_divides_to_divides_b_false
+ [change with
+ (\exists a,b.a*n1 - b*m = gcd_aux n n1 (m \mod n1)
+ \lor b*m - a*n1 = gcd_aux n n1 (m \mod n1)).
+ cut
+ (\exists a,b.a*(m \mod n1) - b*n1= gcd_aux n n1 (m \mod n1)
+ \lor b*n1 - a*(m \mod n1) = gcd_aux n n1 (m \mod n1))
+ [elim Hcut2.elim H5.elim H6
+ [(* first case *)
+ rewrite < H7.
+ apply (ex_intro ? ? (a1+a*(m / n1))).
+ apply (ex_intro ? ? a).
+ right.
+ rewrite < sym_plus.
+ rewrite < (sym_times n1).
+ rewrite > distr_times_plus.
+ rewrite > (sym_times n1).
+ rewrite > (sym_times n1).
+ rewrite > (div_mod m n1) in \vdash (? ? (? % ?) ?)
+ [rewrite > assoc_times.
+ rewrite < sym_plus.
+ rewrite > distr_times_plus.
+ rewrite < eq_minus_minus_minus_plus.
+ rewrite < sym_plus.
+ rewrite < plus_minus
+ [rewrite < minus_n_n.reflexivity
+ |apply le_n
+ ]
+ |assumption
+ ]
+ |(* second case *)
+ rewrite < H7.
+ apply (ex_intro ? ? (a1+a*(m / n1))).
+ apply (ex_intro ? ? a).
+ left.
+ (* clear Hcut2.clear H5.clear H6.clear H. *)
+ rewrite > sym_times.
+ rewrite > distr_times_plus.
+ rewrite > sym_times.
+ rewrite > (sym_times n1).
+ rewrite > (div_mod m n1) in \vdash (? ? (? ? %) ?)
+ [rewrite > distr_times_plus.
+ rewrite > assoc_times.
+ rewrite < eq_minus_minus_minus_plus.
+ rewrite < sym_plus.
+ rewrite < plus_minus
+ [rewrite < minus_n_n.reflexivity
+ |apply le_n
+ ]
+ |assumption
+ ]
+ ]
+ |apply (H n1 (m \mod n1))
+ [cut (O \lt m \mod n1 \lor O = m \mod n1)
+ [elim Hcut2
+ [assumption
+ |absurd (n1 \divides m)
+ [apply mod_O_to_divides
+ [assumption
+ |symmetry.assumption
+ ]
+ |assumption
+ ]
+ ]
+ |apply le_to_or_lt_eq.
+ apply le_O_n
+ ]
+ |apply lt_to_le.
+ apply lt_mod_m_m.
+ assumption
+ |apply le_S_S_to_le.
+ apply (trans_le ? n1)
+ [change with (m \mod n1 < n1).
+ apply lt_mod_m_m.
+ assumption
+ |assumption
+ ]
+ ]
+ ]
+ |assumption
+ |assumption
+ ]
+ ]
+ |apply (decidable_divides n1 m).
+ assumption
+ ]
+ |apply (lt_to_le_to_lt ? n1);assumption
+ ]
+ ]
qed.
theorem eq_minus_gcd:
intros.unfold lt.apply le_S_S.apply le_O_n.
qed.
+theorem gcd_n_n: \forall n.gcd n n = n.
+intro.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]
+ ]
+ ]
+ ]
+qed.
+
+theorem gcd_SO_to_lt_O: \forall i,n. (S O) < n \to gcd i n = (S O) \to
+O < i.
+intros.
+elim (le_to_or_lt_eq ? ? (le_O_n i))
+ [assumption
+ |absurd ((gcd i n) = (S O))
+ [assumption
+ |rewrite < H2.
+ simplify.
+ unfold.intro.
+ apply (lt_to_not_eq (S O) n H).
+ apply sym_eq.assumption
+ ]
+ ]
+qed.
+
+theorem gcd_SO_to_lt_n: \forall i,n. (S O) < n \to i \le n \to gcd i n = (S O) \to
+i < n.
+intros.
+elim (le_to_or_lt_eq ? ? H1)
+ [assumption
+ |absurd ((gcd i n) = (S O))
+ [assumption
+ |rewrite > H3.
+ rewrite > gcd_n_n.
+ unfold.intro.
+ apply (lt_to_not_eq (S O) n H).
+ apply sym_eq.assumption
+ ]
+ ]
+qed.
+
+theorem gcd_n_times_nm: \forall n,m. O < m \to gcd n (n*m) = n.
+intro.apply (nat_case n)
+ [intros.reflexivity
+ |intros.
+ 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.rewrite > (times_n_O O).
+ apply lt_times[apply lt_O_S|assumption]
+ |apply divides_d_gcd
+ [apply (witness ? ? m1).reflexivity
+ |apply divides_n_n
+ ]
+ ]
+ ]
+ ]
+qed.
+
theorem symmetric_gcd: symmetric nat gcd.
(*CSC: bug here: unfold symmetric does not work *)
change with
theorem le_gcd_times: \forall m,n,p:nat. O< p \to gcd m n \le gcd m (n*p).
intros.
-apply (nat_case n).reflexivity.
+apply (nat_case n).apply le_n.
intro.
apply divides_to_le.
apply lt_O_gcd.
(* for the "converse" of the previous result see the end of this development *)
+theorem eq_gcd_SO_to_not_divides: \forall n,m. (S O) < n \to
+(gcd n m) = (S O) \to \lnot (divides n m).
+intros.unfold.intro.
+elim H2.
+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)
+ [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));
+ [assumption
+ |apply False_ind.
+ apply (le_to_not_lt n (S O))
+ [rewrite < H4.
+ apply divides_to_le
+ [rewrite > H4.apply lt_O_S
+ |apply divides_d_gcd
+ [apply (witness ? ? n2).reflexivity
+ |apply divides_n_n
+ ]
+ ]
+ |assumption
+ ]
+ ]
+ ]
+qed.
+
theorem gcd_SO_n: \forall n:nat. gcd (S O) n = (S O).
intro.
apply antisym_le.apply divides_to_le.unfold lt.apply le_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.
rewrite > distr_times_minus.
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))
+ elim H1.
+ (*
+ rewrite > H6.
+ applyS (witness n (n*(q*a-a1*n2)) (q*a-a1*n2))
reflexivity. *);
- applyS (witness n ? ? (refl_eq ? ?)).
+ applyS (witness n ? ? (refl_eq ? ?)) (* timeout=50 *).
(*
rewrite < (sym_times n).rewrite < assoc_times.
rewrite > (sym_times q).rewrite > assoc_times.
]
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.
rewrite > (times_n_O O).
apply lt_times.assumption.assumption.
qed.
+
+theorem gcd_SO_to_divides_times_to_divides: \forall m,n,p:nat. O < n \to
+gcd n m = (S O) \to n \divides (m*p) \to n \divides p.
+intros.
+cut (n \divides p \lor n \ndivides p)
+ [elim Hcut
+ [assumption
+ |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 *)
+ 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 ? ?)) (* 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 ? ?)).
+ ](* end second case *)
+ |rewrite < H1.apply eq_minus_gcd.
+ ]
+ ]
+ |apply (decidable_divides n p).
+ assumption.
+ ]
+qed.
+
projects / helm.git / blobdiff