📥 Download raw
{-# OPTIONS --cubical-compatible #-}
module Padova2025.ComputationalContent.Fictions.InfinitelyMany (⊥ : Set) where

Infinite subsequences

open import Padova2025.ProgrammingBasics.Booleans
open import Padova2025.ProgrammingBasics.Naturals.Base
open import Padova2025.ProgrammingBasics.Naturals.Arithmetic
open import Padova2025.ProvingBasics.Equality.Base
open import Padova2025.ProvingBasics.Connectives.Disjunction
open import Padova2025.ProvingBasics.Connectives.Existential
open import Padova2025.ProvingBasics.Connectives.Conjunction
open import Padova2025.ProvingBasics.Termination.Ordering
open import Padova2025.ComputationalContent.DoubleNegation (⊥)

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

The condition Boundedly α P expresses that the predicate P is satisfied by the values of α only finitely often.

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

The condition Infinitely α P expresses, in a positive way, that the values of α satisfy P infinitely often.

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

lemma : {X : Set} → {α : ℕ → X} {P : X → Set} → ¬ Boundedly α P → Infinitely α P
lemma {α = α} {P = P} p a = oracle {∃[ b ] b ≥ a × P (α b)} ⟫= λ
  { (left  q) → {!!}
  ; (right q) → {!!}
  }

InfinitaryPigeonholePrinciple : (ℕ → Bool) → Set
InfinitaryPigeonholePrinciple α = Infinitely α (false ≡_) ⊎ Infinitely α (true ≡_)

infinitary-pigeonhole-principle : (α : ℕ → Bool) → ¬ ¬ InfinitaryPigeonholePrinciple α
infinitary-pigeonhole-principle α = oracle {Boundedly α (true ≡_)} ⟫= λ
  { (left  (a , p)) → {!!}
  ; (right p)       → {!!}
  }