-
Notifications
You must be signed in to change notification settings - Fork 197
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
base: master
Are you sure you want to change the base?
Typeclass hints #2254
Conversation
Spaces/No.v contains: Require HoTT.Spaces.No.Core.
Include HoTT.Spaces.No.Core. I think these two lines should be merged into a The Categories library uses separate |
This is a poor man's version of namespacing, so that everything can be There's an alternative pattern that avoids Another option would be to rename |
@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? |
I think that this term does a slight disservice to the ML module system 😆
Yes, I will make a note of this. |
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. |
Ah, thanks. I wasn't familiar with the command |
No, I'm the one who is confused. |
Maybe this is good? coqc ... | grep -o '\w*(level' | sed 's/(.*//' | sort -u |
With
where there may be nested parentheses in "pattern". I think you could strip |
My suggestion prints all of the words before "(level", so I think it matches what you suggest. |
That sed one-liner appears to work well.
There are some hints here that don't have much to do with group theory, such as theorems about apartness. |
3afb65d
to
9cdc153
Compare
Okay. I think this is done, though it's possible I overlooked some instances while looking through the diff lists. |
6d8a803
to
26b3e29
Compare
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.)
Can you give an example of new hints in master and new "Export module" lines? |
There was a problem hiding this 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 ⊓). |
There was a problem hiding this comment.
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).
There was a problem hiding this comment.
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
There was a problem hiding this comment.
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). |
There was a problem hiding this comment.
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 (-). |
There was a problem hiding this comment.
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 (//). |
There was a problem hiding this comment.
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. |
There was a problem hiding this comment.
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. |
There was a problem hiding this comment.
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. |
There was a problem hiding this comment.
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. |
There was a problem hiding this comment.
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.
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
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. |
Oh, and don't forget about the fix to Spaces/No.v |
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:
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.