set "baseuri" "cic:/matita/nat/euler_theorem".
-include "nat/iteration.ma".
+include "nat/map_iter_p.ma".
include "nat/totient.ma".
-(* da spostare *)
-lemma le_to_le_to_eq: \forall n,m. n \le m \to m \le n \to n = m.
-apply nat_elim2
- [intros.apply le_n_O_to_eq.assumption
- |intros.apply sym_eq.apply le_n_O_to_eq.assumption
- |intros.apply eq_f.apply H
- [apply le_S_S_to_le.assumption
- |apply le_S_S_to_le.assumption
- ]
- ]
-qed.
-
-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 )
+
lemma totient_card: \forall n.
totient n = card n (\lambda i.eqb (gcd i n) (S O)).
intro.apply (nat_case n)
]
]
qed.
+*)
-(* da spostare *)
-lemma 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
+(*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
]
-qed.
-
-(* da spostare *)
-lemma 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
+| 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
]
- |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
+ | 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
]
- |assumption
- ]
]
]
+]
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).
+
+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.
+ [rewrite > pi_p_S.
cut (eqb (gcd (S O) n) (S O) = true)
[rewrite > Hcut.
- change with ((gcd n (S O)) = (S O)).auto
- |apply eq_to_eqb_true.auto
+ 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.
+ |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)).
+ ((gcd n ((S n1)*(pi_p (\lambda i.eqb (gcd i n) (S O)) n1))) = (S O)).
apply eq_gcd_times_SO
[unfold.apply le_S.assumption
- |apply lt_O_Pi_P.
+ |apply lt_O_pi_p.
|rewrite > sym_gcd. assumption.
|apply H2.
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)).
+ (gcd n (pi_p (\lambda i.eqb (gcd i n) (S O)) n1) = (S O)).
apply H2.
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.
+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))
+(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
- [rewrite > map_iter_P_O.
+ [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
+ rewrite > map_iter_p_S_true
+ [rewrite > map_iter_p_S_true
[apply congruent_times
[assumption
|apply congruent_n_mod_n.assumption
|apply eq_to_eqb_true.assumption
]
|intro.
- rewrite > map_iter_P_S_false
- [rewrite > map_iter_P_S_false
+ rewrite > map_iter_p_S_false
+ [rewrite > map_iter_p_S_false
[assumption
|apply not_eq_to_eqb_false.assumption
]
]
qed.
-theorem lt_S_to_lt: \forall n,m. S n < m \to n < m.
-intros.
-apply (trans_lt ? (S n))
- [apply le_n|assumption]
-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 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.
|apply mod_O_to_divides
[assumption
|rewrite > distr_times_minus.
- auto
+ 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).
+ ]
+ ]
]
]
]
- |auto
+ | apply (le_minus_m j i).
]
]
|intro.assumption
|apply mod_O_to_divides
[assumption
|rewrite > distr_times_minus.
- auto
+ 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).
+ ]
+ ]
]
]
]
- |auto
+ | 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))
+ |apply (gcd_SO_to_divides_times_to_divides (pi_p (\lambda i.eqb (gcd i n) (S O)) n))
[apply (trans_lt ? (S O)).apply lt_O_S. assumption
- |apply gcd_Pi_P
+ |apply gcd_pi_p
[apply (trans_lt ? (S O)).apply lt_O_S. assumption
|apply le_n
]
rewrite > (sym_times (S O)).
rewrite < times_n_SO.
rewrite > totient_card.
- rewrite > a_times_Pi_P.
+ rewrite > a_times_pi_p.
apply congruent_to_divides
[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))
- [apply (congruent_map_iter_P_times ? n n).
+ (map_iter_p n (\lambda i.eqb (gcd i n) (S O)) (\lambda x.a*x \mod n) (S O) times))
+ [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))
+ |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
[assumption|apply sym_eq.assumption]
]
]
- ]
-qed.
-
\ No newline at end of file
+ ]
+qed.
projects / helm.git / blobdiff