meta.yml

---
fullname: Hydra battles and Cie (_work in progress_)
shortname: hydra-battles
organization: coq-community
community: true
action: true

synopsis: Exploration of some properties of Kirby and Paris' hydra battles, with the help of Coq

description: |-
  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_).

build: |-
  ## 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.

  - 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/hydras.pdf

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

publications:
- pub_url: https://faculty.baruch.cuny.edu/lkirby/accessible_independence_results.pdf
  pub_title: Accessible Independence Results for Peano Arithmetic
  pub_doi: 10.1112/blms/14.4.285
- pub_url: https://www.jstor.org/stable/2006985
  pub_title: Rapidly Growing Ramsey Functions
  pub_doi: 10.2307/2006985
- pub_url: https://link.springer.com/book/10.1007/978-3-642-66473-1
  pub_title: Proof Theory
  pub_doi: 10.1007/978-3-642-66473-1

authors:
- name: Pierre Castéran

maintainers:
- name: Pierre Castéran
  nickname: Casteran

opam-file-maintainer: palmskog@gmail.com

opam-file-version: dev

license:
  fullname: MIT License
  identifier: MIT

supported_coq_versions:
  text: 8.13 or later
  opam: '{(>= "8.13" & < "8.14~") | (= "dev")}'

tested_coq_opam_versions:
- version: 'coq-dev'
  repo: 'mathcomp/mathcomp-dev'
- version: '1.12.0-coq-8.13'
  repo: 'mathcomp/mathcomp'

dependencies:
- opam:
    name: coq-equations
    version: '{(>= "1.2" & < "1.3~") | (= "dev")}'
  description: |-
    [Equations](https://github.com/mattam82/Coq-Equations) 1.2 or later
- opam:
    name: coq-paramcoq
    version: '{(>= "1.1.2" & < "1.2~") | (= "dev")}'
  description: |-
    [Paramcoq](https://github.com/coq-community/paramcoq) 1.1.2 or later
- opam:
    name: coq-mathcomp-ssreflect
    version: '{(>= "1.12.0" & < "1.13~") | (= "dev")}'
  description: |-
    [MathComp SSReflect](https://github.com/math-comp/math-comp) 1.12 or later
- opam:
    name: coq-mathcomp-algebra
  description: |-
    MathComp Algebra

namespace: hydras

keywords:
- name: Ketonen-Solovay machinery
- name: ordinals
- name: primitive recursive functions

categories:
- name: Mathematics/Combinatorics and Graph Theory
- name: Mathematics/Logic/Foundations

documentation: |-
  ##   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.
---