Investigation of Hofstadter's G function and tree and mirror

A Coq development by Pierre Letouzey, Summer 2015

• The Git repository on github
• The tarball of Version 1.4 (for Coq 8.4)
• The technical report, with proofs in English, and its page on HAL
• The browsable documentation via coqdoc (without the proofs)
• Here comes the README:

  To be compiled with Coq 8.4.
  
  Use "make gallinahtml" to generate the short html documentation.
  Use "pdflatex report" to generate the pdf of the technical report.
  
  Summary of files:
  ----------------
  
  - DeltaList: lists of natural numbers with constrained differences
  - Fib: Fibonacci sequence and decomposition
  - FunG: Hofstadter's G function and tree
  - FunG_prog: Alternative definition of Hofstadter's G function
  - Phi: Hofstadter G function and the golden ratio
  - FlipG: Hofstadter's flipped G tree
  
  References:
  ----------
  
  - Hofstadter's book: Goedel, Escher, Bach, page 137.
  - For G : http://oeis.org/A005206
  - For flipped-G : http://oeis.org/A123070
  
  License
  -------
  
  The Coq files of this development are released in the Public Domain,
  see the LICENSE file in the current directory.
  
  The technical report report.tex is released under the CC-BY 4.0 license,
  see http://creativecommons.org/licenses/by/4.0/