From 68881776450a44573b26ed32673baf7f61ce7670 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Mon, 27 Nov 2006 11:59:16 +0000 Subject: [PATCH] Small changes --- matita/library/nat/gcd.ma | 8 +- matita/library/nat/totient.ma | 151 +++++++++++++++++++--------------- 2 files changed, 89 insertions(+), 70 deletions(-) diff --git a/matita/library/nat/gcd.ma b/matita/library/nat/gcd.ma index 036167bd0..66bc6f865 100644 --- a/matita/library/nat/gcd.ma +++ b/matita/library/nat/gcd.ma @@ -519,10 +519,12 @@ cut (n \divides p \lor n \ndivides p) 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 ? ?)) timeout=50. + applyS (witness n ? ? (refl_eq ? ?)) (* timeout=50 *). (* rewrite < (sym_times n).rewrite < assoc_times. rewrite > (sym_times q).rewrite > assoc_times. diff --git a/matita/library/nat/totient.ma b/matita/library/nat/totient.ma index 2c6061e0b..b4f575a40 100644 --- a/matita/library/nat/totient.ma +++ b/matita/library/nat/totient.ma @@ -31,71 +31,88 @@ qed. theorem totient_times: \forall n,m:nat. (gcd m n) = (S O) \to totient (n*m) = (totient n)*(totient m). intro. -apply (nat_case n). -intro.simplify.intro.reflexivity. -intros 2.apply (nat_case m1). -rewrite < sym_times. -rewrite < (sym_times (totient O)). -simplify.intro.reflexivity. -intros. -unfold totient. -apply (count_times m m2 ? ? ? -(\lambda b,a. cr_pair (S m) (S m2) a b) (\lambda x. x \mod (S m)) (\lambda x. x \mod (S m2))). -intros.unfold cr_pair. -apply (le_to_lt_to_lt ? (pred ((S m)*(S m2)))). -unfold min. -apply le_min_aux_r.unfold lt. -apply (nat_case ((S m)*(S m2))).apply le_n. -intro.apply le_n. -intros. -generalize in match (mod_cr_pair (S m) (S m2) a b H1 H2 H). -intro.elim H3. -apply H4. -intros. -generalize in match (mod_cr_pair (S m) (S m2) a b H1 H2 H). -intro.elim H3. -apply H5. -intros. -generalize in match (mod_cr_pair (S m) (S m2) a b H1 H2 H). -intro.elim H3. -apply eqb_elim. -intro. -rewrite > eq_to_eqb_true. -rewrite > eq_to_eqb_true. -reflexivity. -rewrite < H4. -rewrite > sym_gcd. -rewrite > gcd_mod. -apply (gcd_times_SO_to_gcd_SO ? ? (S m2)). -unfold lt.apply le_S_S.apply le_O_n. -unfold lt.apply le_S_S.apply le_O_n. -assumption. -unfold lt.apply le_S_S.apply le_O_n. -rewrite < H5. -rewrite > sym_gcd. -rewrite > gcd_mod. -apply (gcd_times_SO_to_gcd_SO ? ? (S m)). -unfold lt.apply le_S_S.apply le_O_n. -unfold lt.apply le_S_S.apply le_O_n. -rewrite > sym_times. -assumption. -unfold lt.apply le_S_S.apply le_O_n. -intro. -apply eqb_elim. -intro.apply eqb_elim. -intro.apply False_ind. -apply H6. -apply eq_gcd_times_SO. -unfold lt.apply le_S_S.apply le_O_n. -unfold lt.apply le_S_S.apply le_O_n. -rewrite < gcd_mod. -rewrite > H4. -rewrite > sym_gcd.assumption. -unfold lt.apply le_S_S.apply le_O_n. -rewrite < gcd_mod. -rewrite > H5. -rewrite > sym_gcd.assumption. -unfold lt.apply le_S_S.apply le_O_n. -intro.reflexivity. -intro.reflexivity. +apply (nat_case n) + [intros.simplify.reflexivity + |intros 2.apply (nat_case m1) + [rewrite < sym_times. + rewrite < (sym_times (totient O)). + simplify.intro.reflexivity. + |intros. + unfold totient. + apply (count_times m m2 ? ? ? + (\lambda b,a. cr_pair (S m) (S m2) a b) + (\lambda x. x \mod (S m)) (\lambda x. x \mod (S m2))) + [intros.unfold cr_pair. + apply (le_to_lt_to_lt ? (pred ((S m)*(S m2)))) + [unfold min. + apply le_min_aux_r + |unfold lt. + apply (nat_case ((S m)*(S m2))) + [apply le_n|intro.apply le_n] + ] + |intros. + generalize in match (mod_cr_pair (S m) (S m2) a b H1 H2 H). + intro.elim H3. + apply H4 + |intros. + generalize in match (mod_cr_pair (S m) (S m2) a b H1 H2 H). + intro.elim H3. + apply H5 + |intros. + generalize in match (mod_cr_pair (S m) (S m2) a b H1 H2 H). + intro.elim H3. + apply eqb_elim + [intro. + rewrite > eq_to_eqb_true + [rewrite > eq_to_eqb_true + [reflexivity + |rewrite < H4. + rewrite > sym_gcd. + rewrite > gcd_mod + [apply (gcd_times_SO_to_gcd_SO ? ? (S m2)) + [unfold lt.apply le_S_S.apply le_O_n + |unfold lt.apply le_S_S.apply le_O_n + |assumption + ] + |unfold lt.apply le_S_S.apply le_O_n + ] + ] + |rewrite < H5. + rewrite > sym_gcd. + rewrite > gcd_mod + [apply (gcd_times_SO_to_gcd_SO ? ? (S m)) + [unfold lt.apply le_S_S.apply le_O_n + |unfold lt.apply le_S_S.apply le_O_n + |rewrite > sym_times.assumption + ] + |unfold lt.apply le_S_S.apply le_O_n + ] + ] + |intro. + apply eqb_elim + [intro.apply eqb_elim + [intro.apply False_ind. + apply H6. + apply eq_gcd_times_SO + [unfold lt.apply le_S_S.apply le_O_n. + |unfold lt.apply le_S_S.apply le_O_n. + |rewrite < gcd_mod + [rewrite > H4. + rewrite > sym_gcd.assumption + |unfold lt.apply le_S_S.apply le_O_n + ] + |rewrite < gcd_mod + [rewrite > H5. + rewrite > sym_gcd.assumption + |unfold lt.apply le_S_S.apply le_O_n + ] + ] + |intro.reflexivity + ] + |intro.reflexivity + ] + ] + ] + ] + ] qed. \ No newline at end of file -- 2.39.2