]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/library/nat/factorization2.ma
...
[helm.git] / helm / software / matita / library / nat / factorization2.ma
1 (**************************************************************************)
2 (*       ___                                                                *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
8 (*      ||A||       E.Tassi, S.Zacchiroli                                 *)
9 (*      \   /                                                             *)
10 (*       \ /        Matita is distributed under the terms of the          *)
11 (*        v         GNU Lesser General Public License Version 2.1         *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 include "nat/factorization.ma".
16 include "list/list.ma".
17
18 definition cache ≝ 
19   [2;3;5;7;11;13;17;19;23;29;31;37;41;43;47;53;59;61;67;71;
20    73;79;83;89;97;101;103;107;109;113;
21    127;131;137;139;149;151;157;163;167;173;
22    179;181;191;193;197;199;211;223;227;229;
23    233;239;241;251;257;263;269;271;277;281;
24    283;293;307;311;313;317;331;337;347;349;
25    353;359;367;373;379;383;389;397;401;409;
26    419;421;431;433;439;443;449;457;461;463;
27    467;479;487;491;499;503;509;521;523;541;
28    547;557;563;569;571;577;587;593(*;599;601;
29    607;613;617;619;631;641;643;647;653;659;
30    661;673;677;683;691;701;709;719;727;733;
31    739;743;751;757;761;769;773;787;797;809;
32    811;821;823;827;829;839;853;857;859;863;
33    877;881;883;887;907;911;919;929;937;941;
34    947;953;967;971;977;983;991;997;1009;1013;
35    1019;1021;1031;1033;1039;1049;1051;1061;1063;1069;
36    1087;1091;1093;1097;1103;1109;1117;1123;1129;1151;
37    1153;1163;1171;1181;1187;1193;1201;1213;1217;1223;
38    1229;1231;1237;1249;1259;1277;1279;1283;1289;1291;
39    1297;1301;1303;1307;1319;1321;1327;1361;1367;1373;
40    1381;1399;1409;1423;1427;1429;1433;1439;1447;1451;
41    1453;1459;1471;1481;1483;1487;1489;1493;1499;1511;
42    1523;1531;1543;1549;1553;1559;1567;1571;1579;1583;
43    1597;1601;1607;1609;1613;1619;1621;1627;1637;1657;
44    1663;1667;1669;1693;1697;1699;1709;1721;1723;1733;
45    1741;1747;1753;1759;1777;1783;1787;1789;1801;1811;
46    1823;1831;1847;1861;1867;1871;1873;1877;1879;1889;
47    1901;1907;1913;1931;1933;1949;1951;1973;1979;1987;
48    1993;1997;1999;2003;2011;2017;2027;2029;2039;2053;
49    2063;2069;2081;2083;2087;2089;2099;2111;2113;2129;
50    2131;2137;2141;2143;2153;2161;2179;2203;2207;2213;
51    2221;2237;2239;2243;2251;2267;2269;2273;2281;2287;
52    2293;2297;2309;2311;2333;2339;2341;2347;2351;2357;
53    2371;2377;2381;2383;2389;2393;2399;2411;2417;2423;
54    2437;2441;2447;2459;2467;2473;2477;2503;2521;2531;
55    2539;2543;2549;2551;2557;2579;2591;2593;2609;2617;
56    2621;2633;2647;2657;2659;2663;2671;2677;2683;2687;
57    2689;2693;2699;2707;2711;2713;2719;2729;2731;2741;
58    2749;2753;2767;2777;2789;2791;2797;2801;2803;2819;
59    2833;2837;2843;2851;2857;2861;2879;2887;2897;2903;
60    2909;2917;2927;2939;2953;2957;2963;2969;2971;2999;
61    3001;3011;3019;3023;3037;3041;3049;3061;3067;3079;
62    3083;3089;3109;3119;3121;3137;3163;3167;3169;3181;
63    3187;3191;3203;3209;3217;3221;3229;3251;3253;3257;
64    3259;3271;3299;3301;3307;3313;3319;3323;3329;3331;
65    3343;3347;3359;3361;3371;3373;3389;3391;3407;3413;
66    3433;3449;3457;3461;3463;3467;3469;3491;3499;3511;
67    3517;3527;3529;3533;3539;3541;3547;3557;3559;3571;
68    3581;3583;3593;3607;3613;3617;3623;3631;3637;3643;
69    3659;3671;3673;3677;3691;3697;3701;3709;3719;3727;
70    3733;3739;3761;3767;3769;3779;3793;3797;3803;3821 *)
71   ].
72   
73 include "nat/sieve.ma".  
74   
75 let rec rev (acc : list nat) l on l ≝
76   match l with 
77   [ nil ⇒ acc
78   | cons x tl ⇒ rev (x :: acc) tl]. 
79
80 (*  
81 lemma foo: rev [] (sieve 594) = cache. reflexivity; qed. 
82 *)
83
84 definition smart_nth_prime ≝ λcache,i.nth nat cache (nth_prime i) i.
85
86 lemma nth_empty: ∀T:Type.∀n,def.nth T [] def n = def.
87 intros; elim n; [reflexivity]
88 simplify; assumption;
89 qed. 
90
91 lemma nth_short: ∀T:Type.∀def,n,l.length ? l ≤ n → nth T l def n = def.
92 intros 3; elim n 0;
93 [1: intro; cases l; [intros; reflexivity| simplify; intros; cases (?:False);
94     apply (not_le_Sn_n (length T l1) ?).
95       apply (transitive_le (S (length T l1)) O (length T l1) ? ?);
96       [apply (H).
97       |apply (le_O_n (length T l1))]]
98 |2: simplify; intros 3; elim l 0;
99     [1: simplify; intros; apply nth_empty;
100     |2: simplify; intros; apply H; 
101         apply le_S_S_to_le; apply H2;]]
102 qed.
103
104 definition good_cache_spec ≝
105   λcache.∀i.i ≤ length ? cache → nth_prime i = nth nat cache (nth_prime i) i.
106
107 lemma smart_nth_prime_ok:
108   ∀cache.good_cache_spec cache →
109     ∀i.smart_nth_prime cache i = nth_prime i.
110 unfold good_cache_spec; intros; unfold smart_nth_prime;
111 generalize in match (H i);
112 elim i 0;
113 [1: simplify; cases cache;
114     [1: simplify; intros; reflexivity;
115     |2: simplify; intro H; rewrite > H; [reflexivity] apply le_O_n;] 
116 |2: intro; cases cache;
117     [1: simplify in ⊢ (?→(%→?)→?); intros; rewrite > nth_empty; reflexivity;
118     |2: simplify in ⊢ (((? ? %→?)→?)→?);
119         simplify in ⊢ (?→(? ? %→?)→?); 
120         intros; cases (?:n < length ? l ∨ length ? l ≤ n); 
121         [1: generalize in match (leb_to_Prop (length ? l) n); cases (leb (length ? l) n);
122             simplify; intros;[right;assumption|left;apply not_le_to_lt; assumption;]
123         |2: rewrite < H2;[reflexivity] apply le_S; assumption;
124         |3: clear H2; apply nth_short; simplify; apply le_S_S; apply H3;]]]
125 qed.
126
127 let rec by_cases (p:nat→bool) n on n : bool ≝
128   match n with
129   [ O ⇒ p O
130   | S m ⇒ andb (p (S m)) (by_cases p m)].
131   
132 lemma by_cases_ok:
133   ∀m,P.by_cases P m = true → ∀n.n≤m → P n = true.
134 intros 2; elim m;
135 [1: rewrite > (?:n=O);[2:
136       apply (symmetric_eq nat O n ?).apply (le_n_O_to_eq n ?).apply (H1)]
137     apply H;
138 |2: simplify in H1; 
139     cases (le_to_or_lt_eq ?? H2);
140     [2: rewrite > H3; apply (andb_true_true ?? H1);  
141     |1: apply H;
142         [1: apply (andb_true_true_r ?? H1); ] apply le_S_S_to_le; apply H3;]] 
143 qed.
144
145 (*    
146 lemma good_cache : good_cache_spec cache.
147 unfold; intros 2; apply eqb_true_to_eq;
148 apply (by_cases_ok (length ? cache) (λi. eqb (nth_prime i) (nth ? cache (nth_prime i) i)) ? i H);
149 reflexivity;
150 qed. 
151 *)
152
153 let rec factorize_aux2 i n b on b ≝
154  match b with
155   [ O ⇒ nfa_zero
156   | S b' ⇒
157      let p ≝ smart_nth_prime cache i in
158       match p_ord n p with
159        [ pair q r ⇒
160           match r with
161           [ O ⇒ nfa_zero
162           | S r' ⇒
163              match r' with
164              [ O ⇒
165                match q with
166                [ O ⇒ nfa_one
167                | _ ⇒ nfa_proper (nf_last (pred q))]
168              | S _ ⇒
169                 let res ≝ factorize_aux2 (S i) r b' in
170                  match res with
171                  [ nfa_zero ⇒ nfa_zero (* impossible *)
172                  | nfa_one ⇒ nfa_proper (nf_last q)
173                  | nfa_proper l ⇒ nfa_proper (nf_cons q l)]]]]].
174
175 definition factorize2 ≝ λn.factorize_aux2 0 n n.
176
177 let rec nf_id l :=
178   match l with
179   [ nf_last n => nf_last n
180   | nf_cons a l => nf_cons a (nf_id l)].
181   
182 definition nfa_id :=
183   \lambda l.match l with [ nfa_proper l => nfa_proper (nf_id l) | _ => l].
184
185 lemma foo : 
186   let x ≝ (4*7*593) in factorize2 x = nfa_id (factorize2 x).
187 intro;
188 reflexivity;
189 qed.