7 theory Pigeonhole |
7 theory Pigeonhole |
8 imports Util "~~/src/HOL/Library/Code_Target_Numeral" |
8 imports Util "~~/src/HOL/Library/Code_Target_Numeral" |
9 begin |
9 begin |
10 |
10 |
11 text \<open> |
11 text \<open> |
12 We formalize two proofs of the pigeonhole principle, which lead |
12 We formalize two proofs of the pigeonhole principle, which lead |
13 to extracted programs of quite different complexity. The original |
13 to extracted programs of quite different complexity. The original |
14 formalization of these proofs in {\sc Nuprl} is due to |
14 formalization of these proofs in {\sc Nuprl} is due to |
15 Aleksey Nogin @{cite "Nogin-ENTCS-2000"}. |
15 Aleksey Nogin @{cite "Nogin-ENTCS-2000"}. |
16 |
16 |
17 This proof yields a polynomial program. |
17 This proof yields a polynomial program. |
18 \<close> |
18 \<close> |
19 |
19 |
20 theorem pigeonhole: |
20 theorem 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" |
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" |
22 proof (induct n) |
22 proof (induct n) |
23 case 0 |
23 case 0 |
24 hence "Suc 0 \<le> Suc 0 \<and> 0 < Suc 0 \<and> f (Suc 0) = f 0" by simp |
24 then have "Suc 0 \<le> Suc 0 \<and> 0 < Suc 0 \<and> f (Suc 0) = f 0" by simp |
25 thus ?case by iprover |
25 then show ?case by iprover |
26 next |
26 next |
27 case (Suc n) |
27 case (Suc n) |
28 { |
28 have r: |
29 fix k |
29 "k \<le> Suc (Suc n) \<Longrightarrow> |
30 have |
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 "k \<le> Suc (Suc n) \<Longrightarrow> |
31 (\<exists>i j. i \<le> k \<and> j < i \<and> f i = f j)" for k |
32 (\<And>i j. Suc k \<le> i \<Longrightarrow> i \<le> Suc (Suc n) \<Longrightarrow> j < i \<Longrightarrow> f i \<noteq> f j) \<Longrightarrow> |
32 proof (induct k) |
33 (\<exists>i j. i \<le> k \<and> j < i \<and> f i = f j)" |
33 case 0 |
34 proof (induct k) |
34 let ?f = "\<lambda>i. if f i = Suc n then f (Suc (Suc n)) else f i" |
35 case 0 |
35 have "\<not> (\<exists>i j. i \<le> Suc n \<and> j < i \<and> ?f i = ?f j)" |
36 let ?f = "\<lambda>i. if f i = Suc n then f (Suc (Suc n)) else f i" |
36 proof |
37 have "\<not> (\<exists>i j. i \<le> Suc n \<and> j < i \<and> ?f i = ?f j)" |
37 assume "\<exists>i j. i \<le> Suc n \<and> j < i \<and> ?f i = ?f j" |
38 proof |
38 then obtain i j where i: "i \<le> Suc n" and j: "j < i" and f: "?f i = ?f j" |
39 assume "\<exists>i j. i \<le> Suc n \<and> j < i \<and> ?f i = ?f j" |
39 by iprover |
40 then obtain i j where i: "i \<le> Suc n" and j: "j < i" |
40 from j have i_nz: "Suc 0 \<le> i" by simp |
41 and f: "?f i = ?f j" by iprover |
41 from i have iSSn: "i \<le> Suc (Suc n)" by simp |
42 from j have i_nz: "Suc 0 \<le> i" by simp |
42 have S0SSn: "Suc 0 \<le> Suc (Suc n)" by simp |
43 from i have iSSn: "i \<le> Suc (Suc n)" by simp |
43 show False |
44 have S0SSn: "Suc 0 \<le> Suc (Suc n)" by simp |
44 proof cases |
|
45 assume fi: "f i = Suc n" |
45 show False |
46 show False |
46 proof cases |
47 proof cases |
47 assume fi: "f i = Suc n" |
48 assume fj: "f j = Suc n" |
48 show False |
49 from i_nz and iSSn and j have "f i \<noteq> f j" by (rule 0) |
49 proof cases |
50 moreover from fi have "f i = f j" |
50 assume fj: "f j = Suc n" |
51 by (simp add: fj [symmetric]) |
51 from i_nz and iSSn and j have "f i \<noteq> f j" by (rule 0) |
52 ultimately show ?thesis .. |
52 moreover from fi have "f i = f j" |
53 next |
53 by (simp add: fj [symmetric]) |
54 from i and j have "j < Suc (Suc n)" by simp |
54 ultimately show ?thesis .. |
55 with S0SSn and le_refl have "f (Suc (Suc n)) \<noteq> f j" |
55 next |
56 by (rule 0) |
56 from i and j have "j < Suc (Suc n)" by simp |
57 moreover assume "f j \<noteq> Suc n" |
57 with S0SSn and le_refl have "f (Suc (Suc n)) \<noteq> f j" |
58 with fi and f have "f (Suc (Suc n)) = f j" by simp |
58 by (rule 0) |
59 ultimately show False .. |
59 moreover assume "f j \<noteq> Suc n" |
60 qed |
60 with fi and f have "f (Suc (Suc n)) = f j" by simp |
61 next |
61 ultimately show False .. |
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 |
62 qed |
116 qed |
63 next |
117 next |
64 assume fi: "f i \<noteq> Suc n" |
118 assume "i \<noteq> Suc k" |
65 show False |
119 with k have "Suc (Suc k) \<le> i" by simp |
66 proof cases |
120 then show ?thesis using i and j by (rule Suc) |
67 from i have "i < Suc (Suc n)" by simp |
|
68 with S0SSn and le_refl have "f (Suc (Suc n)) \<noteq> f i" |
|
69 by (rule 0) |
|
70 moreover assume "f j = Suc n" |
|
71 with fi and f have "f (Suc (Suc n)) = f i" by simp |
|
72 ultimately show False .. |
|
73 next |
|
74 from i_nz and iSSn and j |
|
75 have "f i \<noteq> f j" by (rule 0) |
|
76 moreover assume "f j \<noteq> Suc n" |
|
77 with fi and f have "f i = f j" by simp |
|
78 ultimately show False .. |
|
79 qed |
|
80 qed |
121 qed |
81 qed |
122 qed |
82 moreover have "\<And>i. i \<le> Suc n \<Longrightarrow> ?f i \<le> n" |
123 then show ?thesis by (iprover intro: le_SucI) |
83 proof - |
124 qed |
84 fix i assume "i \<le> Suc n" |
125 qed |
85 hence i: "i < Suc (Suc n)" by simp |
|
86 have "f (Suc (Suc n)) \<noteq> f i" |
|
87 by (rule 0) (simp_all add: i) |
|
88 moreover have "f (Suc (Suc n)) \<le> Suc n" |
|
89 by (rule Suc) simp |
|
90 moreover from i have "i \<le> Suc (Suc n)" by simp |
|
91 hence "f i \<le> Suc n" by (rule Suc) |
|
92 ultimately show "?thesis i" |
|
93 by simp |
|
94 qed |
|
95 hence "\<exists>i j. i \<le> Suc n \<and> j < i \<and> ?f i = ?f j" |
|
96 by (rule Suc) |
|
97 ultimately show ?case .. |
|
98 next |
|
99 case (Suc k) |
|
100 from search [OF nat_eq_dec] show ?case |
|
101 proof |
|
102 assume "\<exists>j<Suc k. f (Suc k) = f j" |
|
103 thus ?case by (iprover intro: le_refl) |
|
104 next |
|
105 assume nex: "\<not> (\<exists>j<Suc k. f (Suc k) = f j)" |
|
106 have "\<exists>i j. i \<le> k \<and> j < i \<and> f i = f j" |
|
107 proof (rule Suc) |
|
108 from Suc show "k \<le> Suc (Suc n)" by simp |
|
109 fix i j assume k: "Suc k \<le> i" and i: "i \<le> Suc (Suc n)" |
|
110 and j: "j < i" |
|
111 show "f i \<noteq> f j" |
|
112 proof cases |
|
113 assume eq: "i = Suc k" |
|
114 show ?thesis |
|
115 proof |
|
116 assume "f i = f j" |
|
117 hence "f (Suc k) = f j" by (simp add: eq) |
|
118 with nex and j and eq show False by iprover |
|
119 qed |
|
120 next |
|
121 assume "i \<noteq> Suc k" |
|
122 with k have "Suc (Suc k) \<le> i" by simp |
|
123 thus ?thesis using i and j by (rule Suc) |
|
124 qed |
|
125 qed |
|
126 thus ?thesis by (iprover intro: le_SucI) |
|
127 qed |
|
128 qed |
|
129 } |
|
130 note r = this |
|
131 show ?case by (rule r) simp_all |
126 show ?case by (rule r) simp_all |
132 qed |
127 qed |
133 |
128 |
134 text \<open> |
129 text \<open> |
135 The following proof, although quite elegant from a mathematical point of view, |
130 The following proof, although quite elegant from a mathematical point of view, |
136 leads to an exponential program: |
131 leads to an exponential program: |
137 \<close> |
132 \<close> |
138 |
133 |
139 theorem pigeonhole_slow: |
134 theorem pigeonhole_slow: |
140 "\<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" |
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" |
141 proof (induct n) |
136 proof (induct n) |