module Data.Nat.InfinitelyOften where
open import Algebra
open import Category.Monad
open import Data.Empty
open import Data.Function
open import Data.Nat
import Data.Nat.Properties as NatProp
open import Data.Product as Prod hiding (map)
open import Data.Sum hiding (map)
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary
open import Relation.Nullary.Negation
open import Relation.Unary using (_∪_; _⊆_)
open RawMonad ¬¬-Monad
private
module NatLattice = DistributiveLattice NatProp.distributiveLattice
Fin : (ℕ → Set) → Set
Fin P = ∃ λ i → ∀ j → i ≤ j → ¬ P j
_∪-Fin_ : ∀ {P Q} → Fin P → Fin Q → Fin (P ∪ Q)
_∪-Fin_ {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 ≤⟨ NatProp.m≤m⊔n i j ⟩
i ⊔ j ≤⟨ i⊔j≤k ⟩
k ∎) p
helper k i⊔j≤k (inj₂ q) = ¬q k (begin
j ≤⟨ NatProp.m≤m⊔n j i ⟩
j ⊔ i ≡⟨ NatLattice.∧-comm j i ⟩
i ⊔ j ≤⟨ i⊔j≤k ⟩
k ∎) q
Inf : (ℕ → Set) → Set
Inf P = ¬ Fin P
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₂
map : ∀ {P Q} → P ⊆ Q → Inf P → Inf Q
map P⊆Q ¬fin = ¬fin ∘ Prod.map id (λ fin j i≤j → fin j i≤j ∘ P⊆Q)
up : ∀ {P} n → Inf P → Inf (P ∘ _+_ n)
up zero = id
up {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
witness : ∀ {P} → Inf P → ¬ ¬ ∃ P
witness ¬fin ¬p = ¬fin (0 , λ i _ Pi → ¬p (i , Pi))
twoDifferentWitnesses
: ∀ {P} → Inf P → ¬ ¬ ∃₂ λ m n → m ≢ n × P m × P n
twoDifferentWitnesses inf =
witness inf >>= λ w₁ →
witness (up (1 + proj₁ w₁) inf) >>= λ w₂ →
return (_ , _ , NatProp.m≢1+m+n (proj₁ w₁) , proj₂ w₁ , proj₂ w₂)