Theory Pigeonhole
section ‹The pigeonhole principle›
theory Pigeonhole
imports Util "HOL-Library.Realizers" "HOL-Library.Code_Target_Numeral"
begin
text ‹
We formalize two proofs of the pigeonhole principle, which lead
to extracted programs of quite different complexity. The original
formalization of these proofs in {\sc Nuprl} is due to
Aleksey Nogin \<^cite>‹"Nogin-ENTCS-2000"›.
This proof yields a polynomial program.
›
theorem pigeonhole:
"⋀f. (⋀i. i ≤ Suc n ⟹ f i ≤ n) ⟹ ∃i j. i ≤ Suc n ∧ j < i ∧ f i = f j"
proof (induct n)
case 0
then have "Suc 0 ≤ Suc 0 ∧ 0 < Suc 0 ∧ f (Suc 0) = f 0" by simp
then show ?case by iprover
next
case (Suc n)
have r:
"k ≤ Suc (Suc n) ⟹
(⋀i j. Suc k ≤ i ⟹ i ≤ Suc (Suc n) ⟹ j < i ⟹ f i ≠ f j) ⟹
(∃i j. i ≤ k ∧ j < i ∧ f i = f j)" for k
proof (induct k)
case 0
let ?f = "λi. if f i = Suc n then f (Suc (Suc n)) else f i"
have "¬ (∃i j. i ≤ Suc n ∧ j < i ∧ ?f i = ?f j)"
proof
assume "∃i j. i ≤ Suc n ∧ j < i ∧ ?f i = ?f j"
then obtain i j where i: "i ≤ Suc n" and j: "j < i" and f: "?f i = ?f j"
by iprover
from j have i_nz: "Suc 0 ≤ i" by simp
from i have iSSn: "i ≤ Suc (Suc n)" by simp
have S0SSn: "Suc 0 ≤ Suc (Suc n)" by simp
show False
proof cases
assume fi: "f i = Suc n"
show False
proof cases
assume fj: "f j = Suc n"
from i_nz and iSSn and j have "f i ≠ f j" by (rule 0)
moreover from fi have "f i = f j"
by (simp add: fj [symmetric])
ultimately show ?thesis ..
next
from i and j have "j < Suc (Suc n)" by simp
with S0SSn and le_refl have "f (Suc (Suc n)) ≠ f j"
by (rule 0)
moreover assume "f j ≠ Suc n"
with fi and f have "f (Suc (Suc n)) = f j" by simp
ultimately show False ..
qed
next
assume fi: "f i ≠ Suc n"
show False
proof cases
from i have "i < Suc (Suc n)" by simp
with S0SSn and le_refl have "f (Suc (Suc n)) ≠ f i"
by (rule 0)
moreover assume "f j = Suc n"
with fi and f have "f (Suc (Suc n)) = f i" by simp
ultimately show False ..
next
from i_nz and iSSn and j
have "f i ≠ f j" by (rule 0)
moreover assume "f j ≠ Suc n"
with fi and f have "f i = f j" by simp
ultimately show False ..
qed
qed
qed
moreover have "?f i ≤ n" if "i ≤ Suc n" for i
proof -
from that have i: "i < Suc (Suc n)" by simp
have "f (Suc (Suc n)) ≠ f i"
by (rule 0) (simp_all add: i)
moreover have "f (Suc (Suc n)) ≤ Suc n"
by (rule Suc) simp
moreover from i have "i ≤ Suc (Suc n)" by simp
then have "f i ≤ Suc n" by (rule Suc)
ultimately show ?thesis
by simp
qed
then have "∃i j. i ≤ Suc n ∧ j < i ∧ ?f i = ?f j"
by (rule Suc)
ultimately show ?case ..
next
case (Suc k)
from search [OF nat_eq_dec] show ?case
proof
assume "∃j<Suc k. f (Suc k) = f j"
then show ?case by (iprover intro: le_refl)
next
assume nex: "¬ (∃j<Suc k. f (Suc k) = f j)"
have "∃i j. i ≤ k ∧ j < i ∧ f i = f j"
proof (rule Suc)
from Suc show "k ≤ Suc (Suc n)" by simp
fix i j assume k: "Suc k ≤ i" and i: "i ≤ Suc (Suc n)"
and j: "j < i"
show "f i ≠ f j"
proof cases
assume eq: "i = Suc k"
show ?thesis
proof
assume "f i = f j"
then have "f (Suc k) = f j" by (simp add: eq)
with nex and j and eq show False by iprover
qed
next
assume "i ≠ Suc k"
with k have "Suc (Suc k) ≤ i" by simp
then show ?thesis using i and j by (rule Suc)
qed
qed
then show ?thesis by (iprover intro: le_SucI)
qed
qed
show ?case by (rule r) simp_all
qed
text ‹
The following proof, although quite elegant from a mathematical point of view,
leads to an exponential program:
›
theorem pigeonhole_slow:
"⋀f. (⋀i. i ≤ Suc n ⟹ f i ≤ n) ⟹ ∃i j. i ≤ Suc n ∧ j < i ∧ f i = f j"
proof (induct n)
case 0
have "Suc 0 ≤ Suc 0" ..
moreover have "0 < Suc 0" ..
moreover from 0 have "f (Suc 0) = f 0" by simp
ultimately show ?case by iprover
next
case (Suc n)
from search [OF nat_eq_dec] show ?case
proof
assume "∃j < Suc (Suc n). f (Suc (Suc n)) = f j"
then show ?case by (iprover intro: le_refl)
next
assume "¬ (∃j < Suc (Suc n). f (Suc (Suc n)) = f j)"
then have nex: "∀j < Suc (Suc n). f (Suc (Suc n)) ≠ f j" by iprover
let ?f = "λi. if f i = Suc n then f (Suc (Suc n)) else f i"
have "⋀i. i ≤ Suc n ⟹ ?f i ≤ n"
proof -
fix i assume i: "i ≤ Suc n"
show "?thesis i"
proof (cases "f i = Suc n")
case True
from i and nex have "f (Suc (Suc n)) ≠ f i" by simp
with True have "f (Suc (Suc n)) ≠ Suc n" by simp
moreover from Suc have "f (Suc (Suc n)) ≤ Suc n" by simp
ultimately have "f (Suc (Suc n)) ≤ n" by simp
with True show ?thesis by simp
next
case False
from Suc and i have "f i ≤ Suc n" by simp
with False show ?thesis by simp
qed
qed
then have "∃i j. i ≤ Suc n ∧ j < i ∧ ?f i = ?f j" by (rule Suc)
then obtain i j where i: "i ≤ Suc n" and ji: "j < i" and f: "?f i = ?f j"
by iprover
have "f i = f j"
proof (cases "f i = Suc n")
case True
show ?thesis
proof (cases "f j = Suc n")
assume "f j = Suc n"
with True show ?thesis by simp
next
assume "f j ≠ Suc n"
moreover from i ji nex have "f (Suc (Suc n)) ≠ f j" by simp
ultimately show ?thesis using True f by simp
qed
next
case False
show ?thesis
proof (cases "f j = Suc n")
assume "f j = Suc n"
moreover from i nex have "f (Suc (Suc n)) ≠ f i" by simp
ultimately show ?thesis using False f by simp
next
assume "f j ≠ Suc n"
with False f show ?thesis by simp
qed
qed
moreover from i have "i ≤ Suc (Suc n)" by simp
ultimately show ?thesis using ji by iprover
qed
qed
extract pigeonhole pigeonhole_slow
text ‹
The programs extracted from the above proofs look as follows:
@{thm [display] pigeonhole_def}
@{thm [display] pigeonhole_slow_def}
The program for searching for an element in an array is
@{thm [display,eta_contract=false] search_def}
The correctness statement for \<^term>‹pigeonhole› is
@{thm [display] pigeonhole_correctness [no_vars]}
In order to analyze the speed of the above programs,
we generate ML code from them.
›
instantiation nat :: default
begin
definition "default = (0::nat)"
instance ..
end
instantiation prod :: (default, default) default
begin
definition "default = (default, default)"
instance ..
end
definition "test n u = pigeonhole (nat_of_integer n) (λm. m - 1)"
definition "test' n u = pigeonhole_slow (nat_of_integer n) (λm. m - 1)"
definition "test'' u = pigeonhole 8 (List.nth [0, 1, 2, 3, 4, 5, 6, 3, 7, 8])"
ML_val "timeit (@{code test} 10)"
ML_val "timeit (@{code test'} 10)"
ML_val "timeit (@{code test} 20)"
ML_val "timeit (@{code test'} 20)"
ML_val "timeit (@{code test} 25)"
ML_val "timeit (@{code test'} 25)"
ML_val "timeit (@{code test} 500)"
ML_val "timeit @{code test''}"
end