@palmskog @Zimmi48

The branch dev seems to fail with 8.11, probably because of a lemma VectorSpec.Forall_forall (OK in 8.12 and 8.13).
Should we maintain 8.11 compatibility (with a proof of this lemma) ?

On Nix CI, the compilation of hydra-battles-single fails, apparently for not finding the module Prelude.OrdNotations.vo.
Maybe a transient error ?

In the files inherited from Goedel (now in theories/Ackermann), the predicates isPR and isPRrel are of sort Set, but all the proofs of primitive recursivity were opaque (endind by Qed), which forbids us from analysing the implementation of a proven primitive recursive function (code size, for instance).

It happens that changing all Qed into Defined is the proofs of primitive recursivity breaks the compilation of the goedel library (a repeated ltac tactic at line 1552 of codeSysPrf.v loops).

The branch transparent-IsPR restricts this change opaque->transparent to a few modules of Ackermann, so as to prevent the compilation of goedel to fail. If it's OK, I propose to merge it into master.

How is the "addition chains" part of the repo related to the additions contrib? If there is substantial overlap, then I think we should archive the contrib repo and link to here.

The pdf doesn't compile on Github's side, but it is correct on my machine (after some corrections in thebib.bib
file), and my branch is up to date with master

@palmskog @cpitclaudel @start974 @Zimmi48

