Typeclass hints

[patrick-nicodemus]

This PR collects minor fixes relating to the big Global -> export rename. I tried to do this somewhat manually by using a regex to strip universe variables out of the typeclass instances and then diffing the related files but this is too time intensive so I will have to write a proper script to sort and compare them later.

The file HoTT.v relies on the Classes library but does not export it, so after recent changes
hints from the Classes library are no longer added to the typeclass db by HoTT.v. I view this an intentional change, so this is good, but it makes this PR harder because I have to sort out the hints that were supposed to be removed (because they were not exported by HoTT.v) from the ones that were not. These include:

• @orders.lt_transitive
• hints relating to canonical_names.(CutMinus, Compare, SwapOp)
• equality and <= are stable under double negation for types equipped with an apartness relation
• hints about natpair_integers
• hints about integers.IntAbs
• hints about peano_naturals
• hints about orders.naturals
• hints about theory.rationals
• hints about canonical_names.DecRecip
• hints about canonical_names.lattices
• hints about canonical_names.Biinduction

Note that even if a typeclass is defined in the Classes library, it can still have a hint defined in the Homotopy library, so we should still have some of the typeclass hints for these classes.

The original typeclass hint db apparently contained duplicated hints for some hints relating to surreal numbers. Not sure how/why - maybe a file gets exported twice somewhere.

Spaces.Nat.Division doesn't get exported by HoTT, so hints were missing for Division.NatBezout.

[jdchristensen]

The original typeclass hint db apparently contained duplicated hints for some hints relating to surreal numbers. Not sure how/why - maybe a file gets exported twice somewhere.

Spaces/No.v contains:

Require HoTT.Spaces.No.Core.
Include HoTT.Spaces.No.Core.

I think these two lines should be merged into a Require Export, like we use everywhere else, apart from the Categories library.

The Categories library uses separate Require and Include lines a lot in the meta-files, but I don't know why. @JasonGross , can you explain why this is done instead of just doing Require Export?

[JasonGross]

The Categories library uses separate Require and Include lines a lot in the meta-files, but I don't know why. @JasonGross , can you explain why this is done instead of just doing Require Export?

This is a poor man's version of namespacing, so that everything can be Functor.* instead of Functor.Core.* or w/e. This is not important if names are only every used after Importing, but is quite important if you want to use qualified names for disambiguation.

There's an alternative pattern that avoids Include but requires a bit of extra bookkeeping, where, e.g., No.Core would start with Module No. and end with End No.

Another option would be to rename No/Core.v to No/Core/No.v, but this might make From HoTT Require Import No. a bit sad.

[jdchristensen]

@JasonGross Thanks for the explanation. I don't think we need those shorter names, so we should remove that trick from No.v. @patrick-nicodemus , can you add that change to this PR?

[patrick-nicodemus]

This is a poor man's version of namespacing

I think that this term does a slight disservice to the ML module system 😆

can you add that change to this PR?

Yes, I will make a note of this.

[jdchristensen]

To see the list of typeclass instances, doesn't something simple like

  coqc [args] typeclasses.v | sed 's/[ @].*//' | sort -u

give a nice list, where typeclasses.v contains

Require Import HoTT.
Set Printing Width 999999.
Print Typeclasses.

[patrick-nicodemus]

Ah, thanks. I wasn't familiar with the command Print Typeclasses. I was using Print HintDb typeclass_instances, which might have slightly different syntax.

[jdchristensen]

Ah, thanks. I wasn't familiar with the command Print Typeclasses. I was using Print HintDb typeclass_instances, which might have slightly different syntax.

No, I'm the one who is confused. Print Typeclasses prints the typeclasses (not surprisingly!), and not the instances...

[jdchristensen]

Maybe this is good?

coqc ... | grep -o '\w*(level' | sed 's/(.*//' | sort -u

[patrick-nicodemus]

With Set Printing 9999 each class appears on its own line and all instances of the class are given on that line. The pattern is apparently something like

For IsClassname -> [tactic(level n, pattern ..., id k) ]*

where there may be nested parentheses in "pattern". I think you could strip For IsClassname -> from the beginning of each line and then split the line on all matches for (level [0-9], .*, id [0-9]) (where .* is not greedy)

[jdchristensen]

My suggestion prints all of the words before "(level", so I think it matches what you suggest.

