# Hydra battles

**URL:** <https://discourse.rocq-prover.org/t/hydra-battles/1216>\
**Category:** Announcements\
**Created:** [February 22, 2021, 7:33am UTC](https://discourse.rocq-prover.org/t/hydra-battles/1216 "2021-02-22T07:33:19Z")\
**Posts on this page:** 1\
**Page:** 1

<div class="post-metadata">

**Author:** ![casteran](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/casteran/32/451_2.png) [@casteran](https://discourse.rocq-prover.org/u/casteran)\
**Post date:** [February 22, 2021, 7:33am UTC](https://discourse.rocq-prover.org/t/hydra-battles/1216/1 "2021-02-22T07:33:19Z")

</div>

Dear Coq users,

The objective of coq-community \<[coq-community · GitHub](https://github.com/coq-community)\> is to maintain and/or document coq developments. The project hydra-battles (in reference to Kirby and Paris's work) is an attempt to understand which kind of document may go with Coq libraries. It is developped in \<[GitHub - coq-community/hydra-battles: Variations on Kirby & Paris' hydra battles and other entertaining math in Coq (collaborative, documented, includes exercises) [maintainer=@Casteran]](https://github.com/coq-community/hydra-battles)\>

The illustrated topics are:

&nbsp;&nbsp;&nbsp;- ordinal notations, hydra-battles:  
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;This part is an extension of \<[GitHub - coq-contribs/cantor: On Ordinal Notations](https://github.com/coq-contribs/cantor)\>  
&nbsp;&nbsp;&nbsp;- primitive recursive functions and Peano Arithmetic  
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(a part of Russel O'Connor's development on Gödel's 1st incompleteness theorem \<[GitHub - coq-community/goedel: The Gödel-Rosser 1st incompleteness theorem in Coq [maintainer=@Casteran]](https://github.com/coq-community/goedel)\> ).  
&nbsp;&nbsp;&nbsp;- addition chains (exponentiation algorithms)  
(extension of \<[GitHub - coq-contribs/additions: Addition Chains](https://github.com/coq-contribs/additions)\>).

A documentation (in pdf) is available at \<[https://coq-community.org/hydra-battles/hydras.pdf](https://coq-community.org/hydra-battles/hydras.pdf)\>. A few exercises are proposed too.

This is clearly (and it will be for a long time) a work in progress. The following tasks should have priority:  
&nbsp;&nbsp;&nbsp;  
&nbsp;&nbsp;&nbsp;- Maintenance w.r.t. Coq versions. Inclusion of new proof patterns and tactics into the legacy libraries (without causing incompatibilities).  
&nbsp;&nbsp;&nbsp;- Add examples and comments on considered libraries.  
&nbsp;&nbsp;  
&nbsp;&nbsp;&nbsp;- Simplification, bulletization of proofs, coqdoc comments, etc.  
&nbsp;&nbsp;&nbsp;  
&nbsp;&nbsp;&nbsp;- Add more consistency to the names and arguments of functions and lemmas, etc.  
&nbsp;&nbsp;  
We acknowledge in advance any suggestion for improving the libraries and documentation, and any form of participation (issues, PR, etc).

Pierre