alizter / hydra-battles

Variations on Kirby & Paris' hydra battles and other entertaining math in Coq (collaborative, documented, includes exercises) [maintainer=@Casteran]

Hydras & Co.

This Coq-based project has three parts:

• An exploration of some properties of Kirby and Paris' hydra battles, including the study of several representations of ordinal numbers and a part of the so-called Ketonen and Solovay machinery (combinatorial properties of epsilon0).

  This part also hosts the formalization by Russell O'Connor of primitive recursive functions and Peano arithmetic (see the Goedel project).

• Some algorithms for computing x^n with as few multiplications as possible (using addition chains).

• A bridge to definitions and results in the Gaia project, in particular on ordinals.

Both the documentation and the Coq sources are work continuously in progress. For more information on how the project is organized, maintained, and documented, see this paper, to appear in the proceedings of JFLA 2022.

Meta

• Author(s):
  • Yves Bertot
  • Pierre Castéran
  • Évelyne Contejean
  • Jeremy Damour
  • Russell O'Connor
  • Karl Palmskog
  • Clément Pit-Claudel
  • Théo Zimmermann
• Coq-community maintainer(s):
  • Pierre Castéran (@Casteran)
• License: MIT License
• Compatible Coq versions: 8.13 or later
• Additional dependencies:
  • Equations 1.2 or later
  • Paramcoq 1.1.3 or later
  • MathComp SSReflect 1.12 or later
  • MathComp Algebra
  • Gaia's Schütte ordinals 1.14 or later
  • Mczify
  • LibHyps
• Coq namespace: hydras, additions, gaia_hydras
• Related publication(s):
  • Hydras & Co.: Formalized mathematics in Coq for inspiration and entertainment
  • Accessible Independence Results for Peano Arithmetic doi:10.1112/blms/14.4.285
  • Rapidly Growing Ramsey Functions doi:10.2307/2006985
  • Proof Theory doi:10.1007/978-3-642-66473-1

Building and installation

• To get the required dependencies, you can use opam or Nix. With opam:

  • opam install ./coq-hydra-battles.opam --deps-only to get the hydra battles dependencies;
  • opam install ./coq-addition-chains.opam --deps-only to get the addition chains dependencies.
  • opam install ./coq-gaia-hydras.opam --deps-only to get the gaia hydras dependencies.

  With Nix, just run nix-shell to get all the dependencies (including for building the documentation). If you only want the dependencies to build a sub-package, you can run one of:

  • nix-shell --argstr job hydra-battles
  • nix-shell --argstr job addition-chains
  • nix-shell --argstr job gaia-hydras

• Building the PDF documentation also requires Alectryon 1.4 and SerAPI. See doc/movies/Readme.md for details.

• The general Makefile is in the top directory:

  • make : compilation of the Coq scripts
  • make pdf : generation of PDF documentation as doc/hydras.pdf
  • make html : generation of HTML documentation in theories/html

• You may also rely on dune to install just one part. Run:

  • dune build coq-hydra-battles.install to build only the hydra battles part
  • dune build coq-addition-chains.install to build only the addition chains part
  • dune build coq-gaia-hydras.install to build only the gaia hydras part

• Documentation for the master branch is continuously deployed at:

  • https://coq-community.org/hydra-battles/doc/hydras.pdf
  • https://coq-community.org/hydra-battles/theories/html/toc.html

Contents

Coq sources (directory theories)

• theories/ordinals

  • Hydra/*.v

    • Representation in Coq of hydras and hydra battles
    • A proof of termination of all hydra battles (using ordinal numbers below epsilon0)
    • A proof that no variant bounded by some ordinal less than epsilon0 can prove this termination
    • Comparison of the length of some kind of Hydra battles with the Hardy hierarchy of fast growing functions

  • OrdinalNotations/*.v

    • Generic formalization on ordinal notations (well-founded ordered datatypes with a comparison function)

  • Epsilon0/*.v

    • Data types for representing ordinals less than epsilon0 in Cantor normal form
    • The Ketonen-Solovay machinery: canonical sequences, accessibility, paths inside epsilon0
    • Representation of some hierarchies of fast growing functions

  • Schutte/*.v

    • An axiomatization of countable ordinals, after Kurt Schütte. It is intended to be a reference for the data types considered in theories/Epsilon0.

  • Gamma0/*.v

    • A data type for ordinals below Gamma0 in Veblen normal form (draft).

  • rpo/*.v

    • A contribution on recursive path orderings by Evelyne Contejean.

  • Ackermann/*.v

    • Primitive recursive functions, first-order logic, NN, and PA (from Goedel contrib)

  • MoreAck/*.v

    • Complements to the legacy Ackermann library

  • Prelude/*.v

    • Various auxiliary definitions and lemmas

• theories/additions/*.v

  • Addition chains

• theories/gaia/*.v

  • Bridge to the ordinals in Gaia that are encoded following Schütte and Ackermann

Exercises

• exercises/ordinals/*.v

  • Exercises on ordinals

• exercises/primrec/*.v

  • Exercises on primitive recursive functions

Contributions are welcome

Any suggestion for improving the Coq scripts and/or the documentation will be taken into account.

• In particular, we would be delighted to replace proofs with simpler ones, and/or to propose various proofs or definitions of the same concept, in order to illustrate different techniques and patterns. New tactics for automatizing the proofs are welcome too.

• Along the text, we propose several projects, the solution of which is planned to be integrated in the development.

• Please do not hesitate to send your remarks as GitHub issues and your suggestions of improvements (including solutions of "projects") as pull requests.

• Of course, new topics are welcome !

• If you wish to contribute without having to clone the project / install the dependencies on your machine, you may use Gitpod to get an editor and all the dependencies in your browser, with support to open pull requests as well.

• Contact : pierre dot casteran at gmail dot com

A bibliography is at the end of the documentation. Please feel free to suggest more references to us.