[Agda] Termination proof in partiality monad

[Dan Doel]

All right. In light of the input (I didn't realize I was bumping into the same 
old usual problem with codata), I've reformulated the proofs into something 
more akin to Anton Setzer's coalgebraic approach, and got something that types 
now. Enjoy (Prelim again contains Nat and Sigma):

--------------------------------------------------------------------------------

module Partial where

data _⊎_ (a b : Set) : Set where
  inl : a -> a ⊎ b
  inr : b -> a ⊎ b

codata D (a : Set) : Set where
  now   : a -> D a
  later : D a -> D a

_⋆ : {a : Set} -> D a -> a ⊎ D a
now a ⋆    = inl a
later da ⋆ = inr da

never : {a : Set} -> D a
never ~ later never

return : {a : Set} -> a -> D a
return x = now x

infixl 40 _>>=_
_>>=_ : {a b : Set} -> D a -> (a -> D b) -> D b
da >>= f with da ⋆
...      | inl a   ~ f a
...      | inr da' ~ later (da' >>= f)

map-D : {a b : Set} -> (a -> b) -> D a -> D b
map-D f da with da ⋆
...        | inl a   ~ now (f a)
...        | inr da' ~ later (map-D f da')

fix-aux : {a b : Set} (k : a -> D b) (f : (a -> D b) -> a -> D b) -> a -> D b
fix-aux k f a with f k a ⋆
...           | inl v ~ now v
...           | inr _ ~ later (fix-aux (f k) f a)

fix : {a b : Set} (f : (a -> D b) -> a -> D b) -> a -> D b
fix = fix-aux (\_ -> never)

--------------------------------------------------------------------------------

module Convergence where

open import Prelim
open import Partial

mutual
  infix 35 _↓_
  _↓_ : {a : Set} -> D a -> a -> Set
  dx ↓ v with dx ⋆
  ...    | inl x   = ConvergeNow x v
  ...    | inr dx' = ConvergeLater dx' v

  data ConvergeNow {a : Set} (x : a) : a -> Set where
    converge-now : ConvergeNow x x

  data ConvergeLater {a : Set} (dx : D a) (v : a) : Set where
    converge-later : dx ↓ v -> ConvergeLater dx v

_↓ : {a : Set} -> D a -> Set
_↓ {a} dx = Σ a (_↓_ dx)

map-D-↓ : {a b : Set}{dx : D a}{v : a} (f : a -> b) -> dx ↓ v -> map-D f dx ↓ 
f v
map-D-↓ {a}{b}{dx} f pf with dx ⋆
map-D-↓ {a} {b} {dx} {v} f converge-now        | inl .v = converge-now
map-D-↓                  f (converge-later pf) | inr y  = converge-later (map-
D-↓ f pf)

-- Sorry this isn't so pretty. This isn't ever used anywhere, but it may be
-- instructive I suppose.
>>=-↓ : {a b : Set} {dx : D a}{v : a}{v' : b}
        (f : a -> D b) -> dx ↓ v -> f v ↓ v' -> dx >>= f ↓ v'
>>=-↓ {a}{b}{dx} f pfa pfb with dx ⋆
>>=-↓ {a}{b}{dx}{v} f converge-now pfb | inl .v with f v ⋆
>>=-↓ {dx} {b} {_} {v} {v'} f converge-now converge-now
  | inl .v | inl .v' = converge-now 
>>=-↓ f converge-now (converge-later pf) | inl .v | inr y = converge-later pf
>>=-↓ f (converge-later y) pfb | inr dx' = converge-later (>>=-↓ f y pfb)

--------------------------------------------------------------------------------

module Factorial where

open import Prelim
open import Partial
open import Convergence

fac-aux : (Nat -> D Nat) -> Nat -> D Nat
fac-aux _   zero    = return 1
fac-aux fac (suc n) = map-D (_*_ (suc n)) (fac n)

fac : Nat -> D Nat
fac = fix fac-aux

fix-fac-ind : {g : Nat -> D Nat} {n k : Nat}
            -> fix-aux g fac-aux n ↓ k
            -> fix-aux (fac-aux g) fac-aux (suc n) ↓ suc n * k
fix-fac-ind {g} {n} pf with fac-aux g n ⋆
fix-fac-ind {g} {n} {k} converge-now | inl .k = converge-now 
fix-fac-ind (converge-later pf) | inr y = converge-later (fix-fac-ind pf)

fac-↓ : forall {n} -> fac n ↓
fac-↓ {0}     = 1 , converge-now  
fac-↓ {suc n} with fac-↓ {n}
fac-↓ {suc n} | n! , pf-n!-↓
        = (suc n * n! , converge-later (fix-fac-ind pf-n!-↓)) 

--------------------------------------------------------------------------------

And there you have it. A genuine proof of convergence for factorial that 
passes the type checker. Proof for a version of fix that actually works 
correctly is left as an exercise to the reader. :)

Cheers,
-- Dan