Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Typeclass hints #2254

Open
wants to merge 5 commits into
base: master
Choose a base branch
from
Open

Conversation

patrick-nicodemus
Copy link
Contributor

@patrick-nicodemus patrick-nicodemus commented Mar 12, 2025

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
Copy link
Collaborator

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
Copy link
Contributor

JasonGross commented Mar 13, 2025

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
Copy link
Collaborator

@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
Copy link
Contributor Author

patrick-nicodemus commented Mar 13, 2025

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
Copy link
Collaborator

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
Copy link
Contributor Author

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
Copy link
Collaborator

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
Copy link
Collaborator

Maybe this is good?

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

@patrick-nicodemus
Copy link
Contributor Author

patrick-nicodemus commented Mar 13, 2025

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
Copy link
Collaborator

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

@patrick-nicodemus
Copy link
Contributor Author

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
Copy link
Contributor Author

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

@patrick-nicodemus patrick-nicodemus marked this pull request as ready for review March 14, 2025 16:36
@jdchristensen
Copy link
Collaborator

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?

Copy link
Collaborator

@jdchristensen jdchristensen left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

#[export] Instance: forall z, OrderPreserving (z ⊓).
#[export] Instance OrderPreserving_left_meet : forall z, OrderPreserving (z ⊓).
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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).

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

@@ -12,7 +12,7 @@ intros ap e;revert ap.
apply tight_apart. assumption.
Qed.

#[export] Instance: forall x y : A, Stable (x = y).
#[export] Instance apartness_eq_stable: forall x y : A, Stable (x = y).
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

stable_apartness_eq would fit our pattern better.

@@ -52,7 +52,7 @@ Proof.
intros ? E. rewrite <-E. trivial.
Qed.

#[export] Instance: IsStrongInjective (-).
#[export] Instance IsStrongInjective_FieldNegation: IsStrongInjective (-).
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

@@ -67,7 +67,7 @@ repeat (split; try exact _); intros x y E.
apply symmetry;trivial.
Qed.

#[export] Instance: IsStrongInjective (//).
#[export] Instance IsStrongInjective_FieldDivision: IsStrongInjective (//).
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

@@ -296,7 +296,7 @@ Section morphisms.

(* We have the following for morphisms to non-trivial strong rings as well.
However, since we do not have an interface for strong rings, we ignore it. *)
#[export] Instance: IsStrongInjective f.
#[export] Instance IsStrongInjective_FieldHomomorphism : IsStrongInjective f.
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Proof.
refine (from_nat_stmt nat (fun s =>
forall z : s, PropHolds (z <> 0) -> LeftCancellation mult z) _).
simpl. exact nat_mult_cancel_l.
Qed.

#[export] Instance: forall z : N, PropHolds (z <> 0) -> RightCancellation (.*.) z.
#[export] Instance RightCancellation_times_nat : forall z : N, PropHolds (z <> 0) -> RightCancellation (.*.) z.
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

@@ -202,7 +202,7 @@ Section borrowed_from_nat.
apply S_inj in E. destruct (S_neq_0 _ E).
Qed.

#[export] Instance: ZeroProduct N.
#[export] Instance ZeroProduct_N : ZeroProduct N.
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I guess the N should remain capitalized here?

Require Export Nat.Paths.
Require Export Nat.Factorial.
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

@patrick-nicodemus
Copy link
Contributor Author

patrick-nicodemus commented Mar 15, 2025

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
Copy link
Collaborator

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants