The Coq mailing list

[Castéran Pierre <pierre.casteran AT gmail.com>]

Dear Coq users,


The objective of coq-community <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 
<https://github.com/coq-community/hydra-battles>


The illustrated topics are:

   - ordinal notations, hydra-battles:
      This part is an extension of <https://github.com/coq-contribs/cantor>
   - primitive recursive functions and Peano Arithmetic
      (a part of Russel O'Connor's development on Gödel's 1st incompleteness 
theorem <https://github.com/coq-community/goedel> ). 
   - addition chains (exponentiation algorithms)
 (extension of <https://github.com/coq-contribs/additions>).

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