X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2Fnat%2Fprimes.ma;h=50b7d1221bfdca8211184a664add8c73aa392bd5;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=500c8117f70355c181e55924eaa3befbecd23279;hpb=86eaff4471bdce9f632838d3a0b18d082015c2db;p=helm.git diff --git a/helm/matita/library/nat/primes.ma b/helm/matita/library/nat/primes.ma index 500c8117f..50b7d1221 100644 --- a/helm/matita/library/nat/primes.ma +++ b/helm/matita/library/nat/primes.ma @@ -22,218 +22,313 @@ include "nat/factorial.ma". inductive divides (n,m:nat) : Prop \def witness : \forall p:nat.m = times n p \to divides n m. +interpretation "divides" 'divides n m = (cic:/matita/nat/primes/divides.ind#xpointer(1/1) n m). +interpretation "not divides" 'ndivides n m = + (cic:/matita/logic/connectives/Not.con (cic:/matita/nat/primes/divides.ind#xpointer(1/1) n m)). + theorem reflexive_divides : reflexive nat divides. -simplify. +unfold reflexive. intros. -exact witness x x (S O) (times_n_SO x). +exact (witness x x (S O) (times_n_SO x)). qed. theorem divides_to_div_mod_spec : -\forall n,m. O < n \to divides n m \to div_mod_spec m n (div m n) O. +\forall n,m. O < n \to n \divides m \to div_mod_spec m n (m / n) O. intros.elim H1.rewrite > H2. constructor 1.assumption. -apply lt_O_n_elim n H.intros. +apply (lt_O_n_elim n H).intros. rewrite < plus_n_O. rewrite > div_times.apply sym_times. qed. -theorem div_mod_spec_to_div : -\forall n,m,p. div_mod_spec m n p O \to divides n m. +theorem div_mod_spec_to_divides : +\forall n,m,p. div_mod_spec m n p O \to n \divides m. intros.elim H. -apply witness n m p. +apply (witness n m p). rewrite < sym_times. -rewrite > plus_n_O (p*n).assumption. +rewrite > (plus_n_O (p*n)).assumption. qed. theorem divides_to_mod_O: -\forall n,m. O < n \to divides n m \to (mod m n) = O. -intros.apply div_mod_spec_to_eq2 m n (div m n) (mod m n) (div m n) O. +\forall n,m. O < n \to n \divides m \to (m \mod n) = O. +intros.apply (div_mod_spec_to_eq2 m n (m / n) (m \mod n) (m / n) O). apply div_mod_spec_div_mod.assumption. apply divides_to_div_mod_spec.assumption.assumption. qed. theorem mod_O_to_divides: -\forall n,m. O< n \to (mod m n) = O \to divides n m. +\forall n,m. O< n \to (m \mod n) = O \to n \divides m. intros. -apply witness n m (div m n). -rewrite > plus_n_O (n*div m n). +apply (witness n m (m / n)). +rewrite > (plus_n_O (n * (m / n))). rewrite < H1. rewrite < sym_times. -(* perche' hint non lo trova ?*) +(* Andrea: perche' hint non lo trova ?*) apply div_mod. assumption. qed. -theorem divides_n_O: \forall n:nat. divides n O. -intro. apply witness n O O.apply times_n_O. +theorem divides_n_O: \forall n:nat. n \divides O. +intro. apply (witness n O O).apply times_n_O. qed. -theorem divides_SO_n: \forall n:nat. divides (S O) n. -intro. apply witness (S O) n n. simplify.apply plus_n_O. +theorem divides_n_n: \forall n:nat. n \divides n. +intro. apply (witness n n (S O)).apply times_n_SO. +qed. + +theorem divides_SO_n: \forall n:nat. (S O) \divides n. +intro. apply (witness (S O) n n). simplify.apply plus_n_O. qed. theorem divides_plus: \forall n,p,q:nat. -divides n p \to divides n q \to divides n (p+q). +n \divides p \to n \divides q \to n \divides p+q. intros. -elim H.elim H1. apply witness n (p+q) (n2+n1). +elim H.elim H1. apply (witness n (p+q) (n2+n1)). rewrite > H2.rewrite > H3.apply sym_eq.apply distr_times_plus. qed. theorem divides_minus: \forall n,p,q:nat. divides n p \to divides n q \to divides n (p-q). intros. -elim H.elim H1. apply witness n (p-q) (n2-n1). +elim H.elim H1. apply (witness n (p-q) (n2-n1)). rewrite > H2.rewrite > H3.apply sym_eq.apply distr_times_minus. qed. theorem divides_times: \forall n,m,p,q:nat. -divides n p \to divides m q \to divides (n*m) (p*q). +n \divides p \to m \divides q \to n*m \divides p*q. intros. -elim H.elim H1. apply witness (n*m) (p*q) (n2*n1). +elim H.elim H1. apply (witness (n*m) (p*q) (n2*n1)). rewrite > H2.rewrite > H3. -apply trans_eq nat ? (n*(m*(n2*n1))). -apply trans_eq nat ? (n*(n2*(m*n1))). +apply (trans_eq nat ? (n*(m*(n2*n1)))). +apply (trans_eq nat ? (n*(n2*(m*n1)))). apply assoc_times. apply eq_f. -apply trans_eq nat ? ((n2*m)*n1). +apply (trans_eq nat ? ((n2*m)*n1)). apply sym_eq. apply assoc_times. -rewrite > sym_times n2 m.apply assoc_times. +rewrite > (sym_times n2 m).apply assoc_times. apply sym_eq. apply assoc_times. qed. -theorem transitive_divides: \forall n,m,p. -divides n m \to divides m p \to divides n p. +theorem transitive_divides: transitive ? divides. +unfold. intros. -elim H.elim H1. apply witness n p (n2*n1). +elim H.elim H1. apply (witness x z (n2*n)). rewrite > H3.rewrite > H2. apply assoc_times. qed. +variant trans_divides: \forall n,m,p. + n \divides m \to m \divides p \to n \divides p \def transitive_divides. + +theorem eq_mod_to_divides:\forall n,m,p. O< p \to +mod n p = mod m p \to divides p (n-m). +intros. +cut (n \le m \or \not n \le m). +elim Hcut. +cut (n-m=O). +rewrite > Hcut1. +apply (witness p O O). +apply times_n_O. +apply eq_minus_n_m_O. +assumption. +apply (witness p (n-m) ((div n p)-(div m p))). +rewrite > distr_times_minus. +rewrite > sym_times. +rewrite > (sym_times p). +cut ((div n p)*p = n - (mod n p)). +rewrite > Hcut1. +rewrite > eq_minus_minus_minus_plus. +rewrite > sym_plus. +rewrite > H1. +rewrite < div_mod.reflexivity. +assumption. +apply sym_eq. +apply plus_to_minus. +rewrite > sym_plus. +apply div_mod. +assumption. +apply (decidable_le n m). +qed. + +theorem antisymmetric_divides: antisymmetric nat divides. +unfold antisymmetric.intros.elim H. elim H1. +apply (nat_case1 n2).intro. +rewrite > H3.rewrite > H2.rewrite > H4. +rewrite < times_n_O.reflexivity. +intros. +apply (nat_case1 n).intro. +rewrite > H2.rewrite > H3.rewrite > H5. +rewrite < times_n_O.reflexivity. +intros. +apply antisymmetric_le. +rewrite > H2.rewrite > times_n_SO in \vdash (? % ?). +apply le_times_r.rewrite > H4.apply le_S_S.apply le_O_n. +rewrite > H3.rewrite > times_n_SO in \vdash (? % ?). +apply le_times_r.rewrite > H5.apply le_S_S.apply le_O_n. +qed. + (* divides le *) -theorem divides_to_le : \forall n,m. O < m \to divides n m \to n \le m. -intros. elim H1.rewrite > H2.cut O < n2. -apply lt_O_n_elim n2 Hcut.intro.rewrite < sym_times. +theorem divides_to_le : \forall n,m. O < m \to n \divides m \to n \le m. +intros. elim H1.rewrite > H2.cut (O < n2). +apply (lt_O_n_elim n2 Hcut).intro.rewrite < sym_times. simplify.rewrite < sym_plus. apply le_plus_n. -elim le_to_or_lt_eq O n2. -assumption.apply le_O_n. -absurd O H2.rewrite < H3.rewrite < times_n_O. -apply not_le_Sn_n O. +apply (not_le_Sn_n O). +apply le_O_n. qed. -theorem divides_to_lt_O : \forall n,m. O < m \to divides n m \to O < n. +theorem divides_to_lt_O : \forall n,m. O < m \to n \divides m \to O < n. intros.elim H1. -elim le_to_or_lt_eq O n (le_O_n n). +elim (le_to_or_lt_eq O n (le_O_n n)). assumption. -rewrite < H3.absurd O < m.assumption. +rewrite < H3.absurd (O < m).assumption. rewrite > H2.rewrite < H3. -simplify.exact not_le_Sn_n O. +simplify.exact (not_le_Sn_n O). qed. (* boolean divides *) definition divides_b : nat \to nat \to bool \def -\lambda n,m :nat. (eqb (mod m n) O). +\lambda n,m :nat. (eqb (m \mod n) O). theorem divides_b_to_Prop : -\forall n,m:nat. O < n \to O < m \to +\forall n,m:nat. O < n \to match divides_b n m with -[ true \Rightarrow divides n m -| false \Rightarrow \lnot (divides n m)]. +[ true \Rightarrow n \divides m +| false \Rightarrow n \ndivides m]. intros. change with -match eqb (mod m n) O with -[ true \Rightarrow divides n m -| false \Rightarrow \lnot (divides n m)]. +match eqb (m \mod n) O with +[ true \Rightarrow n \divides m +| false \Rightarrow n \ndivides m]. apply eqb_elim. intro.simplify.apply mod_O_to_divides.assumption.assumption. -intro.simplify.intro.apply H2.apply divides_to_mod_O.assumption.assumption. +intro.simplify.unfold Not.intro.apply H1.apply divides_to_mod_O.assumption.assumption. qed. theorem divides_b_true_to_divides : -\forall n,m:nat. O < n \to O < m \to -(divides_b n m = true ) \to divides n m. +\forall n,m:nat. O < n \to +(divides_b n m = true ) \to n \divides m. intros. change with match true with -[ true \Rightarrow divides n m -| false \Rightarrow \lnot (divides n m)]. -rewrite < H2.apply divides_b_to_Prop. -assumption.assumption. +[ true \Rightarrow n \divides m +| false \Rightarrow n \ndivides m]. +rewrite < H1.apply divides_b_to_Prop. +assumption. qed. theorem divides_b_false_to_not_divides : -\forall n,m:nat. O < n \to O < m \to -(divides_b n m = false ) \to \lnot (divides n m). +\forall n,m:nat. O < n \to +(divides_b n m = false ) \to n \ndivides m. intros. change with match false with -[ true \Rightarrow divides n m -| false \Rightarrow \lnot (divides n m)]. -rewrite < H2.apply divides_b_to_Prop. -assumption.assumption. +[ true \Rightarrow n \divides m +| false \Rightarrow n \ndivides m]. +rewrite < H1.apply divides_b_to_Prop. +assumption. +qed. + +theorem decidable_divides: \forall n,m:nat.O < n \to +decidable (n \divides m). +intros.change with ((n \divides m) \lor n \ndivides m). +cut +(match divides_b n m with +[ true \Rightarrow n \divides m +| false \Rightarrow n \ndivides m] \to n \divides m \lor n \ndivides m). +apply Hcut.apply divides_b_to_Prop.assumption. +elim (divides_b n m).left.apply H1.right.apply H1. +qed. + +theorem divides_to_divides_b_true : \forall n,m:nat. O < n \to +n \divides m \to divides_b n m = true. +intros. +cut (match (divides_b n m) with +[ true \Rightarrow n \divides m +| false \Rightarrow n \ndivides m] \to ((divides_b n m) = true)). +apply Hcut.apply divides_b_to_Prop.assumption. +elim (divides_b n m).reflexivity. +absurd (n \divides m).assumption.assumption. +qed. + +theorem not_divides_to_divides_b_false: \forall n,m:nat. O < n \to +\lnot(n \divides m) \to (divides_b n m) = false. +intros. +cut (match (divides_b n m) with +[ true \Rightarrow n \divides m +| false \Rightarrow n \ndivides m] \to ((divides_b n m) = false)). +apply Hcut.apply divides_b_to_Prop.assumption. +elim (divides_b n m). +absurd (n \divides m).assumption.assumption. +reflexivity. qed. (* divides and pi *) -theorem divides_f_pi_f : \forall f:nat \to nat.\forall n,i:nat. -i < n \to divides (f i) (pi n f). -intros 3.elim n.apply False_ind.apply not_le_Sn_O i H. +theorem divides_f_pi_f : \forall f:nat \to nat.\forall n,m,i:nat. +m \le i \to i \le n+m \to f i \divides pi n f m. +intros 5.elim n.simplify. +cut (i = m).rewrite < Hcut.apply divides_n_n. +apply antisymmetric_le.assumption.assumption. simplify. -apply le_n_Sm_elim (S i) n1 H1. -intro. -apply transitive_divides ? (pi n1 f). -apply H.simplify.apply le_S_S_to_le. assumption. -apply witness ? ? (f n1).apply sym_times. -intro.cut i = n1. -rewrite > Hcut. -apply witness ? ? (pi n1 f).reflexivity. -apply inj_S.assumption. +cut (i < S n1+m \lor i = S n1 + m). +elim Hcut. +apply (transitive_divides ? (pi n1 f m)). +apply H1.apply le_S_S_to_le. assumption. +apply (witness ? ? (f (S n1+m))).apply sym_times. +rewrite > H3. +apply (witness ? ? (pi n1 f m)).reflexivity. +apply le_to_or_lt_eq.assumption. qed. +(* theorem mod_S_pi: \forall f:nat \to nat.\forall n,i:nat. -i < n \to (S O) < (f i) \to mod (S (pi n f)) (f i) = (S O). -intros.cut mod (pi n f) (f i) = O. +i < n \to (S O) < (f i) \to (S (pi n f)) \mod (f i) = (S O). +intros.cut (pi n f) \mod (f i) = O. rewrite < Hcut. apply mod_S.apply trans_lt O (S O).apply le_n (S O).assumption. rewrite > Hcut.assumption. apply divides_to_mod_O.apply trans_lt O (S O).apply le_n (S O).assumption. apply divides_f_pi_f.assumption. qed. +*) (* divides and fact *) theorem divides_fact : \forall n,i:nat. -O < i \to i \le n \to divides i (fact n). -intros 3.elim n.absurd O H3. -apply witness ? ? (fact n1).reflexivity. +apply (witness ? ? n1!).reflexivity. qed. theorem mod_S_fact: \forall n,i:nat. -(S O) < i \to i \le n \to mod (S (fact n)) i = (S O). -intros.cut mod (fact n) i = O. +(S O) < i \to i \le n \to (S n!) \mod i = (S O). +intros.cut (n! \mod i = O). rewrite < Hcut. -apply mod_S.apply trans_lt O (S O).apply le_n (S O).assumption. +apply mod_S.apply (trans_lt O (S O)).apply (le_n (S O)).assumption. rewrite > Hcut.assumption. -apply divides_to_mod_O.apply trans_lt O (S O).apply le_n (S O).assumption. -apply divides_fact.apply trans_lt O (S O).apply le_n (S O).assumption. +apply divides_to_mod_O.apply (trans_lt O (S O)).apply (le_n (S O)).assumption. +apply divides_fact.apply (trans_lt O (S O)).apply (le_n (S O)).assumption. assumption. qed. theorem not_divides_S_fact: \forall n,i:nat. -(S O) < i \to i \le n \to \not (divides i (S (fact n))). +(S O) < i \to i \le n \to i \ndivides S n!. intros. apply divides_b_false_to_not_divides. -apply trans_lt O (S O).apply le_n (S O).assumption. -simplify.apply le_S_S.apply le_O_n. -change with (eqb (mod (S (fact n)) i) O) = false. +apply (trans_lt O (S O)).apply (le_n (S O)).assumption. +change with ((eqb ((S n!) \mod i) O) = false). rewrite > mod_S_fact.simplify.reflexivity. assumption.assumption. qed. @@ -241,14 +336,14 @@ qed. (* prime *) definition prime : nat \to Prop \def \lambda n:nat. (S O) < n \land -(\forall m:nat. divides m n \to (S O) < m \to m = n). +(\forall m:nat. m \divides n \to (S O) < m \to m = n). theorem not_prime_O: \lnot (prime O). -simplify.intro.elim H.apply not_le_Sn_O (S O) H1. +unfold Not.unfold prime.intro.elim H.apply (not_le_Sn_O (S O) H1). qed. theorem not_prime_SO: \lnot (prime (S O)). -simplify.intro.elim H.apply not_le_Sn_n (S O) H1. +unfold Not.unfold prime.intro.elim H.apply (not_le_Sn_n (S O) H1). qed. (* smallest factor *) @@ -259,7 +354,7 @@ match n with | (S p) \Rightarrow match p with [ O \Rightarrow (S O) - | (S q) \Rightarrow min_aux q (S(S q)) (\lambda m.(eqb (mod (S(S q)) m) O))]]. + | (S q) \Rightarrow min_aux q (S(S q)) (\lambda m.(eqb ((S(S q)) \mod m) O))]]. (* it works ! theorem example1 : smallest_prime_factor (S(S(S O))) = (S(S(S O))). @@ -274,111 +369,120 @@ theorem example3 : smallest_prime_factor (S(S(S(S(S(S(S O))))))) = (S(S(S(S(S(S( simplify.reflexivity. qed. *) -(* not sure this is what we need *) -theorem lt_S_O_smallest_factor: +theorem lt_SO_smallest_factor: \forall n:nat. (S O) < n \to (S O) < (smallest_factor n). intro. -apply nat_case n.intro.apply False_ind.apply not_le_Sn_O (S O) H. -intro.apply nat_case m.intro. apply False_ind.apply not_le_Sn_n (S O) H. +apply (nat_case n).intro.apply False_ind.apply (not_le_Sn_O (S O) H). +intro.apply (nat_case m).intro. apply False_ind.apply (not_le_Sn_n (S O) H). intros. change with -S O < min_aux m1 (S(S m1)) (\lambda m.(eqb (mod (S(S m1)) m) O)). -apply lt_to_le_to_lt ? (S (S O)). -apply le_n (S(S O)). -cut (S(S O)) = (S(S m1)) - m1. +(S O < min_aux m1 (S(S m1)) (\lambda m.(eqb ((S(S m1)) \mod m) O))). +apply (lt_to_le_to_lt ? (S (S O))). +apply (le_n (S(S O))). +cut ((S(S O)) = (S(S m1)) - m1). rewrite > Hcut. apply le_min_aux. -apply sym_eq.apply plus_to_minus.apply le_S.apply le_n_Sn. +apply sym_eq.apply plus_to_minus. rewrite < sym_plus.simplify.reflexivity. qed. +theorem lt_O_smallest_factor: \forall n:nat. O < n \to O < (smallest_factor n). +intro. +apply (nat_case n).intro.apply False_ind.apply (not_le_Sn_n O H). +intro.apply (nat_case m).intro. +simplify.unfold lt.apply le_n. +intros.apply (trans_lt ? (S O)). +unfold lt.apply le_n. +apply lt_SO_smallest_factor.unfold lt. apply le_S_S. +apply le_S_S.apply le_O_n. +qed. + theorem divides_smallest_factor_n : -\forall n:nat. (S O) < n \to divides (smallest_factor n) n. +\forall n:nat. O < n \to smallest_factor n \divides n. intro. -apply nat_case n.intro.apply False_ind.apply not_le_Sn_O (S O) H. -intro.apply nat_case m.intro. apply False_ind.apply not_le_Sn_n (S O) H. +apply (nat_case n).intro.apply False_ind.apply (not_le_Sn_O O H). +intro.apply (nat_case m).intro. simplify. +apply (witness ? ? (S O)). simplify.reflexivity. intros. apply divides_b_true_to_divides. -apply trans_lt ? (S O).apply le_n (S O).apply lt_S_O_smallest_factor ? H. -apply trans_lt ? (S O).apply le_n (S O).assumption. +apply (lt_O_smallest_factor ? H). change with -eqb (mod (S(S m1)) (min_aux m1 (S(S m1)) - (\lambda m.(eqb (mod (S(S m1)) m) O)))) O = true. +(eqb ((S(S m1)) \mod (min_aux m1 (S(S m1)) + (\lambda m.(eqb ((S(S m1)) \mod m) O)))) O = true). apply f_min_aux_true. -apply ex_intro nat ? (S(S m1)). +apply (ex_intro nat ? (S(S m1))). split.split. apply le_minus_m.apply le_n. rewrite > mod_n_n.reflexivity. -apply trans_lt ? (S O).apply le_n (S O).assumption. +apply (trans_lt ? (S O)).apply (le_n (S O)).unfold lt. +apply le_S_S.apply le_S_S.apply le_O_n. qed. theorem le_smallest_factor_n : \forall n:nat. smallest_factor n \le n. -intro.apply nat_case n.simplify.reflexivity. -intro.apply nat_case m.simplify.reflexivity. +intro.apply (nat_case n).simplify.reflexivity. +intro.apply (nat_case m).simplify.reflexivity. intro.apply divides_to_le. -simplify.apply le_S_S.apply le_O_n. +unfold lt.apply le_S_S.apply le_O_n. apply divides_smallest_factor_n. -simplify.apply le_S_S.apply le_S_S. apply le_O_n. +unfold lt.apply le_S_S.apply le_O_n. qed. theorem lt_smallest_factor_to_not_divides: \forall n,i:nat. -(S O) < n \to (S O) < i \to i < (smallest_factor n) \to \lnot (divides i n). +(S O) < n \to (S O) < i \to i < (smallest_factor n) \to i \ndivides n. intros 2. -apply nat_case n.intro.apply False_ind.apply not_le_Sn_O (S O) H. -intro.apply nat_case m.intro. apply False_ind.apply not_le_Sn_n (S O) H. +apply (nat_case n).intro.apply False_ind.apply (not_le_Sn_O (S O) H). +intro.apply (nat_case m).intro. apply False_ind.apply (not_le_Sn_n (S O) H). intros. apply divides_b_false_to_not_divides. -apply trans_lt O (S O).apply le_n (S O).assumption. -apply trans_lt O (S O).apply le_n (S O).assumption. -change with (eqb (mod (S(S m1)) i) O) = false. -apply lt_min_aux_to_false -(\lambda i:nat.eqb (mod (S(S m1)) i) O) (S(S m1)) m1 i. -cut (S(S O)) = (S(S m1)-m1). +apply (trans_lt O (S O)).apply (le_n (S O)).assumption. +change with ((eqb ((S(S m1)) \mod i) O) = false). +apply (lt_min_aux_to_false +(\lambda i:nat.eqb ((S(S m1)) \mod i) O) (S(S m1)) m1 i). +cut ((S(S O)) = (S(S m1)-m1)). rewrite < Hcut.exact H1. apply sym_eq. apply plus_to_minus. -apply le_S.apply le_n_Sn. rewrite < sym_plus.simplify.reflexivity. exact H2. qed. theorem prime_smallest_factor_n : \forall n:nat. (S O) < n \to prime (smallest_factor n). -intro. change with (S(S O)) \le n \to (S O) < (smallest_factor n) \land -(\forall m:nat. divides m (smallest_factor n) \to (S O) < m \to m = (smallest_factor n)). +intro. change with ((S(S O)) \le n \to (S O) < (smallest_factor n) \land +(\forall m:nat. m \divides smallest_factor n \to (S O) < m \to m = (smallest_factor n))). intro.split. -apply lt_S_O_smallest_factor.assumption. +apply lt_SO_smallest_factor.assumption. intros. -cut le m (smallest_factor n). -elim le_to_or_lt_eq m (smallest_factor n) Hcut. -absurd divides m n. -apply transitive_divides m (smallest_factor n). +cut (le m (smallest_factor n)). +elim (le_to_or_lt_eq m (smallest_factor n) Hcut). +absurd (m \divides n). +apply (transitive_divides m (smallest_factor n)). assumption. apply divides_smallest_factor_n. -exact H. +apply (trans_lt ? (S O)). unfold lt. apply le_n. exact H. apply lt_smallest_factor_to_not_divides. exact H.assumption.assumption.assumption. apply divides_to_le. -apply trans_lt O (S O). -apply le_n (S O). -apply lt_S_O_smallest_factor. +apply (trans_lt O (S O)). +apply (le_n (S O)). +apply lt_SO_smallest_factor. exact H. assumption. qed. theorem prime_to_smallest_factor: \forall n. prime n \to smallest_factor n = n. -intro.apply nat_case n.intro.apply False_ind.apply not_prime_O H. -intro.apply nat_case m.intro.apply False_ind.apply not_prime_SO H. +intro.apply (nat_case n).intro.apply False_ind.apply (not_prime_O H). +intro.apply (nat_case m).intro.apply False_ind.apply (not_prime_SO H). intro. change with -(S O) < (S(S m1)) \land -(\forall m:nat. divides m (S(S m1)) \to (S O) < m \to m = (S(S m1))) \to -smallest_factor (S(S m1)) = (S(S m1)). +((S O) < (S(S m1)) \land +(\forall m:nat. m \divides S(S m1) \to (S O) < m \to m = (S(S m1))) \to +smallest_factor (S(S m1)) = (S(S m1))). intro.elim H.apply H2. apply divides_smallest_factor_n. -assumption. -apply lt_S_O_smallest_factor. +apply (trans_lt ? (S O)).unfold lt. apply le_n.assumption. +apply lt_SO_smallest_factor. assumption. qed. @@ -411,22 +515,22 @@ qed. *) theorem primeb_to_Prop: \forall n. match primeb n with [ true \Rightarrow prime n -| false \Rightarrow \not (prime n)]. +| false \Rightarrow \lnot (prime n)]. intro. -apply nat_case n.simplify.intro.elim H.apply not_le_Sn_O (S O) H1. -intro.apply nat_case m.simplify.intro.elim H.apply not_le_Sn_n (S O) H1. +apply (nat_case n).simplify.unfold Not.unfold prime.intro.elim H.apply (not_le_Sn_O (S O) H1). +intro.apply (nat_case m).simplify.unfold Not.unfold prime.intro.elim H.apply (not_le_Sn_n (S O) H1). intro. change with match eqb (smallest_factor (S(S m1))) (S(S m1)) with [ true \Rightarrow prime (S(S m1)) -| false \Rightarrow \not (prime (S(S m1)))]. -apply eqb_elim (smallest_factor (S(S m1))) (S(S m1)). -intro.change with prime (S(S m1)). +| false \Rightarrow \lnot (prime (S(S m1)))]. +apply (eqb_elim (smallest_factor (S(S m1))) (S(S m1))). +intro.change with (prime (S(S m1))). rewrite < H. apply prime_smallest_factor_n. -simplify.apply le_S_S.apply le_S_S.apply le_O_n. -intro.change with \not (prime (S(S m1))). -change with prime (S(S m1)) \to False. +unfold lt.apply le_S_S.apply le_S_S.apply le_O_n. +intro.change with (\lnot (prime (S(S m1)))). +change with (prime (S(S m1)) \to False). intro.apply H. apply prime_to_smallest_factor. assumption. @@ -437,27 +541,27 @@ primeb n = true \to prime n. intros.change with match true with [ true \Rightarrow prime n -| false \Rightarrow \not (prime n)]. +| false \Rightarrow \lnot (prime n)]. rewrite < H. apply primeb_to_Prop. qed. theorem primeb_false_to_not_prime : \forall n:nat. -primeb n = false \to \not (prime n). +primeb n = false \to \lnot (prime n). intros.change with match false with [ true \Rightarrow prime n -| false \Rightarrow \not (prime n)]. +| false \Rightarrow \lnot (prime n)]. rewrite < H. apply primeb_to_Prop. qed. theorem decidable_prime : \forall n:nat.decidable (prime n). -intro.change with (prime n) \lor \not (prime n). +intro.change with ((prime n) \lor \lnot (prime n)). cut -match primeb n with +(match primeb n with [ true \Rightarrow prime n -| false \Rightarrow \not (prime n)] \to (prime n) \lor \not (prime n). +| false \Rightarrow \lnot (prime n)] \to (prime n) \lor \lnot (prime n)). apply Hcut.apply primeb_to_Prop. elim (primeb n).left.apply H.right.apply H. qed. @@ -465,127 +569,23 @@ qed. theorem prime_to_primeb_true: \forall n:nat. prime n \to primeb n = true. intros. -cut match (primeb n) with +cut (match (primeb n) with [ true \Rightarrow prime n -| false \Rightarrow \not (prime n)] \to ((primeb n) = true). +| false \Rightarrow \lnot (prime n)] \to ((primeb n) = true)). apply Hcut.apply primeb_to_Prop. -elim primeb n.reflexivity. +elim (primeb n).reflexivity. absurd (prime n).assumption.assumption. qed. theorem not_prime_to_primeb_false: \forall n:nat. -\not(prime n) \to primeb n = false. +\lnot(prime n) \to primeb n = false. intros. -cut match (primeb n) with +cut (match (primeb n) with [ true \Rightarrow prime n -| false \Rightarrow \not (prime n)] \to ((primeb n) = false). +| false \Rightarrow \lnot (prime n)] \to ((primeb n) = false)). apply Hcut.apply primeb_to_Prop. -elim primeb n. +elim (primeb n). absurd (prime n).assumption.assumption. reflexivity. qed. -(* upper bound by Bertrand's conjecture. *) -(* Too difficult to prove. -let rec nth_prime n \def -match n with - [ O \Rightarrow (S(S O)) - | (S p) \Rightarrow - let previous_prime \def S (nth_prime p) in - min_aux previous_prime ((S(S O))*previous_prime) primeb]. - -theorem example8 : nth_prime (S(S O)) = (S(S(S(S(S O))))). -normalize.reflexivity. -qed. - -theorem example9 : nth_prime (S(S(S O))) = (S(S(S(S(S(S(S O))))))). -normalize.reflexivity. -qed. - -theorem example10 : nth_prime (S(S(S(S O)))) = (S(S(S(S(S(S(S(S(S(S(S O))))))))))). -normalize.reflexivity. -qed. *) - -theorem smallest_factor_fact: \forall n:nat. -n < smallest_factor (S (fact n)). -intros. -apply not_le_to_lt. -change with smallest_factor (S (fact n)) \le n \to False.intro. -apply not_divides_S_fact n (smallest_factor(S (fact n))) ? ?. -apply divides_smallest_factor_n. -simplify.apply le_S_S.apply le_SO_fact. -apply lt_S_O_smallest_factor. -simplify.apply le_S_S.apply le_SO_fact. -assumption. -qed. - -(* mi sembra che il problem sia ex *) -theorem ex_prime: \forall n. (S O) \le n \to ex nat (\lambda m. -n < m \land m \le (S (fact n)) \land (prime m)). -intros. -elim H. -apply ex_intro nat ? (S(S O)). -split.split.apply le_n (S(S O)). -apply le_n (S(S O)).apply primeb_to_Prop (S(S O)). -apply ex_intro nat ? (smallest_factor (S (fact (S n1)))). -split.split. -apply smallest_factor_fact. -apply le_smallest_factor_n. -(* ancora hint non lo trova *) -apply prime_smallest_factor_n. -change with (S(S O)) \le S (fact (S n1)). -apply le_S.apply le_SSO_fact. -simplify.apply le_S_S.assumption. -qed. - -let rec nth_prime n \def -match n with - [ O \Rightarrow (S(S O)) - | (S p) \Rightarrow - let previous_prime \def (nth_prime p) in - let upper_bound \def S (fact previous_prime) in - min_aux (upper_bound - (S previous_prime)) upper_bound primeb]. - -(* it works, but nth_prime 4 takes already a few minutes - -it must compute factorial of 7 ... - -theorem example11 : nth_prime (S(S O)) = (S(S(S(S(S O))))). -normalize.reflexivity. -qed. - -theorem example12: nth_prime (S(S(S O))) = (S(S(S(S(S(S(S O))))))). -normalize.reflexivity. -qed. - -theorem example13 : nth_prime (S(S(S(S O)))) = (S(S(S(S(S(S(S(S(S(S(S O))))))))))). -normalize.reflexivity. -*) - -theorem prime_nth_prime : \forall n:nat.prime (nth_prime n). -intro. -apply nat_case n. -change with prime (S(S O)). -apply primeb_to_Prop (S(S O)). -intro. -change with -let previous_prime \def (nth_prime m) in -let upper_bound \def S (fact previous_prime) in -prime (min_aux (upper_bound - (S previous_prime)) upper_bound primeb). -apply primeb_true_to_prime. -apply f_min_aux_true. -apply ex_intro nat ? (smallest_factor (S (fact (nth_prime m)))). -split.split. -cut S (fact (nth_prime m))-(S (fact (nth_prime m)) - (S (nth_prime m))) = (S (nth_prime m)). -rewrite > Hcut.exact smallest_factor_fact (nth_prime m). -(* maybe we could factorize this proof *) -apply plus_to_minus. -apply le_minus_m. -apply plus_minus_m_m. -apply le_S_S. -apply le_n_fact_n. -apply le_smallest_factor_n. -apply prime_to_primeb_true. -apply prime_smallest_factor_n. -change with (S(S O)) \le S (fact (nth_prime m)). -apply le_S_S.apply le_SO_fact. -qed. \ No newline at end of file