[Agda] termination proof problem

[Sergei Meshveliani]

Here is a concrete example.
Goal: find the first prime after a given prime  p : ℕ.

 firstPrimeAfter :  
      (p : ℕ) → IsPrime p → 
                (∃ \q →  p < q  ×  IsPrime q  ×  NoPrimeBetween p q)

The function  
             firstNonUnityFactor :  (n : ℕ) → n > 1 → ∃ \p → ...

finds the first non-unity factor in  n.  
It is implemented by searching through  2, 3 ... n.
It is proved in Agda that it returns the least _prime_ factor in  n.

The function
              prime? : Decidable IsPrime p  

is implemented trivially via  firstNonUnityFactor.
Then,  firstPrimeAfter  is programmed as a search-through

             y = 1+p, 2+p, ..., (bound p)

(bound p)  is needed for termination proof.
We put

 bound p = let ps = p1, p2, ..., p   -- all primes up to p
               a  = product ps       -- = p1 * p2 * ... * p
               b  = 1 + a
           in
           firstNonUnityFactor b

It is proved in Agda that  p < bound p  and  IsPrime p.

------------
(bound p)  is needed only for termination proof.
And it must not start to compute at run-time, because this is expensive.
------------

How to arrange this in Agda?

In this particular example, it is possible to combine the two bounds:
(bound n) and 
bound-easyToCompute  -- "there is a prime between  p  and  2*p".

The former is easy to proof but expensive to compute.
The latter is easy to compute at run-time but difficult to prove. 

But there are possible other examples, where it is known only the former
bound.

Regards,

------
Sergei
                 



On Mon, 2016-03-28 at 14:47 +0300, Sergei Meshveliani wrote:
> [..]

>   Having certain   P : ℕ → Set,  P? : Decidable P,   and any  n : ℕ,
>   
>   find the first  y  after  n  such that  P y.
> 
> That is one needs to implement in Agda
> 
>      search :  (n : ℕ) →  ∃ \y →  n < y  ×  P y  ×  IsMinimalSuch y
> 
> And it is already type-checked the program for
> 
>      bound :  (n : ℕ) →  ∃ \y →  n < y  ×  P y 
> 
> Having this `bound', I program a linear search-through for `search',
> where `bound' serves as a counter to prove termination.
>   
> The functions for  P, P?, bound   are simple to type check.
> Also P and P' are fast at run-time, assume that they take one tick of
> time.
> But `bound'  is expensive at run-time. 
> For example, to computing  (bound 50)  makes a linear search-through
> practically unusable -- if it ever applies (bound 50) at run-time.
> 
> [..]