We think that the JFLA (French speaking workshop on functional languages (http://jfla.inria.fr/jfla2022.html) would be a nice opportunity to present the current state and evolution of hydra-battles.

The accompanying article may be written in English (8 pages). We would be very glad if this paper were co-authored by the five of us.

It looks like the following points should be addressed:

• New contents since the 2018 talk (https://hal.inria.fr/hal-01707376/document, pp. 91-104)
• influence of the coq-community eco-system on the library (e.g. Ackermann, Gaia), maintenance and CI
• Documentation with Alectryon
• ???

A draft is on the branch jfla2022 (in doc/FFLA2022/)
Please tell us if you agree with this project.

Pierre and Théo

Next Friday, we will have a meeting in Bordeaux for working about this paper.

@Zimmi48 could it be a good idea to generate coqdoc HTML on all merges to master in the same CI job as the LaTeX one? Maybe this approach to documentation could be used for additional projects until we have more automation for releases?

While doing some proofreading of the pdf before, I noticed that the typeclasses in ordinals are seemingly using the so-called semibundled approach when defining typeclasses, and not the unbundled approach recommended by Spitters and van der Weegen. For a development of the current size, I believe the unbundled approach will maximize reusability and benefits of type class automation - the risk of exponential blowups will be low with such a small hierarchy.

I will give a key example, which I tried out quickly in an experimental branch.

Consider the following classes from Prelude/DecPreOrder.v:

Class Total {A:Type}(R: relation A) :=
  totalness : forall a b:A, R a b \/ R b a.             

Class Decidable {A:Type}(R: relation A) :=
  rel_dec : forall a b, {R a b} + {~ R a b}.

Class TotalDec {A:Type}(R: relation A):=
  { total_dec :> Total R ;
    dec_dec :> Decidable R}.

Class TotalDecPreOrder {A:Type}(le: relation A) :=
  {
    total_dec_pre_order :> PreOrder le;
    total_dec_total  :> TotalDec le 
  }.

(* ... *)

Lemma le_lt_equiv_dec  {A:Type}(le : relation A)
      (P0: TotalDecPreOrder le) (a b:A) :
   le a b -> {lt a b}+{preorder_equiv a b}.
Proof.
  intro H;  destruct (rel_dec b a).
 -   right;split;auto.
 -  left;split;auto.
Defined.

If we fully apply the unbundled approach, this leads to further factoring of classes and parameters:

Class Total {A} (R : relation A) := 
 totalness x y : R x y \/ R y x.

Class Decision (P : Prop) := decide : {P} + {~P}.

Class RelDecision {A B} (R : A -> B -> Prop) :=
  decide_rel x y :> Decision (R x y).

Notation EqDecision A := (RelDecision (@eq A)).

Class TotalPreOrder {A} (R : relation A) : Prop := {
  total_pre_order_pre :> PreOrder R;
  total_pre_order_total :> Total R
}.

(* ... *)

Definition le_lt_equiv_dec {A} {le : relation A}
 {P0 : TotalPreOrder le} {dec : RelDecision le} (a b : A) :
 le a b -> {lt a b}+{preorder_equiv a b}.
Proof.
  intro H; destruct (decide (le b a)).
  - right;split;auto.
  - left;split;auto.
Defined.

One important idea here is to never mix Prop-sorted and Type-sorted class members, and always let the latter live in singleton "operational" type classes. See p. 7 in the paper by Spitters and van der Weegen.

But I guess the big question is, what is the design philosophy for type classes in ordinal? If the idea is to aim for unbundledness, then I could package up my experiments into some PR later on.

Mentionned as cpitclaudel/alectryon#94

On the branch snippeting-chapter9, the subgoals are badly displayed (Lemma doubleIsPR, p. 174 of hydras.pdf )
The snippet is on file theories/ordinals/MoreAck/PrimRecExamples.v .

I would like to use a small part of a contrib by Russel Oconnor (Goedel). I'm interested in the formalisation of primitive recursive functions, not in the proof of Gödel's theorem. The full contrib seems to be unmaintained after Coq 8.10, together with the pocklington contrib, which it requires (but not in the part I'm interested in)

The simplest solution would be to include just three. .v files in theories/ordinals/ and add credits to Russel.

What do you think ?

On branch utf8 I added a snippet utf8tryat the end of gaia/T1Bridge.v with the utf8 character for omega. The file movies/snippets/T1Bridge.tex looks to be OK,
but in hydras.pdf all the occurrences of the greek letter are missing (page 206).

Is there a standard way to use utf8 characters all along the toolchain ?

We discussed the current tagline for the project on Zulip, and there seems to be consensus that "funny maths" sounds a bit weird. I theorized that it may be a translation of mathématiques amusantes, whence a more reasonable translation to UK English might be "entertaining maths" or just plain "interesting maths". However, since we seem to lean towards US English in coq-community, maybe:

Variations on Kirby & Paris' hydra battles and other entertaining math (collaborative, documented, includes exercises)

@palmskog You were worried about CI length: it turns out that the CI job that was already the lengthiest (building the documentation) is impacted by the addition of Gaia as a dependency, since it also needs to install all of hydra-battles dependencies. I'll open a separate issue about this.

Originally posted by @Zimmi48 in #55 (comment)

More generally, the duration issues of this job come from several sources:

• install dependencies: 9 minutes
  • the introduction of Gaia impacted this duration by about 6 minutes
  • before then, there was already the issue of building mathcomp, because the workflow uses the standard Coq images to be able to set the correct OCaml compiler version for SerAPI
• install Alectryon: 4 minutes (this includes in particular building SerAPI and its dependencies).

It seems to me that there are only two solutions: building a custom Docker image or updating this workflow to rely on Nix instead of Docker-Coq-Action. I will attempt the latter, but it may take a while.

As mentioned in the issue before transferring this repository, there is the idea that the repository will host several projects documented in the same style. In https://github.com/coq-community/hydra-battles/tree/with-additions, @Casteran has pushed a new project (theories/additions) and retitled the repository's README into "Hydra Battles and Cie".

However, the various projects have very different dependencies (hydras use Equations and additions use ParamCoq, SSReflect and math-comp) and it would make sense to publish them as independent opam packages so that people can depend on them without pulling the whole thing (additions should subsume the existing coq-additions and hydras should subsume coq-cantor).

@palmskog What do you think is the best way to organize this repository? It seems to me that it is probably to have one top-level folder per package (instead of keeping theories) and one opam file per package. The documentation could still be shared in the doc/ folder. Do you agree?

I'm currently trying to build the PDF document with a Nix-installed Alectryon and SerAPI and I'm facing some issues which lead to external Coq modules not being found. This has led me to discover some issues when some snippet evaluation fails.

On page 194 of the PDF, I get the unexpected output:

The reference naryFunc was not found in the current environment.

But still the PDF was built successfully. This means that errors in PDF generation could go undetected.

In this case, the snippet is movies/snippets/AckNotPR/majorizedDefs. Running make AckNotPR.tex in doc/movies gives:

Convert '../../theories/ordinals/MoreAck/AckNotPR.v' to latex.
<string>:(11:4)-(11:68): (WARNING/2) Coq raised an exception:
     > Cannot load Equations.Init: no physical path bound to Equations
     >
   The offending chunk is delimited by >>>…<<< below:
     >
     >
     > >>>Require Import primRec Arith ArithRing List Ack MoreVectors Lia.<<<
     > Require Import Compare_dec Max.
     > Import extEqualNat  VectorNotations. 
   Results past this point may be unreliable.

and a lot more similar warnings but in the end the command exits with success.

This comes directly from the behavior of the underlying python3 extract_snippets.py AckNotPR.tex -o ./snippets/ -d -R ../../theories/ordinals hydras command.

And this probably comes in turn from Alectryon not raising an exception in such cases. I don't know if there is a way to make Alectryon raise an exception instead of printing a warning (cc @cpitclaudel).

To reproduce, I guess you just need to uninstall Equations before running make pdf (but after having built all the vo files with make).

In the file theories/ordinals/MoreAck/Ack.v I added a small example of Equations (from a post by @anton-trunov).
If I remove the (noind) option, it fails on 8.11 and 8.12, and signals a warning on 8.13 and 8.13.dev (but it compiles)
(Commit 11c4323)

Warning:
Solve Obligations tactic returned error: Proof is not complete.
This will become an error in the future [solve_obligation_error,tactics]
1 obligation remaining
Obligation 1 of Ack_graph_correct:
(forall p : nat * nat, Ack_graph p (Ack p)).
Warning:
Functional induction principle could not be proved automatically, it is left as an obligation.

the opam version of equations is 1.2.4+8.13 (installed yesterday)

@palmskog @Zimmi48 @anton-trunov

Which is the best solution ?

• Waiting for coq-equations to stabilize, add a (noind) to Ackermann's equations ?
• Removing 8.11 and 8.12 ?

@start974 @Zimmi48 @palmskog @cpitclaudel

The part of hydra-battles's documentation dedicated to ordinals is now made with Alectryon.
(sniipets extracted from theories/ordinals//.v )

This document is stiil a draft, and I will re-read it slowly now. After the corrections, it would be nice to make a release.

I noticed two issues:

• sometimes, the implication arrow -> is broken into two pieces (in long formulas) .
• There were also big vertical spaces between two adjacent snippets.

Many thanks to all of you !

I found a bug in the implementation of ordinal multiplication in ordinals/OmegaOmega/
The ordinal (fin 1 * omega) is found greater than omega.

I put the buggy files in a branch FixOmegaOmega.

Nevertheless, this implementation is ad-hoc and cannot be simply generalized to any power of omega.

I suggest to build a new implementation:

• First define a generic instance of ON, which maps an ordinal notation for alpha, using type A, into an ordinal notation for omega^alpha, based on multisets (or sorted lists) of type A.
• Instantiate alpha to omega,
• establish a morhism form the new omega^omega to epsilon0

I obtained the following message (compilation of hydras.pdf)

Error: The sources of the following couldn't be obtained, aborting:
- coq-equations.1.2.4+8.13: Curl failed

Note: make pdfworks locally

I noticed that the movies/*.tex files contain all the Coq code and answers of the corresponding .v file (even the lines which are not contained in any snippet). I don't know wether it really affects the performance of document generation on
long modules (like theories/ordinals/Epsilon0/T1.v or theories/ordinals/Epsilon0/Paths.v.
Perhaps a "lazy" snippet generation is hard to design.

@Casteran wrote in #53:

Thanks for the opam release for Gaia!
I've just intialized an experimental branch Bridge within a theories/Bridgesdirectory. My first objective is to tranfer for instance the associativity of multiplication (proven in Gaia) to hydra-battles.

Let's use this separate issue to discuss the organization and results for the bridge to gaia ordinals. Right now, Pierre is doing experimental work in a separate branch, but once he thinks it is ready to merge we should decide about file/package name and placement and CI.

@Zimmi48 gaia currently takes around 10 minutes to build in CI. If we set up a separate job to check the bridge, this means the whole hydra-battles CI jumps to around 13-14 minutes. Should we do this for all PRs? It may affect the velocity of hydra-battles development. If we do set up CI, I would favor doing a completely separate opam package that depends on both coq-gaia and coq-hydra-battles. Opinions?

I'm opening this as a memento to adapt Nix Toolbox CI to the new packaging of Gaia. Specifically, the Gaia Hydras package now only depends on the Gaia Schütte part of Gaia, which usually takes less than a minute to check. However, the Nix Toolbox is currently set up to depend on the whole Gaia (albeit with caching). We could probably save a few minutes in fresh CI time.

cc: @Zimmi48

@palmskog

I wrote a new version (without 8.11 and with references to Russel's work) on the branch remove-8-11,
but the script generate.sh fails (I used the opam version of mustache)

---.opam: File name too long
Fatal error: exception Ezjsonm.Parse_error(870828711, "JSON.of_buffer illegal number (---)")
Generating resources/index.md...
Fatal error: exception Ezjsonm.Parse_error(870828711, "JSON.of_buffer illegal number (---)")
Fatal error: exception Ezjsonm.Parse_error(870828711, "JSON.of_buffer illegal number (---)")
Fatal error: exception Ezjsonm.Parse_error(870828711, "JSON.of_buffer illegal number (---)")
Generating .github/workflows/nix-action.yml...
Fatal error: exception Ezjsonm.Parse_error(870828711, "JSON.of_buffer illegal number (---)")
Fatal error: exception Ezjsonm.Parse_error(870828711, "JSON.of_buffer illegal number (---)")
Generating .travis.yml...
Fatal error: exception Ezjsonm.Parse_error(870828711, "JSON.of_buffer illegal number (---)")