/hydra-battles

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

Primary LanguageCoqMIT LicenseMIT

Hydras & Co.

Docker CI Contributing Code of Conduct Zulip

This Coq-based project has four 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 a formalization by Russell O'Connor of primitive recursive functions and Peano Arithmetic (PA).

  • 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.

  • A proof originally by Russell O'Connor of the Gödel-Rosser 1st incompleteness theorem, which says that any first order theory extending NN (which is PA without induction) that is complete is inconsistent.

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 from the proceedings of JFLA 2022.

Meta

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.
    • opam install ./coq-goedel.opam --deps-only to get the Goedel 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
    • nix-shell --argstr job goedel

  • 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
    • dune build coq-goedel.install to build only the goedel part

  • Documentation for the master branch is continuously deployed at:

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

    • 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

  • theories/goedel/*.v

    • Gödel's 1st incompleteness theorem and its variations

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.