New case study: pigeonhole principle.

--- /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");