[Agda] proofs for (NON)TERMINATING

[Sergei Meshveliani]

On Mon, 2018-02-05 at 11:33 +0100, Jesper Cockx wrote:
> 
>         It is needed to represent and prove the statement
>                         "if (f 0) terminates, then  Even (f 0)"
>          (I).
> I don't think it's possible to formulate inside Agda what it means for
> a function with a {-# NON_TERMINATING #-} pragma to terminate. So I
> also don't think it's possible to represent the statement you want. If
> you want to reason in Agda about termination of functions, I'd
> recommend to use the Delay monad as Nils suggested.


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)



-------------------------------------------------------------------
open import Relation.Nullary using (yes; no)
open import Relation.Unary   using (Decidable)
open import Data.Nat         using (ℕ; suc; _+_)

postulate  P  : ℕ → Set
           p? : Decidable P

{-# NON_TERMINATING #-}
f : ℕ → ℕ             -- find n satisfying (P n) and return  n + n
f n
    with p? n
... | yes _ = n + n      -- found
... | no  _ = f (suc n)  -- try next


data Even : ℕ → Set
     where
     even0  : Even 0
     even+2 : {n : ℕ} → Even n → Even (suc (suc n))

postulate
  even-n+n : ∀ n → Even (n + n)  -- the proof skipped for brevity
----------------------------------------------------------------------


Thanks,

------
Sergei