[Agda] proofs for (NON)TERMINATING

[Sergei Meshveliani]

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