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

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

module Data.Nat.InfinitelyOften where

open import Effect.Monad using (RawMonad)
open import Level using (Level; 0ℓ)
open import Data.Empty using (⊥-elim)
open import Data.Nat.Base
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
open import Relation.Nullary.Negation using (¬_)
open import Relation.Nullary.Negation using (¬¬-Monad; call/cc)
open import Relation.Unary using (Pred; _∪_; _⊆_)

open RawMonad (¬¬-Monad {a = 0ℓ})

private
  variable
    ℓ : Level

infixr  _∪-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 →  + i ≤ j → ¬ P j
    helper ._ (s≤s i≤j) = fin _ i≤j

-- A witness.

witness : ∀ {P} → Inf {ℓ} P → ¬ ¬ ∃ P
witness ¬fin ¬p = ¬fin ( , λ 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 ( + proj₁ w₁) inf) >>= λ w₂ →
  pure (_ , _ , m≢1+m+n (proj₁ w₁) , proj₂ w₁ , proj₂ w₂)