[Agda] proofs for (NON)TERMINATING

[Nils Anders Danielsson]

On 2018-02-05 12:36, Sergei Meshveliani wrote:
> Can anybody, please, demonstrate the usage of the Delay monad on the
> below example of  f : ℕ → ℕ  and expressing the statement
> 
>                    "if (f 0) terminates, then  Even (f 0)"         (I)

.agda-lib file:

   depend: equality delay-monad

.agda file:

   module _ where

   open import Delay-monad
   open import Delay-monad.Always
   open import Delay-monad.Monad
   open import Equality.Propositional
   open import Prelude

   open import Monad equality-with-J

   Even : ℕ → Set
   Even n = ∃ λ k → n ≡ k + k

   module _
     (P  : ℕ → Set)
     (p? : ∀ n → Dec (P n))
     where

     f : ∀ {i} → ℕ → Delay ℕ i
     f n with p? n
     ... | yes _ = return (n + n)
     ... | no  _ = later λ { .force → f (suc n) }

     f-even : ∀ {i} n → □ i Even (f n)
     f-even n with p? n
     ... | yes _ = now (n , refl)
     ... | no  _ = later λ { .force → f-even (suc n) }

-- 
/NAD