The Coq mailing list

[Kenneth Adam Miller <kennethadammiller AT gmail.com>]

These properties are likely going to be very helpful! I was actually digging around for some listing of these so that I could leverage them even just as you sent that. The links are rather very different to me, I probably would not have found them.

On Fri, Oct 27, 2017 at 12:29 PM, Pierre Letouzey <pierre.letouzey AT inria.fr> wrote:

That's probably not what you're looking for, but I couldn't resist advertizing this:

https://hal.inria.fr/hal-01195587/document
https://www.irif.fr/~letouzey/hofstadter_g/

tl;dr: playing with the recursive function g(n)=if n=0 then 0 else n-g(g(n-1)) leads to
strange worlds filled with Fibonacci numbers and fractal trees.

Regards
Pierre L.

----- Mail original -----

> Cool thanks!
>
> I'm looking for analytic continuations of the continuous series as well as
> an alternative to starting at zero, and lastly some theoretic derivations
> of it's convergence point, with the work shown.
>
> On Fri, Oct 27, 2017 at 2:51 AM, Laurent Thery <Laurent.Thery AT inria.fr>
> wrote:
>
> >
> >
> > On 10/26/2017 09:44 PM, Kenneth Adam Miller wrote:
> > > Hello,
> > >
> > > Does anybody know of any theorems or number theoretic work done using
> > > fibonacci in Coq?
> > >
> > > Thanks in advance!
> >
> > I don't know which results you have in mind. The mathcomp has only some
> > basic properties of the fib function
> >
> > https://github.com/math-comp/math-comp/blob/master/mathcomp/attic/fib.v
> >
> > --
> > Laurent
> >
> > Ps: fib.v is not part of the standard  mathcomp library
> >
>