Quelle  Pigeonhole.thy

(*  Title:      HOL/Proofs/Extraction/Pigeonhole.thy
  Author: Stefan Berghofer, TU Muenchen
*)

section ‹The pigeonhole principle›

theory Pigeonhole
imports Util "HOL-Library.Realizers" "HOL-Library.Code_Target_Numeral"
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 🍋‹"Nogin-ENTCS-2000"›.
 
  This proof yields a polynomial program.
 ›

theorem pigeonhole:
  "∧f. (∧i. i ≤ Suc n ==> f i ≤ n) ==> ∃i j. i ≤ Suc n ∧ j < i ∧ f i = f j"
proof (induct n)
  case 0
  then have "Suc 0 ≤ Suc 0 ∧ 0 < Suc 0 ∧ f (Suc 0) = f 0" by simp
  then show ?case by iprover
next
  case (Suc n)
  have r:
    "k ≤ Suc (Suc n) ==>
    (∧i j. Suc k ≤ i ==> i ≤ Suc (Suc n) ==> j < i ==> f i ≠ f j) ==>
    (∃i j. i ≤ k ∧ j < i ∧ f i = f j)" for k
  proof (induct k)
    case 0
    let ?f = "λi. if f i = Suc n then f (Suc (Suc n)) else f i"
    have "¬ (∃i j. i ≤ Suc n ∧ j < i ∧ ?f i = ?f j)"
    proof
      assume "∃i j. i ≤ Suc n ∧ j < i ∧ ?f i = ?f j"
      then obtain i j where i: "i ≤ Suc n" and j: "j < i" and f: "?f i = ?f j"
        by iprover
      from j have i_nz: "Suc 0 ≤ i" by simp
      from i have iSSn: "i ≤ Suc (Suc n)" by simp
      have S0SSn: "Suc 0 ≤ 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 ≠ 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)) ≠ f j"
            by (rule 0)
          moreover assume "f j ≠ Suc n"
          with fi and f have "f (Suc (Suc n)) = f j" by simp
          ultimately show False ..
        qed
      next
        assume fi: "f i ≠ 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)) ≠ 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 ≠ f j" by (rule 0)
          moreover assume "f j ≠ Suc n"
          with fi and f have "f i = f j" by simp
          ultimately show False ..
        qed
      qed
    qed
    moreover have "?f i ≤ n" if "i ≤ Suc n" for i
    proof -
      from that have i: "i < Suc (Suc n)" by simp
      have "f (Suc (Suc n)) ≠ f i"
        by (rule 0) (simp_all add: i)
      moreover have "f (Suc (Suc n)) ≤ Suc n"
        by (rule Suc) simp
      moreover from i have "i ≤ Suc (Suc n)" by simp
      then have "f i ≤ Suc n" by (rule Suc)
      ultimately show ?thesis
        by simp
    qed
    then have "∃i j. i ≤ Suc n ∧ j < i ∧ ?f i = ?f j"
      by (rule Suc)
    ultimately show ?case ..
  next
    case (Suc k)
    from search [OF nat_eq_dec] show ?case
    proof
      assume "∃j
      then show ?case by (iprover intro: le_refl)
    next
      assume nex: "¬ (∃j
      have "∃i j. i ≤ k ∧ j < i ∧ f i = f j"
      proof (rule Suc)
        from Suc show "k ≤ Suc (Suc n)" by simp
        fix i j assume k: "Suc k ≤ i" and i: "i ≤ Suc (Suc n)"
          and j: "j < i"
        show "f i ≠ f j"
        proof cases
          assume eq: "i = Suc k"
          show ?thesis
          proof
            assume "f i = f j"
            then have "f (Suc k) = f j" by (simp add: eq)
            with nex and j and eq show False by iprover
          qed
        next
          assume "i ≠ Suc k"
          with k have "Suc (Suc k) ≤ i" by simp
          then show ?thesis using i and j by (rule Suc)
        qed
      qed
      then show ?thesis by (iprover intro: le_SucI)
    qed
  qed
  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:
  "∧f. (∧i. i ≤ Suc n ==> f i ≤ n) ==> ∃i j. i ≤ Suc n ∧ j < i ∧ f i = f j"
proof (induct n)
  case 0
  have "Suc 0 ≤ Suc 0" ..
  moreover have "0 < Suc 0" ..
  moreover from 0 have "f (Suc 0) = f 0" by simp
  ultimately show ?case by iprover
next
  case (Suc n)
  from search [OF nat_eq_dec] show ?case
  proof
    assume "∃j < Suc (Suc n). f (Suc (Suc n)) = f j"
    then show ?case by (iprover intro: le_refl)
  next
    assume "¬ (∃j < Suc (Suc n). f (Suc (Suc n)) = f j)"
    then have nex: "∀j < Suc (Suc n). f (Suc (Suc n)) ≠ f j" by iprover
    let ?f = "λi. if f i = Suc n then f (Suc (Suc n)) else f i"
    have "∧i. i ≤ Suc n ==> ?f i ≤ n"
    proof -
      fix i assume i: "i ≤ Suc n"
      show "?thesis i"
      proof (cases "f i = Suc n")
        case True
        from i and nex have "f (Suc (Suc n)) ≠ f i" by simp
        with True have "f (Suc (Suc n)) ≠ Suc n" by simp
        moreover from Suc have "f (Suc (Suc n)) ≤ Suc n" by simp
        ultimately have "f (Suc (Suc n)) ≤ n" by simp
        with True show ?thesis by simp
      next
        case False
        from Suc and i have "f i ≤ Suc n" by simp
        with False show ?thesis by simp
      qed
    qed
    then have "∃i j. i ≤ Suc n ∧ j < i ∧ ?f i = ?f j" by (rule Suc)
    then obtain i j where i: "i ≤ Suc n" and ji: "j < i" and f: "?f i = ?f j"
      by iprover
    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 ≠ Suc n"
        moreover from i ji nex have "f (Suc (Suc n)) ≠ 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)) ≠ f i" by simp
        ultimately show ?thesis using False f by simp
      next
        assume "f j ≠ Suc n"
        with False f show ?thesis by simp
      qed
    qed
    moreover from i have "i ≤ Suc (Suc n)" by simp
    ultimately show ?thesis using ji by iprover
  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 🍋‹pigeonhole› is
  @{thm [display] pigeonhole_correctness [no_vars]}
 
  In order to analyze the speed of the above programs,
  we generate ML code from them.
 ›

instantiation nat :: default
begin

definition "default = (0::nat)"

instance ..

end

instantiation prod :: (default, default) default
begin

definition "default = (default, default)"

instance ..

end

definition "test n u = pigeonhole (nat_of_integer n) (λm. m - 1)"
definition "test' n u = pigeonhole_slow (nat_of_integer n) (λm. m - 1)"
definition "test'' u = pigeonhole 8 (List.nth [0, 1, 2, 3, 4, 5, 6, 3, 7, 8])"

ML_val "timeit (@{code test} 10)"
ML_val "timeit (@{code test'} 10)"
ML_val "timeit (@{code test} 20)"
ML_val "timeit (@{code test'} 20)"
ML_val "timeit (@{code test} 25)"
ML_val "timeit (@{code test'} 25)"
ML_val "timeit (@{code test} 500)"
ML_val "timeit @{code test''}"

end