From e62ffc0d340dabcca90d4cb91a46f5d5d40b18d6 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 11 Jun 2008 18:00:20 +0000 Subject: [PATCH] New, much faster implementation of factorize. --- .../matita/library/nat/factorization2.ma | 39 +++++++++++++++++++ 1 file changed, 39 insertions(+) create mode 100644 helm/software/matita/library/nat/factorization2.ma diff --git a/helm/software/matita/library/nat/factorization2.ma b/helm/software/matita/library/nat/factorization2.ma new file mode 100644 index 000000000..52a1b9a70 --- /dev/null +++ b/helm/software/matita/library/nat/factorization2.ma @@ -0,0 +1,39 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| A.Asperti, C.Sacerdoti Coen, *) +(* ||A|| E.Tassi, S.Zacchiroli *) +(* \ / *) +(* \ / Matita is distributed under the terms of the *) +(* v GNU Lesser General Public License Version 2.1 *) +(* *) +(**************************************************************************) + +include "nat/factorization.ma". + +let rec factorize_aux2 i n b on b ≝ + match b with + [ O ⇒ nfa_zero + | S b' ⇒ + let p ≝ nth_prime i in + match p_ord n p with + [ pair q r ⇒ + match r with + [ O ⇒ nfa_zero + | S r' ⇒ + match r' with + [ O ⇒ + match q with + [ O ⇒ nfa_one + | _ ⇒ nfa_proper (nf_last (pred q))] + | S _ ⇒ + let res ≝ factorize_aux2 (S i) r b' in + match res with + [ nfa_zero ⇒ nfa_zero (* impossible *) + | nfa_one ⇒ nfa_proper (nf_last q) + | nfa_proper l ⇒ nfa_proper (nf_cons q l)]]]]]. + +definition factorize2 ≝ λn.factorize_aux2 0 n n. \ No newline at end of file -- 2.39.2