17024

1 
(* Title: HOL/Extraction/Pigeonhole.thy


2 
ID: $Id$


3 
Author: Stefan Berghofer, TU Muenchen


4 
*)


5 


6 
header {* The pigeonhole principle *}


7 


8 
theory Pigeonhole imports EfficientNat begin


9 


10 
text {*


11 
We formalize two proofs of the pigeonhole principle, which lead


12 
to extracted programs of quite different complexity. The original


13 
formalization of these proofs in {\sc Nuprl} is due to


14 
Aleksey Nogin \cite{NoginENTCS2000}.


15 


16 
We need decidability of equality on natural numbers:


17 
*}


18 

21127

19 
lemma nat_eq_dec: "(m\<Colon>nat) = n \<or> m \<noteq> n"


20 
apply (induct m arbitrary: n)

17024

21 
apply (case_tac n)


22 
apply (case_tac [3] n)

17604

23 
apply (simp only: nat.simps, iprover?)+

17024

24 
done


25 


26 
text {*

17027

27 
We can decide whether an array @{term "f"} of length @{term "l"}

17024

28 
contains an element @{term "x"}.


29 
*}


30 


31 
lemma search: "(\<exists>j<(l::nat). (x::nat) = f j) \<or> \<not> (\<exists>j<l. x = f j)"


32 
proof (induct l)


33 
case 0


34 
have "\<not> (\<exists>j<0. x = f j)"


35 
proof


36 
assume "\<exists>j<0. x = f j"

17604

37 
then obtain j where j: "j < (0::nat)" by iprover

17024

38 
thus "False" by simp


39 
qed


40 
thus ?case ..


41 
next


42 
case (Suc l)


43 
thus ?case


44 
proof


45 
assume "\<exists>j<l. x = f j"


46 
then obtain j where j: "j < l"

17604

47 
and eq: "x = f j" by iprover

17024

48 
from j have "j < Suc l" by simp

17604

49 
with eq show ?case by iprover

17024

50 
next


51 
assume nex: "\<not> (\<exists>j<l. x = f j)"


52 
from nat_eq_dec show ?case


53 
proof


54 
assume eq: "x = f l"


55 
have "l < Suc l" by simp

17604

56 
with eq show ?case by iprover

17024

57 
next


58 
assume neq: "x \<noteq> f l"


59 
have "\<not> (\<exists>j<Suc l. x = f j)"


60 
proof


61 
assume "\<exists>j<Suc l. x = f j"


62 
then obtain j where j: "j < Suc l"

17604

63 
and eq: "x = f j" by iprover

17024

64 
show False


65 
proof cases


66 
assume "j = l"


67 
with eq have "x = f l" by simp


68 
with neq show False ..


69 
next


70 
assume "j \<noteq> l"


71 
with j have "j < l" by simp

17604

72 
with nex and eq show False by iprover

17024

73 
qed


74 
qed


75 
thus ?case ..


76 
qed


77 
qed


78 
qed


79 


80 
text {*


81 
This proof yields a polynomial program.


82 
*}


83 


84 
theorem pigeonhole:


85 
"\<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"


86 
proof (induct n)


87 
case 0


88 
hence "Suc 0 \<le> Suc 0 \<and> 0 < Suc 0 \<and> f (Suc 0) = f 0" by simp

17604

89 
thus ?case by iprover

17024

90 
next


91 
case (Suc n)


