Joshua Grosso (Apr 27 2021 at 23:24): Joshua Grosso (Apr 27 2021 at 23:24):If I have a data type and an equivalence relation over it, are there "rules" for when or not I can define an extensionality axiom for it? I'm thinking that, naïvely, it should be sufficient to 1) have an equivalence relation and 2) make the data type implementation abstract (e.g. via the module system). But, since adding axioms is rather dangerous, I want to first see if there are gaps in my idea.
Joshua Grosso (Apr 27 2021 at 23:24):(Of course, if this is an X-Y problem and it's a bad idea to start with, please let me know that too!)
Joshua Grosso (Apr 27 2021 at 23:26):For context, I want to define an extensionality axiom in order to be able to easily use standard library definitions (e.g. In) that implicitly rely on definitional equality (except with my new equivalence relation instead).
Emilio Jesús Gallego Arias (Apr 27 2021 at 23:57):Hi @Joshua Grosso , IIUC what you are proposing is walking a bit on dangerous waters, assume your definition is for now an interface [as done in math-comp] , then if you have only the extensionality axiom you may be safe, but at any point your interface ships more properties indeed only fully instantiating it may be provide consistency.
Actually you are excellently observing the X-Y situation if your motivation is In . I never use In myself, but prefer the generic \in predicate shipped in math-comp which has a large amount of advantages.
Maybe while other comment you could explain a bit more what the trouble with in is?
Actually, if you are gonna redefine in, you can just provide the right machinery for quotients, or if you can go a bit more "classical" in your reasoning, you could even use the quotient machine of math-comp as long you wanna deal with decidable equivalence relations [and in this case, using LEM to make the relation decidable is a much safer approach I feel]
Joshua Grosso (Apr 28 2021 at 00:36):Ah, it totally slipped my mind that quotient types are what I'm really looking for here. A tangentially-related question: In theory, could the standard library be modified such that quotient types (setoids?) are used instead of = (e.g. what you suggest with "just provide the right machinery for quotients") everywhere? I assume that isn't the case, because then the "quotient types in Lean break subject reduction" discussion would become a non sequiter—or am I misunderstanding?
Jasper Hugunin (Apr 28 2021 at 02:27):In case you don't already know, the standard library has a definition of many list predicates and corresponding lemmas that work with custom equivalence relations in the SetoidList library.
Jasper Hugunin (Apr 28 2021 at 02:29):The tradeoff between the convenience of propositional equality and the safety of being axiom-free is a complex one, but this is another possibility.
Joshua Grosso (Apr 28 2021 at 04:04):SetoidList seems exactly like what I'm looking for (at least, in this specific instance), thanks a bunch @Jasper Hugunin! I think my issue is resolved then, pending my earlier unrelated question.
Paolo Giarrusso (Apr 28 2021 at 11:49):@Joshua Grosso IIRC, you can use actual quotient types in Coq (not setoids) if you’re willing to add postulates.
Paolo Giarrusso (Apr 28 2021 at 11:49):I think that is the “right machinery for setoids” above.
Paolo Giarrusso (Apr 28 2021 at 11:50):The problem in Lean is that they go beyond those axioms and extend definitional equality.
Paolo Giarrusso (Apr 28 2021 at 11:55):And IIRC, since they add a restricted form of equality reflection, the problems are essentially about decidability;
Paolo Giarrusso (Apr 28 2021 at 11:57):but you might be right that it breaks subject reduction for their algorithmic system, since it's incomplete wrt the declarative system. I'd check our Carneiro's master thesis if you want the details and their rules for quotients.
Joshua Grosso (Apr 28 2021 at 18:24):Googling "Carniero Coq quotient" brought up https://gist.github.com/Blaisorblade/78441b030a7c0e20ab1242c8e6662db6 as the first result, thanks in advance for the educational material!
Joshua Grosso (Apr 28 2021 at 18:26):I'm starting to think that, no matter my question, you'll have written something about it already @Paolo Giarrusso (which makes my life so much easier, so thank you!)
Joshua Grosso (Apr 28 2021 at 18:27):Paolo Giarrusso said:
but you might be right that it breaks subject reduction for their algorithmic system, since it's incomplete wrt the declarative system. I'd check our Carneiro's master thesis if you want the details and their rules for quotients.
I got this from skimming the famous(?) "setoid hell" GH issue (https://github.com/coq/coq/issues/10871), please don't take my word for it lol nvm, this is in the second sentence of your Gist
Joshua Grosso (Apr 28 2021 at 18:31):Joshua Grosso said:
Ah, it totally slipped my mind that quotient types are what I'm really looking for here. A tangentially-related question: In theory, could the standard library be modified such that quotient types (setoids?) are used instead of
=(e.g. what you suggest with "just provide the right machinery for quotients") everywhere? I assume that isn't the case, because then the "quotient types in Lean break subject reduction" discussion would become a non sequiter—or am I misunderstanding?
Ah, so this is possible (viz stdpp or Iris)... good to know! Maybe in 10 years it'll be the default :-)
Paolo Giarrusso (Apr 28 2021 at 18:33):lol I had forgot that gist and I would not have expected it to lead on google! I must have tweeted it
Paolo Giarrusso (Apr 28 2021 at 18:33):and honestly, I still think that subject reduction is overrated :-).
Paolo Giarrusso (Apr 28 2021 at 18:34):stdpp does live in setoid hell — I use it every day but as I said, setoids are not what I’d recommed for casual use. I use them because I have too many equivalence relations on the same type, so quotients don’t help so much
Paolo Giarrusso (Apr 28 2021 at 18:37):finally: setoids and quotient types are not the same thing, and IIRC you _can_ have quotients without Lean’s problems (details in the issue you found, but I haven’t rechecked them).
Last updated: Apr 18 2024 at 22:02 UTC