Stream: Beginner Questions

Topic: Fix some parameters in a locale

Jan van Brügge (May 05 2025 at 18:41):

If I have a locale with several fixes and assumes, but for many operations some of the fixes will always be the same, what is the best way of providing a partially instantiated locale?
Written differenctly: let's say the locale L has fixes A, B and C and assumes P1, P2, P3. P3 only depends on C. What is the best way to provide the locale L A B K (where C is fixed to some constant K) that only assumes P1 and P2 (because I can prove P3 for K)?

Jan van Brügge (May 05 2025 at 18:45):

Currently I can only think of a lemma P1 ⟹ P2 ⟹ L A B K, is there a better way that does not require restating P1 and P2?

Jan van Brügge (May 05 2025 at 19:30):

Ok, that is very inconvenient for the user as they won't be able to use interpretation easily (at least as far as I can tell). So I think the solution is to define a new locale L' A B that assumes P1 and P2, then interpret L A B K inside L' and provide an abbreviation for the derived constants that I care about and use lemmas statements as abbreviations for the derived theorems from the inner locale. Is there a better way?

Balazs Toth (May 11 2025 at 17:34):

Jan van Brügge said:

Ok, that is very inconvenient for the user as they won't be able to use interpretation easily (at least as far as I can tell). So I think the solution is to define a new locale L' A B that assumes P1 and P2, then interpret L A B K inside L' and provide an abbreviation for the derived constants that I care about and use lemmas statements as abbreviations for the derived theorems from the inner locale. Is there a better way?

I do pretty much the same what you describe, just that I use sublocale for the inner locale. Then you don't have to provide the abbreviations and the lemmas statement

Dmitriy Traytel (May 12 2025 at 07:20):

You could also rearrange the locales: have a locale C c assuming P3 and have your L = C c + fixes a b assumes P1 P2

Dmitriy Traytel (May 12 2025 at 07:21):

Then you can interpret your C with your constant, which should avoid you needing to reinterpret it when interpreting L.

Last updated: May 31 2025 at 04:25 UTC