Dear Coq users,
The objective of coq-community <coq-community · GitHub> 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]>
The illustrated topics are:
- ordinal notations, hydra-battles:
This part is an extension of <GitHub - coq-contribs/cantor: On Ordinal Notations>
- primitive recursive functions and Peano Arithmetic
(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]> ).
- addition chains (exponentiation algorithms)
(extension of <GitHub - coq-contribs/additions: Addition Chains>).
A documentation (in pdf) is available at <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:
- Maintenance w.r.t. Coq versions. Inclusion of new proof patterns and tactics into the legacy libraries (without causing incompatibilities).
- Add examples and comments on considered libraries.
- Simplification, bulletization of proofs, coqdoc comments, etc.
- Add more consistency to the names and arguments of functions and lemmas, etc.
We acknowledge in advance any suggestion for improving the libraries and documentation, and any form of participation (issues, PR, etc).
Pierre