summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | berghofe |

Fri, 05 Aug 2005 19:57:57 +0200 | |

changeset 17024 | ae4a8446df16 |

parent 17023 | 7425bf9f0f4b |

child 17025 | b4a6b987aebe |

New case study: pigeonhole principle.

src/HOL/Extraction/Pigeonhole.thy | file | annotate | diff | comparison | revisions | |

src/HOL/Extraction/ROOT.ML | file | annotate | diff | comparison | revisions |

--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Extraction/Pigeonhole.thy Fri Aug 05 19:57:57 2005 +0200 @@ -0,0 +1,303 @@ +(* Title: HOL/Extraction/Pigeonhole.thy + ID: $Id$ + Author: Stefan Berghofer, TU Muenchen +*) + +header {* The pigeonhole principle *} + +theory Pigeonhole imports EfficientNat 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}. + +We need decidability of equality on natural numbers: +*} + +lemma nat_eq_dec: "\<And>n::nat. m = n \<or> m \<noteq> n" + apply (induct m) + apply (case_tac n) + apply (case_tac [3] n) + apply (simp only: nat.simps, rules?)+ + done + +text {* +We can decide whether an array @{term "f"} of length @{term "l+(1::nat)"} +contains an element @{term "x"}. +*} + +lemma search: "(\<exists>j<(l::nat). (x::nat) = f j) \<or> \<not> (\<exists>j<l. x = f j)" +proof (induct l) + case 0 + have "\<not> (\<exists>j<0. x = f j)" + proof + assume "\<exists>j<0. x = f j" + then obtain j where j: "j < (0::nat)" by rules + thus "False" by simp + qed + thus ?case .. +next + case (Suc l) + thus ?case + proof + assume "\<exists>j<l. x = f j" + then obtain j where j: "j < l" + and eq: "x = f j" by rules + from j have "j < Suc l" by simp + with eq show ?case by rules + next + assume nex: "\<not> (\<exists>j<l. x = f j)" + from nat_eq_dec show ?case + proof + assume eq: "x = f l" + have "l < Suc l" by simp + with eq show ?case by rules + next + assume neq: "x \<noteq> f l" + have "\<not> (\<exists>j<Suc l. x = f j)" + proof + assume "\<exists>j<Suc l. x = f j" + then obtain j where j: "j < Suc l" + and eq: "x = f j" by rules + show False + proof cases + assume "j = l" + with eq have "x = f l" by simp + with neq show False .. + next + assume "j \<noteq> l" + with j have "j < l" by simp + with nex and eq show False by rules + qed + qed + thus ?case .. + qed + qed +qed + +text {* +This proof yields a polynomial program. +*} + +theorem pigeonhole: + "\<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" +proof (induct n) + case 0 + hence "Suc 0 \<le> Suc 0 \<and> 0 < Suc 0 \<and> f (Suc 0) = f 0" by simp + thus ?case by rules +next + case (Suc n) + { + fix k + have + "k \<le> Suc (Suc n) \<Longrightarrow> + (\<And>i j. Suc k \<le> i \<Longrightarrow> i \<le> Suc (Suc n) \<Longrightarrow> j < i \<Longrightarrow> f i \<noteq> f j) \<Longrightarrow> + (\<exists>i j. i \<le> k \<and> j < i \<and> f i = f j)" + proof (induct k) + case 0 + let ?f = "\<lambda>i. if f i = Suc n then f (Suc (Suc n)) else f i" + have "\<not> (\<exists>i j. i \<le> Suc n \<and> j < i \<and> ?f i = ?f j)" + proof + assume "\<exists>i j. i \<le> Suc n \<and> j < i \<and> ?f i = ?f j" + then obtain i j where i: "i \<le> Suc n" and j: "j < i" + and f: "?f i = ?f j" by rules + from j have i_nz: "Suc 0 \<le> i" by simp + from i have iSSn: "i \<le> Suc (Suc n)" by simp + have S0SSn: "Suc 0 \<le> 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 \<noteq> 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)) \<noteq> f j" + by (rule 0) + moreover assume "f j \<noteq> Suc n" + with fi and f have "f (Suc (Suc n)) = f j" by simp + ultimately show False .. + qed + next + assume fi: "f i \<noteq> 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)) \<noteq> 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 \<noteq> f j" by (rule 0) + moreover assume "f j \<noteq> Suc n" + with fi and f have "f i = f j" by simp + ultimately show False .. + qed + qed + qed + moreover have "\<And>i. i \<le> Suc n \<Longrightarrow> ?f i \<le> n" + proof - + fix i assume "i \<le> Suc n" + hence i: "i < Suc (Suc n)" by simp + have "f (Suc (Suc n)) \<noteq> f i" + by (rule 0) (simp_all add: i) + moreover have "f (Suc (Suc n)) \<le> Suc n" + by (rule Suc) simp + moreover from i have "i \<le> Suc (Suc n)" by simp + hence "f i \<le> Suc n" by (rule Suc) + ultimately show "?thesis i" + by simp + qed + hence "\<exists>i j. i \<le> Suc n \<and> j < i \<and> ?f i = ?f j" + by (rule Suc) + ultimately show ?case .. + next + case (Suc k) + from search show ?case + proof + assume "\<exists>j<Suc k. f (Suc k) = f j" + thus ?case by (rules intro: le_refl) + next + assume nex: "\<not> (\<exists>j<Suc k. f (Suc k) = f j)" + have "\<exists>i j. i \<le> k \<and> j < i \<and> f i = f j" + proof (rule Suc) + from Suc show "k \<le> Suc (Suc n)" by simp + fix i j assume k: "Suc k \<le> i" and i: "i \<le> Suc (Suc n)" + and j: "j < i" + show "f i \<noteq> f j" + proof cases + assume eq: "i = Suc k" + show ?thesis + proof + assume "f i = f j" + hence "f (Suc k) = f j" by (simp add: eq) + with nex and j and eq show False by rules + qed + next + assume "i \<noteq> Suc k" + with k have "Suc (Suc k) \<le> i" by simp + thus ?thesis using i and j by (rule Suc) + qed + qed + thus ?thesis by (rules intro: le_SucI) + qed + qed + } + note r = this + 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: + "\<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" +proof (induct n) + case 0 + have "Suc 0 \<le> Suc 0" .. + moreover have "0 < Suc 0" .. + moreover from 0 have "f (Suc 0) = f 0" by simp + ultimately show ?case by rules +next + case (Suc n) + from search show ?case + proof + assume "\<exists>j < Suc (Suc n). f (Suc (Suc n)) = f j" + thus ?case by (rules intro: le_refl) + next + assume "\<not> (\<exists>j < Suc (Suc n). f (Suc (Suc n)) = f j)" + hence nex: "\<forall>j < Suc (Suc n). f (Suc (Suc n)) \<noteq> f j" by rules + let ?f = "\<lambda>i. if f i = Suc n then f (Suc (Suc n)) else f i" + have "\<And>i. i \<le> Suc n \<Longrightarrow> ?f i \<le> n" + proof - + fix i assume i: "i \<le> Suc n" + show "?thesis i" + proof (cases "f i = Suc n") + case True + from i and nex have "f (Suc (Suc n)) \<noteq> f i" by simp + with True have "f (Suc (Suc n)) \<noteq> Suc n" by simp + moreover from Suc have "f (Suc (Suc n)) \<le> Suc n" by simp + ultimately have "f (Suc (Suc n)) \<le> n" by simp + with True show ?thesis by simp + next + case False + from Suc and i have "f i \<le> Suc n" by simp + with False show ?thesis by simp + qed + qed + hence "\<exists>i j. i \<le> Suc n \<and> j < i \<and> ?f i = ?f j" by (rule Suc) + then obtain i j where i: "i \<le> Suc n" and ji: "j < i" and f: "?f i = ?f j" + by rules + 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 \<noteq> Suc n" + moreover from i ji nex have "f (Suc (Suc n)) \<noteq> 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)) \<noteq> f i" by simp + ultimately show ?thesis using False f by simp + next + assume "f j \<noteq> Suc n" + with False f show ?thesis by simp + qed + qed + moreover from i have "i \<le> Suc (Suc n)" by simp + ultimately show ?thesis using ji by rules + 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. +*} + +consts_code + arbitrary :: "nat \<times> nat" ("{* (0::nat, 0::nat) *}") + +generate_code + test = "\<lambda>n. pigeonhole n (\<lambda>m. m - 1)" + test' = "\<lambda>n. pigeonhole_slow n (\<lambda>m. m - 1)" + sel = "op !" + +ML "timeit (fn () => test 10)" +ML "timeit (fn () => test' 10)" +ML "timeit (fn () => test 20)" +ML "timeit (fn () => test' 20)" +ML "timeit (fn () => test 25)" +ML "timeit (fn () => test' 25)" +ML "timeit (fn () => test 500)" + +ML "pigeonhole 8 (sel [0,1,2,3,4,5,6,3,7,8])" + +end

--- a/src/HOL/Extraction/ROOT.ML Fri Aug 05 19:56:58 2005 +0200 +++ b/src/HOL/Extraction/ROOT.ML Fri Aug 05 19:57:57 2005 +0200 @@ -10,4 +10,6 @@ (proofs := 2; time_use_thy "QuotRem"; time_use_thy "Warshall"; - time_use_thy "Higman"); + time_use_thy "Higman"; + no_document time_use_thy "EfficientNat"; + time_use_thy "Pigeonhole");