(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/nat/gcd_properties1".
-
include "nat/gcd.ma".
(* this file contains some important properites of gcd in N *)
-(*it's a generalization of the existing theorem divides_gcd_aux (in which
- c = 1), proved in file gcd.ma
- *)
-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.
-
-(*it's a generalization of the existing theorem divides_gcd_d (in which
- c = 1), proved in file gcd.ma
- *)
-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.
-change with
-(d \divides c *
-match leb n m with
- [ true \Rightarrow
- match n with
- [ O \Rightarrow m
- | (S p) \Rightarrow gcd_aux (S p) m (S p) ]
- | false \Rightarrow
- 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 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.
-
(* an alternative characterization for gcd *)
theorem gcd1: \forall a,b,c:nat.
c \divides a \to c \divides b \to
intros.
elim (H2 ((gcd a b)))
[ apply (antisymmetric_divides (gcd a b) c)
- [ apply (witness (gcd a b) c n2).
+ [ apply (witness (gcd a b) c n1).
assumption
| apply divides_d_gcd;
assumption
intros.
apply (inj_times_r1 m H).
rewrite > (sym_times m ((gcd a b)/m)).
-rewrite > (divides_to_times_div (gcd a b) m)
+rewrite > (divides_to_div m (gcd a b))
[ rewrite < eq_gcd_times_times_times_gcd.
rewrite > (sym_times m (a/m)).
rewrite > (sym_times m (b/m)).
- rewrite > (divides_to_times_div a m H H1).
- rewrite > (divides_to_times_div b m H H2).
+ rewrite > (divides_to_div m a H1).
+ rewrite > (divides_to_div m b H2).
reflexivity
-| assumption
| apply divides_d_gcd;
assumption
]
[ cut (O \lt (gcd a b))
[ apply (gcd_SO_to_divides_times_to_divides (b/(gcd a b)) (a/(gcd a b)) c)
[ apply (O_lt_times_to_O_lt (a/(gcd a b)) (gcd a b)).
- rewrite > (divides_to_times_div a (gcd a b))
+ rewrite > (divides_to_div (gcd a b) a)
[ assumption
- | assumption
| apply divides_gcd_n
]
| rewrite < (div_n_n (gcd a b)) in \vdash (? ? ? %)
]
| assumption
]
- | apply (witness ? ? n2).
+ | apply (witness ? ? n1).
apply (inj_times_r1 (gcd a b) Hcut1).
rewrite < assoc_times.
rewrite < sym_times in \vdash (? ? (? % ?) ?).
- rewrite > (divides_to_times_div b (gcd a b))
+ rewrite > (divides_to_div (gcd a b) b)
[ rewrite < assoc_times in \vdash (? ? ? %).
rewrite < sym_times in \vdash (? ? ? (? % ?)).
- rewrite > (divides_to_times_div a (gcd a b))
+ rewrite > (divides_to_div (gcd a b) a)
[ assumption
- | assumption
| apply divides_gcd_n
]
- | assumption
| apply divides_gcd_m
]
]
| intros.
elim H1.
elim H2.
- cut(b = (d*n2) + a)
- [ cut (b - (d*n2) = a)
+ cut(b = (d*n1) + a)
+ [ cut (b - (d*n1) = a)
[ rewrite > H4 in Hcut1.
- rewrite < (distr_times_minus d n n2) in Hcut1.
+ rewrite < (distr_times_minus d n n1) in Hcut1.
apply divides_d_gcd
[ assumption
- | apply (witness d a (n - n2)).
+ | apply (witness d a (n - n1)).
apply sym_eq.
assumption
]