From 21d7aa4df8d5d4bfe1073720ea4f9410e9cec879 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 23 Jul 2007 15:14:29 +0000 Subject: [PATCH] Prototype of min_aux changed. Now (min_aux off n f) find the smallest i such that * f i = true or i = n+off * \forall j, n <= j <= n+off, f j = false The new function does no longer compute with off. Thus we obtain for free a great computational speed-up in every function defined in terms of it. --- .../matita/library/nat/chinese_reminder.ma | 7 +- .../matita/library/nat/minimization.ma | 123 +++++++++++------- helm/software/matita/library/nat/nth_prime.ma | 50 +++---- helm/software/matita/library/nat/primes.ma | 34 ++--- helm/software/matita/library/nat/totient.ma | 3 +- 5 files changed, 116 insertions(+), 101 deletions(-) diff --git a/helm/software/matita/library/nat/chinese_reminder.ma b/helm/software/matita/library/nat/chinese_reminder.ma index 31b976dcf..766b85f71 100644 --- a/helm/software/matita/library/nat/chinese_reminder.ma +++ b/helm/software/matita/library/nat/chinese_reminder.ma @@ -223,14 +223,15 @@ simplify. intro.apply False_ind. apply not_eq_true_false.apply sym_eq.assumption. apply (f_min_aux_true -(\lambda x. andb (eqb (x \mod m) a) (eqb (x \mod n) b)) (pred (m*n)) (pred (m*n))). +(\lambda x. andb (eqb (x \mod m) a) (eqb (x \mod n) b)) (pred (m*n)) O). elim (and_congruent_congruent_lt m n a b). apply (ex_intro ? ? a1).split.split. -rewrite < minus_n_n.apply le_O_n. +apply le_O_n. elim H3.apply le_S_S_to_le.apply (trans_le ? (m*n)). assumption.apply (nat_case (m*n)).apply le_O_n. intro. -rewrite < pred_Sn.apply le_n. +rewrite < pred_Sn. +rewrite < plus_n_O.apply le_n. elim H3.elim H4. apply andb_elim. cut (a1 \mod m = a). diff --git a/helm/software/matita/library/nat/minimization.ma b/helm/software/matita/library/nat/minimization.ma index 2d273e180..8b4b83c2f 100644 --- a/helm/software/matita/library/nat/minimization.ma +++ b/helm/software/matita/library/nat/minimization.ma @@ -161,19 +161,19 @@ elim n qed. let rec min_aux off n f \def - match f (n-off) with - [ true \Rightarrow (n-off) + match f n with + [ true \Rightarrow n | false \Rightarrow match off with [ O \Rightarrow n - | (S p) \Rightarrow min_aux p n f]]. + | (S p) \Rightarrow min_aux p (S n) f]]. definition min : nat \to (nat \to bool) \to nat \def -\lambda n.\lambda f. min_aux n n f. +\lambda n.\lambda f. min_aux n O f. theorem min_aux_O_f: \forall f:nat \to bool. \forall i :nat. min_aux O i f = i. -intros.simplify.rewrite < minus_n_O. +intros.simplify. elim (f i).reflexivity. simplify.reflexivity. qed. @@ -184,34 +184,35 @@ intro.apply (min_aux_O_f f O). qed. theorem min_aux_S : \forall f: nat \to bool. \forall i,n:nat. -(f (n -(S i)) = true \land min_aux (S i) n f = (n - (S i))) \lor -(f (n -(S i)) = false \land min_aux (S i) n f = min_aux i n f). -intros.simplify.elim (f (n - (S i))). +((f n) = true \land min_aux (S i) n f = n) \lor +((f n) = false \land min_aux (S i) n f = min_aux i (S n) f). +intros.simplify.elim (f n). simplify.left.split.reflexivity.reflexivity. simplify.right.split.reflexivity.reflexivity. qed. theorem f_min_aux_true: \forall f:nat \to bool. \forall off,m:nat. -(\exists i. le (m-off) i \land le i m \land f i = true) \to +(\exists i. le m i \land le i (off + m) \land f i = true) \to f (min_aux off m f) = true. intros 2. elim off.elim H.elim H1.elim H2. cut (a = m). rewrite > (min_aux_O_f f).rewrite < Hcut.assumption. -apply (antisym_le a m).assumption.rewrite > (minus_n_O m).assumption. +apply (antisym_le a m).assumption.assumption. simplify. apply (bool_ind (\lambda b:bool. -(f (m-(S n)) = b) \to (f (match b in bool with -[ true \Rightarrow m-(S n) -| false \Rightarrow (min_aux n m f)])) = true)). -simplify.intro.assumption. -simplify.intro.apply H. +(f m = b) \to (f (match b in bool with +[ true \Rightarrow m +| false \Rightarrow (min_aux n (S m) f)])) = true)). +intro; assumption. +intro. apply H. elim H1.elim H3.elim H4. -elim (le_to_or_lt_eq (m-(S n)) a H6). +elim (le_to_or_lt_eq ? a H6). apply (ex_intro nat ? a). split.split. -apply lt_minus_S_n_to_le_minus_n.assumption. -assumption.assumption. +assumption. +rewrite < plus_n_Sm; assumption. +assumption. absurd (f a = false).rewrite < H8.assumption. rewrite > H5. apply not_eq_true_false. @@ -219,45 +220,67 @@ reflexivity. qed. theorem lt_min_aux_to_false : \forall f:nat \to bool. -\forall n,off,m:nat. (n-off) \leq m \to m < (min_aux off n f) \to f m = false. +\forall n,off,m:nat. n \leq m \to m < (min_aux off n f) \to f m = false. intros 3. -elim off.absurd (le n m).rewrite > minus_n_O.assumption. -apply lt_to_not_le.rewrite < (min_aux_O_f f n).assumption. -generalize in match H1. -elim (min_aux_S f n1 n). -elim H3. -absurd (n - S n1 \le m).assumption. -apply lt_to_not_le.rewrite < H6.assumption. -elim H3. -elim (le_to_or_lt_eq (n -(S n1)) m). -apply H.apply lt_minus_S_n_to_le_minus_n.assumption. -rewrite < H6.assumption. -rewrite < H7.assumption. -assumption. +generalize in match n; clear n. +elim off.absurd (le n1 m).assumption. +apply lt_to_not_le.rewrite < (min_aux_O_f f n1).assumption. +elim (le_to_or_lt_eq ? ? H1); + [ unfold lt in H3; + apply (H (S n1)); + [ assumption + | elim (min_aux_S f n n1); + [ elim H4; + elim (not_le_Sn_n n1); + rewrite > H6 in H2; + apply (lt_to_le (S n1) n1 ?). + apply (le_to_lt_to_lt (S n1) m n1 ? ?); + [apply (H3). + |apply (H2). + ] + | elim H4; + rewrite < H6; + assumption + ] + ] + | rewrite < H3 in H2 ⊢ %. + elim (min_aux_S f n n1); + [ elim H4; + rewrite > H6 in H2; + unfold lt in H2; + elim (not_le_Sn_n ? H2) + | elim H4; + assumption + ] + ] qed. -theorem le_min_aux : \forall f:nat \to bool. -\forall n,off:nat. (n-off) \leq (min_aux off n f). + +lemma le_min_aux : \forall f:nat \to bool. +\forall n,off:nat. n \leq (min_aux off n f). intros 3. -elim off.rewrite < minus_n_O. -rewrite > (min_aux_O_f f n).apply le_n. -elim (min_aux_S f n1 n). +generalize in match n. clear n. +elim off. +rewrite > (min_aux_O_f f n1).apply le_n. +elim (min_aux_S f n n1). elim H1.rewrite > H3.apply le_n. elim H1.rewrite > H3. -apply (trans_le (n-(S n1)) (n-n1)). -apply monotonic_le_minus_r. -apply le_n_Sn. -assumption. +apply (transitive_le ? (S n1)); + [ apply le_n_Sn + | apply (H (S n1)) + ] qed. theorem le_min_aux_r : \forall f:nat \to bool. -\forall n,off:nat. (min_aux off n f) \le n. +\forall n,off:nat. (min_aux off n f) \le n+off. intros. -elim off.simplify.rewrite < minus_n_O. -elim (f n).simplify.apply le_n. -simplify.apply le_n. -simplify.elim (f (n -(S n1))). -simplify.apply le_plus_to_minus. -rewrite < sym_plus.apply le_plus_n. -simplify.assumption. -qed. +generalize in match n. clear n. +elim off.simplify. +elim (f n1).simplify.rewrite < plus_n_O.apply le_n. +simplify.rewrite < plus_n_O.apply le_n. +simplify.elim (f n1). +simplify. +apply (le_plus_n_r (S n) n1). +simplify.rewrite < plus_n_Sm. +apply (H (S n1)). +qed. \ No newline at end of file diff --git a/helm/software/matita/library/nat/nth_prime.ma b/helm/software/matita/library/nat/nth_prime.ma index 9d01e99f2..f675e80ba 100644 --- a/helm/software/matita/library/nat/nth_prime.ma +++ b/helm/software/matita/library/nat/nth_prime.ma @@ -74,11 +74,9 @@ match n with | (S p) \Rightarrow let previous_prime \def (nth_prime p) in let upper_bound \def S previous_prime! in - min_aux (upper_bound - (S previous_prime)) upper_bound primeb]. + min_aux upper_bound (S previous_prime) primeb]. -(* it works, but nth_prime 4 takes already a few minutes - -it must compute factorial of 7 ...*) - +(* it works theorem example11 : nth_prime (S(S O)) = (S(S(S(S(S O))))). normalize.reflexivity. qed. @@ -91,10 +89,11 @@ theorem example13 : nth_prime (S(S(S(S O)))) = (S(S(S(S(S(S(S(S(S(S(S O))))))))) normalize.reflexivity. qed. -(* -theorem example14 : nth_prime (S(S(S(S(S O))))) = (S(S(S(S(S(S(S(S(S(S(S O))))))))))). +alias num (instance 0) = "natural number". +theorem example14 : nth_prime 18 = 67. normalize.reflexivity. -*) +qed. +*) theorem prime_nth_prime : \forall n:nat.prime (nth_prime n). intro. @@ -104,19 +103,17 @@ intro. change with (let previous_prime \def (nth_prime m) in let upper_bound \def S previous_prime! in -prime (min_aux (upper_bound - (S previous_prime)) upper_bound primeb)). +prime (min_aux upper_bound (S previous_prime) primeb)). apply primeb_true_to_prime. apply f_min_aux_true. apply (ex_intro nat ? (smallest_factor (S (nth_prime m)!))). split.split. -cut (S (nth_prime m)!-(S (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 plus_minus_m_m. -apply le_S_S. -apply le_n_fact_n. -apply le_smallest_factor_n. +apply smallest_factor_fact. +apply transitive_le; + [2: apply le_smallest_factor_n + | skip + | apply (le_plus_n_r (S (nth_prime m)) (S (fact (nth_prime m)))) + ]. apply prime_to_primeb_true. apply prime_smallest_factor_n.unfold lt. apply le_S_S.apply le_SO_fact. @@ -129,15 +126,9 @@ intros. change with (let previous_prime \def (nth_prime n) in let upper_bound \def S previous_prime! in -(S previous_prime) \le min_aux (upper_bound - (S previous_prime)) upper_bound primeb). +(S previous_prime) \le min_aux upper_bound (S previous_prime) primeb). intros. -cut (upper_bound - (upper_bound -(S previous_prime)) = (S previous_prime)). -rewrite < Hcut in \vdash (? % ?). apply le_min_aux. -apply plus_to_minus. -apply plus_minus_m_m. -apply le_S_S. -apply le_n_fact_n. qed. variant lt_nth_prime_n_nth_prime_Sn :\forall n:nat. @@ -184,14 +175,13 @@ intros. apply primeb_false_to_not_prime. letin previous_prime \def (nth_prime n). letin upper_bound \def (S previous_prime!). -apply (lt_min_aux_to_false primeb upper_bound (upper_bound - (S previous_prime)) m). -cut (S (nth_prime n)!-(S (nth_prime n)! - (S (nth_prime n))) = (S (nth_prime n))). -rewrite > Hcut.assumption. -apply plus_to_minus. -apply plus_minus_m_m. -apply le_S_S. -apply le_n_fact_n. +apply (lt_min_aux_to_false primeb (S previous_prime) upper_bound m). assumption. +unfold lt. +apply (transitive_le (S m) (nth_prime (S n)) (min_aux (S (fact (nth_prime n))) (S (nth_prime n)) primeb) ? ?); + [apply (H1). + |apply (le_n (min_aux (S (fact (nth_prime n))) (S (nth_prime n)) primeb)). + ] qed. (* nth_prime enumerates all primes *) diff --git a/helm/software/matita/library/nat/primes.ma b/helm/software/matita/library/nat/primes.ma index d2e89b8f1..a95b2e88f 100644 --- a/helm/software/matita/library/nat/primes.ma +++ b/helm/software/matita/library/nat/primes.ma @@ -397,18 +397,18 @@ 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 ((S(S q)) \mod m) O))]]. + | (S q) \Rightarrow min_aux q (S (S O)) (\lambda m.(eqb ((S(S q)) \mod m) O))]]. -(* it works ! -theorem example1 : smallest_prime_factor (S(S(S O))) = (S(S(S O))). +(* it works ! +theorem example1 : smallest_factor (S(S(S O))) = (S(S(S O))). normalize.reflexivity. qed. -theorem example2: smallest_prime_factor (S(S(S(S O)))) = (S(S O)). +theorem example2: smallest_factor (S(S(S(S O)))) = (S(S O)). normalize.reflexivity. qed. -theorem example3 : smallest_prime_factor (S(S(S(S(S(S(S O))))))) = (S(S(S(S(S(S(S O))))))). +theorem example3 : smallest_factor (S(S(S(S(S(S(S O))))))) = (S(S(S(S(S(S(S O))))))). simplify.reflexivity. qed. *) @@ -419,7 +419,7 @@ 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 ((S(S m1)) \mod m) O))). +(S O < min_aux m1 (S (S O)) (\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). @@ -449,15 +449,18 @@ apply (witness ? ? (S O)). simplify.reflexivity. intros. apply divides_b_true_to_divides. change with -(eqb ((S(S m1)) \mod (min_aux m1 (S(S m1)) +(eqb ((S(S m1)) \mod (min_aux m1 (S (S O)) (\lambda m.(eqb ((S(S m1)) \mod m) O)))) O = true). apply f_min_aux_true. 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)).unfold lt. -apply le_S_S.apply le_S_S.apply le_O_n. +apply (le_S_S_to_le (S (S O)) (S (S m1)) ?). +apply (minus_le_O_to_le (S (S (S O))) (S (S (S m1))) ?). +apply (le_n O). +rewrite < sym_plus. simplify. apply le_n. +apply (eq_to_eqb_true (mod (S (S m1)) (S (S m1))) O ?). +apply (mod_n_n (S (S m1)) ?). +apply (H). qed. theorem le_smallest_factor_n : @@ -478,12 +481,9 @@ 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 (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. -rewrite < sym_plus.simplify.reflexivity. -exact H2. +(\lambda i:nat.eqb ((S(S m1)) \mod i) O) (S (S O)) m1 i). +assumption. +assumption. qed. theorem prime_smallest_factor_n : diff --git a/helm/software/matita/library/nat/totient.ma b/helm/software/matita/library/nat/totient.ma index 730ec8b56..03e2587a8 100644 --- a/helm/software/matita/library/nat/totient.ma +++ b/helm/software/matita/library/nat/totient.ma @@ -63,7 +63,8 @@ apply (nat_case1 n) [intros.unfold cr_pair. apply (le_to_lt_to_lt ? (pred ((S m2)*(S m1)))) [unfold min. - apply le_min_aux_r + apply transitive_le; + [2: apply le_min_aux_r | skip | apply le_n] |unfold lt. apply (nat_case ((S m2)*(S m1))) [apply le_n|intro.apply le_n] -- 2.39.2