Florian Sextl (Dec 08 2021 at 14:40): Florian Sextl (Dec 08 2021 at 14:40):Hi, I'm currently formalizing the base logic of the Iris separation logic framework in Isabelle and found that some theoretic constructs can be formalized quite well as subtypes (mostly some specialized function types). After reading about how to work with subtypes, quotient types and the lifting/transfer packages as well as experimenting with a few simple logical extensions to the base logic I came to asking myself, whether it would be easier to express the subtype semantics as simple predicates over the raw type.
My use cases for subtpyes are on the one hand for defining the assertion language and on the other hand for the underlying generic structure (so called cameras).
I found that subtypes and lifting seem to be a rather standard technique for formalizing assertions (e.g. the separation logic of Imperativ HOL uses them). Yet, this approach requires to also lift many lemmas necessary for a good automation. This might be even worse than for Imperative HOL as the Iris assertions contain more custom connectives. The subtype in question can be found here and a "paper formalization" of the assertion language can be found here in section 5.
The other use case might be similar to some mathematical constructions. I defined the camera structure as a type class which requires functions that are of a specific subtype, see here. In this case, the lifting and lowering seems to only decrease the readability without providing better usability.
Do these use cases make sense for semantic subtypes with lifting or would the necessary overhead be too much in the long run? And what are good rules of thumb to decide when to use semantic subtypes?
Thanks a lot in advance.
Last updated: Dec 21 2024 at 12:33 UTC