/
pigeons.tex
406 lines (359 loc) · 12.4 KB
/
pigeons.tex
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
\documentclass[a4paper,10pt,draft]{article}
\usepackage{times}
\usepackage[T1]{fontenc}
\usepackage{a4wide}
\usepackage{ucs}
\usepackage[utf8x]{inputenc}
\usepackage{amsmath}
\usepackage[noxy]{virginialake}
\usepackage[pdftex,pdfborder={0 0 0}]{hyperref}
\usepackage{amsthm}
\theoremstyle{plain}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{corollary}[theorem]{Corollary}
\theoremstyle{definition}
\newtheorem{definition}[theorem]{Definition}
\newtheorem{remark}[theorem]{Remark}
\newtheorem{notation}[theorem]{Notation}
\newtheorem{para}[theorem]{}
\title{Polynomial Proof of the Pigeon Hole Principle}
\author{Lutz and Tom}
\begin{document}
\maketitle
\newcommand{\fff }{{\mathsf{f}}}
\newcommand{\ttt }{{\mathsf{t}}}
\newcommand{\ai }{{\mathsf{ai}}}
\newcommand{\aw }{{\mathsf{aw}}}
\newcommand{\ac }{{\mathsf{ac}}}
\newcommand{\aid }{{\ai{\downarrow}}}
\newcommand{\awd }{{\aw{\downarrow}}}
\newcommand{\acd }{{\ac{\downarrow}}}
\newcommand{\aiu }{{\ai{\uparrow}}}
\newcommand{\awu }{{\aw{\uparrow}}}
\newcommand{\acu }{{\ac{\uparrow}}}
\newcommand{\swi }{\mathsf{s}}
\newcommand{\med }{\mathsf{m}}
\newcommand{\asor }{{=_\mathsf{a}{\downarrow}}}
\newcommand{\asand}{{=_\mathsf{a}{\uparrow}}}
\newcommand{\coor }{{=_{\vee\mathsf{c}}}}
\newcommand{\coand}{{=_{\wedge\mathsf{c}}}}
\newcommand{\fffd }{{{=_{\fff}}{\downarrow}}}
\newcommand{\fffu }{{{=_{\fff}}{\uparrow}}}
\newcommand{\tttd }{{{=_{\ttt}}{\downarrow}}}
\newcommand{\tttu }{{{=_{\ttt}}{\uparrow}}}
\newcommand{\tttord }{{{=_{\ttt\vee}}{\downarrow}}}
\newcommand{\fffandd }{{{=_{\fff\wedge}}{\downarrow}}}
\newcommand{\tttoru }{{{=_{\ttt\vee}}{\uparrow}}}
\newcommand{\fffandu }{{{=_{\fff\wedge}}{\uparrow}}}
\newcommand{\AND}[2]{\bigwedge_{#1}^{#2}}
\newcommand{\OR}[2]{\bigvee_{#1}^{#2}}
\newcommand{\Count}{\mathsf{Count}}
\newcommand{\PHP}[1]{\mathsf{PHP}_{#1}}
\begin{remark}
We will encode numbers by sequences of formulae. When we define operations on numbers, we expect the inputs to have the same number of bits, and the output will increase the number of bits if and only if this is necessary to ensure there is no overflow.
\end{remark}
\newcommand{\Add}{\mathsf{Add}}
\begin{lemma}\label{lem:basics}
Some basic results
\begin{enumerate}
% \item
% \[
% \vlproof{}{}{\Add(a,b)=\Add(b,a)}
% \quad,\]
% \item
% \[
% \vlder{}{}{\Add(a_1,a_2)<\Add(b_1,b_2)}{\vls(a_1\leq b_1.a_2< b_2)}
% \]
\item
\[
\vlder{}{}{a>c}{\vls(a>b.b=c)}
\]
\item
\[
\vlder{}{}{c<a}{\vls(b>a.b=c)}
\quad,\quad\text{and}\]
\item
\[
\vlder{}{}{\vls[a_1> b_1.a_2> b_2]}{\Add(a_1,a_2)>\Add(b_1,b_2)}
\quad.
\]
\end{enumerate}
\end{lemma}
\newcommand{\AddCarryF}{\mathsf{AddCarry4}}
\newcommand{\AddSaveF}{\mathsf{AddSave4}}
\newcommand{\AddCarry}{\mathsf{AddCarry}}
\newcommand{\AddSave}{\mathsf{AddSave}}
\newcommand{\CountCarry}{\mathsf{CountCarry}}
\newcommand{\CountSave}{\mathsf{CountSave}}
\begin{definition}
Definitions of some predicates:
\begin{itemize}
\item $\AddCarryF(\vec a,\vec b,\vec c,\vec d)=\AddCarry(\AddCarry(\vec a,\vec b,\vec c),\AddSave(\vec a,\vec b,\vec c),\vec d)$,
\item $\AddSaveF(\vec a,\vec b,\vec c,\vec d)=\AddSave(\AddCarry(\vec a,\vec b,\vec c),\AddSave(\vec a,\vec b,\vec c),\vec d)$,
\item $\CountCarry(a_1)=\fff$,
\item $\CountCarry(a_1,\dots,a_{2^\rho})=\AddCarryF(\CountCarry(a_1,\dots,a_{2^{\rho-1}}),\CountSave(a_1,\dots,a_{2^{\rho-1}}),\CountCarry(a_{2^{\rho-1}+1},\dots,a_{2^\rho}),\CountSave(a_{2^{\rho-1}+1},\dots,a_{2^\rho}))$,
\item $\CountSave(a_1)=a_1$,
\item $\CountSave(a_1,\dots,a_{2^\rho})=\AddSaveF(\CountCarry(a_1,\dots,a_{2^{\rho-1}}),\CountSave(a_1,\dots,a_{2^{\rho-1}}),\CountCarry(a_{2^{\rho-1}+1},\dots,a_{2^\rho}),\CountSave(a_{2^{\rho-1}+1},\dots,a_{2^\rho}))$, and
\item $\Count(a_1,\dots,a_{2^\rho}) = \Add(\CountCarry(a_1,\dots,a_{2^\rho}),\CountSave(a_1,\dots,a_{2^\rho}))$
\end{itemize}
\end{definition}
% AddCarry(as,bs,cs)=zipWith3 xor as bs cs
% AddSave(as,bs,cs)=zipWith3
%
% CountCarry(a_1) = \fff
% CountCarry(as++bs) = AddCarry4(CountCarry(as),CountSave(as),CountCarry(bs),CountSave(bs))
% CountSave(a_1) = a_1
% CountSave(as++bs) = AddSave4(CountCarry(as),CountSave(as),CountCarry(bs),CountSave(bs))
%
% Count(a_1,\dots,a_n) = Add(CountCarry(a_1,\dots,a_n),CountSave(a_1,\dots,a_n))
\begin{lemma}\label{lem:CSAdd4}
Carry-save addition is correct with respect to normal addition
\[
\vlproof{}{}
{
\Add(\AddCarryF(a,b,c,d),\AddSaveF(a,b,c,d))=\Add(\Add(a,b),\Add(c,d))
}
\]
\end{lemma}
\begin{lemma}\label{lem:count-decomp}
\[\vlproof{}{}{\Add(\Count(\vec b_1), \Count(\vec b_2))=\Count(\vec b_1,\vec b_2)}\]
\end{lemma}
All the above definitions and results are only there to prove the following two results (so whatever is not needed can be changed or removed):
\begin{lemma}\label{lem:at-most-full}
$\Count$ is bounded by its number of arguments
\[
\vlproof{}{}{n\geq\Count(a_1,\dots,a_n)}
\quad.\]
\end{lemma}
\begin{proof}
By induction. The base case is:
\[
\vlproof{}{}{1\geq\Count(a)}
\quad.
\]
The inductive case is:
\[
\vlderivation
{
\vlde{}{}
{
n\geq\Count(a_1,\dots,a_n)
}
{
\vlde{}{}
{
\Add(n/2,n/2)\geq\Add(\Count(a_1,\dots,a_{n/2}),\Count(a_{n/2+1},\dots,a_n))
}
{
\vlhy
{
\vls(n/2\geq\Count(a_1,\dots,a_{n/2}).n/2\geq\Count(a_{n/2+1},\dots,a_n))
}
}
}
}
\quad.
\]
\end{proof}
\begin{lemma}\label{lem:push-comparisons-one-step}
Given two sets of atoms, if the count of the first set is greater than the count of the second set, then either the count of the first half of the first set is greater than the count of the first half of the second set, or the count of the second half of the first set is greater than the count of the second half of the second set.
Given atoms $a_1$, $\dots$, $a_{2^\rho}$ and $b_1$, $\dots$, $b_{2^\rho}$, the following derivation can be constructed:
\[
\vlder{}{}
{
\vls
[
\Count(a_1, \dots, a_{2^{\rho-1}})>\Count(b_1, \dots, b_{2^{\rho-1}})
.
\Count(a_{2^{\rho-1}+1}, \dots, a_{2^\rho})>\Count(b_{2^{\rho-1}+1}, \dots, b_{2^\rho})
]
}
{
\Count(a_1, \dots, a_{2^\rho})>\Count(b_1, \dots, b_{2^\rho})
}
\quad.\]
\end{lemma}
\begin{proof}
By Lemmas~\ref{lem:basics} and \ref{lem:CSAdd4}:
\[
\vlderivation{
\vlde{\Phi_3}{}
{
\vls
[
\Count(a_1, \dots, a_{2^{\rho-1}})>\Count(b_1, \dots, b_{2^{\rho-1}})
.
\Count(a_{2^{\rho-1}+1}, \dots, a_{2^\rho})>\Count(b_{2^{\rho-1}+1}, \dots, b_{2^\rho})
]
}
{
\vlde{\Phi_2}{}
{
\Add(\Count(a_1, \dots, a_{2^{\rho-1}}),\Count(a_{2^{\rho-1}+1}, \dots, a_{2^\rho}))>\Add(\Count(b_1, \dots, b_{2^{\rho-1}}),\Count(b_{2^{\rho-1}+1}, \dots, b_{2^\rho}))
}
{
\vlde{\Phi_1}{}
{
\Add(\Count(a_1, \dots, a_{2^{\rho-1}}),\Count(a_{2^{\rho-1}+1}, \dots, a_{2^\rho}))>\Count(b_1, \dots, b_{2^\rho})
}
{
\vlhy
{
\Count(a_1, \dots, a_{2^\rho})>\Count(b_1, \dots, b_{2^\rho})
}
}
}
}
}
\quad.\]
\begin{itemize}
\item $\Phi_1$ relies on: $\vlder{}{}{\vls[a_1>b_1.a_2>b_2]}{\Add(a_1,a_2)>\Add(b_1,b_2)}$;
\item $\Phi_2$ relies on: $\vlder{}{}{\vls(a>b.b=c)}{a>c}\;$ and Lemma~\ref{lem:count-decomp}; and
\item $\Phi_3$ relies on: $\vlder{}{}{\vls(b>a.b=c)}{c>a}\;$ and Lemma~\ref{lem:count-decomp}.
\end{itemize}
\end{proof}
\begin{definition}
This is the intuitive meaning of the atoms and predicates we will use:
\begin{itemize}
\item $p_{i,j}$: pigeon $i$ is in hole $j$;
\item $r_j^m\leftrightarrow\OR{i=0}{m}p_{i,j}$: one of the first $m+1$ pigeons is in hole $j$;
\item $\Count(r_0^m,\dots,r_{n-1}^m)$: the number of holes inhabited by one of the first $m+1$ pigeons; and
\item $\PHP{n}$: if there are $n+1$ pigeons and $n$ holes, and every pigeon is in a hole, then there is a hole with two pigeons.
\end{itemize}
\end{definition}
\begin{lemma}\label{lem:push-comparisons}
Select a subset of the holes, by dividing the holes in two $\rho$ times and picking the $t^\text{th}$ subset, so obtained. If adding the $m+2^\text{nd}$ pigeon decreases the number of the selected holes that are inhabited, and at most all of the selected holes are inhabited, then one of the selected holes was inhabited by one of the first $m+1$ pigeons, but not by the first $m+2$.
For $0\leq\rho$, such that $2^\rho<n$ and $0\leq t\leq n$.
\[
\vlder{}{}
{
\OR{j={t2^\rho}}{(t+1)2^\rho-1}\vlsbr(r_j^m.\bar r_j^{m+1})
}
{
\vls(\Count(r_{t2^\rho}^m,\dots,r_{(t+1)2^\rho-1}^m)>\Count(r_{t(2^\rho)}^{m+1},\dots,r_{(t+1)2^\rho-1}^{m+1}).2^\rho>\Count(r_{t2^\rho}^{m+1},\dots,r_{(t+1)2^\rho-1}^{m+1}))
}
\quad.\]
\end{lemma}
\begin{proof}
By induction and Lemma~\ref{lem:push-comparisons-one-step}.
\end{proof}
\begin{lemma}\label{lem:decrease:evacuation}
If adding the $m+2^\text{nd}$ pigeon decreased the number of inhabited holes,
then there is a hole that was inhabited by one of the first $m+1$ pigeons, but is not inhabited by one of the first $m+2$ pigeons.
\[
\vlder{}{}
{
\OR{j=0}{n-1}\vlsbr(r_j^m.\bar r_j^{m+1})
}
{
\Count(r_0^m,\dots,r_{n-1}^m)>\Count(r_0^{m+1},\dots,r_{n-1}^{m+1})
}
\quad.\]
\end{lemma}
\begin{proof}
By Lemma~\ref{lem:push-comparisons}.
\end{proof}
\begin{lemma}\label{lem:not-increasing:no-new-hole_subtract}
If adding the $m+2^\text{nd}$ pigeon did not increase the number of inhabited holes,
then either every hole inhabited by one of the $m+2$ first pigeons was also inhabited by one of the $m+1$ first pigeons,
or there is a hole that was inhabited by one of the first $m+1$ pigeons, but is not inhabited by one of the first $m+2$ pigeons.
\[
\vlder{}{}{\vlsbr[\AND{j=0}{n-1}\vlsbr[r_j^m.\bar r_j^{m+1}].\OR{j=0}{n-1}\vlsbr(r_j^m.\bar r_j^{m+1})]}{\Count(r_0^m,\dots,r_{n-1}^m)\geq\Count(r_0^{m+1},\dots,r_{n-1}^{m+1})}
\quad.\]
\end{lemma}
\begin{proof}
By Lemma~\ref{lem:decrease:evacuation}
\end{proof}
\begin{lemma}\label{lem:no-new-hole:PHP}
If no hole that was not inhabited by the first $m+1$ pigeons is inhabited by the first $m+2$ pigeons, then there is a hole with two pigeons, so the pigeon hole principle holds.
\[
\vlder{}{}{\PHP{n}}{\AND{j=0}{n-1}\vlsbr[r_j^m.\bar r_j^{m+1}]}
\quad.\]
\end{lemma}
\begin{proof}
\[
\vlderivation
{
\vlde{}{\{\awd\}}
{
\PHP{n}
}
{
\vlde{}{\{\swi\}}
{
\vls[\OR{j=0}{m}\OR{j=0}{n-1}\vlsbr(p_{i,j}.p_{m+1,j})\;.\;\AND{j=0}{n-1}\bar p_{m+1,j}]
}
{
\vlhy
{
\AND{j=0}{n-1}
\left(
\vlder{}{\swi}
{
\vls[\OR{i=0}{m}\vlsbr(p_{i,j}.p_{m+1,j}).\vlinf{}{}{\bar p_{m+1,j}}{\vls[\bar p_{m+1,j}.\bar p_{m+1,j}]}]
}
{
\vls[\OR{i=0}{m}\vlsbr(p_{i,j}.\vlinf{}{}{\vls[p_{m+1,j}.\bar p_{m+1,j}]}{\ttt}).(\vlinf{}{}{\ttt}{\bar r_j^m}\;.\;\bar p_{m+1,j})]
}
\right)
}
}
}
}
\quad.\]
\end{proof}
\begin{lemma}\label{lem:subtract:contradiction}
For a hole that was inhabited by the first $m+1$ pigeons to not be inhabited by the first $m+2$ pigeons, is a contradiction.
\[
\vlder{}{}{\fff}{\OR{j=0}{n-1}\vlsbr(r_j^m.\bar r_j^{m+1})}
\quad.\]
\end{lemma}
\begin{proof}
\[
\OR{j=0}{n-1}\vlsbr(\vlinf{}{}{\fff}{\vls(r_j^m.\bar r_j^m)}\;.\;\vlinf{}{}{\ttt}{\bar p_{m+1,j}})
\quad.\]
\end{proof}
\begin{lemma}\label{lem:not-increasing:PHP}
If adding one pigeon does not increase the number of holes inhabited, then there is a hole with two pigeons, so the pigeon hole principle holds.
\[
\vlder{}{}{\PHP{n}}{\Count(r_0^m,\dots,r_{n-1}^m)\geq\Count(r_0^{m+1},\dots,r_{n-1}^{m+1})}
\quad.\]
\end{lemma}
\begin{proof}
By Lemmas~\ref{lem:no-new-hole:PHP}, \ref{lem:subtract:contradiction} and \ref{lem:not-increasing:no-new-hole_subtract}.
\end{proof}
\begin{lemma}\label{lem:no-pigeon:PHP}
If the first pigeon is not in a hole, then the pigeon hole principle holds.
\[
\vlder{}{}{\PHP{n}}{0\geq\Count(r_0^0,\dots,r_{n-1}^0)}
\quad.\]
\end{lemma}
\begin{lemma}\label{lem:bound:not-increasing_bound}
If at most $m$ holes are inhabeted by the first $m+1$ pigeons, then either adding the $m+1^\text{st}$ pigeon did not increase the number of holes inhabited, or it did, and at most $m-1$ holes are inhabited by the first $m$ pigeons.
\[
\vlder{}{}
{
\vls
[
\Count(r_0^{m-1},\dots,r_{n-1}^{m-1})\geq\Count(r_0^m,\dots,r_{n-1}^m)
\;.\;
(m-1)\geq\Count(r_0^{m-1},\dots,r_{n-1}^{m-1})
]
}
{
m\geq\Count(r_0^m,\dots,r_{n-1}^m)
}
\quad.\]
\end{lemma}
\begin{theorem}
Given $n$ pigeons and $n-1$ pigeon holes, if every pigeon is in a hole, then there is a hole with two pigeons.
\[
\vlproof{}{}{\PHP{n}}
\quad.\]
\end{theorem}
\begin{proof}
By Lemmas~\ref{lem:at-most-full}, \ref{lem:no-pigeon:PHP}, \ref{lem:not-increasing:PHP} and \ref{lem:bound:not-increasing_bound}.
\end{proof}
\end{document}