Stream: Coq users

Topic: Import Variables from Section


view this post on Zulip 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?

view this post on Zulip Gaëtan Gilbert (Mar 10 2021 at 09:32):

no

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Enrico Tassi (Mar 10 2021 at 11:21):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Mar 11 2021 at 09:53):

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

view this post on Zulip 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: Feb 09 2023 at 00:03 UTC