[patrick-nicodemus]

That sed one-liner appears to work well.

theories/Algebra/Groups/Group.v exports several modules in the Classes library:

Require Export (hints) Classes.interfaces.abstract_algebra.
Require Export (hints) Classes.interfaces.canonical_names.
(** We only export the parts of these that will be most useful to users of this file. *)
Require Export Classes.interfaces.canonical_names (SgOp, sg_op, MonUnit, mon_unit,
    LeftIdentity, left_identity, RightIdentity, right_identity,
    Inverse, inv, Associative, simple_associativity, associativity, associative_flip,
    LeftInverse, left_inverse, RightInverse, right_inverse, Commutative, commutativity).
Export canonical_names.BinOpNotations.
Require Export Classes.interfaces.abstract_algebra (IsGroup(..), group_monoid, inverse_l, inverse_r,
    IsSemiGroup(..), sg_set, sg_ass,
    IsMonoid(..), monoid_left_id, monoid_right_id, monoid_semigroup,
    IsMonoidPreserving(..), monmor_unitmor, monmor_sgmor,
    IsSemiGroupPreserving, preserves_sg_op, IsUnitPreserving, preserves_mon_unit).
Require Export Classes.theory.groups.

There are some hints here that don't have much to do with group theory, such as theorems about apartness.
This is in turn exported by AbelianGroups.v. Is this good?

[patrick-nicodemus]

Okay. I think this is done, though it's possible I overlooked some instances while looking through the diff lists.

[jdchristensen]

There are some hints here that don't have much to do with group theory, such as theorems about apartness.
This is in turn exported by AbelianGroups.v. Is this good?

I'm not sure if this is good. Is it possible to selectively export hints? (IIUC, this question is independent of this PR, and the hints that are exported are the same before and after the "Global" changes, right? But it's still a good question.)

There are several new hints in master since the original commit where I started removing Global annotations, my assumption is that these are due to later changes where new "Export module" lines were added to various files in the library.

Can you give an example of new hints in master and new "Export module" lines?

[jdchristensen]

That's a surprisingly small list of export annotations you needed to add!

[jdchristensen]

Oh, I didn't know you could have an unnamed instance. Does Coq just generate a name?

In any case, can you make the new names here and in other places all lowercase? While we often capitalize type formers and class names, we are supposed to use lowercase when referring to those types in other identifiers (but are not consistent about this).

[patrick-nicodemus]

I was not aware of this feature either, I found these while going through the typeclass hints and investigating them. I suppose that it makes sense, if you only want to use it as a typeclass instance without ever writing code to refer to it explicitly, but the auto generated names only refer to the class itself, i.e. StronglyOrderPreserving_instance_0 where for debugging typeclass resolution failures I would prefer a name that describes also the subject of the predicate, StronglyOrderPreserving_ring_homomorphism

[Alizter]

Yes, you can have unnamed hints, but it is a really fragile "feature" and best if we don't rely on it.

[jdchristensen]

stable_apartness_eq would fit our pattern better.

[jdchristensen]

Below you used plus_field to name the operation, and I think we should follow that pattern: isstronginjective_negation_field.

[jdchristensen]

isstronginjective_recip_field? I think // denotes the unary reciprocal operation.

[jdchristensen]

In addition to lowercase changes, insert underscore: "field_homomorphism", here and elsewhere.

[jdchristensen]

mult instead of times. (mul is also used, but mult seems more common in the Classes library.)

[jdchristensen]

I guess the N should remain capitalized here?

[jdchristensen]

Please add newline, and if possible, tell your editor to always end files with a newline.

[patrick-nicodemus]

There are several new hints in master since the original commit where I started removing Global annotations, my assumption is that these are due to later changes where new "Export module" lines were added to various files in the library.

Can you give an example of new hints in master and new "Export module" lines?

This comment was incorrect and based on me not understanding how dune works. Dune has a size limited internal buffer on how much it will output on stderr. The user must disable this with --no-buffer (optionally -j1 if it's important to compile files one at a time so that output from different files is not interleaved). Something like

dune build --no-buffer file.vo 2> output.txt

should work to get all output from a Coq file (and all dependencies that it needs to rebuild). The output text file contains terminal color control characters for pretty printing which have to be stripped away.

[jdchristensen]

Oh, and don't forget about the fix to Spaces/No.v