[Agda] termination proof problem

[Ulf Norell]

A trick you can use is to skip checking the bound until after a finite (but
possibly large) number of steps. Basically you write a fast search that
takes a counter starting at a billion (say) that ignores the bound and only
when that counter reaches zero do you switch to the slow search where you
check the bound. For your example:

https://gist.github.com/UlfNorell/f2d8674b1d6b98172827

Apologies for making a mess of the ordering proofs, I don't really know my
way around the standard library.

/ Ulf

On Mon, Mar 28, 2016 at 5:48 PM, Sergei Meshveliani <mechvel at botik.ru>
wrote:

> On Mon, 2016-03-28 at 16:46 +0300, Sergei Meshveliani wrote:
> > 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)
> > [..]
>
> >  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.
> > [..]
>
>
> Sorry, fixing a typo:
>
>  It is proved in Agda that  p < bound p  and  IsPrime (bound p).
>
>
> ------
> Sergei
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20160329/fe0b2556/attachment-0001.html