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 SC
and 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?
Edit:
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 H0
between the two images. Notice that Coq introduces τ0: Syntax.ty
which replaces τ: SC.ty
, but I want to keep τ: SC.ty
.
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
for instance:
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.
here, SC
is usable normally, but anybody wanting to use SC_Syntax
must be written like SC_Typing
.
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 13 2024 at 01:02 UTC