The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

On 1/3/20 7:37 AM, Thorsten Altenkirch wrote:
> Both Coq and Lean fail in properly supporting structures with a 
> non-trivial equality. Lean doesn’t really offer an answer to setoid 
> hell but just adds quotients as an axiomatic principle with no 
> computational explanation. This is despite us knowing since a while (I 
> wrote a paper on this in ’99) how to turn setoid hell into setoid 
> heaven by working within the setoid model: that is if you want to talk 
> about setoids all the time just accept that every type comes with its 
> own eqaulity and build your type theory around this.
I think one factor that might lead to surprisingly different 
perspectives from different people in this discussion is that, as far as 
I can tell, quotient reasoning is much more common in pure math than in 
program verification.  Yes, it comes up often enough that everyone 
working on program verification has used it in a few projects, but it 
hardly seems to rise to the level of an essential foundation for all 
work (which raises questions of whether it is worth complicating the 
core type theory to support, expanding the trusted base).  I don't think 
too many program-verification projects are avoiding quotient reasoning 
because it is awkward rather than just not especially applicable.