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