92 
{


93 
fix k


94 
have


95 
"k \<le> Suc (Suc n) \<Longrightarrow>


96 
(\<And>i j. Suc k \<le> i \<Longrightarrow> i \<le> Suc (Suc n) \<Longrightarrow> j < i \<Longrightarrow> f i \<noteq> f j) \<Longrightarrow>


97 
(\<exists>i j. i \<le> k \<and> j < i \<and> f i = f j)"


98 
proof (induct k)


99 
case 0


100 
let ?f = "\<lambda>i. if f i = Suc n then f (Suc (Suc n)) else f i"


101 
have "\<not> (\<exists>i j. i \<le> Suc n \<and> j < i \<and> ?f i = ?f j)"


102 
proof


103 
assume "\<exists>i j. i \<le> Suc n \<and> j < i \<and> ?f i = ?f j"


104 
then obtain i j where i: "i \<le> Suc n" and j: "j < i"

17604

105 
and f: "?f i = ?f j" by iprover

17024

106 
from j have i_nz: "Suc 0 \<le> i" by simp


107 
from i have iSSn: "i \<le> Suc (Suc n)" by simp


108 
have S0SSn: "Suc 0 \<le> Suc (Suc n)" by simp


109 
show False


110 
proof cases


111 
assume fi: "f i = Suc n"


112 
show False


113 
proof cases


114 
assume fj: "f j = Suc n"


115 
from i_nz and iSSn and j have "f i \<noteq> f j" by (rule 0)


116 
moreover from fi have "f i = f j"


117 
by (simp add: fj [symmetric])


118 
ultimately show ?thesis ..


119 
next


120 
from i and j have "j < Suc (Suc n)" by simp


121 
with S0SSn and le_refl have "f (Suc (Suc n)) \<noteq> f j"


122 
by (rule 0)


123 
moreover assume "f j \<noteq> Suc n"


124 
with fi and f have "f (Suc (Suc n)) = f j" by simp


125 
ultimately show False ..


126 
qed


127 
next


128 
assume fi: "f i \<noteq> Suc n"


129 
show False


130 
proof cases


131 
from i have "i < Suc (Suc n)" by simp


132 
with S0SSn and le_refl have "f (Suc (Suc n)) \<noteq> f i"


133 
by (rule 0)


134 
moreover assume "f j = Suc n"


135 
with fi and f have "f (Suc (Suc n)) = f i" by simp


136 
ultimately show False ..


137 
next


138 
from i_nz and iSSn and j


139 
have "f i \<noteq> f j" by (rule 0)


140 
moreover assume "f j \<noteq> Suc n"


141 
with fi and f have "f i = f j" by simp


142 
ultimately show False ..


143 
qed


144 
qed


145 
qed


146 
moreover have "\<And>i. i \<le> Suc n \<Longrightarrow> ?f i \<le> n"


147 
proof 


148 
fix i assume "i \<le> Suc n"


149 
hence i: "i < Suc (Suc n)" by simp


150 
have "f (Suc (Suc n)) \<noteq> f i"


151 
by (rule 0) (simp_all add: i)


152 
moreover have "f (Suc (Suc n)) \<le> Suc n"


153 
by (rule Suc) simp


154 
moreover from i have "i \<le> Suc (Suc n)" by simp


155 
hence "f i \<le> Suc n" by (rule Suc)


156 
ultimately show "?thesis i"


157 
by simp


158 
qed


159 
hence "\<exists>i j. i \<le> Suc n \<and> j < i \<and> ?f i = ?f j"


160 
by (rule Suc)


161 
ultimately show ?case ..


162 
next


163 
case (Suc k)


164 
from search show ?case


165 
proof


166 
assume "\<exists>j<Suc k. f (Suc k) = f j"

17604

167 
thus ?case by (iprover intro: le_refl)

17024

168 
next


169 
assume nex: "\<not> (\<exists>j<Suc k. f (Suc k) = f j)"


170 
have "\<exists>i j. i \<le> k \<and> j < i \<and> f i = f j"


171 
proof (rule Suc)


172 
from Suc show "k \<le> Suc (Suc n)" by simp


173 
fix i j assume k: "Suc k \<le> i" and i: "i \<le> Suc (Suc n)"


174 
and j: "j < i"


175 
show "f i \<noteq> f j"


176 
proof cases


177 
assume eq: "i = Suc k"


178 
show ?thesis


179 
proof


180 
assume "f i = f j"


181 
hence "f (Suc k) = f j" by (simp add: eq)

17604

182 
with nex and j and eq show False by iprover

17024

183 
qed


184 
next


185 
assume "i \<noteq> Suc k"


186 
with k have "Suc (Suc k) \<le> i" by simp


187 
thus ?thesis using i and j by (rule Suc)


188 
qed


189 
qed

17604

190 
thus ?thesis by (iprover intro: le_SucI)

17024

191 
qed


192 
qed


193 
}


194 
note r = this


195 
show ?case by (rule r) simp_all


196 
qed


197 


198 
text {*


199 
The following proof, although quite elegant from a mathematical point of view,


200 
leads to an exponential program:


201 
*}


202 


203 
theorem pigeonhole_slow:


204 
"\<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"


205 
proof (induct n)


206 
case 0


207 
have "Suc 0 \<le> Suc 0" ..


208 
moreover have "0 < Suc 0" ..


209 
moreover from 0 have "f (Suc 0) = f 0" by simp

17604

210 
ultimately show ?case by iprover

17024

211 
next


212 
case (Suc n)


213 
from search show ?case


214 
proof


215 
assume "\<exists>j < Suc (Suc n). f (Suc (Suc n)) = f j"

17604

216 
thus ?case by (iprover intro: le_refl)

17024

217 
next


218 
assume "\<not> (\<exists>j < Suc (Suc n). f (Suc (Suc n)) = f j)"

17604

219 
hence nex: "\<forall>j < Suc (Suc n). f (Suc (Suc n)) \<noteq> f j" by iprover

17024

220 
let ?f = "\<lambda>i. if f i = Suc n then f (Suc (Suc n)) else f i"


221 
have "\<And>i. i \<le> Suc n \<Longrightarrow> ?f i \<le> n"


222 
proof 


223 
fix i assume i: "i \<le> Suc n"


224 
show "?thesis i"


225 
proof (cases "f i = Suc n")


226 
case True


