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