Hi, in my project I have introduced a lot of locales, which are generalizations of oneanother. Specifically i have the hierarchy:

stochastic_process $\supseteq$ adapted_process $\supseteq$ progressive_process $\supseteq$ predictable_process

For each of these locales, I have two additional "instantiations":

nat_stochastic_process = stochastic_process ........

nat_adapted_process = adapted_process ........

.....

and

real_stochastic_process = stochastic_process ........

real_adapted_process = adapted_process ........

Furthermore, I have two other conditions, one: the underlying filtrations can be sigma finite, two: the codomain of the processes can be ordered banach spaces. Therefore currently I have introduced all possible combinations of locales, ranging from "stochastic_process_order" to "real_sigma_finite_predictable_process_order".

In total, I have around 40-50 locales and 10-20 sublocale relations covering all possible combinations.

Today, I noticed that I also need to consider the case where the measure space is finite, so I need to add at least 40 other locales to cover all possible combinations and also prove all sublocale relations (something like nat_adapted_process $\subseteq$ nat_stochastic_process is not generated automatically).

From a style perspective, would it make more sense to include all possibilities, or should I only introduce the locales that I will actually use, and leave the rest to others (or me in the future) who will (hopefully) use my formalization for their purposes. I only really need sigma_finite_adapted_process, nat_sigma_finite_predictable_process and a couple more for example.

**TLDR; Should I introduce locales for all combinations of type classes, or should I only introduce the locales that I will actually use?**

I have decided to take the second path and introduce only those locales that I will directly need. I have deleted all other locale statements to avoid clutter. But please provide me with suggestions if you have any experience with (or opinion on) an issue similar to this.

I think that it mostly depend on your usage.:

- Make sure to instantiate all locales at least once (it is very stupid to accidentally contradicting assumptions! Happened to me once, but I found out early enough)
- More locales and more relations actually help catching mistakes…
- … but you need to maintain and adapt the proofs

I would say that: don't add too many locales as long as you might still be changing them (aka when you follow a math book, this is not too important) and then, add the ones that feel important, but not everything you can

Last updated: Dec 07 2023 at 20:16 UTC