+++ /dev/null
-(**************************************************************************)
-(* __ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| A.Asperti, C.Sacerdoti Coen, *)
-(* ||A|| E.Tassi, S.Zacchiroli *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU Lesser General Public License Version 2.1 *)
-(* *)
-(**************************************************************************)
-
-set "baseuri" "cic:/matita/library_autobatch/nat/euler_theorem".
-
-include "auto/nat/map_iter_p.ma".
-include "auto/nat/totient.ma".
-
-(* 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)).
-intro.
-apply (nat_case n)
-[ reflexivity
-| intro.
- apply (nat_case m)
- [ reflexivity
- | intro.
- apply count_card1;autobatch
- (*[ reflexivity
- | autobatch.rewrite > gcd_n_n.
- reflexivity
- ]*)
- ]
-]
-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.
- autobatch
- (*change with ((gcd n (S O)) = (S O)).
- autobatch*)
- | autobatch
- (*apply eq_to_eqb_true.autobatch*)
- ]
-| rewrite > pi_p_S.
- apply eqb_elim
- [ intro.
- change with
- ((gcd n ((S n1)*(pi_p (\lambda i.eqb (gcd i n) (S O)) n1))) = (S O)).
- apply eq_gcd_times_SO
- [ autobatch
- (*unfold.
- apply le_S.
- assumption*)
- | apply lt_O_pi_p.
- | autobatch
- (*rewrite > sym_gcd.
- assumption.*)
- | apply H2.
- autobatch
- (*apply (trans_le ? (S n1))
- [ apply le_n_Sn
- | assumption
- ]*)
- ]
- | intro.
- change with
- (gcd n (pi_p (\lambda i.eqb (gcd i n) (S O)) n1) = (S O)).
- apply H2.
- autobatch
- (*apply (trans_le ? (S n1))
- [ apply le_n_Sn
- | assumption
- ]*)
- ]
-]
-qed.
-
-theorem congruent_map_iter_p_times:\forall f:nat \to nat. \forall a,n:nat.
-O < a \to
-congruent
-(map_iter_p n (\lambda i.eqb (gcd i a) (S O)) (\lambda x.f x) (S O) times)
-(map_iter_p n (\lambda i.eqb (gcd i a) (S O))
- (\lambda x.f x \mod a) (S O) times) a.
-intros.
-elim n
-[ autobatch
- (*rewrite > map_iter_p_O.
- apply (congruent_n_n ? a)*)
-| apply (eqb_elim (gcd (S n1) a) (S O))
- [ intro.
- rewrite > map_iter_p_S_true
- [ rewrite > map_iter_p_S_true
- [ apply congruent_times
- [ assumption
- | autobatch
- (*apply congruent_n_mod_n.
- assumption*)
- | (*NB qui autobatch non chiude il goal*)
- assumption
- ]
- | autobatch
- (*apply eq_to_eqb_true.
- assumption*)
- ]
- | autobatch
- (*apply eq_to_eqb_true.
- assumption*)
- ]
- | intro.
- rewrite > map_iter_p_S_false
- [ rewrite > map_iter_p_S_false
- [ (*BN qui autobatch non chiude il goal*)
- assumption
- | autobatch
- (*apply not_eq_to_eqb_false.
- assumption*)
- ]
- | autobatch
- (*apply not_eq_to_eqb_false.
- assumption*)
- ]
- ]
-]
-qed.
-
-theorem permut_p_mod: \forall a,n. S O < n \to O < a \to gcd a n = (S O) \to
-permut_p (\lambda x:nat.a*x \mod n) (\lambda i:nat.eqb (gcd i n) (S O)) n.
-intros.
-lapply (lt_S_to_lt ? ? H) as H3.
-unfold permut_p.
-simplify.
-intros.
-split
-[ split
- [ autobatch
- (*apply lt_to_le.
- apply lt_mod_m_m.
- assumption*)
- | rewrite > sym_gcd.
- rewrite > gcd_mod
- [ apply eq_to_eqb_true.
- rewrite > sym_gcd.
- apply eq_gcd_times_SO
- [ assumption
- | apply (gcd_SO_to_lt_O i n H).
- autobatch
- (*apply eqb_true_to_eq.
- assumption*)
- | autobatch
- (*rewrite > sym_gcd.
- assumption*)
- | autobatch
- (*rewrite > sym_gcd.
- apply eqb_true_to_eq.
- assumption*)
- ]
- | assumption
- ]
- ]
-| intros.
- lapply (gcd_SO_to_lt_n ? ? H H4 (eqb_true_to_eq ? ? H5)) as H9.
- lapply (gcd_SO_to_lt_n ? ? H H7 (eqb_true_to_eq ? ? H6)) as H10.
- lapply (gcd_SO_to_lt_O ? ? H (eqb_true_to_eq ? ? H5)) as H11.
- lapply (gcd_SO_to_lt_O ? ? H (eqb_true_to_eq ? ? H6)) as H12.
- unfold Not.
- intro.
- apply H8.
- apply (nat_compare_elim i j)
- [ intro.
- absurd (j < n)
- [ assumption
- | apply le_to_not_lt.
- apply (trans_le ? (j -i))
- [ apply divides_to_le
- [(*fattorizzare*)
- unfold lt.autobatch.
- (*apply (lt_plus_to_lt_l i).
- simplify.
- rewrite < (plus_minus_m_m)
- [ assumption
- | apply lt_to_le.
- assumption
- ]*)
- | apply (gcd_SO_to_divides_times_to_divides a)
- [ assumption
- | autobatch
- (*rewrite > sym_gcd.
- assumption*)
- | apply mod_O_to_divides
- [ assumption
- | rewrite > distr_times_minus.
- autobatch
- ]
- ]
- ]
- | autobatch
- ]
- ]
- | autobatch
- (*intro.
- assumption*)
- | intro.
- absurd (i < n)
- [ assumption
- | apply le_to_not_lt.
- apply (trans_le ? (i -j))
- [ apply divides_to_le
- [(*fattorizzare*)
- unfold lt.autobatch.
- (*apply (lt_plus_to_lt_l j).
- simplify.
- rewrite < (plus_minus_m_m)
- [ assumption
- | apply lt_to_le.
- assumption
- ]*)
- | apply (gcd_SO_to_divides_times_to_divides a)
- [ assumption
- | autobatch
- (*rewrite > sym_gcd.
- assumption*)
- | apply mod_O_to_divides
- [ assumption
- | rewrite > distr_times_minus.
- autobatch
- ]
- ]
- ]
- | autobatch
- ]
- ]
- ]
-]
-qed.
-
-theorem congruent_exp_totient_SO: \forall n,a:nat. (S O) < n \to
-gcd a n = (S O) \to congruent (exp a (totient n)) (S O) n.
-intros.
-cut (O < a)
-[ apply divides_to_congruent
- [ autobatch
- (*apply (trans_lt ? (S O)).
- apply lt_O_S.
- assumption*)
- | autobatch
- (*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))
- [ autobatch
- (*apply (trans_lt ? (S O)).
- apply lt_O_S.
- assumption*)
- | autobatch
- (*apply gcd_pi_p
- [ apply (trans_lt ? (S O)).
- apply lt_O_S.
- assumption
- | apply le_n
- ]*)
- | rewrite < sym_times.
- rewrite > times_minus_l.
- rewrite > (sym_times (S O)).
- rewrite < times_n_SO.
- rewrite > totient_card.
- rewrite > a_times_pi_p.
- apply congruent_to_divides
- [ autobatch
- (*apply (trans_lt ? (S O)).
- apply lt_O_S.
- assumption*)
- | apply (transitive_congruent n ?
- (map_iter_p n (\lambda i.eqb (gcd i n) (S O)) (\lambda x.a*x \mod n) (S O) times))
- [ autobatch
- (*apply (congruent_map_iter_p_times ? n n).
- apply (trans_lt ? (S O))
- [ apply lt_O_S
- | assumption
- ]*)
- | unfold pi_p.
- cut ( (map_iter_p n (\lambda i:nat.eqb (gcd i n) (S O)) (\lambda n:nat.n) (S O) times)
- = (map_iter_p n (\lambda i:nat.eqb (gcd i n) (S O)) (\lambda x:nat.a*x\mod n) (S O) times))
- [ rewrite < Hcut1.
- apply congruent_n_n
- | apply (eq_map_iter_p_permut ? ? ? ? ? (λm.m))
- [ apply assoc_times
- | apply sym_times
- | apply (permut_p_mod ? ? H Hcut H1)
- | simplify.
- apply not_eq_to_eqb_false.
- unfold.
- intro.
- autobatch
- (*apply (lt_to_not_eq (S O) n)
- [ assumption
- | apply sym_eq.
- assumption
- ]*)
- ]
- ]
- ]
- ]
- ]
- ]
-| elim (le_to_or_lt_eq O a (le_O_n a));autobatch
- (*[ assumption
- | autobatch.absurd (gcd a n = S O)
- [ assumption
- | rewrite < H2.
- simplify.
- unfold.intro.
- apply (lt_to_not_eq (S O) n)
- [ assumption
- | apply sym_eq.
- assumption
- ]
- ]
- ]*)
-]
-qed.
-
\ No newline at end of file
projects / helm.git / blobdiff