```
{-# 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 ⟫= go
  where
  go : (∃[ b ] b ≥ a × P (α b)) ⊎ ((∃[ b ] b ≥ a × P (α b)) → ⊥) → ¬ ¬ (∃[ b ] b ≥ a × P (α b))
  go (left  q) = {!!}
  go (right q) = {!!}
```

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

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