coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Fibonacci in Coq?

From: Kenneth Adam Miller <kennethadammiller AT gmail.com>
To: coq-club Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Fibonacci in Coq?
Date: Fri, 27 Oct 2017 11:23:41 -0400
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=kennethadammiller AT gmail.com; spf=Pass smtp.mailfrom=kennethadammiller AT gmail.com; spf=None smtp.helo=postmaster AT mail-lf0-f53.google.com
Ironport-phdr: 9a23:TKVPeRbDViYTAePHS4Wj1rT/LSx+4OfEezUN459isYplN5qZpcyybnLW6fgltlLVR4KTs6sC0LWG9f24EUU7or+/81k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i76xXcoFx7+LQt4IPjuUs6X1pzvlrP6x5qGaAJRwTG5fLk6BxGrp02Fvc4PxIBmN6wZyx3To3IOdf4Alk1yIlfGvBv64Mqs/NZK/y1V89cg88pNS+2ufKk+S7FEDD0qOmUw5cnvuAPrQg6G539aWWITxEkbSzPZ5Q33C8+i+hDxsfBwjWzDZZX7

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

[Coq-Club] Fibonacci in Coq?, Kenneth Adam Miller, 10/26/2017
- Re: [Coq-Club] Fibonacci in Coq?, Laurent Thery, 10/27/2017
  - Re: [Coq-Club] Fibonacci in Coq?, Kenneth Adam Miller, 10/27/2017
    - Re: [Coq-Club] Fibonacci in Coq?, Pierre Letouzey, 10/27/2017
      - Re: [Coq-Club] Fibonacci in Coq?, Kenneth Adam Miller, 10/27/2017