berghofe@17024
|
1 |
(* Title: HOL/Extraction/Pigeonhole.thy
|
berghofe@17024
|
2 |
Author: Stefan Berghofer, TU Muenchen
|
berghofe@17024
|
3 |
*)
|
berghofe@17024
|
4 |
|
berghofe@17024
|
5 |
header {* The pigeonhole principle *}
|
berghofe@17024
|
6 |
|
haftmann@22737
|
7 |
theory Pigeonhole
|
berghofe@25418
|
8 |
imports Util Efficient_Nat
|
haftmann@22737
|
9 |
begin
|
berghofe@17024
|
10 |
|
berghofe@17024
|
11 |
text {*
|
berghofe@17024
|
12 |
We formalize two proofs of the pigeonhole principle, which lead
|
berghofe@17024
|
13 |
to extracted programs of quite different complexity. The original
|
berghofe@17024
|
14 |
formalization of these proofs in {\sc Nuprl} is due to
|
berghofe@17024
|
15 |
Aleksey Nogin \cite{Nogin-ENTCS-2000}.
|
berghofe@17024
|
16 |
|
berghofe@17024
|
17 |
This proof yields a polynomial program.
|
berghofe@17024
|
18 |
*}
|
berghofe@17024
|
19 |
|
berghofe@17024
|
20 |
theorem pigeonhole:
|
berghofe@17024
|
21 |
"\<And>f. (\<And>i. i \<le> Suc n \<Longrightarrow> f i \<le> n) \<Longrightarrow> \<exists>i j. i \<le> Suc n \<and> j < i \<and> f i = f j"
|
berghofe@17024
|
22 |
proof (induct n)
|
berghofe@17024
|
23 |
case 0
|
berghofe@17024
|
24 |
hence "Suc 0 \<le> Suc 0 \<and> 0 < Suc 0 \<and> f (Suc 0) = f 0" by simp
|
nipkow@17604
|
25 |
thus ?case by iprover
|
berghofe@17024
|
26 |
next
|
berghofe@17024
|
27 |
case (Suc n)
|
berghofe@17024
|
28 |
{
|
berghofe@17024
|
29 |
fix k
|
berghofe@17024
|
30 |
have
|
berghofe@17024
|
31 |
"k \<le> Suc (Suc n) \<Longrightarrow>
|
berghofe@17024
|
32 |
(\<And>i j. Suc k \<le> i \<Longrightarrow> i \<le> Suc (Suc n) \<Longrightarrow> j < i \<Longrightarrow> f i \<noteq> f j) \<Longrightarrow>
|
berghofe@17024
|
33 |
(\<exists>i j. i \<le> k \<and> j < i \<and> f i = f j)"
|
berghofe@17024
|
34 |
proof (induct k)
|
berghofe@17024
|
35 |
case 0
|
berghofe@17024
|
36 |
let ?f = "\<lambda>i. if f i = Suc n then f (Suc (Suc n)) else f i"
|
berghofe@17024
|
37 |
have "\<not> (\<exists>i j. i \<le> Suc n \<and> j < i \<and> ?f i = ?f j)"
|
berghofe@17024
|
38 |
proof
|
wenzelm@32962
|
39 |
assume "\<exists>i j. i \<le> Suc n \<and> j < i \<and> ?f i = ?f j"
|
wenzelm@32962
|
40 |
then obtain i j where i: "i \<le> Suc n" and j: "j < i"
|
wenzelm@32962
|
41 |
and f: "?f i = ?f j" by iprover
|
wenzelm@32962
|
42 |
from j have i_nz: "Suc 0 \<le> i" by simp
|
wenzelm@32962
|
43 |
from i have iSSn: "i \<le> Suc (Suc n)" by simp
|
wenzelm@32962
|
44 |
have S0SSn: "Suc 0 \<le> Suc (Suc n)" by simp
|
wenzelm@32962
|
45 |
show False
|
wenzelm@32962
|
46 |
proof cases
|
wenzelm@32962
|
47 |
assume fi: "f i = Suc n"
|
wenzelm@32962
|
48 |
show False
|
wenzelm@32962
|
49 |
proof cases
|
wenzelm@32962
|
50 |
assume fj: "f j = Suc n"
|
wenzelm@32962
|
51 |
from i_nz and iSSn and j have "f i \<noteq> f j" by (rule 0)
|
wenzelm@32962
|
52 |
moreover from fi have "f i = f j"
|
wenzelm@32962
|
53 |
by (simp add: fj [symmetric])
|
wenzelm@32962
|
54 |
ultimately show ?thesis ..
|
wenzelm@32962
|
55 |
next
|
wenzelm@32962
|
56 |
from i and j have "j < Suc (Suc n)" by simp
|
wenzelm@32962
|
57 |
with S0SSn and le_refl have "f (Suc (Suc n)) \<noteq> f j"
|
wenzelm@32962
|
58 |
by (rule 0)
|
wenzelm@32962
|
59 |
moreover assume "f j \<noteq> Suc n"
|
wenzelm@32962
|
60 |
with fi and f have "f (Suc (Suc n)) = f j" by simp
|
wenzelm@32962
|
61 |
ultimately show False ..
|
wenzelm@32962
|
62 |
qed
|
wenzelm@32962
|
63 |
next
|
wenzelm@32962
|
64 |
assume fi: "f i \<noteq> Suc n"
|
wenzelm@32962
|
65 |
show False
|
wenzelm@32962
|
66 |
proof cases
|
wenzelm@32962
|
67 |
from i have "i < Suc (Suc n)" by simp
|
wenzelm@32962
|
68 |
with S0SSn and le_refl have "f (Suc (Suc n)) \<noteq> f i"
|
wenzelm@32962
|
69 |
by (rule 0)
|
wenzelm@32962
|
70 |
moreover assume "f j = Suc n"
|
wenzelm@32962
|
71 |
with fi and f have "f (Suc (Suc n)) = f i" by simp
|
wenzelm@32962
|
72 |
ultimately show False ..
|
wenzelm@32962
|
73 |
next
|
wenzelm@32962
|
74 |
from i_nz and iSSn and j
|
wenzelm@32962
|
75 |
have "f i \<noteq> f j" by (rule 0)
|
wenzelm@32962
|
76 |
moreover assume "f j \<noteq> Suc n"
|
wenzelm@32962
|
77 |
with fi and f have "f i = f j" by simp
|
wenzelm@32962
|
78 |
ultimately show False ..
|
wenzelm@32962
|
79 |
qed
|
wenzelm@32962
|
80 |
qed
|
berghofe@17024
|
81 |
qed
|
berghofe@17024
|
82 |
moreover have "\<And>i. i \<le> Suc n \<Longrightarrow> ?f i \<le> n"
|
berghofe@17024
|
83 |
proof -
|
wenzelm@32962
|
84 |
fix i assume "i \<le> Suc n"
|
wenzelm@32962
|
85 |
hence i: "i < Suc (Suc n)" by simp
|
wenzelm@32962
|
86 |
have "f (Suc (Suc n)) \<noteq> f i"
|
wenzelm@32962
|
87 |
by (rule 0) (simp_all add: i)
|
wenzelm@32962
|
88 |
moreover have "f (Suc (Suc n)) \<le> Suc n"
|
wenzelm@32962
|
89 |
by (rule Suc) simp
|
wenzelm@32962
|
90 |
moreover from i have "i \<le> Suc (Suc n)" by simp
|
wenzelm@32962
|
91 |
hence "f i \<le> Suc n" by (rule Suc)
|
wenzelm@32962
|
92 |
ultimately show "?thesis i"
|
wenzelm@32962
|
93 |
by simp
|
berghofe@17024
|
94 |
qed
|
berghofe@17024
|
95 |
hence "\<exists>i j. i \<le> Suc n \<and> j < i \<and> ?f i = ?f j"
|
wenzelm@32962
|
96 |
by (rule Suc)
|
berghofe@17024
|
97 |
ultimately show ?case ..
|
berghofe@17024
|
98 |
next
|
berghofe@17024
|
99 |
case (Suc k)
|
berghofe@25418
|
100 |
from search [OF nat_eq_dec] show ?case
|
berghofe@17024
|
101 |
proof
|
wenzelm@32962
|
102 |
assume "\<exists>j<Suc k. f (Suc k) = f j"
|
wenzelm@32962
|
103 |
thus ?case by (iprover intro: le_refl)
|
berghofe@17024
|
104 |
next
|
wenzelm@32962
|
105 |
assume nex: "\<not> (\<exists>j<Suc k. f (Suc k) = f j)"
|
wenzelm@32962
|
106 |
have "\<exists>i j. i \<le> k \<and> j < i \<and> f i = f j"
|
wenzelm@32962
|
107 |
proof (rule Suc)
|
wenzelm@32962
|
108 |
from Suc show "k \<le> Suc (Suc n)" by simp
|
wenzelm@32962
|
109 |
fix i j assume k: "Suc k \<le> i" and i: "i \<le> Suc (Suc n)"
|
wenzelm@32962
|
110 |
and j: "j < i"
|
wenzelm@32962
|
111 |
show "f i \<noteq> f j"
|
wenzelm@32962
|
112 |
proof cases
|
wenzelm@32962
|
113 |
assume eq: "i = Suc k"
|
wenzelm@32962
|
114 |
show ?thesis
|
wenzelm@32962
|
115 |
proof
|
wenzelm@32962
|
116 |
assume "f i = f j"
|
wenzelm@32962
|
117 |
hence "f (Suc k) = f j" by (simp add: eq)
|
wenzelm@32962
|
118 |
with nex and j and eq show False by iprover
|
wenzelm@32962
|
119 |
qed
|
wenzelm@32962
|
120 |
next
|
wenzelm@32962
|
121 |
assume "i \<noteq> Suc k"
|
wenzelm@32962
|
122 |
with k have "Suc (Suc k) \<le> i" by simp
|
wenzelm@32962
|
123 |
thus ?thesis using i and j by (rule Suc)
|
wenzelm@32962
|
124 |
qed
|
wenzelm@32962
|
125 |
qed
|
wenzelm@32962
|
126 |
thus ?thesis by (iprover intro: le_SucI)
|
berghofe@17024
|
127 |
qed
|
berghofe@17024
|
128 |
qed
|
berghofe@17024
|
129 |
}
|
berghofe@17024
|
130 |
note r = this
|
berghofe@17024
|
131 |
show ?case by (rule r) simp_all
|
berghofe@17024
|
132 |
qed
|
berghofe@17024
|
133 |
|
berghofe@17024
|
134 |
text {*
|
berghofe@17024
|
135 |
The following proof, although quite elegant from a mathematical point of view,
|
berghofe@17024
|
136 |
leads to an exponential program:
|
berghofe@17024
|
137 |
*}
|
berghofe@17024
|
138 |
|
berghofe@17024
|
139 |
theorem pigeonhole_slow:
|
berghofe@17024
|
140 |
"\<And>f. (\<And>i. i \<le> Suc n \<Longrightarrow> f i \<le> n) \<Longrightarrow> \<exists>i j. i \<le> Suc n \<and> j < i \<and> f i = f j"
|
berghofe@17024
|
141 |
proof (induct n)
|
berghofe@17024
|
142 |
case 0
|
berghofe@17024
|
143 |
have "Suc 0 \<le> Suc 0" ..
|
berghofe@17024
|
144 |
moreover have "0 < Suc 0" ..
|
berghofe@17024
|
145 |
moreover from 0 have "f (Suc 0) = f 0" by simp
|
nipkow@17604
|
146 |
ultimately show ?case by iprover
|
berghofe@17024
|
147 |
next
|
berghofe@17024
|
148 |
case (Suc n)
|
berghofe@25418
|
149 |
from search [OF nat_eq_dec] show ?case
|
berghofe@17024
|
150 |
proof
|
berghofe@17024
|
151 |
assume "\<exists>j < Suc (Suc n). f (Suc (Suc n)) = f j"
|
nipkow@17604
|
152 |
thus ?case by (iprover intro: le_refl)
|
berghofe@17024
|
153 |
next
|
berghofe@17024
|
154 |
assume "\<not> (\<exists>j < Suc (Suc n). f (Suc (Suc n)) = f j)"
|
nipkow@17604
|
155 |
hence nex: "\<forall>j < Suc (Suc n). f (Suc (Suc n)) \<noteq> f j" by iprover
|
berghofe@17024
|
156 |
let ?f = "\<lambda>i. if f i = Suc n then f (Suc (Suc n)) else f i"
|
berghofe@17024
|
157 |
have "\<And>i. i \<le> Suc n \<Longrightarrow> ?f i \<le> n"
|
berghofe@17024
|
158 |
proof -
|
berghofe@17024
|
159 |
fix i assume i: "i \<le> Suc n"
|
berghofe@17024
|
160 |
show "?thesis i"
|
berghofe@17024
|
161 |
proof (cases "f i = Suc n")
|
wenzelm@32962
|
162 |
case True
|
wenzelm@32962
|
163 |
from i and nex have "f (Suc (Suc n)) \<noteq> f i" by simp
|
wenzelm@32962
|
164 |
with True have "f (Suc (Suc n)) \<noteq> Suc n" by simp
|
wenzelm@32962
|
165 |
moreover from Suc have "f (Suc (Suc n)) \<le> Suc n" by simp
|
wenzelm@32962
|
166 |
ultimately have "f (Suc (Suc n)) \<le> n" by simp
|
wenzelm@32962
|
167 |
with True show ?thesis by simp
|
berghofe@17024
|
168 |
next
|
wenzelm@32962
|
169 |
case False
|
wenzelm@32962
|
170 |
from Suc and i have "f i \<le> Suc n" by simp
|
wenzelm@32962
|
171 |
with False show ?thesis by simp
|
berghofe@17024
|
172 |
qed
|
berghofe@17024
|
173 |
qed
|
berghofe@17024
|
174 |
hence "\<exists>i j. i \<le> Suc n \<and> j < i \<and> ?f i = ?f j" by (rule Suc)
|
berghofe@17024
|
175 |
then obtain i j where i: "i \<le> Suc n" and ji: "j < i" and f: "?f i = ?f j"
|
nipkow@17604
|
176 |
by iprover
|
berghofe@17024
|
177 |
have "f i = f j"
|
berghofe@17024
|
178 |
proof (cases "f i = Suc n")
|
berghofe@17024
|
179 |
case True
|
berghofe@17024
|
180 |
show ?thesis
|
berghofe@17024
|
181 |
proof (cases "f j = Suc n")
|
wenzelm@32962
|
182 |
assume "f j = Suc n"
|
wenzelm@32962
|
183 |
with True show ?thesis by simp
|
berghofe@17024
|
184 |
next
|
wenzelm@32962
|
185 |
assume "f j \<noteq> Suc n"
|
wenzelm@32962
|
186 |
moreover from i ji nex have "f (Suc (Suc n)) \<noteq> f j" by simp
|
wenzelm@32962
|
187 |
ultimately show ?thesis using True f by simp
|
berghofe@17024
|
188 |
qed
|
berghofe@17024
|
189 |
next
|
berghofe@17024
|
190 |
case False
|
berghofe@17024
|
191 |
show ?thesis
|
berghofe@17024
|
192 |
proof (cases "f j = Suc n")
|
wenzelm@32962
|
193 |
assume "f j = Suc n"
|
wenzelm@32962
|
194 |
moreover from i nex have "f (Suc (Suc n)) \<noteq> f i" by simp
|
wenzelm@32962
|
195 |
ultimately show ?thesis using False f by simp
|
berghofe@17024
|
196 |
next
|
wenzelm@32962
|
197 |
assume "f j \<noteq> Suc n"
|
wenzelm@32962
|
198 |
with False f show ?thesis by simp
|
berghofe@17024
|
199 |
qed
|
berghofe@17024
|
200 |
qed
|
berghofe@17024
|
201 |
moreover from i have "i \<le> Suc (Suc n)" by simp
|
nipkow@17604
|
202 |
ultimately show ?thesis using ji by iprover
|
berghofe@17024
|
203 |
qed
|
berghofe@17024
|
204 |
qed
|
berghofe@17024
|
205 |
|
berghofe@17024
|
206 |
extract pigeonhole pigeonhole_slow
|
berghofe@17024
|
207 |
|
berghofe@17024
|
208 |
text {*
|
berghofe@17024
|
209 |
The programs extracted from the above proofs look as follows:
|
berghofe@17024
|
210 |
@{thm [display] pigeonhole_def}
|
berghofe@17024
|
211 |
@{thm [display] pigeonhole_slow_def}
|
berghofe@17024
|
212 |
The program for searching for an element in an array is
|
berghofe@17024
|
213 |
@{thm [display,eta_contract=false] search_def}
|
berghofe@17024
|
214 |
The correctness statement for @{term "pigeonhole"} is
|
berghofe@17024
|
215 |
@{thm [display] pigeonhole_correctness [no_vars]}
|
berghofe@17024
|
216 |
|
berghofe@17024
|
217 |
In order to analyze the speed of the above programs,
|
berghofe@17024
|
218 |
we generate ML code from them.
|
berghofe@17024
|
219 |
*}
|
berghofe@17024
|
220 |
|
haftmann@27982
|
221 |
instantiation nat :: default
|
haftmann@27982
|
222 |
begin
|
haftmann@27982
|
223 |
|
haftmann@27982
|
224 |
definition "default = (0::nat)"
|
haftmann@27982
|
225 |
|
haftmann@27982
|
226 |
instance ..
|
haftmann@27982
|
227 |
|
haftmann@27982
|
228 |
end
|
haftmann@27982
|
229 |
|
haftmann@27982
|
230 |
instantiation * :: (default, default) default
|
haftmann@27982
|
231 |
begin
|
haftmann@27982
|
232 |
|
haftmann@27982
|
233 |
definition "default = (default, default)"
|
haftmann@27982
|
234 |
|
haftmann@27982
|
235 |
instance ..
|
haftmann@27982
|
236 |
|
haftmann@27982
|
237 |
end
|
haftmann@27982
|
238 |
|
haftmann@20837
|
239 |
definition
|
haftmann@23810
|
240 |
"test n u = pigeonhole n (\<lambda>m. m - 1)"
|
wenzelm@21404
|
241 |
definition
|
haftmann@23810
|
242 |
"test' n u = pigeonhole_slow n (\<lambda>m. m - 1)"
|
haftmann@22507
|
243 |
definition
|
haftmann@22507
|
244 |
"test'' u = pigeonhole 8 (op ! [0, 1, 2, 3, 4, 5, 6, 3, 7, 8])"
|
haftmann@20837
|
245 |
|
haftmann@37287
|
246 |
ML "timeit (@{code test} 10)"
|
haftmann@37287
|
247 |
ML "timeit (@{code test'} 10)"
|
haftmann@37287
|
248 |
ML "timeit (@{code test} 20)"
|
haftmann@37287
|
249 |
ML "timeit (@{code test'} 20)"
|
haftmann@37287
|
250 |
ML "timeit (@{code test} 25)"
|
haftmann@37287
|
251 |
ML "timeit (@{code test'} 25)"
|
haftmann@37287
|
252 |
ML "timeit (@{code test} 500)"
|
haftmann@37287
|
253 |
ML "timeit @{code test''}"
|
haftmann@37287
|
254 |
|
haftmann@37287
|
255 |
consts_code
|
haftmann@37287
|
256 |
"default :: nat" ("{* 0::nat *}")
|
haftmann@37287
|
257 |
"default :: nat \<times> nat" ("{* (0::nat, 0::nat) *}")
|
haftmann@37287
|
258 |
|
haftmann@27436
|
259 |
code_module PH
|
haftmann@22507
|
260 |
contains
|
haftmann@22507
|
261 |
test = test
|
haftmann@22507
|
262 |
test' = test'
|
haftmann@22507
|
263 |
test'' = test''
|
haftmann@22507
|
264 |
|
haftmann@27436
|
265 |
ML "timeit (PH.test 10)"
|
haftmann@27436
|
266 |
ML "timeit (PH.test' 10)"
|
haftmann@27436
|
267 |
ML "timeit (PH.test 20)"
|
haftmann@27436
|
268 |
ML "timeit (PH.test' 20)"
|
haftmann@27436
|
269 |
ML "timeit (PH.test 25)"
|
haftmann@27436
|
270 |
ML "timeit (PH.test' 25)"
|
haftmann@27436
|
271 |
ML "timeit (PH.test 500)"
|
haftmann@27436
|
272 |
ML "timeit PH.test''"
|
haftmann@20837
|
273 |
|
berghofe@17024
|
274 |
end
|
haftmann@37287
|
275 |
|