Unbundled or semibundled typeclasses? about hydra-battles HOT 7 OPEN

@palmskog I'd a look at your experimental branch. That's much better ! Thanks !

from hydra-battles.

@Casteran in this case, I will probably package the branch as a sequence of smaller pull requests in the next few weeks.

Specifically, besides the above on total pre-orders, I also thought it could be a good idea to introduce an operational typeclass for comparisons:

Class Compare A := compare : A -> A -> comparison.

Class Comparable {A} (lt: relation A) (cmp : Compare A) : Prop := {
  sto :> StrictOrder lt;
  compare_correct: forall a b, CompareSpec (a = b) (lt a b) (lt b a) (compare a b);
}.

This enables using a consistent infix notation across all the comparisons between different types, e.g., x <? y or x <?> y instead of compare x y.

from hydra-battles.

Since the pdf is now made with Alectryon, we won't have to update too much the latex files, except for a link to Bas Spitter and van der Weegen's article (already cited, section 10.3.1, p. 202, but it's a long time I didn't re-read it).

Since I defined the ONclass much later than E0, I suspect I have proved some specific lemmas about ordinals in Cantor normal form which could have been proved for any ordinal notation. Well, to be considered later!

from hydra-battles.

It should be noted that there are actually serious developments based on the semibundled approach. The most well-known might be Lean's mathlib, and the mathlib authors describe their approach in a quite recent paper (page 4). However, even they typically use the decision typeclass as a parameter type and not as a member type (p. 5).

from hydra-battles.

from hydra-battles.

To me, there are right now only two ways of using booleans in a disciplined way in Coq: SSReflect and the Decision typeclass. Anything else will seemingly devolve into a cascade of ad-hoc lemmas connecting boolean functions with Props. Bob Harper's comments about boolean blindness are unfortunately pertinent in many Coq projects that do not use MathComp or stdpp. Probably this can be viewed as a "cost" of moving from a non-computational logic like HOL (where bool and Prop are conflated) to a dependently typed one.

from hydra-battles.

When we add more stuff in hydra-gaia, it will be interesting to comment and compare both styles, and choose a style for writing bridge lemmas and their proofs.

from hydra-battles.