```------------------------------------------------------------------------
-- The Agda standard library
--
-- Definition of and lemmas related to "true infinitely often"
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}

module Data.Nat.InfinitelyOften where

open import Level using (Level; 0ℓ)
open import Data.Empty using (⊥-elim)
open import Data.Nat.Base using (ℕ; _≤_; _⊔_; _+_; suc; zero; s≤s)
open import Data.Nat.Properties
open import Data.Product.Base as Prod hiding (map)
open import Data.Sum.Base using (inj₁; inj₂; _⊎_)
open import Function.Base using (_∘_; id)
open import Relation.Binary.PropositionalEquality.Core using (_≢_)
open import Relation.Nullary.Negation using (¬_)
open import Relation.Nullary.Negation using (¬¬-Monad; call/cc)
open import Relation.Unary using (Pred; _∪_; _⊆_)

private
variable
ℓ : Level

infixr 1 _∪-Fin_

-- Only true finitely often.

Fin : Pred ℕ ℓ → Set ℓ
Fin P = ∃ λ i → ∀ j → i ≤ j → ¬ P j

-- A non-constructive definition of "true infinitely often".

Inf : Pred ℕ ℓ → Set ℓ
Inf P = ¬ Fin P

-- Fin is preserved by binary sums.

_∪-Fin_ : ∀ {ℓp ℓq P Q} → Fin {ℓp} P → Fin {ℓq} Q → Fin (P ∪ Q)
_∪-Fin_ {P = P} {Q} (i , ¬p) (j , ¬q) = (i ⊔ j , helper)
where
open ≤-Reasoning

helper : ∀ k → i ⊔ j ≤ k → ¬ (P ∪ Q) k
helper k i⊔j≤k (inj₁ p) = ¬p k (begin
i      ≤⟨ m≤m⊔n i j ⟩
i ⊔ j  ≤⟨ i⊔j≤k ⟩
k      ∎) p
helper k i⊔j≤k (inj₂ q) = ¬q k (begin
j      ≤⟨ m≤m⊔n j i ⟩
j ⊔ i  ≡⟨ ⊔-comm j i ⟩
i ⊔ j  ≤⟨ i⊔j≤k ⟩
k      ∎) q

-- Inf commutes with binary sums (in the double-negation monad).

commutes-with-∪ : ∀ {P Q} → Inf (P ∪ Q) → ¬ ¬ (Inf P ⊎ Inf Q)
commutes-with-∪ p∪q =
call/cc λ ¬[p⊎q] →
(λ ¬p ¬q → ⊥-elim (p∪q (¬p ∪-Fin ¬q)))
<\$> ¬[p⊎q] ∘ inj₁ ⊛ ¬[p⊎q] ∘ inj₂

-- Inf is functorial.

map : ∀ {ℓp ℓq P Q} → P ⊆ Q → Inf {ℓp} P → Inf {ℓq} Q
map P⊆Q ¬fin = ¬fin ∘ Prod.map id (λ fin j i≤j → fin j i≤j ∘ P⊆Q)

-- Inf is upwards closed.

up : ∀ {P} n → Inf {ℓ} P → Inf (P ∘ _+_ n)
up     zero    = id
up {P = P} (suc n) = up n ∘ up₁
where
up₁ : Inf P → Inf (P ∘ suc)
up₁ ¬fin (i , fin) = ¬fin (suc i , helper)
where
helper : ∀ j → 1 + i ≤ j → ¬ P j
helper ._ (s≤s i≤j) = fin _ i≤j

-- A witness.

witness : ∀ {P} → Inf {ℓ} P → ¬ ¬ ∃ P
witness ¬fin ¬p = ¬fin (0 , λ i _ Pi → ¬p (i , Pi))

-- Two different witnesses.

twoDifferentWitnesses
: ∀ {P} → Inf P → ¬ ¬ ∃₂ λ m n → m ≢ n × P m × P n
twoDifferentWitnesses inf =
witness inf                     >>= λ w₁ →
witness (up (1 + proj₁ w₁) inf) >>= λ w₂ →
pure (_ , _ , m≢1+m+n (proj₁ w₁) , proj₂ w₁ , proj₂ w₂)
```