{-# OPTIONS --allow-unsolved-metas #-}
module Verona2024.DoubleNegation.Pigeonhole where

open import Data.Nat
open import Data.Nat.Properties
open import Data.Bool using (Bool; false; true)
open import Data.Sum
open import Data.Product
open import Relation.Binary.PropositionalEquality

module Classical where
  data  : Set where

  ⊥-elim : {X : Set}    X
  ⊥-elim ()

  ¬_ : Set  Set
  ¬ X = X  
  
  not-true-is-false : {x : Bool}  ¬ (true  x)  false  x
  not-true-is-false {false} p = {!!}
  not-true-is-false {true}  p = {!!}

  -- "Boundedly α P" expresses that the predicate P is satisfied by the values
  -- of α only finitely often.
  Boundedly : {X : Set}  (  X)  (X  Set)  Set
  Boundedly α P = Σ[ a   ] ((b : )  b  a  ¬ P (α b))

  -- "Infinitely α P" expresses, in a positive way, that the values of α
  -- satisfy P infinitely often.
  Infinitely : {X : Set}  (  X)  (X  Set)  Set
  Infinitely α P = (a : )  Σ[ b   ] b  a × P (α b)

  postulate
    oracle : {A : Set}  A  (¬ A)

  lemma : {X : Set}  {α :   X} {P : X  Set}  ¬ Boundedly α P  Infinitely α P
  lemma {P = P} p a with oracle
  ... | inj₁ q = q
  ... | inj₂ q = {!!}

  module _ (α :   Bool) where
    theorem : Infinitely α (false ≡_)  Infinitely α (true ≡_)
    theorem with oracle {Boundedly α (true ≡_)}
    ... | inj₁ (a , p) = {!!}
    ... | inj₂ p       = {!!}

    go : {x : Bool}  Infinitely α (x ≡_)  ∃[ i ] ∃[ j ] i < j × α i  α j
    go p =
      {!!}

    corollary : ∃[ i ] ∃[ j ] i < j × α i  α j
    corollary with theorem
    ... | inj₁ p = go p
    ... | inj₂ p = go p

module ConstructiveButUninformative ( : Set) where
  ¬_ : Set  Set
  ¬ X = X  
  
  ⊥-elim : {X : Set}    ¬ ¬ X
  ⊥-elim a = λ _  a

  return : {X : Set}  X  ¬ ¬ X
  return x = λ k  k x

  _⟫=_ : {X Y : Set}  ¬ ¬ X  (X  ¬ ¬ Y)  ¬ ¬ Y
  m ⟫= f = λ k  m  x  f x k)

  escape : ¬ ¬   
  escape m = m  a  a)

  not-true-is-false : {x : Bool}  ¬ (true  x)  ¬ ¬ (false  x)
  not-true-is-false {false} p = {!!}
  not-true-is-false {true}  p = {!!}

  Boundedly : {X : Set}  (  X)  (X  Set)  Set
  Boundedly f P = Σ[ a   ] ((b : )  b  a  ¬ P (f b))

  Infinitely : {X : Set}  (  X)  (X  Set)  Set
  Infinitely f P = (a : )  ¬ ¬ (Σ[ b   ] b  a × P (f b))

  oracle : {A : Set}  ¬ ¬ (A  (¬ A))
  oracle = λ k  k (inj₂  x  k (inj₁ x)))

  lemma : {X : Set}  {α :   X} {P : X  Set}  ¬ Boundedly α P  Infinitely α P
  lemma {α = α} {P = P} p a = {!!}

  module _ (α :   Bool) where
    theorem : ¬ ¬ (Infinitely α (false ≡_)  Infinitely α (true ≡_))
    theorem = {!!}

    go : {x : Bool}  Infinitely α (x ≡_)  ¬ ¬ (∃[ i ] ∃[ j ] i < j × α i  α j)
    go p = {!!}

    corollary : ¬ ¬ (∃[ i ] ∃[ j ] i < j × α i  α j)
    corollary = theorem ⟫= λ { (inj₁ p)  go p; (inj₂ p)  go p }

module Constructive where
  module _ (α :   Bool) where
    Claim : Set
    Claim = ∃[ i ] ∃[ j ] i < j × α i  α j

    open ConstructiveButUninformative (Claim)

    result : Claim
    result = escape (corollary α) 
    -- Run "C-c C-n Constructive.result" (in the Agdapad, "C-c C-v Constructive.result")
    -- to inspect the unrolled proof term. It references α 3 and hence definitely does NOT
    -- coincide with the straightforward proof which just inspects α 0, α 1 and α 2
    -- and looks for two equal values among these three values.