Search Blacklist everything but what's imported? · Coq users

Stream: Coq users

Topic: Search Blacklist everything but what's imported?

Pierre Rousselin (Dec 05 2023 at 06:46):

I want to Import selectively a very small part of Arith.PeanoNat.Nat and then Add Search Blacklist everything else.

Is it possible? I have tried Add Search Blacklist "PeanoNat". but this blacklists the imported lemmas as well.
Is there any way with Search to get only what's imported? (Bonus: And what is added in the file itself?)

Cyril Cohen (Dec 05 2023 at 10:39):

During the last 15 years, I never found out how to properly pre-configure the filtering out of search results nor hack a way to do it. There are two things I usually do though:

inserting distinguished strings in the name: either the preprogrammed "_subdef" and "_subproof substrings, or custom ones with Add Search Blacklist "my_own_substring" (which you cannot do for your use case, because module names do not count).
or filtering out at search time using the in/inside directive (which is heavy for your case).

Michael Soegtrop (Dec 05 2023 at 11:26):

I use Elpi for advanced symbol management, but afaik it doesn't have a search blacklist command. If it would have, the things you want to do should be easy with Elpi. @Enrico Tassi : would this be hard to add?

Of course this doesn't help you with current Coq, but what you can do with Elpi as is is to auto generate a Coq file with fine grained blacklist commands and include this in your student work. I can send you example code which I use for managing delta symbol lists. You can use the same frontend and just replace the file output. I also write include files I then use for Ltac2.

Michael Soegtrop (Dec 05 2023 at 11:27):

Btw.: another application for symbol set management commands in Coq.

Enrico Tassi (Dec 05 2023 at 12:17):

For this use case, I'd add #[blacklist] to both lemmas/definitions and modules.
And yes, the blacklist attribue could be an instance of #[label="search_blacklist"] with a corresponding API for meta programs to get the set of constants with a given label., covering also the use case of @Michael Soegtrop / VST.

Paolo Giarrusso (Dec 05 2023 at 12:30):

@Enrico Tassi I think Pierre can't use a (definition-time) attribute (tho it'd be nice elsewhere): he's teaching an intro class, and wants to hide things that normally should be seen.

Michael Soegtrop (Dec 05 2023 at 12:46):

@Enrico Tassi : what I more envisioned is some sort of module set operation interface to blacklist search results. I have something like this (very simple) for delta list, which would need only few changes to create include files. What would be convenient is an elpi command to add / remove symbols to the search black list.

Pierre Rousselin (Dec 05 2023 at 15:13):

Thank you very much all of you for your answers.

definition-time attribute would indeed be very nice
is there anything close to the static (or just static inline) attributes in C?
IIUC, Search and Add/Remove Search Blacklist need more work, and there is a question about whether it should be Coq's job or other layers (UI, LSP, another language on top, ...)

Gaëtan Gilbert (Dec 05 2023 at 15:20):

is there anything close to the static (or just static inline) attributes in C?

Can you rephrase for those who don't know C?

Karl Palmskog (Dec 05 2023 at 15:22):

I guess "static" is meant in this sense:

A static global variable or a function is "seen" only in the file it's declared in

Karl Palmskog (Dec 05 2023 at 15:23):

the other sense of static doesn't make sense in a pure language

Pierre Rousselin (Dec 05 2023 at 15:25):

and static inline is the same but asking gently to the compiler to replace the function by its definition if possible, to avoid a function call.

Karl Palmskog (Dec 05 2023 at 15:27):

one problem with analogies to C is that Coq has no compile-time/runtime phase distinction

Pierre Rousselin (Dec 05 2023 at 15:28):

Karl Palmskog said:

one problem with analogies to C is that Coq has no compile-time/runtime phase distinction

but it could be asked that the proof term is replaced whenever it is used.

Karl Palmskog (Dec 05 2023 at 15:29):

"replace when used" seems like an implementation detail (optimization?) and not a semantics/interface thing

Pierre Rousselin (Dec 05 2023 at 15:31):

Wouldn't it make it easier to hide say #[static] Lemma A from the rest of the world if it were replaced everywhere by its definition? (I'm starting to feel scared that my huge ignorance will be revealed...)

Karl Palmskog (Dec 05 2023 at 15:36):

hmm, I'm not sure I follow the terminology here, here's what I usually use:

Coq's Lemma/Definition results in adding a constant to the Coq state. A constant has a name, a type, and a body.
If the constant is opaque, one can't access its body. For example, the constant could be declared as an axiom/parameter.

"hiding A from the rest of the world" could have several meanings:

hiding the constant name A (all about A is completely inaccessible)
not allowing "anyone" to access the body of A (this is frequently done)
not allowing anyone to access the type of A (not sure this makes sense)

Kenji Maillard (Dec 05 2023 at 15:41):

Pierre Rousselin said:

but it could be asked that the proof term is replaced whenever it is used.

I think the Let vernacular does this kind of inlining (or rather substitutions). But it's not an attribute on Lemma/Definition.

Karl Palmskog (Dec 05 2023 at 15:42):

right, I think Let processing is done before actually creating constants?

Pierre Rousselin (Dec 05 2023 at 15:44):

Thank you very much. I will investigate about Letto see if it can be used to tidy things up (instead of the current _subproof or Private).

Karl Palmskog (Dec 05 2023 at 15:47):

so, maybe one can say that Let triggers inlining at constant creation time, since to my knowledge there is no event in Coq for a term getting "used" at runtime

Gaëtan Gilbert (Dec 05 2023 at 15:49):

Let is only in sections, probably won't be useful for you

Paolo Giarrusso (Dec 05 2023 at 15:55):

the closest things to static inline are Notation (easy to use, but has restrictions) and Parameter Inline (only relevant with module linking).

Paolo Giarrusso (Dec 06 2023 at 11:11):

Pierre Rousselin said:

Thank you very much. I will investigate about Letto see if it can be used to tidy things up (instead of the current _subproof or Private).

The point of _subproof is to _intentionally_ deinline parts of a term to fix transparency problems.

Definition some_num (n : nat) : { m : nat | n + m < n + 10 }.
exists 0.
(* goal n + 0 < n + 10 *) abstract lia.
Defined.

here, we want 0 to be visible to clients, and the proof produced by lia should be hidden into a separate, Qed'ed _subproof constant — otherwise, Eval compute in some_num ). Program can create similar proof terms. Avoiding abstract` will avoid the extra constant, but normalizing the result will be more expensive

Last updated: Oct 13 2024 at 01:02 UTC