I have this coq file, for example aFile.v, that has a bunch of definitions and parameters and axioms and lemmas, some depending on each other. So for example, let's say aFile.v looks something like this:

```
Definition def1 := ..
Parameter param1 :=..
Definition def2 :=.. (* uses parameters & definitions from above *)
Axiom ax1 :.. (* uses parameters & definitions from above *)
Lemma lem1: (* uses parameters & definitions from above *)
```

Is there a way to turn this file into something like a module that I can instantiate in other coq files in a way that allows me to define the parameters and prove the axioms in this instantiation?

I tried turning it into a module type, but then when I tried instantiating it I had to basically write down all the definitions again, otherwise I'd get an error. I want something similar to this but where I only define `Parameter`

s and prove `Axiom`

s, and any `Definition`

s or `Lemma`

s are just imported as is.

sometimes, it's practical to split your interface between `Parameter`

and `Definition`

s — and you can reuse the `Definition`

s by putting them into a `Module Type`

that you `Include`

. Coq's Numbers library is written like that.

But if you need to alternate `Parameter`

s and `Definition`

s, your interface will be split into many `Module Type`

s.

Using records might work better.

Typeclasses or canonical structures might also be relevant, but with either one you get extra type inference questions.

Is the use of "Axiom" really intended above or is it a way to describe a parameter? If you really want to declare an axiom based on previous definitions then the only way I know is modules.

Records can contain definitions too. And your question seems strange, since Axiom and Parameter are technically equivalent for this discussion

A parameter should be written with axiom iff it is in Prop, but that's just a convention. Do I miss sth?

Last updated: Jun 23 2024 at 05:02 UTC