------------------------------------------------------------------------
-- 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 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; _∪_; _⊆_)

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

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₂)