[Agda] proofs for (NON)TERMINATING

[Jesper Cockx]

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.

-- Jesper

On Mon, Feb 5, 2018 at 10:48 AM, Sergei Meshveliani <mechvel at botik.ru>
wrote:

> On Tue, 2018-01-23 at 15:21 +0100, Jesper Cockx wrote:
>
> JC: -------------------------------------------------------------------
> If you define a function with a {-# NON_TERMINATING #-} pragma then
> it's generally not possible to prove things about it because Agda will
> refuse to evaluate it. This is also the problem in your example: even
> though in this case evaluation is terminating, Agda will play it safe
> and block *all* evaluation of the NON_TERMINATING function. So I don't
> think what you're trying to do is currently possible in Agda.
>
> A workaround is to postulate the clauses of the non-terminating function
> as propositional equalities (i.e. elements of the ≡ type). This allows
> you to prove properties of the non-terminating function without breaking
> the Agda typechecker (as you risk doing when using TERMINATING). In your
> example:
> [..]
>
> postulate
>   find-yes : (m n : ℕ) ( pmn :   P m n) → p? m n ≡ yes pmn →
>                                           find m n ≡ (n , pmn)
>   find-no  : (m n : ℕ) (¬pmn : ¬ P m n) → p? m n ≡ no ¬pmn →
>                                           find m n ≡ find m (suc n)
> [..]
>
> Something we could consider adding to Agda is some facility to get hold
> of the clauses of a non-terminating function automatically, so you
> wouldn't have to postulate them.
> -------------------------------------------------------------------------
>
>
>
> Thank you. This is interesting.
>
> My goal is to find a simple way to express in Agda proofs about an
> algorithm which termination domain is not known.
> Is there a simpler approach than applying coinductive types and `delay'
> monad?
>
> I try your approach of "postulate-clauses" on the following simple
> example.
>
> f (m : ℕ)  searches for  n ≥ m  such that  P n,  and when finds,
> returns  n + n.
> It is needed to represent and prove the statement
>                 "if (f 0) terminates, then  Even (f 0)"     (I).
>
> --------------------------------------------------------------------
> open import Function         using (_∘_)
> open import Relation.Nullary using (Dec; yes; no; ¬_)
> open import Relation.Unary   using (Decidable)
> open import Relation.Binary.PropositionalEquality as PE using
>                                   (_≡_; refl; sym; trans; cong; subst)
> open import Data.Product using (_×_; _,_; ∃)
> open import Data.Nat using (ℕ; suc; _+_; _<_; _>_; _≤_)
> open import Data.Nat.Properties using
>             (≤-refl; ≤-reflexive; ≤-trans; m+n∸m≡n; +-comm; +-assoc;
>              m≤m+n; <⇒≱; ≰⇒>; module ≤-Reasoning)
>
> 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
>
>
> postulate  f-yes :  ∀ n → P n   → f n ≡ n + n
>            f-no  :  ∀ n → ¬ P n → f n ≡ f (suc n)
>
> 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
>
> postulate
>   minimizeSolution :  ∀ m → P m → ∃ (\n → P n × f 0 ≡ f n)
>   --
>   -- Can be proved by moving from m to minimal i such that (P i),
>   -- and by applying  f-yes, f-no.
>
> theorem :  ∀ m → P m → Even (f 0)
> theorem m pm =
>   let
>     (n , pn , f0≡fn) = minimizeSolution m pm
>     fn≡n+n  = f-yes n pn
>     even-fn = subst Even (sym fn≡n+n) (even-n+n n)
>   in
>   subst Even (sym f0≡fn) even-fn
> ------------------------------------------------------------------
>
>
> First, I think that  (Even (f 0))  cannot be proved. Right?
>
> Further, the condition  "if (f 0) terminates"  is replaced with
> "∀ m → P m".
>
> I have an impression that `theorem' represents (I), in a certain sense,
> and proves it.
> Am I missing something?
>
> In general:
> this approach works when the programmer is able to formulate the
> statement
>                     "(g x1 ... xn)  terminates"
>
> as some Agda predicate in  x1 ... xn.
> For example, this is possible for any semidecision procedure  g
> (?)
> I wonder: how generic is this approach.
>
> What people think?
>
> Thanks,
>
> ------
> Sergei
>
>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180205/254c61f3/attachment.html>