[Agda] termination proof problem

[Sergei Meshveliani]

No.
The problem is

  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.

Concerning all the rest -- see my first letter on the subject.

Being not an expert in constructive mathematics, I understand the case
as follows:

------------------------------------------------
It is given a terminating algorithm for `bound'. In a linear
search-through with  y = n+1, n+2 ...,  with checking each (P? y), 
the event of (P y) will happen not later than  y = bound n.  
Hence this search-through is proved terminating. 
Hence there is no need to compare  y  to  (bound n) for each current  y
at the run-time computation.
One only has to check (P? y). If (yes _), the search stops, otherwise go
to (suc y).
------------------------------------------------

How to express a similar approach in Agda?
In my attempts, the program applies for each  y  the comparison  
((bound n) - y)  to  0,  and even a single such comparison spoils
performance when it happens at run-time.

Thanks,

------
Sergei


On Mon, 2016-03-28 at 18:37 +0900, Andrea Vezzosi wrote:
> Do you also mean "y < n" ?
> 
> On Mon, Mar 28, 2016 at 5:01 AM, Sergei Meshveliani <mechvel at botik.ru> wrote:
> > On Sun, 2016-03-27 at 23:56 +0400, Sergei Meshveliani wrote:
> >> Can people explain, please, the following subject concerning termination
> >> proof tools?
> >>
> >> Having certain
> >>                    P : ℕ → Set  and   P? : Decidable P,
> >>
> >> one needs to implement
> >>
> >>     search :  (n : ℕ) → ∃ \y →  m < y × P y × IsMinimalSuch y
> >>
> >> -- find the first  y  after  m  such that  P y.
> >> [..]
> >
> >
> > Fixing a typo:  replace  "m"  with  "n"  in these two lines.
> >
> []




> > ------
> > Sergei
> >
> > _______________________________________________
> > Agda mailing list
> > Agda at lists.chalmers.se
> > https://lists.chalmers.se/mailman/listinfo/agda
>