Jan van Brügge (May 05 2025 at 18:41): 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?
Last updated: May 09 2025 at 08:28 UTC