Stream: Coq users

Topic: Modularizing Coq Scripts with Defining Parameters

view this post on Zulip Kalernor (Nov 23 2023 at 15:07):

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 Parameters and prove Axioms, and any Definitions or Lemmas are just imported as is.

view this post on Zulip Paolo Giarrusso (Nov 23 2023 at 17:21):

sometimes, it's practical to split your interface between Parameter and Definitions — and you can reuse the Definitions by putting them into a Module Type that you Include. Coq's Numbers library is written like that.
But if you need to alternate Parameters and Definitions, your interface will be split into many Module Types.
Using records might work better.

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

view this post on Zulip Pierre Courtieu (Nov 24 2023 at 08:54):

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.

view this post on Zulip Paolo Giarrusso (Nov 25 2023 at 00:23):

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

view this post on Zulip Paolo Giarrusso (Nov 25 2023 at 00:24):

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