[Agda] proofs for (NON)TERMINATING

[Martin Escardo]

On 05/02/18 10:33, Jesper at sikanda.be 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.

Or you can define a relation R, and show that if R 0 y then y is even.

M.

> 
> -- Jesper
> 
> On Mon, Feb 5, 2018 at 10:48 AM, Sergei Meshveliani <mechvel at botik.ru 
> <mailto: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
> 
> 
> 
> 
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
> 

-- 
Martin Escardo
http://www.cs.bham.ac.uk/~mhe