227 
from i and nex have "f (Suc (Suc n)) \<noteq> f i" by simp


228 
with True have "f (Suc (Suc n)) \<noteq> Suc n" by simp


229 
moreover from Suc have "f (Suc (Suc n)) \<le> Suc n" by simp


230 
ultimately have "f (Suc (Suc n)) \<le> n" by simp


231 
with True show ?thesis by simp


232 
next


233 
case False


234 
from Suc and i have "f i \<le> Suc n" by simp


235 
with False show ?thesis by simp


236 
qed


237 
qed


238 
hence "\<exists>i j. i \<le> Suc n \<and> j < i \<and> ?f i = ?f j" by (rule Suc)


239 
then obtain i j where i: "i \<le> Suc n" and ji: "j < i" and f: "?f i = ?f j"

17604

240 
by iprover

17024

241 
have "f i = f j"


242 
proof (cases "f i = Suc n")


243 
case True


244 
show ?thesis


245 
proof (cases "f j = Suc n")


246 
assume "f j = Suc n"


247 
with True show ?thesis by simp


248 
next


249 
assume "f j \<noteq> Suc n"


250 
moreover from i ji nex have "f (Suc (Suc n)) \<noteq> f j" by simp


251 
ultimately show ?thesis using True f by simp


252 
qed


253 
next


254 
case False


255 
show ?thesis


256 
proof (cases "f j = Suc n")


257 
assume "f j = Suc n"


258 
moreover from i nex have "f (Suc (Suc n)) \<noteq> f i" by simp


259 
ultimately show ?thesis using False f by simp


260 
next


261 
assume "f j \<noteq> Suc n"


262 
with False f show ?thesis by simp


263 
qed


264 
qed


265 
moreover from i have "i \<le> Suc (Suc n)" by simp

17604

266 
ultimately show ?thesis using ji by iprover

17024

267 
qed


268 
qed


269 


270 
extract pigeonhole pigeonhole_slow


271 


272 
text {*


273 
The programs extracted from the above proofs look as follows:


274 
@{thm [display] pigeonhole_def}


275 
@{thm [display] pigeonhole_slow_def}


276 
The program for searching for an element in an array is


277 
@{thm [display,eta_contract=false] search_def}


278 
The correctness statement for @{term "pigeonhole"} is


279 
@{thm [display] pigeonhole_correctness [no_vars]}


280 


281 
In order to analyze the speed of the above programs,


282 
we generate ML code from them.


283 
*}


284 


285 
consts_code


286 
arbitrary :: "nat \<times> nat" ("{* (0::nat, 0::nat) *}")


287 

17145

288 
code_module PH


289 
contains

17024

290 
test = "\<lambda>n. pigeonhole n (\<lambda>m. m  1)"


291 
test' = "\<lambda>n. pigeonhole_slow n (\<lambda>m. m  1)"


292 
sel = "op !"


293 

17145

294 
ML "timeit (fn () => PH.test 10)"


295 
ML "timeit (fn () => PH.test' 10)"


296 
ML "timeit (fn () => PH.test 20)"


297 
ML "timeit (fn () => PH.test' 20)"


298 
ML "timeit (fn () => PH.test 25)"


299 
ML "timeit (fn () => PH.test' 25)"


300 
ML "timeit (fn () => PH.test 500)"

17024

301 

17145

302 
ML "PH.pigeonhole 8 (PH.sel [0,1,2,3,4,5,6,3,7,8])"

17024

303 

20837

304 
definition


305 
arbitrary_nat :: "nat \<times> nat"

21062

306 
[symmetric, code inline]: "arbitrary_nat = arbitrary"

20933

307 
arbitrary_nat_subst :: "nat \<times> nat"


308 
"arbitrary_nat_subst = (0, 0)"

20837

309 

21062

310 
code_axioms

20933

311 
arbitrary_nat \<equiv> arbitrary_nat_subst

20837

312 


313 
definition


314 
"test n = pigeonhole n (\<lambda>m. m  1)"


315 
"test' n = pigeonhole_slow n (\<lambda>m. m  1)"


316 

21127

317 
code_gen test test' "op !" (SML *)

20837

318 


319 
ML "timeit (fn () => ROOT.Pigeonhole.test 10)"


320 
ML "timeit (fn () => ROOT.Pigeonhole.test' 10)"


321 
ML "timeit (fn () => ROOT.Pigeonhole.test 20)"


322 
ML "timeit (fn () => ROOT.Pigeonhole.test' 20)"


323 
ML "timeit (fn () => ROOT.Pigeonhole.test 25)"


324 
ML "timeit (fn () => ROOT.Pigeonhole.test' 25)"


325 
ML "timeit (fn () => ROOT.Pigeonhole.test 500)"


326 


327 
ML "ROOT.Pigeonhole.pigeonhole 8 (ROOT.List.nth [0,1,2,3,4,5,6,3,7,8])"


328 

17024

329 
end
