{-# 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 : {X : Set} → (ℕ → X) → (X → Set) → Set
Boundedly α P = Σ[ a ∈ ℕ ] ((b : ℕ) → b ≥ a → ¬ P (α b))
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 α)