Simple seemingly impossible Agda

Search.agda

module Search where

open import Coinduction
open import Function
open import Data.Empty
open import Data.Nat
open import Data.Product
open import Relation.Nullary

-- Thanks to Ed Kmett for helping me clarify what I was getting at here,
-- and for pointing out that I needed the other half (¬Exists) to make a
-- real statement

data Result (P : ℕ → Set) : Set where
  now   : (p : P zero) → Result P
  later : (r : ∞ (Result (P ∘ suc))) → Result P

-- Hilbert's epsilon
ε : ∀ {P : ℕ → Set} → ((n : ℕ) → Dec (P n)) → Result P
ε p with p zero
ε p | yes q = now q
ε p | no ¬q = later (♯ (ε (p ∘ suc)))


-- The ε gave a finite result
data Exists {P} : Result P → Set where
  now   : (p : P zero) → Exists (now p)
  later : ∀ {r′} (r : Exists (♭ r′)) → Exists (later r′)

-- If the ε gave a result, the predicate is satisfiable
exists : ∀ {P : ℕ → Set} (p : (n : ℕ) → Dec (P n)) → Exists (ε p) → ∃ P
exists p t with p zero
exists p (now  .q) | yes q = zero , q
exists p (later r) | no ¬q with exists (p ∘ suc) r
exists p (later r) | no ¬q | n , pf = suc n , pf

-- If the predicate is satisfiable, ε will give a result
exists′ : ∀ {P : ℕ → Set} (p : (n : ℕ) → Dec (P n)) → ∃ P → Exists (ε p)
exists′ p (n , pf) = helper p n pf
  where
  helper : ∀ {P : ℕ → Set} (p : (n : ℕ) → Dec (P n)) → ∀ n → P n → Exists (ε p)
  helper p n pf with p zero
  helper p n pf | yes q = now q
  helper p zero pf | no ¬q = ⊥-elim (¬q pf)
  helper p (suc n) pf | no ¬q = later (helper (p ∘ suc) n pf)




-- The ε didn't give a finite result
data ¬Exists {P} : Result P → Set where
  later : ∀ {r′} (r : ∞ (¬Exists (♭ r′))) → ¬Exists (later r′)

-- If the ε didn't give a finite result, the predicate is not satisfiable
¬exists : ∀ {P : ℕ → Set} (p : (n : ℕ) → Dec (P n)) → ¬Exists (ε p) → ¬ ∃ P
¬exists p f (n , pf) = helper p f n pf
  where
  helper : ∀ {P : ℕ → Set} (p : (n : ℕ) → Dec (P n)) → ¬Exists (ε p) → ∀ n → P n → ⊥
  helper p f n pf with p zero
  helper p () n pf | yes q
  helper p f zero pf | no ¬q = ¬q pf
  helper p (later f) (suc n) pf | no ¬q = helper (p ∘ suc) (♭ f) n pf

-- If the predicate is not satisfiable, ε won't give a result
¬exists′ : ∀ {P : ℕ → Set} (p : (n : ℕ) → Dec (P n)) → ¬ ∃ P → ¬Exists (ε p)
¬exists′ p ¬∃ with p zero
¬exists′ p ¬∃ | yes q = ⊥-elim (¬∃ (zero , q))
¬exists′ p ¬∃ | no ¬q = later (♯ (¬exists′ (p ∘ suc) (λ { (n , pf) → ¬∃ (suc n , pf) })))