module InfinitePigeonLessEfficient where

open import Logic
open import LogicalFacts
open import Two
open import Naturals
open import Order
open import Cantor
open import Equality
open import K-AC-N
open import JK-LogicalFacts

-- 29 April -3rd May 2011.

-- We prove a theorem that involves the classical existential
-- quantifier K∃ (called pigeonhole below). The proof uses excluded
-- middle and classical countable choice (i.e. choice formulated with
-- the classical existential quantifier), which is implemented using
-- the K-shift (more commonly known as the double negation shift) in
-- the modules JK-Choice.agda and Infinite-JK-Shifts.agda.
--
-- In the module FinitePigeon.agda we derive a statement that uses the
-- intuitionistic quantifiers (and doesn't mention the double negation
-- modality K at all), using the classical result as a lemma. In the
-- module Examples.agda we run it.

-- This is the first version. Much improved ones are in other files.
-- Also, this proof switches the case analysis, and this causes funny
-- subsequences in some cases.

-- Definition

Pigeonhole-Lemma : {R : Ω}  ₂ℕ  Ω
Pigeonhole-Lemma {R} α =
\(b : )   \(f :   )  ∀(n : )  K{R}(α(n + f n + 1)  b)

pigeonhole-lemma : {R : Ω}
----------------

∀(α : ₂ℕ)  K (Pigeonhole-Lemma α)

pigeonhole-lemma {R} α =  K-∨-elim case₀ case₁ K-Excluded-Middle
where
A : Ω
A = ∀(n : )  K∃ \(i : )  K(α(n + i + 1)  )

case₀ : A  K(Pigeonhole-Lemma α)
case₀ a = K-functor lemma₂ lemma₁
where
lemma₁ : K∃ \(f :   )  ∀(n : )  K(α(n + f n + 1)  )
lemma₁ = K-AC-ℕ  n  λ r  ∃-intro 0  p  r)) a

lemma₂ : ( \(f :   )  ∀(n : )  K(α(n + f n + 1)  ))
\(b : )   \(f :   )  ∀(n : )  K(α(n + f n + 1)  b)
lemma₂ = ∃-intro

case₁ : (A  R)  K(Pigeonhole-Lemma α)
case₁ p = lemma₇
where
lemma₃ :
K∃ \(n : )  ( \(i : )  K(α(n + i + 1)  ))  R
lemma₃ = not-forall-not-implies-K-exists p

lemma₄-₁ :
( \(n : )  ( \(i : )   K(α(n + i + 1)  ))  R)
\(n : )     (i : )  (K(α(n + i + 1)  ))  R
lemma₄-₁ (∃-intro n e) = ∃-intro n (not-exists-implies-forall-not e)

lemma₄ :
K∃ \(n : )  ∀(i : )  (K(α(n + i + 1)  ))  R
lemma₄ = K-functor lemma₄-₁ lemma₃

lemma₅-₁ :
( \(n : )   (i : )  K(α(n + i + 1)    R))
\(n : )   (i : )  K(α(n + i + 1)  )
lemma₅-₁ (∃-intro n f) =
∃-intro n  i  not-1-must-be-0 (α(n + i + 1)) (f i))

lemma₅ :
K∃ \(n : )  ∀(i : )  K(α(n + i + 1)  )
lemma₅ = K-functor lemma₅-₁ lemma₄

lemma₆-₁ :
( \(n : )  ∀(i : )  K(α(n + i + 1)  ))
\(n : )  ∀(i : )  K(α(i + n + 1)  )
lemma₆-₁ (∃-intro n h) = ∃-intro n  i  K-functor(lemma₆-₁-₁ i)(h i))
where
lemma₆-₁-₁ : ∀(i : )  α(n + i + 1)    α(i + n + 1)
lemma₆-₁-₁ i r = two-things-equal-to-a-third-are-equal lemma₆-₁-₁-₁ r
where
lemma₆-₁-₁-₁ : α(n + i + 1)  α(i + n + 1)
lemma₆-₁-₁-₁ =
compositionality  k  α(k + 1)) (addition-commutativity n i)

lemma₆ :
K∃ \(i : )  ∀(n : )  K(α(n + i + 1)  )
lemma₆ = K-functor lemma₆-₁ lemma₅

lemma₇-₁ :
( \(i : )  ∀(n : )  K(α(n + i + 1)  ))
\(b : )   \(f :   )  ∀(n : )  K{R}(α(n + f n + 1)  b)
lemma₇-₁ (∃-intro i a) = ∃-intro  (∃-intro  n  i) a)

lemma₇ : K(Pigeonhole-Lemma α)
lemma₇ = K-functor lemma₇-₁ lemma₆

-- Definition

Pigeonhole : {R : Ω}  ₂ℕ  Ω
Pigeonhole {R} α =
\(b : )   \(g :   )
∀(i : )  g i < g(i + 1)  K {R} (α(g i)  b)

pigeonhole : {R : Ω}
----------

∀(α : ₂ℕ)  K(Pigeonhole α)

pigeonhole {R} α = K-functor lemma₀ (pigeonhole-lemma {R} α)
where
lemma₀ :
( \(b : )   \(f :   )  ∀(n : )  K(α(n + f n + 1)  b))
\(b : )   \(g :   )  ∀(n : )  g n < g(n + 1)  K {R}(α(g n)  b)
lemma₀ (∃-intro b (∃-intro f h)) =
∃-intro b (∃-intro g λ n  ∧-intro (lemma₁ n) (lemma₂ n))
where g :
g 0 = 0 + f 0 + 1
g(succ n) = let m = g n in m + f m + 1

lemma₁ : ∀(n : )  g n < g(n + 1)
lemma₁ n = less-proof(f(g n))

lemma₂ : ∀(n : )  K(α(g n)  b)
lemma₂ 0 = h 0
lemma₂ (succ n) = h(g n)