search

coq / coq

Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
https://coq.inria.fr/
GNU Lesser General Public License v2.1
4.84k stars 647 forks source link

Global Hint (Resolve etc) in sections #16048

Open Blaisorblade opened 2 years ago

Blaisorblade commented 2 years ago

Description of the problem

Global Hint Resolve foo : db does not work in sections, while the very similar Global Instance foo already works. This limitation seems arbitrary. Beyond consistency, with long sections lemmas must often be (re-)registered as hints far away from their proofs.

Could this limitation be lifted?

Coq Version

Still true as of 8.15.1. I couldn't find a duplicate.

Janno commented 1 year ago

It would be really great if this could be fixed. A lot of our files look like this here: https://github.com/bedrocksystems/BRiCk/blob/master/theories/lang/cpp/logic/zstring.v#L948 with huge blocks (larger than this one) of hints that refer to definitions hundreds and thousands of lines earlier in the file. It is quite the maintenance nightmare.

Even worse, in many of our internal files we have to register these hints right after the corresponding lemmas are defined because the hints are used in the following lemmas.. only to then re-register them at the end of the file to make them available to clients of the file.

We had the same issue with Hint Opaque and when that got fixed the rate of definitions that were accidentally left transparent dropped drastically.

It's fine if the feature only works for constants and not for arbitrary terms.

@ppedrot you mentioned in https://github.com/coq/coq/pull/14697 that there was some cleanup needed to support Hint Resolve. Is that still the case?

Blaisorblade commented 1 year ago

Permalink: https://github.com/bedrocksystems/BRiCk/blob/5d27b524ce67385708371edaf471ebff2d4d97c4/theories/lang/cpp/logic/zstring.v#L948.

FWIW: we don't need #[global] Hint Resolve term, only #[global] Hint Resolve name. Is this blocked on dropping the feature altogether, or could the two things be disentangled?

Blaisorblade commented 1 year ago

New Zulip comment from SkySkimmer: https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Get.20Hints.20out.20of.20Section.

Janno commented 1 week ago

@ppedrot do you know what the current state is for #[global] Hint Resolve in sections? I know some changes around deprecating arbitrary hint terms were merged. Do we need to wait until terms are illegal entirely or could there be a way to allow #[global] Hint Resolve on just references (with an error for arbitrary terms)?

gmalecha commented 5 days ago

This would be a very useful building block for other work that we are doing at BlueRock.

SkySkimmer commented 5 days ago

I think we would need to do some cleanup in hints.ml before we can implement discharge. Maybe it's possible to make the libobject contain hints_entry https://github.com/coq/coq/blob/e1bb0cae4c70e62cbdafc8185ee6188b14d7bc4f/tactics/hints.ml#L1460 instead of hint_entry https://github.com/coq/coq/blob/e1bb0cae4c70e62cbdafc8185ee6188b14d7bc4f/tactics/hints.ml#L175? that seems like it would be much easier to discharge (very confusing pair of names btw)

ppedrot commented 4 days ago

In theory in the current state of hints.ml most of the impediments that used to exist for this feature should have been solved. So it's mostly a matter of 1. actually implementing the thing and 2. pick the right discharge semantics (I guess export is fine?)