[Agda] proofs for (NON)TERMINATING

[Sergei Meshveliani]

On Mon, 2018-02-05 at 14:06 +0100, Nils Anders Danielsson wrote:
> 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) }
> 



Thank you. I shall keep this in mind.
One day the DoCon-A library may need to prove something about a function
with unsolved termination domain.

------
Sergei