Stream: Coq users

Topic: Import Variables from Section

Yishuai Li (Mar 10 2021 at 09:13):

In one file I have a section with lots of Variables, and in another file I hope to reuse those Variables. Is there a shortcut of "Import all Variables in Section blah" without retyping them?

Gaëtan Gilbert (Mar 10 2021 at 09:32):

no

Yishuai Li (Mar 10 2021 at 09:36):

After retyping all the variables, I'll also need to explicitly provide them as arguments:

Section A.
Variable foo bar baz : Type.
Definition fine : Type := foo * bar * baz.
End A.

Section B.
Variable foo bar baz : Type.
Definition wat : Type := @fine foo bar baz * @fine foo bar baz * @fine foo bar baz.
End B.

Is this "feeding everything to fine when defining wat" also unavoidable?
If yes, this seems to suggest that Section only works well within the same file.

Yannick Zakowski (Mar 10 2021 at 09:44):

I once did the following not so elegant solution: package all your parameters into a Record, make it a type class MyParameters, and you just need in your new Section to have a Context {myparam: MyParameters} and you don't need to feed your arguments. The drawback is that you lose any fine granularity on depenencies, everything depends on all your parameters, so I do not know if it makes sense for you here

Yishuai Li (Mar 10 2021 at 09:48):

I'll first try putting everything in the same file, and use the Context when the file gets too large.

Théo Zimmermann (Mar 10 2021 at 10:42):

What you're asking is basically the ability to "reopen" sections. This is also something I've wished for. I'm not sure but it might not be so complicated to implement. Maybe worth opening an issue about.

Guillaume Melquiond (Mar 10 2021 at 11:16):

What would be the semantics? If you have closed the section, it was so that you could use a generalized version of a symbol and use it. But if you reopen the section, which symbol you get? The old one or the generalized one? And what about all the symbols that were defined on top of that symbol?

Enrico Tassi (Mar 10 2021 at 11:21):

I think there are two use cases for "reopening a section":

• generalizing a symbol is very frequent but is an xy problem, things should be generalized immediately and have implicit arguments with a default value within the section. So the section does not need to be closed in the first place, hence not reopened either
• reusing a bunch of variable declarations and factoids about them (eg Let stuf), a la Isabelle's locales. This is another story, much more complex at the design level. IMO this is what we talk about in this stream.

Enrico Tassi (Mar 10 2021 at 11:23):

I imagine fine is very much linked to the context "named" A. If it is not the case, then this has nothing to do with reopening sections, IMO. It's more about filling in arguments, which can be done via type classes or functors.

Paolo Giarrusso (Mar 11 2021 at 09:51):

@Yishuai Li I prefer either typeclasses or functors, but I've seen people emulate "reopening sections" by adding, in Section B., Notation fine := (@fine foo bar baz). It sort-of works if you make that a design pattern that you skip over when reading, and you can use it consistently enough.

Paolo Giarrusso (Mar 11 2021 at 09:53):

the remaining annoyance is that moving lemmas across sections with different Notations fails.

Yannick Forster (Mar 11 2021 at 15:19):

Here's a related GitHub issue from 1.5 years ago: https://github.com/coq/coq/issues/10737

Last updated: Sep 30 2023 at 06:01 UTC