Semidecidability!

Semidecidable.agda

module Semidecidable where

open import Coinduction
open import Function
open import Data.Empty
open import Relation.Nullary
open import Relation.Binary hiding (Rel)
import Relation.Binary.PropositionalEquality as PropEq
open import Category.Monad

open import Category.Monad.Partiality renaming (_⊥ to Partial)

open PropEq using (_≡_)
module M {f} = RawMonad (monad {f})
open Equivalence

data Terminates {a} {A : Set a} : Partial A → Set a where
  now   : (x : A) → Terminates (now x)
  later : ∀ {x} (t : Terminates (♭ x)) → Terminates (later x)

get : ∀ {a} {A : Set a} {P : Partial A} → Terminates P → A
get (now x) = x
get (later t) = get t


data Loops {a} {A : Set a} : Partial A → Set a where
  later : ∀ {x} (l : ∞ (Loops (♭ x))) → Loops (later x)

module Respects {a ℓ} {A : Set a} (_∼_ : A → A → Set ℓ) where
  open Equality _∼_

  terminates : ∀ {x y} k → {eq : Equality k} → Rel k x y → Terminates x → Terminates y
  terminates k       (Equality.now {y = y} x∼y) (now x) = now y
  terminates ._      (Equality.laterʳ r)             x  = later (terminates _ r x)
  terminates k  {eq} (Equality.later x∼y)    (later tx) = later (terminates k {eq} (♭ x∼y) tx)
  terminates ._ {eq} (Equality.laterˡ r)     (later tx) = terminates _ {eq} r tx

  loops : ∀ {x y} k → Rel k x y → Loops x → Loops y
  loops k  (Equality.later x∼y) (later l) = later (♯ (loops k (♭ x∼y) (♭ l)))
  loops ._ (Equality.laterʳ  r) (later l) = later (♯ (loops _ r (later l)))
  loops ._ (Equality.laterˡ  r) (later l) = loops _ r (♭ l)

>>=-terminates : ∀ {a} {A : Set a} {B : Set a} 
         {x : Partial A} (tx : Terminates x) {f : A → Partial B} (tf : ∀ x → Terminates (f x))
       → Terminates (x M.>>= f)
>>=-terminates (now x) tf = tf x
>>=-terminates {B = B} (later tx) tf = terminates (other weak) (Equality.laterʳ (refl PropEq.refl)) (>>=-terminates tx tf)
  where open Respects {A = B} _≡_

record Semidecidable {A} (P : A → Set) : Set where
  field
    decide          : ∀ x → Partial (P x)
    true-terminates : ∀ x → P x → Terminates (decide x)

-- Thanks to twanvl, benmachine, and the inhabitants of #Agda for pointing out that this didn't need to be a field of Semidecidable and
-- to twanvl in particular fo rwriting this implementation.
false-loops : ∀ {a} {A : Set a} → (decider : Partial A) → ¬ A → Loops decider
false-loops (now   x) ¬A = ⊥-elim (¬A x)
false-loops (later x) ¬A = later (♯ false-loops (♭ x) ¬A)  




open import Data.Conat renaming (setoid to Coℕ-setoid)

data Finite : Coℕ → Set where
  zero : Finite zero
  suc  : ∀ {n} (i : Finite (♭ n)) → Finite (suc n)

finite : Semidecidable Finite
finite = record
  { decide          = decide
  ; true-terminates = true-terminates
  }
  where
  open Workaround
  open Correct

  mutual
    decide-lemma : ∀ x → (Finite x) ⊥P
    decide-lemma x = later (♯ decide-helper x)

    decide-helper : ∀ x → (Finite x) ⊥P
    decide-helper zero    = now zero
    decide-helper (suc n) = decide-lemma (♭ n) >>= (now ∘′ suc)

  decide : ∀ x → Partial (Finite x)
  decide x = ⟦ decide-helper x ⟧P

  true-terminates : ∀ x → Finite x → Terminates (decide x)
  true-terminates zero zero = now zero
  true-terminates (suc n) (suc f) = 
      terminates strong 
        (sym PropEq.sym _ (>>=-hom (decide-lemma (♭ n)) (now ∘′ suc)))
        (later (>>=-terminates (true-terminates (♭ n) f) (λ x → now (suc x))))
    where open Respects {A = Finite (suc n)} _≡_