I'm trying to figure out the best way to organize my Coq project, which formalizes a source to IR translation. Currently, the directories look like this
/Source Syntax.v Typing.v /IR Syntax.v Typing.v source2IR.v
In source2IR.v, I combine the files into modules
IR so that they are in different namespaces, like below
Require Import Source.Syntax Source.Typing IR.Syntax IR.Typing. Module SC := Source.Syntax <+ Source.Typing. Module IR := IR.Syntax <+ IR.Typing. Definition translation: SC.term -> IR.term -> Prop.
Am I doing it right?
The problem with my approach is that when I do
induction on the proposition from the newly created module, Coq introduces variables whose types are from the original file, but I don't want that. For example, I did a
induction H0between the two images. Notice that Coq introduces
τ0: Syntax.ty which replaces
τ: SC.ty, but I want to keep
FYI the constructor for
SC.ok_term is below
| ok_term_val : forall E H v τ, ok_val E H v τ -> ok_term E H (trm_val v) (τ, nil)
That's a bug with Include (and the <+ syntax), and that's unlikely to be fixed soon. Sometimes it works to turn the Module you're including into a Module Type, but that's probably a hassle here. I'd rather recommend a different namespacing tech; coq-elpi + NES is a promising option, and I use it a lot
However, NES does something else. It does not create an alias with a different type; it rather lets you put the original definitions in the SC and IR "namespaces" directly.
how is it a bug?
Inside Source and IR, you can respectively use Import SC (or rather, NES.Open SC) and ditto with IR.
Gaetan: let me change that to "infelicity"; I'm not interested in arguing the difference.
More precisely: let's pretend Include implements the spec correctly (which it doesn't, as PMP points out). It's still unclear whether that spec is useful to accomplish some actual goal.
I usually run into slightly different problems, but "avoid Including concrete modules, and avoid Include here at all" remains IMHO the simplest advice.
("Follow Coq's numeric hierarchy" aka "only use Include on Module Type" seems the second-best option to use Include, and I've done it and can explain it, but it's far from a clear win).
Thanks Paolo. I'd like to learn about using Module Type to achieve my goal. If I simply replace the keyword Module with Module Type, I can't refer to anything inside.
Can you give a short example?
I can try later, but the solution involves learning more about the Coq module system and writing ML-style functors
Module Type SC_Syntax. (* current contents of Source/Syntax.v *) End Syntax. Module Type SC_Typing (Import S : SC_Syntax). (* current contents of Source/Typing.v *) End Typing (S : Syntax). Module SC. Include SC_Syntax <+ SC_Typing. End SC.
SC is usable normally, but anybody wanting to use
SC_Syntax must be written like
It can get worse if your hierarchy grows:
Module Type SC_Typing_Correctness (Import S : SC_Syntax) (Import T : SC_Typing S). ... End SC_Typing_Correctness.
if I added enough examples, the
Module Type SC_Foo ... line would have a quadratic size. There are variants with subtle tradeoffs.
I wouldn't recommend such a setup to most people, and it's definitely overkill for the original question. That's why I recommend https://github.com/LPCIC/coq-elpi/blob/master/apps/NES/examples/usage_NES.v instead...
Thanks. NES looks very promising. Let me try it out.
Last updated: Oct 04 2023 at 23:01 UTC