include "nat/map_iter_p.ma".
include "nat/totient.ma".
-lemma 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.
-
-
+(*
lemma count_card: \forall p.\forall n.
p O = false \to count (S n) p = card n p.
intros.elim n
qed.
-(* a reformulation of totient using card insted of count *)
+( a reformulation of totient using card insted of count )
lemma totient_card: \forall n.
totient n = card n (\lambda i.eqb (gcd i n) (S O)).
]
]
qed.
+*)
+
+(*this obvious property is useful because simplify, sometimes,
+ "simplifies too much", and doesn't allow to obtain this simple result.
+ *)
+theorem card_Sn: \forall n:nat. \forall p:nat \to bool.
+card (S n) p = (bool_to_nat (p (S n))) + (card n p).
+intros.
+simplify.
+reflexivity.
+qed.
+
+(* a reformulation of totient using card insted of sigma_p *)
+
+theorem totient_card_aux: \forall n,m: nat.
+m = n \to
+sigma_p (S (S n)) (\lambda m:nat.eqb (gcd m (S (S n))) (S O)) (\lambda x:nat. (S O))
+= card (S n) (\lambda m:nat.eqb (gcd m (S (S n))) (S O)).
+intros.
+rewrite < H in \vdash (? ? (? % ? ?) ?).
+rewrite < H in \vdash (? ? ? (? % ?)).
+elim (m)
+[ rewrite > card_Sn.
+ cut ((eqb (gcd (S O)(S (S n))) (S O) ) = true)
+ [ rewrite > Hcut.
+ simplify in \vdash (? ? ? %).
+ rewrite > true_to_sigma_p_Sn
+ [ rewrite > false_to_sigma_p_Sn in \vdash (? ? (? ? %) ?)
+ [ simplify in \vdash (? ? % ?).
+ reflexivity
+ | rewrite > gcd_O_n.
+ apply not_eq_to_eqb_false.
+ apply cic:/matita/nat/nat/not_eq_S.con.
+ unfold Not.
+ intro.
+ cut ( (S n) \le O)
+ [ apply (not_le_Sn_n n ?).
+ apply (transitive_le (S n) O n ? ?);
+ [ apply (Hcut1)
+ | apply (le_O_n n)
+ ]
+ | rewrite > H1.
+ apply le_n
+ ]
+ ]
+ | assumption
+ ]
+ | apply eq_to_eqb_true.
+ rewrite > gcd_SO_n.
+ reflexivity
+ ]
+| cut ((eqb (gcd (S (S n1)) (S (S n))) (S O)) = true
+ \lor (eqb (gcd (S (S n1)) (S (S n))) (S O)) = false)
+ [ elim Hcut
+ [ rewrite > card_Sn.
+ rewrite > true_to_sigma_p_Sn
+ [ rewrite > H2.
+ simplify in \vdash (? ? ? (? % ?)).
+ apply eq_f.
+ assumption
+ | assumption
+ ]
+ | rewrite > card_Sn.
+ rewrite > false_to_sigma_p_Sn
+ [ rewrite > H2.
+ simplify in \vdash (? ? ? (? % ?)).
+ rewrite > sym_plus.
+ rewrite < plus_n_O.
+ assumption
+ | assumption
+ ]
+ ]
+ | elim (eqb (gcd (S (S n1)) (S (S n))) (S O))
+ [ left.
+ reflexivity
+ | right.
+ reflexivity
+ ]
+ ]
+]
+qed.
+
+
+lemma totient_card: \forall n.
+totient n = card n (\lambda i.eqb (gcd i n) (S O)).
+intros.
+elim n
+[ simplify.
+ reflexivity
+| elim n1
+ [ simplify.
+ reflexivity
+ |
+ (*unfold card.
+ intros.*)
+ (* here simplify creates problems: it seems it simplifies too much. I had to
+ * introduce the obvious theorem card_Sn.
+ *)
+ rewrite > card_Sn.
+ rewrite > (gcd_n_n (S (S n2))).
+ cut ((eqb (S (S n2)) (S O)) = false)
+ [ rewrite > Hcut.
+ simplify in \vdash (? ? ? (? % ?)).
+ rewrite > sym_plus.
+ rewrite < (plus_n_O).
+ unfold totient.
+ apply (totient_card_aux n2 n2).
+ reflexivity
+ | apply not_eq_to_eqb_false.
+ apply cic:/matita/nat/nat/not_eq_S.con.
+ unfold Not.
+ intro.
+ cut ( (S n2) \le O)
+ [ apply (not_le_Sn_n n2 ?).
+ apply (transitive_le (S n2) O n2 ? ?);
+ [ apply (Hcut)
+ | apply (le_O_n n2)
+ ]
+ | rewrite > H2.
+ apply le_n
+ ]
+ ]
+ ]
+]
+qed.
+
theorem gcd_pi_p: \forall n,k. O < k \to k \le n \to
gcd n (pi_p (\lambda i.eqb (gcd i n) (S O)) k) = (S O).
intros 3.elim H
[rewrite > pi_p_S.
cut (eqb (gcd (S O) n) (S O) = true)
[rewrite > Hcut.
- change with ((gcd n (S O)) = (S O)).autobatch
- |apply eq_to_eqb_true.autobatch
+ change with ((gcd n (S O)) = (S O)).
+ apply (transitive_eq nat (gcd n (S O)) (gcd (S O) n) (S O) ? ?);
+ [ apply (sym_eq nat (gcd (S O) n) (gcd n (S O)) ?).
+ apply (symmetric_gcd (S O) n).
+ | apply (gcd_SO_n n).
+ ]
+ |apply eq_to_eqb_true.
+ apply (gcd_SO_n n)
]
|rewrite > pi_p_S.
apply eqb_elim
|apply mod_O_to_divides
[assumption
|rewrite > distr_times_minus.
- autobatch
+ apply (divides_to_mod_O n (minus (times a j) (times a i)) ? ?);
+ [ apply (H3).
+ | apply (eq_mod_to_divides (times a j) (times a i) n ? ?);
+ [ apply (H3).
+ |apply (sym_eq nat (mod (times a i) n) (mod (times a j) n) ?).
+ apply (H13).
+ ]
+ ]
]
]
]
- |autobatch
+ | apply (le_minus_m j i).
]
]
|intro.assumption
|apply mod_O_to_divides
[assumption
|rewrite > distr_times_minus.
- autobatch
+ apply (divides_to_mod_O n (minus (times a i) (times a j)) ? ?);
+ [apply (H3).
+ | apply (eq_mod_to_divides (times a i) (times a j) n ? ?);
+ [apply (H3).
+ |apply (H13).
+ ]
+ ]
]
]
]
- |autobatch
+ | apply (le_minus_m i j).
]
]
]
gcd a n = (S O) \to congruent (exp a (totient n)) (S O) n.
intros.
cut (O < a)
- [apply divides_to_congruent
+ [ apply divides_to_congruent
[apply (trans_lt ? (S O)).apply lt_O_S. assumption
|change with (O < exp a (totient n)).apply lt_O_exp.assumption
|apply (gcd_SO_to_divides_times_to_divides (pi_p (\lambda i.eqb (gcd i n) (S O)) n))
[assumption|apply sym_eq.assumption]
]
]
- ]
-qed.
-
\ No newline at end of file
+ ]
+qed.
include "nat/primes.ma".
include "nat/ord.ma".
include "nat/generic_sigma_p.ma".
+include "nat/count.ma".(*necessary just to use bool_to_nat and bool_to_nat_andb*)
(* sigma_p on nautral numbers is a specialization of sigma_p_gen *)
]
qed.
+(*some properties of sigma_p invoked with an "always true" predicate (in this
+ way sigma_p just counts the elements, without doing any control) or with
+ the nat \to nat function which always returns (S O).
+ It 's not easily possible proving these theorems in a general form
+ in generic_sigma_p.ma
+ *)
+
+theorem sigma_p_true: \forall n:nat.
+(sigma_p n (\lambda x.true) (\lambda x.S O)) = n.
+intros.
+elim n
+[ simplify.
+ reflexivity
+| rewrite > (true_to_sigma_p_Sn n1 (\lambda x:nat.true) (\lambda x:nat.S O))
+ [ rewrite > H.
+ simplify.
+ reflexivity
+ | reflexivity
+ ]
+]
+qed.
+
+theorem sigma_P_SO_to_sigma_p_true: \forall n:nat. \forall g:nat \to bool.
+sigma_p n g (\lambda n:nat. (S O)) =
+sigma_p n (\lambda x:nat.true) (\lambda i:nat.bool_to_nat (g i)).
+intros.
+elim n
+[ simplify.
+ reflexivity
+| cut ((g n1) = true \lor (g n1) = false)
+ [ rewrite > true_to_sigma_p_Sn in \vdash (? ? ? %)
+ [ elim Hcut
+ [ rewrite > H1.
+ rewrite > true_to_sigma_p_Sn in \vdash (? ? % ?)
+ [ simplify.
+ apply eq_f.
+ assumption
+ | assumption
+ ]
+ | rewrite > H1.
+ rewrite > false_to_sigma_p_Sn in \vdash (? ? % ?)
+ [ simplify.
+ assumption
+ | assumption
+ ]
+ ]
+ | reflexivity
+ ]
+ | elim (g n1)
+ [ left.
+ reflexivity
+ | right.
+ reflexivity
+ ]
+ ]
+]
+qed.
+
+(* I introduce an equivalence in the form map_iter_i in order to use
+ * the existing result about permutation in that part of the library.
+ *)
+
+theorem eq_map_iter_i_sigma_p_alwaysTrue: \forall n:nat.\forall g:nat \to nat.
+map_iter_i n g plus O = sigma_p (S n) (\lambda c:nat.true) g.
+intros.
+elim n
+[ simplify.
+ rewrite < plus_n_O.
+ reflexivity
+| rewrite > true_to_sigma_p_Sn
+ [ simplify in \vdash (? ? % ?).
+ rewrite < plus_n_O.
+ apply eq_f.
+ assumption
+ | reflexivity
+ ]
+]
+qed.
+
+theorem sigma_p_plus_1: \forall n:nat. \forall f,g:nat \to nat.
+sigma_p n (\lambda b:nat. true) (\lambda a:nat.(f a) + (g a)) =
+sigma_p n (\lambda b:nat. true) f + sigma_p n (\lambda b:nat. true) g.
+intros.
+elim n
+[ simplify.
+ reflexivity
+| rewrite > true_to_sigma_p_Sn
+ [ rewrite > (true_to_sigma_p_Sn n1 (\lambda c:nat.true) f)
+ [ rewrite > (true_to_sigma_p_Sn n1 (\lambda c:nat.true) g)
+ [ rewrite > assoc_plus in \vdash (? ? ? %).
+ rewrite < assoc_plus in \vdash (? ? ? (? ? %)).
+ rewrite < sym_plus in \vdash (? ? ? (? ? (? % ?))).
+ rewrite > assoc_plus in \vdash (? ? ? (? ? %)).
+ rewrite < assoc_plus in \vdash (? ? ? %).
+ apply eq_f.
+ assumption
+ | reflexivity
+ ]
+ | reflexivity
+ ]
+ | reflexivity
+ ]
+]
+qed.
+
+
+theorem eq_sigma_p_sigma_p_times1 : \forall n,m:nat.\forall f:nat \to nat.
+sigma_p (n*m) (\lambda x:nat.true) f =
+sigma_p m (\lambda x:nat.true)
+ (\lambda a.(sigma_p n (\lambda x:nat.true) (\lambda b.f (b*m + a)))).
+intro.
+elim n
+[ simplify.
+ elim m
+ [ simplify.
+ reflexivity
+ | rewrite > true_to_sigma_p_Sn
+ [ rewrite < H.
+ reflexivity
+ | reflexivity
+ ]
+ ]
+| change in \vdash (? ? ? (? ? ? (\lambda a:?.%))) with ((f ((n1*m)+a)) +
+ (sigma_p n1 (\lambda x:nat.true) (\lambda b:nat.f (b*m +a)))).
+ rewrite > sigma_p_plus_1 in \vdash (? ? ? %).
+ rewrite > (sym_times (S n1) m).
+ rewrite < (times_n_Sm m n1).
+ rewrite > sigma_p_plus in \vdash (? ? % ?).
+ apply eq_f2
+ [ rewrite < (sym_times m n1).
+ apply eq_sigma_p
+ [ intros.
+ reflexivity
+ | intros.
+ rewrite < (sym_plus ? (m * n1)).
+ reflexivity
+ ]
+ | rewrite > (sym_times m n1).
+ apply H
+ ]
+]
+qed.
+
+theorem eq_sigma_p_sigma_p_times2 : \forall n,m:nat.\forall f:nat \to nat.
+sigma_p (n *m) (\lambda c:nat.true) f =
+sigma_p n (\lambda c:nat.true)
+ (\lambda a.(sigma_p m (\lambda c:nat.true) (\lambda b:nat.f (b* n + a)))).
+intros.
+rewrite > sym_times.
+apply eq_sigma_p_sigma_p_times1.
+qed.
+
+
+theorem sigma_p_times:\forall n,m:nat.
+\forall f,f1,f2:nat \to bool.
+\forall g:nat \to nat \to nat.
+\forall g1,g2: nat \to nat.
+(\forall a,b:nat. a < (S n) \to b < (S m) \to (g b a) < (S n)*(S m)) \to
+(\forall a,b:nat. a < (S n) \to b < (S m) \to (g1 (g b a)) = a) \to
+(\forall a,b:nat. a < (S n) \to b < (S m) \to (g2 (g b a)) = b) \to
+(\forall a,b:nat. a < (S n) \to b < (S m) \to f (g b a) = andb (f2 b) (f1 a)) \to
+(sigma_p ((S n) * (S m)) f (\lambda c:nat.(S O))) =
+sigma_p (S n) f1 (\lambda c:nat.(S O)) * sigma_p (S m) f2 (\lambda c:nat.(S O)).
+intros.
+
+rewrite > (sigma_P_SO_to_sigma_p_true ).
+rewrite > (S_pred ((S n)*(S m))) in \vdash (? ? (? % ? ?) ?)
+[ rewrite < (eq_map_iter_i_sigma_p_alwaysTrue (pred ((S n)* (S m)))).
+ rewrite > (permut_to_eq_map_iter_i plus assoc_plus sym_plus ? ? ?
+ (\lambda i.g (div i (S n)) (mod i (S n))))
+ [ rewrite > eq_map_iter_i_sigma_p_alwaysTrue.
+ rewrite < S_pred
+ [ rewrite > eq_sigma_p_sigma_p_times2.
+ apply (trans_eq ? ? (sigma_p (S n) (\lambda c:nat.true)
+ (\lambda a. sigma_p (S m) (\lambda c:nat.true)
+ (\lambda b.(bool_to_nat (f2 b))*(bool_to_nat (f1 a))))))
+ [ apply eq_sigma_p;intros
+ [ reflexivity
+ | apply eq_sigma_p;intros
+ [ reflexivity
+ |
+ rewrite > (div_mod_spec_to_eq (x1*(S n) + x) (S n) ((x1*(S n) + x)/(S n))
+ ((x1*(S n) + x) \mod (S n)) x1 x)
+ [ rewrite > (div_mod_spec_to_eq2 (x1*(S n) + x) (S n) ((x1*(S n) + x)/(S n))
+ ((x1*(S n) + x) \mod (S n)) x1 x)
+ [ rewrite > H3
+ [ apply bool_to_nat_andb
+ | assumption
+ | assumption
+ ]
+ | apply div_mod_spec_div_mod.
+ apply lt_O_S
+ | constructor 1
+ [ assumption
+ | reflexivity
+ ]
+ ]
+ | apply div_mod_spec_div_mod.
+ apply lt_O_S
+ | constructor 1
+ [ assumption
+ | reflexivity
+ ]
+ ]
+ ]
+ ]
+ | apply (trans_eq ? ?
+ (sigma_p (S n) (\lambda c:nat.true) (\lambda n.((bool_to_nat (f1 n)) *
+ (sigma_p (S m) (\lambda c:nat.true) (\lambda n.bool_to_nat (f2 n)))))))
+ [ apply eq_sigma_p;intros
+ [ reflexivity
+ | rewrite > distributive_times_plus_sigma_p.
+ apply eq_sigma_p;intros
+ [ reflexivity
+ | rewrite > sym_times.
+ reflexivity
+ ]
+ ]
+ | apply sym_eq.
+ rewrite > sigma_P_SO_to_sigma_p_true.
+ rewrite > sigma_P_SO_to_sigma_p_true in \vdash (? ? (? ? %) ?).
+ rewrite > sym_times.
+ rewrite > distributive_times_plus_sigma_p.
+ apply eq_sigma_p;intros
+ [ reflexivity
+ | rewrite > distributive_times_plus_sigma_p.
+ rewrite < sym_times.
+ rewrite > distributive_times_plus_sigma_p.
+ apply eq_sigma_p;
+ intros; reflexivity
+ ]
+ ]
+ ]
+ | apply lt_O_times_S_S
+ ]
+
+ | unfold permut.
+ split
+ [ intros.
+ rewrite < plus_n_O.
+ apply le_S_S_to_le.
+ rewrite < S_pred in \vdash (? ? %)
+ [ change with ((g (i/(S n)) (i \mod (S n))) \lt (S n)*(S m)).
+ apply H
+ [ apply lt_mod_m_m.
+ unfold lt.
+ apply le_S_S.
+ apply le_O_n
+ | apply (lt_times_to_lt_l n).
+ apply (le_to_lt_to_lt ? i)
+ [ rewrite > (div_mod i (S n)) in \vdash (? ? %)
+ [ rewrite > sym_plus.
+ apply le_plus_n
+ | unfold lt.
+ apply le_S_S.
+ apply le_O_n
+ ]
+ | unfold lt.
+ rewrite > S_pred in \vdash (? ? %)
+ [ apply le_S_S.
+ rewrite > plus_n_O in \vdash (? ? %).
+ rewrite > sym_times.
+ assumption
+ | apply lt_O_times_S_S
+ ]
+ ]
+ ]
+ | apply lt_O_times_S_S
+ ]
+ | rewrite < plus_n_O.
+ unfold injn.
+ intros.
+ cut (i < (S n)*(S m))
+ [ cut (j < (S n)*(S m))
+ [ cut ((i \mod (S n)) < (S n))
+ [ cut ((i/(S n)) < (S m))
+ [ cut ((j \mod (S n)) < (S n))
+ [ cut ((j/(S n)) < (S m))
+ [ rewrite > (div_mod i (S n))
+ [ rewrite > (div_mod j (S n))
+ [ rewrite < (H1 (i \mod (S n)) (i/(S n)) Hcut2 Hcut3).
+ rewrite < (H2 (i \mod (S n)) (i/(S n)) Hcut2 Hcut3) in \vdash (? ? (? % ?) ?).
+ rewrite < (H1 (j \mod (S n)) (j/(S n)) Hcut4 Hcut5).
+ rewrite < (H2 (j \mod (S n)) (j/(S n)) Hcut4 Hcut5) in \vdash (? ? ? (? % ?)).
+ rewrite > H6.
+ reflexivity
+ | unfold lt.
+ apply le_S_S.
+ apply le_O_n
+ ]
+ | unfold lt.
+ apply le_S_S.
+ apply le_O_n
+ ]
+ | apply (lt_times_to_lt_l n).
+ apply (le_to_lt_to_lt ? j)
+ [ rewrite > (div_mod j (S n)) in \vdash (? ? %)
+ [ rewrite > sym_plus.
+ apply le_plus_n
+ | unfold lt. apply le_S_S.
+ apply le_O_n
+ ]
+ | rewrite < sym_times.
+ assumption
+ ]
+ ]
+ | apply lt_mod_m_m.
+ unfold lt.
+ apply le_S_S.
+ apply le_O_n
+ ]
+ | apply (lt_times_to_lt_l n).
+ apply (le_to_lt_to_lt ? i)
+ [ rewrite > (div_mod i (S n)) in \vdash (? ? %)
+ [ rewrite > sym_plus.
+ apply le_plus_n
+ | unfold lt.
+ apply le_S_S.
+ apply le_O_n
+ ]
+ | rewrite < sym_times.
+ assumption
+ ]
+ ]
+ | apply lt_mod_m_m.
+ unfold lt.
+ apply le_S_S.
+ apply le_O_n
+ ]
+ | unfold lt.
+ rewrite > S_pred in \vdash (? ? %)
+ [ apply le_S_S.
+ assumption
+ | apply lt_O_times_S_S
+ ]
+ ]
+ | unfold lt.
+ rewrite > S_pred in \vdash (? ? %)
+ [ apply le_S_S.
+ assumption
+ | apply lt_O_times_S_S
+ ]
+ ]
+ ]
+ | intros.
+ apply False_ind.
+ apply (not_le_Sn_O m1 H4)
+ ]
+| apply lt_O_times_S_S
+]
+qed.
set "baseuri" "cic:/matita/nat/totient".
-include "nat/count.ma".
include "nat/chinese_reminder.ma".
+include "nat/iteration2.ma".
+(*a new definition of totient, which uses sigma_p instead of sigma *)
+(*there's a little difference between this definition and the classic one:
+ the classic definition of totient is:
+
+ phi (n) is the number of naturals i (less or equal than n) so then gcd (i,n) = 1.
+ (so this definition considers the values i=1,2,...,n)
+
+ sigma_p doesn't work ok the value n (but the first value it works on is (pred n))
+ but works also on 0. That's not a problem, in fact
+ - if n <> 1, gcd (n,0) <>1 and gcd (n,n) = n <> 1.
+ - if n = 1, then Phi(n) = 1, and (totient n), as defined below, returns 1.
+
+ *)
definition totient : nat \to nat \def
-\lambda n. count n (\lambda m. eqb (gcd m n) (S O)).
-
-theorem totient3: totient (S(S(S O))) = (S(S O)).
-reflexivity.
-qed.
-
-theorem totient6: totient (S(S(S(S(S(S O)))))) = (S(S O)).
-reflexivity.
-qed.
+\lambda n.sigma_p n (\lambda m. eqb (gcd m n) (S O)) (\lambda m.S O).
+
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)
- [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))))
+intros.
+unfold totient.
+apply (nat_case1 n)
+[ apply (nat_case1 m)
+ [ intros.
+ simplify.
+ reflexivity
+ | intros.
+ simplify.
+ reflexivity
+ ]
+| apply (nat_case1 m)
+ [ intros.
+ change in \vdash (? ? ? (? ? %)) with (O).
+ rewrite > (sym_times (S m1) O).
+ rewrite > sym_times in \vdash (? ? ? %).
+ simplify.
+ reflexivity
+ | intros.
+ rewrite > H2 in H.
+ rewrite > H1 in H.
+ apply (sigma_p_times m2 m1 ? ? ?
+ (\lambda b,a. cr_pair (S m2) (S m1) a b)
+ (\lambda x. x \mod (S m2)) (\lambda x. x \mod (S m1)))
+ [intros.unfold cr_pair.
+ apply (le_to_lt_to_lt ? (pred ((S m2)*(S m1))))
[unfold min.
apply le_min_aux_r
|unfold lt.
- apply (nat_case ((S m)*(S m2)))
+ apply (nat_case ((S m2)*(S m1)))
[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
+ generalize in match (mod_cr_pair (S m2) (S m1) a b H3 H4 H).
+ intro.elim H5.
+ apply H6
|intros.
- generalize in match (mod_cr_pair (S m) (S m2) a b H1 H2 H).
- intro.elim H3.
- apply H5
+ generalize in match (mod_cr_pair (S m2) (S m1) a b H3 H4 H).
+ intro.elim H5.
+ apply H7
|intros.
- generalize in match (mod_cr_pair (S m) (S m2) a b H1 H2 H).
- intro.elim H3.
+ generalize in match (mod_cr_pair (S m2) (S m1) a b H3 H4 H).
+ intro.elim H5.
apply eqb_elim
[intro.
rewrite > eq_to_eqb_true
[rewrite > eq_to_eqb_true
[reflexivity
- |rewrite < H4.
+ |rewrite < H6.
rewrite > sym_gcd.
rewrite > gcd_mod
- [apply (gcd_times_SO_to_gcd_SO ? ? (S m2))
+ [apply (gcd_times_SO_to_gcd_SO ? ? (S m1))
[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 < H7.
rewrite > sym_gcd.
rewrite > gcd_mod
- [apply (gcd_times_SO_to_gcd_SO ? ? (S m))
+ [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
|rewrite > sym_times.assumption
apply eqb_elim
[intro.apply eqb_elim
[intro.apply False_ind.
- apply H6.
+ apply H8.
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 > H6.
rewrite > sym_gcd.assumption
|unfold lt.apply le_S_S.apply le_O_n
]
|rewrite < gcd_mod
- [rewrite > H5.
+ [rewrite > H7.
rewrite > sym_gcd.assumption
|unfold lt.apply le_S_S.apply le_O_n
]
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/nat/totient1".
+
+include "nat/totient.ma".
+include "nat/iteration2.ma".
+include "nat/propr_div_mod_lt_le_totient1_aux.ma".
+include "nat/gcd_properties1.ma".
+
+(* This file contains the proof of the following theorem about Euler's totient
+ * function:
+
+ The sum of the applications of Phi function over the divisor of a natural
+ number n is equal to n
+ *)
+
+(*two easy properties of gcd, directly obtainable from the more general theorem
+ eq_gcd_times_times_eqv_times_gcd*)
+
+theorem gcd_bTIMESd_aTIMESd_eq_d_to_gcd_a_b_eq_SO:\forall a,b,d:nat.
+O \lt d \to O \lt b \to gcd (b*d) (a*d) = d \to (gcd a b) = (S O).
+intros.
+apply (inj_times_r1 d)
+[ assumption
+| rewrite < (times_n_SO d).
+ rewrite < (eq_gcd_times_times_eqv_times_gcd a b d).
+ rewrite > sym_gcd.
+ rewrite > (sym_times d a).
+ rewrite > (sym_times d b).
+ assumption
+]
+qed.
+
+theorem gcd_SO_to_gcd_times: \forall a,b,c:nat.
+O \lt c \to (gcd a b) = (S O) \to (gcd (a*c) (b*c)) = c.
+intros.
+rewrite > (sym_times a c).
+rewrite > (sym_times b c).
+rewrite > (eq_gcd_times_times_eqv_times_gcd a b c).
+rewrite > H1.
+apply sym_eq.
+apply times_n_SO.
+qed.
+
+
+(* The proofs of the 6 sub-goals activated after the application of the theorem
+ eq_sigma_p_gh in the proof of the main theorem
+ *)
+
+
+
+(* 2nd*)
+theorem sum_divisor_totient1_aux2: \forall i,n:nat.
+(S O) \lt n \to i<n*n \to
+ (i/n) \divides (pred n) \to
+ (i \mod n) \lt (i/n) \to
+ (gcd (i \mod n) (i/n)) = (S O) \to
+ gcd (pred n) ((i\mod n)* (pred n)/(i/n)) = (pred n) / (i/n).
+intros.
+cut (O \lt (pred n))
+[ cut(O \lt (i/n))
+ [ rewrite < (NdivM_times_M_to_N (pred n) (i/n)) in \vdash (? ? (? % ?) ?)
+ [ rewrite > (sym_times ((pred n)/(i/n)) (i/n)).
+ cut ((i \mod n)*(pred n)/(i/n) = (i \mod n) * ((pred n) / (i/n)))
+ [ rewrite > Hcut2.
+ apply (gcd_SO_to_gcd_times (i/n) (i \mod n) ((pred n)/(i/n)))
+ [ apply (lt_O_a_lt_O_b_a_divides_b_to_lt_O_aDIVb (i/n) (pred n));
+ assumption
+ | rewrite > sym_gcd.
+ assumption
+ ]
+ | apply sym_eq.
+ apply (separazioneFattoriSuDivisione (i \mod n) (pred n) (i/n));
+ assumption.
+ ]
+ | assumption
+ | assumption
+ ]
+ | apply (divides_to_lt_O (i/n) (pred n));
+ assumption
+ ]
+| apply n_gt_Uno_to_O_lt_pred_n.
+ assumption.
+]
+qed.
+
+
+(*3rd*)
+theorem aux_S_i_mod_n_le_i_div_n: \forall i,n:nat.
+i < n*n \to (divides_b (i/n) (pred n) \land
+ (leb (S(i\mod n)) (i/n) \land
+ eqb (gcd (i\mod n) (i/n)) (S O))) =true
+ \to
+ (S (i\mod n)) \le (i/n).
+intros.
+cut (leb (S (i \mod n)) (i/n) = true)
+[ change with (
+ match (true) with
+ [ true \Rightarrow (S (i \mod n)) \leq (i/n)
+ | false \Rightarrow (S (i \mod n)) \nleq (i/n)]
+ ).
+ rewrite < Hcut.
+ apply (leb_to_Prop (S(i \mod n)) (i/n))
+| apply (andb_true_true (leb (S(i\mod n)) (i/n)) (divides_b (i/n) (pred n)) ).
+ apply (andb_true_true ((leb (S(i\mod n)) (i/n)) \land (divides_b (i/n) (pred n)))
+ (eqb (gcd (i\mod n) (i/n)) (S O))
+ ).
+ rewrite > andb_sym in \vdash (? ? (? % ?) ?).
+ rewrite < (andb_assoc) in \vdash (? ? % ?).
+ assumption
+]
+qed.
+
+
+(*the following theorem is just a particular case of the theorem
+ divides_times, prooved in primes.ma
+ *)
+theorem a_divides_b_to_a_divides_b_times_c: \forall a,b,c:nat.
+a \divides b \to a \divides (b*c).
+intros.
+rewrite > (times_n_SO a).
+apply (divides_times).
+assumption.
+apply divides_SO_n.
+qed.
+
+theorem sum_divisor_totient1_aux_3: \forall i,n:nat.
+i < n*n \to
+ (divides_b (i/n) (pred n)
+\land (leb (S(i\mod n)) (i/n)
+\land eqb (gcd (i\mod n) (i/n)) (S O)))
+ =true
+ \to i\mod n*pred n/(i/n)<(pred n).
+intros.
+apply (lt_to_le_to_lt ((i \mod n)*(pred n) / (i/n))
+ ((i/n)*(pred n) / (i/n))
+ (pred n))
+[ apply (lt_times_n_to_lt (i/n) ((i\mod n)*(pred n)/(i/n)) ((i/n)*(pred n)/(i/n)))
+ [ apply (Sa_le_b_to_O_lt_b (i \mod n) (i/n)).
+ apply (aux_S_i_mod_n_le_i_div_n i n);
+ assumption.
+ | rewrite > (NdivM_times_M_to_N )
+ [ rewrite > (NdivM_times_M_to_N ) in \vdash (? ? %)
+ [ apply (monotonic_lt_times_variant (pred n))
+ [ apply (nat_case1 n)
+ [ intros.
+ rewrite > H2 in H:(? ? %).
+ change in H:(? ? %) with (O).
+ change in H:(%) with ((S i) \le O).
+ apply False_ind.
+ apply (not_le_Sn_O i H)
+ | intro.
+ elim m
+ [ rewrite > H2 in H1:(%).
+ rewrite > H2 in H:(%).
+ simplify in H.
+ cut (i = O)
+ [ rewrite > Hcut in H1:(%).
+ simplify in H1.
+ apply False_ind.
+ apply (not_eq_true_false H1)
+ | change in H:(%) with((S i) \le (S O)).
+ cut (i \le O )
+ [ apply (nat_case1 i)
+ [ intros.
+ reflexivity
+ | intros.
+ rewrite > H3 in Hcut:(%).
+ apply False_ind.
+ apply (not_le_Sn_O m1 Hcut)
+ ]
+ | apply (le_S_S_to_le i O).
+ assumption
+ ]
+ ]
+ | change with ((S O) \le (S n1)).
+ apply (le_S_S O n1).
+ apply (le_O_n n1)
+ ]
+ ]
+ | change with ((S (i\mod n)) \le (i/n)).
+ apply (aux_S_i_mod_n_le_i_div_n i n);
+ assumption
+ ]
+ | apply (Sa_le_b_to_O_lt_b (i \mod n) (i/n)).
+ apply (aux_S_i_mod_n_le_i_div_n i n);
+ assumption
+ | rewrite > (times_n_SO (i/n)) in \vdash (? % ?).
+ apply (divides_times).
+ apply divides_n_n.
+ apply divides_SO_n
+ ]
+ | apply (Sa_le_b_to_O_lt_b (i \mod n) (i/n)).
+ apply (aux_S_i_mod_n_le_i_div_n i n);
+ assumption
+ | rewrite > (times_n_SO (i/n)).
+ rewrite > (sym_times (i \mod n) (pred n)).
+ apply (divides_times)
+ [ apply divides_b_true_to_divides.
+ apply (andb_true_true (divides_b (i/n) (pred n)) (leb (S (i\mod n)) (i/n))).
+ apply (andb_true_true
+ ((divides_b (i/n) (pred n)) \land (leb (S (i\mod n)) (i/n)))
+ (eqb (gcd (i\mod n) (i/n)) (S O))).
+ rewrite < (andb_assoc) in \vdash (? ? % ?).
+ assumption
+ | apply divides_SO_n
+ ]
+ ]
+ ]
+| rewrite > (sym_times).
+ rewrite > (div_times_ltO )
+ [ apply (le_n (pred n)).
+
+ | apply (Sa_le_b_to_O_lt_b (i \mod n) (i/n)).
+ apply (aux_S_i_mod_n_le_i_div_n i n);
+ assumption.
+ ]
+]qed.
+
+
+(*4th*)
+theorem sum_divisor_totient1_aux_4: \forall j,n:nat.
+j \lt (pred n) \to (S O) \lt n \to
+((divides_b ((pred n/gcd (pred n) j*n+j/gcd (pred n) j)/n) (pred n))
+ \land ((leb (S ((pred n/gcd (pred n) j*n+j/gcd (pred n) j)\mod n))
+ ((pred n/gcd (pred n) j*n+j/gcd (pred n) j)/n))
+ \land (eqb
+ (gcd ((pred n/gcd (pred n) j*n+j/gcd (pred n) j)\mod n)
+ ((pred n/gcd (pred n) j*n+j/gcd (pred n) j)/n)) (S O))))
+=true.
+intros.
+cut (O \lt (pred n))
+[ cut ( O \lt (gcd (pred n) j))
+ [ cut (j/(gcd (pred n) j) \lt n)
+ [ cut (((pred n/gcd (pred n) j*n+j/gcd (pred n) j)/n) = pred n/gcd (pred n) j)
+ [ cut (((pred n/gcd (pred n) j*n+j/gcd (pred n) j) \mod n) = j/gcd (pred n) j)
+ [ rewrite > Hcut3.
+ rewrite > Hcut4.
+ apply andb_t_t_t
+ [ apply divides_to_divides_b_true
+ [ apply (lt_times_n_to_lt (gcd (pred n) j) O (pred n/gcd (pred n) j))
+ [ assumption
+ | rewrite > (sym_times O (gcd (pred n) j)).
+ rewrite < (times_n_O (gcd (pred n) j)).
+ rewrite > (NdivM_times_M_to_N (pred n) (gcd (pred n) j))
+ [ assumption
+ | assumption
+ | apply (divides_gcd_n (pred n))
+ ]
+ ]
+ | apply (witness (pred n/(gcd (pred n) j)) (pred n) (gcd (pred n) j)).
+ rewrite > (NdivM_times_M_to_N (pred n) (gcd (pred n) j))
+ [ reflexivity
+ | assumption
+ | apply (divides_gcd_n (pred n))
+ ]
+ ]
+ | apply (le_to_leb_true).
+ apply lt_S_to_le.
+ apply cic:/matita/algebra/finite_groups/lt_S_S.con.
+ apply (lt_times_n_to_lt (gcd (pred n) j) ? ?)
+ [ assumption
+ | rewrite > (NdivM_times_M_to_N j (gcd (pred n) j))
+ [ rewrite > (NdivM_times_M_to_N (pred n) (gcd (pred n) j))
+ [ assumption
+ | assumption
+ | apply divides_gcd_n
+ ]
+ | assumption
+ | rewrite > sym_gcd.
+ apply divides_gcd_n
+ ]
+ ]
+ | apply cic:/matita/nat/compare/eq_to_eqb_true.con.
+ apply (gcd_bTIMESd_aTIMESd_eq_d_to_gcd_a_b_eq_SO ? ? (gcd (pred n) j))
+ [ assumption
+ | apply (lt_times_n_to_lt (gcd (pred n) j) ? ?)
+ [ assumption
+ | simplify.
+ rewrite > NdivM_times_M_to_N
+ [ assumption
+ | assumption
+ | apply divides_gcd_n
+ ]
+ ]
+ | rewrite > NdivM_times_M_to_N
+ [ rewrite > (NdivM_times_M_to_N j (gcd (pred n) j))
+ [ reflexivity
+ | assumption
+ | rewrite > sym_gcd.
+ apply divides_gcd_n
+ ]
+ | assumption
+ | apply divides_gcd_n
+ ]
+ ]
+ ]
+ | apply (mod_plus_times).
+ assumption
+ ]
+ | apply (div_plus_times).
+ assumption
+ ]
+ | apply (lt_times_n_to_lt (gcd (pred n) j) ? ?)
+ [ assumption
+ | rewrite > NdivM_times_M_to_N
+ [ apply (lt_to_le_to_lt j (pred n) ?)
+ [ assumption
+ | apply (lt_to_le).
+ apply (lt_to_le_to_lt ? n ?)
+ [ change with ((S (pred n)) \le n).
+ rewrite < (S_pred n)
+ [ apply le_n
+ | apply (trans_lt ? (S O) ?)
+ [ change with ((S O) \le (S O)).
+ apply (le_n (S O))
+ | assumption
+ ]
+ ]
+ | rewrite > (times_n_SO n) in \vdash (? % ?).
+ apply (le_times n)
+ [ apply (le_n n)
+ | change with (O \lt (gcd (pred n) j)).
+ assumption
+ ]
+ ]
+ ]
+ | assumption
+ | rewrite > sym_gcd.
+ apply (divides_gcd_n)
+ ]
+ ]
+ ]
+ | rewrite > sym_gcd.
+ apply (lt_O_gcd).
+ assumption
+ ]
+| apply n_gt_Uno_to_O_lt_pred_n.
+ assumption
+]
+qed.
+
+
+
+
+(*5th*)
+theorem sum_divisor_totient1_aux5: \forall a,b,c:nat.
+O \lt c \to O \lt b \to a \lt c \to b \divides a \to b \divides c \to
+a / b * c / (c/b) = a.
+intros.
+elim H3.
+elim H4.
+cut (O \lt n)
+[ rewrite > H6 in \vdash (? ? (? ? %) ?).
+ rewrite > sym_times in \vdash (? ? (? ? %) ?).
+ rewrite > (div_times_ltO n b)
+ [ cut (n \divides c)
+ [ cut (a/b * c /n = a/b * (c/n))
+ [ rewrite > Hcut2.
+ cut (c/n = b)
+ [ rewrite > Hcut3.
+ apply (NdivM_times_M_to_N a b);
+ assumption
+ | rewrite > H6.
+ apply (div_times_ltO b n).
+ assumption
+ ]
+ | elim Hcut1.
+ rewrite > H7.
+ rewrite < assoc_times in \vdash (? ? (? % ?) ?).
+ rewrite > (sym_times ((a/b)*n) n1).
+ rewrite < (assoc_times n1 (a/b) n).
+ rewrite > (div_times_ltO (n1*(a/b)) n)
+ [ rewrite > (sym_times n n1).
+ rewrite > (div_times_ltO n1 n)
+ [ rewrite > (sym_times (a/b) n1).
+ reflexivity
+ | assumption
+ ]
+ | assumption
+ ]
+ ]
+ | apply (witness n c b).
+ rewrite > (sym_times n b).
+ assumption
+ ]
+ | assumption
+ ]
+| apply (nat_case1 n)
+ [ intros.
+ rewrite > H7 in H6.
+ rewrite > sym_times in H6.
+ simplify in H6.
+ rewrite > H6 in H.
+ apply False_ind.
+ change in H with ((S O) \le O).
+ apply (not_le_Sn_O O H)
+ | intros.
+ apply (lt_O_S m)
+ ]
+]
+qed.
+
+
+
+
+(*6th*)
+theorem sum_divisor_totient1_aux_6: \forall j,n:nat.
+j \lt (pred n) \to (S O) \lt n \to ((pred n)/(gcd (pred n) j))*n+j/(gcd (pred n) j)<n*n.
+intros.
+apply (nat_case1 n)
+[ intros.
+ rewrite > H2 in H.
+ apply False_ind.
+ apply (not_le_Sn_O j H)
+| intros.
+ rewrite < (pred_Sn m).
+ rewrite < (times_n_Sm (S m) m).
+ rewrite > (sym_plus (S m) ((S m) * m)).
+ apply le_to_lt_to_plus_lt
+ [ rewrite > (sym_times (S m) m).
+ apply le_times_l.
+ apply (lt_to_divides_to_div_le)
+ [ apply (nat_case1 m)
+ [ intros.
+ rewrite > H3 in H2.
+ rewrite > H2 in H1.
+ apply False_ind.
+ apply (le_to_not_lt (S O) (S O))
+ [ apply le_n
+ | assumption
+ ]
+ | intros.
+ rewrite > sym_gcd in \vdash (? ? %).
+ apply (lt_O_gcd j (S m1)).
+ apply (lt_O_S m1)
+ ]
+ | apply divides_gcd_n
+ ]
+ | apply (le_to_lt_to_lt (j / (gcd m j)) j (S m))
+ [
+ apply lt_to_divides_to_div_le
+ [ apply (nat_case1 m)
+ [ intros.
+ rewrite > H3 in H2.
+ rewrite > H2 in H1.
+ apply False_ind.
+ apply (le_to_not_lt (S O) (S O))
+ [ apply le_n
+ | assumption
+ ]
+ | intros.
+ rewrite > sym_gcd in \vdash (? ? %).
+ apply (lt_O_gcd j (S m1)).
+ apply (lt_O_S m1)
+ ]
+ | rewrite > sym_gcd in \vdash (? % ?).
+ apply divides_gcd_n
+ ]
+ | rewrite > H2 in H.
+ rewrite < (pred_Sn m) in H.
+ apply (trans_lt j m (S m))
+ [ assumption.
+ | change with ((S m) \le (S m)).
+ apply (le_n (S m))
+ ]
+ ]
+ ]
+]
+qed.
+
+
+
+
+(* The main theorem, adding the hypotesis n > 1 (the cases n= 0
+ and n = 1 are dealed as particular cases in theorem
+ sum_divisor_totiet)
+ *)
+theorem sum_divisor_totient1: \forall n. (S O) \lt n \to sigma_p n (\lambda d.divides_b d (pred n)) totient = (pred n).
+intros.
+unfold totient.
+apply (trans_eq ? ?
+(sigma_p n (\lambda d:nat.divides_b d (pred n))
+(\lambda d:nat.sigma_p n (\lambda m:nat.andb (leb (S m) d) (eqb (gcd m d) (S O))) (\lambda m:nat.S O))))
+ [ apply eq_sigma_p1
+ [ intros.
+ reflexivity
+ | intros.
+ apply sym_eq.
+ apply (trans_eq ? ?
+ (sigma_p x (\lambda m:nat.leb (S m) x\land eqb (gcd m x) (S O)) (\lambda m:nat.S O)))
+ [ apply false_to_eq_sigma_p
+ [ apply lt_to_le.
+ assumption
+ | intros.
+ rewrite > lt_to_leb_false
+ [ reflexivity
+ | apply le_S_S.
+ assumption
+ ]
+ ]
+ | apply eq_sigma_p
+ [ intros.
+ rewrite > le_to_leb_true
+ [ reflexivity
+ | assumption
+ ]
+ | intros.
+ reflexivity
+ ]
+ ]
+ ]
+ | rewrite < (sigma_p2' n n
+ (\lambda d:nat.divides_b d (pred n))
+ (\lambda d,m:nat.leb (S m) d\land eqb (gcd m d) (S O))
+ (\lambda x,y.(S O))).
+ apply (trans_eq ? ? (sigma_p (pred n) (\lambda x.true) (\lambda x.S O)))
+ [ apply (eq_sigma_p_gh
+ (\lambda x:nat. (S O))
+ (\lambda i:nat. (((i \mod n)*(pred n)) / (i / n) ) )
+ (\lambda j:nat. (((pred n)/(gcd (pred n) j))*n + (j / (gcd (pred n) j))) )
+ (n*n)
+ (pred n)
+ (\lambda x:nat.
+ divides_b (x/n) (pred n)
+ \land (leb (S (x \mod n)) (x/n)
+ \land eqb (gcd (x \mod n) (x/n)) (S O)))
+ (\lambda x:nat.true)
+ )
+ [ intros.
+ reflexivity
+ | intros.
+ cut ((i/n) \divides (pred n))
+ [ cut ((i \mod n ) \lt (i/n))
+ [ cut ((gcd (i \mod n) (i / n)) = (S O))
+ [ cut ((gcd (pred n) ((i \mod n)*(pred n)/ (i/n)) = (pred n) / (i/n)))
+ [ rewrite > Hcut3.
+ cut ((i \mod n) * (pred n)/(i/n)/((pred n)/(i/n)) = (i \mod n))
+ [ rewrite > Hcut4.
+ cut ((pred n)/ ((pred n)/(i/n)) = (i/n))
+ [ rewrite > Hcut5.
+ apply sym_eq.
+ apply div_mod.
+ apply (trans_lt O (S O) n)
+ [ apply (lt_O_S O)
+ | assumption
+ ]
+ | elim Hcut.
+ rewrite > H3 in \vdash (? ? (? ? (? % ?)) ?).
+ rewrite > sym_times in \vdash (? ? (? ? (? % ?)) ?).
+ rewrite > (div_times_ltO n2 (i/n))
+ [ rewrite > H3.
+ apply div_times_ltO.
+ apply (divides_to_lt_O n2 (pred n))
+ [ apply (n_gt_Uno_to_O_lt_pred_n n).
+ assumption
+ | apply (witness n2 (pred n) (i/n)).
+ rewrite > sym_times.
+ assumption
+ ]
+ | apply (divides_to_lt_O (i/n) (pred n))
+ [ apply (n_gt_Uno_to_O_lt_pred_n n).
+ assumption
+ | apply (witness (i/n) (pred n) n2).
+ assumption
+ ]
+ ]
+ ]
+ | elim Hcut.
+ cut (( i \mod n * (pred n)/(i/n)) = ( i\mod n * ((pred n)/(i/n))))
+ [ rewrite > Hcut4.
+ rewrite > H3.
+ rewrite < (sym_times n2 (i/n)).
+ rewrite > (div_times_ltO n2 (i/n))
+ [ rewrite > (div_times_ltO (i \mod n) n2)
+ [ reflexivity
+ | apply (divides_to_lt_O n2 (pred n))
+ [ apply (n_gt_Uno_to_O_lt_pred_n n).
+ assumption
+ | apply (witness n2 (pred n) (i/n)).
+ rewrite > sym_times.
+ assumption
+ ]
+ ]
+ | apply (divides_to_lt_O (i/n) (pred n))
+ [ apply (n_gt_Uno_to_O_lt_pred_n n).
+ assumption
+ | assumption
+ ]
+ ]
+ | apply (sym_eq).
+ apply (separazioneFattoriSuDivisione (i \mod n) (pred n) (i/n))
+ [ apply (n_gt_Uno_to_O_lt_pred_n n).
+ assumption
+ | assumption
+ ]
+ ]
+ ]
+ | apply (sum_divisor_totient1_aux2);
+ assumption
+ ]
+ | apply (eqb_true_to_eq (gcd (i \mod n) (i/n)) (S O)).
+ apply (andb_true_true
+ (eqb (gcd (i\mod n) (i/n)) (S O))
+ (leb (S (i\mod n)) (i/n))
+ ).
+ apply (andb_true_true
+ ((eqb (gcd (i\mod n) (i/n)) (S O))
+ \land
+ (leb (S (i\mod n)) (i/n)))
+ (divides_b (i/n) (pred n))
+ ).
+ rewrite > andb_sym.
+ rewrite > andb_sym in \vdash (? ? (? ? %) ?).
+ assumption
+ ]
+ | change with (S (i \mod n) \le (i/n)).
+ cut (leb (S (i \mod n)) (i/n) = true)
+ [ change with (
+ match (true) with
+ [ true \Rightarrow (S (i \mod n)) \leq (i/n)
+ | false \Rightarrow (S (i \mod n)) \nleq (i/n)]
+ ).
+ rewrite < Hcut1.
+ apply (leb_to_Prop (S(i \mod n)) (i/n))
+ | apply (andb_true_true (leb (S(i\mod n)) (i/n)) (divides_b (i/n) (pred n)) ).
+ apply (andb_true_true ((leb (S(i\mod n)) (i/n)) \land (divides_b (i/n) (pred n)))
+ (eqb (gcd (i\mod n) (i/n)) (S O))
+ ).
+ rewrite > andb_sym in \vdash (? ? (? % ?) ?).
+ rewrite < (andb_assoc) in \vdash (? ? % ?).
+ assumption
+ ]
+ ]
+ | apply (divides_b_true_to_divides ).
+ apply (andb_true_true (divides_b (i/n) (pred n))
+ (leb (S (i\mod n)) (i/n))).
+ apply (andb_true_true ( (divides_b (i/n) (pred n)) \land (leb (S (i\mod n)) (i/n)) )
+ (eqb (gcd (i\mod n) (i/n)) (S O))
+ ).
+ rewrite < andb_assoc.
+ assumption.
+ ]
+ | intros.
+ apply (sum_divisor_totient1_aux_3);
+ assumption.
+ | intros.
+ apply (sum_divisor_totient1_aux_4);
+ assumption.
+ | intros.
+ cut (j/(gcd (pred n) j) \lt n)
+ [ rewrite > (div_plus_times n (pred n/gcd (pred n) j) (j/gcd (pred n) j))
+ [ rewrite > (mod_plus_times n (pred n/gcd (pred n) j) (j/gcd (pred n) j))
+ [ apply (sum_divisor_totient1_aux5 j (gcd (pred n) j) (pred n))
+ [ apply (n_gt_Uno_to_O_lt_pred_n n).
+ assumption
+ | rewrite > sym_gcd.
+ apply lt_O_gcd.
+ apply (n_gt_Uno_to_O_lt_pred_n n).
+ assumption
+ | assumption
+ | apply divides_gcd_m
+ | rewrite > sym_gcd.
+ apply divides_gcd_m
+ ]
+ | assumption
+ ]
+ | assumption
+ ]
+ | apply (le_to_lt_to_lt (j/gcd (pred n) j) j n)
+ [ apply (lt_to_divides_to_div_le)
+ [ rewrite > sym_gcd.
+ apply lt_O_gcd.
+ apply (n_gt_Uno_to_O_lt_pred_n n).
+ assumption
+ | apply divides_gcd_m
+ ]
+ | apply (lt_to_le_to_lt j (pred n) n)
+ [ assumption
+ | apply le_pred_n
+ ]
+ ]
+ ]
+ | intros.
+ apply (sum_divisor_totient1_aux_6);
+ assumption.
+ ]
+ | apply (sigma_p_true).
+ ]
+ ]
+qed.
+
+
+(*there's a little difference between the following definition of the
+ theorem, and the abstract definition given before.
+ in fact (sigma_p n f p) works on (pred n), and not on n, as first element.
+ that's why in the definition of the theorem the summary is set equal to
+ (pred n).
+ *)
+theorem sum_divisor_totient: \forall n.
+sigma_p n (\lambda d.divides_b d (pred n)) totient = (pred n).
+intros.
+apply (nat_case1 n)
+[ intros.
+ simplify.
+ reflexivity
+| intros.
+ apply (nat_case1 m)
+ [ intros.
+ simplify.
+ reflexivity
+ | intros.
+ rewrite < H1.
+ rewrite < H.
+ rewrite > (pred_Sn m).
+ rewrite < H.
+ apply( sum_divisor_totient1).
+ rewrite > H.
+ rewrite > H1.
+ apply cic:/matita/algebra/finite_groups/lt_S_S.con.
+ apply lt_O_S
+ ]
+]
+qed.
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
projects / helm.git / commitdiff