(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/nat/factorization".
-
include "nat/ord.ma".
-include "nat/gcd.ma".
-include "nat/nth_prime.ma".
(* the following factorization algorithm looks for the largest prime
factor. *)
definition max_prime_factor \def \lambda n:nat.
(max n (\lambda p:nat.eqb (n \mod (nth_prime p)) O)).
+theorem lt_SO_max_prime: \forall m. S O < m \to
+S O < max m (λi:nat.primeb i∧divides_b i m).
+intros.
+apply (lt_to_le_to_lt ? (smallest_factor m))
+ [apply lt_SO_smallest_factor.assumption
+ |apply f_m_to_le_max
+ [apply le_smallest_factor_n
+ |apply true_to_true_to_andb_true
+ [apply prime_to_primeb_true.
+ apply prime_smallest_factor_n.
+ assumption
+ |apply divides_to_divides_b_true
+ [apply lt_O_smallest_factor.apply lt_to_le.assumption
+ |apply divides_smallest_factor_n.
+ apply lt_to_le.assumption
+ ]
+ ]
+ ]
+ ]
+qed.
(* max_prime_factor is indeed a factor *)
theorem divides_max_prime_factor_n:
\forall n:nat. (S O) < n
\to nth_prime (max_prime_factor n) \divides n.
-intros; apply divides_b_true_to_divides;
-[ apply lt_O_nth_prime_n;
-| apply (f_max_true (\lambda p:nat.eqb (n \mod (nth_prime p)) O) n);
- cut (\exists i. nth_prime i = smallest_factor n);
+intros.
+apply divides_b_true_to_divides.
+apply (f_max_true (\lambda p:nat.eqb (n \mod (nth_prime p)) O) n);
+cut (\exists i. nth_prime i = smallest_factor n);
[ elim Hcut.
apply (ex_intro nat ? a);
split;
| rewrite > H1;
apply le_smallest_factor_n; ]
| rewrite > H1;
- (*CSC: simplify here does something nasty! *)
change with (divides_b (smallest_factor n) n = true);
apply divides_to_divides_b_true;
[ apply (trans_lt ? (S O));
[ unfold lt; apply le_n;
| apply lt_SO_smallest_factor; assumption; ]
- | letin x \def le.auto.
- (*
- apply divides_smallest_factor_n;
- apply (trans_lt ? (S O));
- [ unfold lt; apply le_n;
- | assumption; ] *) ] ]
- | letin x \def prime. auto.
+ | apply divides_smallest_factor_n;
+ autobatch; ] ]
+ | apply prime_to_nth_prime;
+ autobatch.
(*
apply prime_to_nth_prime;
apply prime_smallest_factor_n;
- assumption; *) ] ]
+ assumption; *) ]
+qed.
+
+lemma divides_to_prime_divides : \forall n,m.1 < m \to m < n \to m \divides n \to
+ \exists p.p \leq m \land prime p \land p \divides n.
+intros;apply (ex_intro ? ? (nth_prime (max_prime_factor m)));split
+ [split
+ [apply divides_to_le
+ [apply lt_to_le;assumption
+ |apply divides_max_prime_factor_n;assumption]
+ |apply prime_nth_prime;]
+ |apply (transitive_divides ? ? ? ? H2);apply divides_max_prime_factor_n;
+ assumption]
qed.
theorem divides_to_max_prime_factor : \forall n,m. (S O) < n \to O < m \to n \divides m \to
cut (prime (nth_prime (max_prime_factor n))).
apply lt_O_nth_prime_n.apply prime_nth_prime.
cut (nth_prime (max_prime_factor n) \divides n).
-auto.
-auto.
+autobatch.
+autobatch.
(*
[ apply (transitive_divides ? n);
[ apply divides_max_prime_factor_n.
*)
qed.
+theorem divides_to_max_prime_factor1 : \forall n,m. O < n \to O < m \to n \divides m \to
+max_prime_factor n \le max_prime_factor m.
+intros 3.
+elim (le_to_or_lt_eq ? ? H)
+ [apply divides_to_max_prime_factor
+ [assumption|assumption|assumption]
+ |rewrite < H1.
+ simplify.apply le_O_n.
+ ]
+qed.
+
+theorem max_prime_factor_to_not_p_ord_O : \forall n,p,r.
+ (S O) < n \to
+ p = max_prime_factor n \to
+ p_ord n (nth_prime p) \neq pair nat nat O r.
+intros.unfold Not.intro.
+apply (p_ord_O_to_not_divides ? ? ? ? H2)
+ [apply (trans_lt ? (S O))[apply lt_O_S|assumption]
+ |rewrite > H1.
+ apply divides_max_prime_factor_n.
+ assumption
+ ]
+qed.
+
theorem p_ord_to_lt_max_prime_factor: \forall n,p,q,r. O < n \to
p = max_prime_factor n \to
(pair nat nat q r) = p_ord n (nth_prime p) \to
assumption.unfold Not.
intro.
cut (r \mod (nth_prime (max_prime_factor n)) \neq O);
- [unfold Not in Hcut1.auto.
+ [ apply Hcut1; autobatch depth=2;
(*
apply Hcut1.apply divides_to_mod_O;
[ apply lt_O_nth_prime_n.
| assumption.
]
*)
- |letin z \def le.
- cut(pair nat nat q r=p_ord_aux n n (nth_prime (max_prime_factor n)));
- [2: rewrite < H1.assumption.|letin x \def le.auto width = 4]
- (* CERCA COME MAI le_n non lo applica se lo trova come Const e non Rel *)
- ].
-(*
- apply (p_ord_aux_to_not_mod_O n n ? q r);
+ | unfold p_ord in H2; lapply depth=0 le_n; autobatch width = 4 depth = 2;
+ (*apply (p_ord_aux_to_not_mod_O n n ? q r);
[ apply lt_SO_nth_prime_n.
| assumption.
| apply le_n.
| rewrite < H1.assumption.
- ]
+ ]*)
].
-*)
-cut (n=r*(nth_prime p)\sup(q));
- [letin www \def le.letin www1 \def divides.
- auto.
-(*
+
apply (le_to_or_lt_eq (max_prime_factor r) (max_prime_factor n)).
apply divides_to_max_prime_factor.
assumption.assumption.
apply (witness r n ((nth_prime p) \sup q)).
-*)
- |
rewrite < sym_times.
apply (p_ord_aux_to_exp n n ? q r).
apply lt_O_nth_prime_n.assumption.
-]
qed.
theorem p_ord_to_lt_max_prime_factor1: \forall n,p,q,r. O < n \to
apply (le_to_or_lt_eq ? p H1).
qed.
+lemma lt_max_prime_factor_to_not_divides: \forall n,p:nat.
+O < n \to n=S O \lor max_prime_factor n < p \to
+(nth_prime p \ndivides n).
+intros.unfold Not.intro.
+elim H1
+ [rewrite > H3 in H2.
+ apply (le_to_not_lt (nth_prime p) (S O))
+ [apply divides_to_le[apply le_n|assumption]
+ |apply lt_SO_nth_prime_n
+ ]
+ |apply (not_le_Sn_n p).
+ change with (p < p).
+ apply (le_to_lt_to_lt ? ? ? ? H3).
+ unfold max_prime_factor.
+ apply f_m_to_le_max
+ [apply (trans_le ? (nth_prime p))
+ [apply lt_to_le.
+ apply lt_n_nth_prime_n
+ |apply divides_to_le;assumption
+ ]
+ |apply eq_to_eqb_true.
+ apply divides_to_mod_O
+ [apply lt_O_nth_prime_n|assumption]
+ ]
+ ]
+qed.
+
(* datatypes and functions *)
inductive nat_fact : Set \def
intro.
apply (nat_case n).reflexivity.
intro.apply (nat_case m).reflexivity.
-intro.(*CSC: simplify here does something really nasty *)
+intro.
change with
(let p \def (max (S(S m1)) (\lambda p:nat.eqb ((S(S m1)) \mod (nth_prime p)) O)) in
defactorize (match p_ord (S(S m1)) (nth_prime p) with
cut ((S(S m1)) = (nth_prime p) \sup q *r).
cut (O<r).
rewrite > defactorize_aux_factorize_aux.
-(*CSC: simplify here does something really nasty *)
change with (r*(nth_prime p) \sup (S (pred q)) = (S(S m1))).
cut ((S (pred q)) = q).
rewrite > Hcut2.
unfold lt.apply le_S_S.apply le_S_S. apply le_O_n.
cut ((S(S m1)) = r).
rewrite > Hcut3 in \vdash (? (? ? %)).
-(*CSC: simplify here does something really nasty *)
change with (nth_prime p \divides r \to False).
intro.
apply (p_ord_aux_to_not_mod_O (S(S m1)) (S(S m1)) (nth_prime p) q r).
rewrite > Hcut.rewrite < H1.rewrite < times_n_O.reflexivity.
apply le_to_or_lt_eq.apply le_O_n.
(* prova del cut *)
-goal 20.
apply (p_ord_aux_to_exp (S(S m1))).
apply lt_O_nth_prime_n.
assumption.
reflexivity.
qed.
-theorem divides_exp_to_divides:
-\forall p,n,m:nat. prime p \to
-p \divides n \sup m \to p \divides n.
-intros 3.elim m.simplify in H1.
-apply (transitive_divides p (S O)).assumption.
-apply divides_SO_n.
-cut (p \divides n \lor p \divides n \sup n1).
-elim Hcut.assumption.
-apply H.assumption.assumption.
-apply divides_times_to_divides.assumption.
-exact H2.
-qed.
-
-theorem divides_exp_to_eq:
-\forall p,q,m:nat. prime p \to prime q \to
-p \divides q \sup m \to p = q.
+lemma eq_p_max: \forall n,p,r:nat. O < n \to
+O < r \to
+r = (S O) \lor (max r (\lambda p:nat.eqb (r \mod (nth_prime p)) O)) < p \to
+p = max_prime_factor (r*(nth_prime p)\sup n).
intros.
-unfold prime in H1.
-elim H1.apply H4.
-apply (divides_exp_to_divides p q m).
-assumption.assumption.
-unfold prime in H.elim H.assumption.
+apply sym_eq.
+unfold max_prime_factor.
+apply max_spec_to_max.
+split
+ [split
+ [rewrite > times_n_SO in \vdash (? % ?).
+ rewrite > sym_times.
+ apply le_times
+ [assumption
+ |apply lt_to_le.
+ apply (lt_to_le_to_lt ? (nth_prime p))
+ [apply lt_n_nth_prime_n
+ |rewrite > exp_n_SO in \vdash (? % ?).
+ apply le_exp
+ [apply lt_O_nth_prime_n
+ |assumption
+ ]
+ ]
+ ]
+ |apply eq_to_eqb_true.
+ apply divides_to_mod_O
+ [apply lt_O_nth_prime_n
+ |apply (lt_O_n_elim ? H).
+ intro.
+ apply (witness ? ? ((r*(nth_prime p) \sup m))).
+ rewrite < assoc_times.
+ rewrite < sym_times in \vdash (? ? ? (? % ?)).
+ rewrite > exp_n_SO in \vdash (? ? ? (? (? ? %) ?)).
+ rewrite > assoc_times.
+ rewrite < exp_plus_times.
+ reflexivity
+ ]
+ ]
+ |intros.
+ apply not_eq_to_eqb_false.
+ unfold Not.intro.
+ lapply (mod_O_to_divides ? ? ? H5)
+ [apply lt_O_nth_prime_n
+ |cut (Not (divides (nth_prime i) ((nth_prime p)\sup n)))
+ [elim H2
+ [rewrite > H6 in Hletin.
+ simplify in Hletin.
+ rewrite < plus_n_O in Hletin.
+ apply Hcut.assumption
+ |elim (divides_times_to_divides ? ? ? ? Hletin)
+ [apply (lt_to_not_le ? ? H3).
+ apply lt_to_le.
+ apply (le_to_lt_to_lt ? ? ? ? H6).
+ apply f_m_to_le_max
+ [apply (trans_le ? (nth_prime i))
+ [apply lt_to_le.
+ apply lt_n_nth_prime_n
+ |apply divides_to_le[assumption|assumption]
+ ]
+ |apply eq_to_eqb_true.
+ apply divides_to_mod_O
+ [apply lt_O_nth_prime_n|assumption]
+ ]
+ |apply prime_nth_prime
+ |apply Hcut.assumption
+ ]
+ ]
+ |unfold Not.intro.
+ apply (lt_to_not_eq ? ? H3).
+ apply sym_eq.
+ elim (prime_nth_prime p).
+ apply injective_nth_prime.
+ apply H8
+ [apply (divides_exp_to_divides ? ? ? ? H6).
+ apply prime_nth_prime.
+ |apply lt_SO_nth_prime_n
+ ]
+ ]
+ ]
+ ]
qed.
theorem not_divides_defactorize_aux: \forall f:nat_fact. \forall i,j:nat.
defactorize_aux f i = defactorize_aux g i \to f = g.
intro.
elim f.
-generalize in match H.
-elim g.
+elim g in H ⊢ %.
apply eq_f.
apply inj_S. apply (inj_exp_r (nth_prime i)).
apply lt_SO_nth_prime_n.
assumption.
apply False_ind.
-apply (not_eq_nf_last_nf_cons n2 n n1 i H2).
-generalize in match H1.
-elim g.
+apply (not_eq_nf_last_nf_cons n2 n n1 i H1).
+elim g in H1 ⊢ %.
apply False_ind.
apply (not_eq_nf_last_nf_cons n1 n2 n i).
apply sym_eq. assumption.
-simplify in H3.
-generalize in match H3.
+simplify in H2.
+generalize in match H2.
apply (nat_elim2 (\lambda n,n2.
((nth_prime i) \sup n)*(defactorize_aux n1 (S i)) =
((nth_prime i) \sup n2)*(defactorize_aux n3 (S i)) \to
[ (nf_last m) \Rightarrow m
| (nf_cons m g) \Rightarrow m ] = m).
rewrite > Hcut.simplify.reflexivity.
-apply H4.simplify in H5.
+apply H3.simplify in H4.
apply (inj_times_r1 (nth_prime i)).
apply lt_O_nth_prime_n.
rewrite < assoc_times.rewrite < assoc_times.assumption.
unfold injective.
change with (\forall f,g.defactorize f = defactorize g \to f=g).
intro.elim f.
-generalize in match H.elim g.
+elim g in H ⊢ %.
(* zero - zero *)
reflexivity.
(* zero - one *)
simplify in H1.
apply False_ind.
-apply (not_eq_O_S O H1).
+apply (not_eq_O_S O H).
(* zero - proper *)
simplify in H1.
apply False_ind.
apply (not_le_Sn_n O).
-rewrite > H1 in \vdash (? ? %).
+rewrite > H in \vdash (? ? %).
change with (O < defactorize_aux n O).
apply lt_O_defactorize_aux.
-generalize in match H.
-elim g.
+elim g in H ⊢ %.
(* one - zero *)
simplify in H1.
apply False_ind.
simplify in H1.
apply False_ind.
apply (not_le_Sn_n (S O)).
-rewrite > H1 in \vdash (? ? %).
+rewrite > H in \vdash (? ? %).
change with ((S O) < defactorize_aux n O).
apply lt_SO_defactorize_aux.
-generalize in match H.elim g.
+elim g in H ⊢ %.
(* proper - zero *)
simplify in H1.
apply False_ind.
apply (not_le_Sn_n O).
-rewrite < H1 in \vdash (? ? %).
+rewrite < H in \vdash (? ? %).
change with (O < defactorize_aux n O).
apply lt_O_defactorize_aux.
(* proper - one *)
simplify in H1.
apply False_ind.
apply (not_le_Sn_n (S O)).
-rewrite < H1 in \vdash (? ? %).
+rewrite < H in \vdash (? ? %).
change with ((S O) < defactorize_aux n O).
apply lt_SO_defactorize_aux.
(* proper - proper *)
apply eq_f.
apply (injective_defactorize_aux O).
-exact H1.
+exact H.
qed.
theorem factorize_defactorize:
-\forall f,g: nat_fact_all. factorize (defactorize f) = f.
+\forall f: nat_fact_all. factorize (defactorize f) = f.
intros.
apply injective_defactorize.
apply defactorize_factorize.
projects / helm.git / blobdiff