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.

(Of course, if this is an X-Y problem and it's a bad idea to start with, please let me know that too!)

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).

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]

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?

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.

The tradeoff between the convenience of propositional equality and the safety of being axiom-free is a complex one, but this is another possibility.

`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.

@Joshua Grosso IIRC, you can use actual quotient types in Coq (not setoids) if you’re willing to add postulates.

I think *that* is the “right machinery for setoids” above.

The problem in Lean is that they go beyond those axioms and extend definitional equality.

And IIRC, since they add a restricted form of equality reflection, the problems are essentially about decidability;

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.

Googling "Carniero Coq quotient" brought up https://gist.github.com/Blaisorblade/78441b030a7c0e20ab1242c8e6662db6 as the first result, thanks in advance for the educational material!

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!)

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 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 anon 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 :-)

lol I had forgot that gist and I would not have expected it to lead on google! I must have tweeted it

and honestly, I still think that subject reduction is overrated :-).

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

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: Jan 29 2023 at 05:03 UTC