cpitclaudel/hydra-battles

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

Hydra battles and Cie (work in progress)

This contribution contains two parts:

• An exploration of some properties of Kirby and Paris' hydra battles, with the help of the Coq Proof assistant. This development includes the study of several representations of ordinal numbers, and a part of the so-called Ketonen and Solovay machinery (combinatorial properties of epsilon0).

  • This project also hosts the formalization by Russel O'Connor of primitive recursive functions and Peano arithmetics (see https://github.com/coq-community/goedel)

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

Meta

• Author(s):
  • Pierre Castéran
• 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.2 or later
  • MathComp SSReflect 1.12 or later
  • MathComp Algebra
• Coq namespace: hydras + additions
• Related publication(s):
  • 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

Installation

• To get the required dependencies, the easiest way is to use opam. Run:

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

• Building the PDF documentation also requires Alectryon 1.3.1 or later, 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 the documentation
  • make html : generation of coqdoc html files

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

Documentation

Documentation for the master branch is continuously deployed at: https://coq-community.org/hydra-battles/doc/hydras.pdf

The command make pdf generates a local copy as doc/hydras.pdf.

Contents

coqdoc html files

• directory theories/html

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

Exercises

• directory exercises/

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 !

• Contact : pierre dot casteran at gmail dot com

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