Think about equivalences and proper functions

[Zdancewic]

This is just reflecting some of our discussions (and comments in the code) as a Github issue.

The problem: working with itrees up to tau (and more generally, monads with a non-trivial equality) is a pain, especially for rewriting. This issue isn't specific to itrees, so it probably should be handled more generally in extlib.

One experiment along these lines that I worked on over the summer was adapting the monad library from math-classes to user PERs for stating the monad laws. You can see the resulting interface here:

https://github.com/Zdancewic/math-classes/blob/master/interfaces/monads.v

[gmalecha]

Just to clarify, is the idea that there are three (somewhat orthogonal) issues:

• [ ] compositional co-induction (paco?)
• [ ] reasoning about quotients
• [ ] defining equivalence up to tau

The last one is done, but somewhat depends on the first because we still need to prove a lot of theorems about it.

[Zdancewic]

Yes, I was more thinking about #2 of the things you mention.

[Lysxia]

We've gone a long way since this issue was opened, and we're doing well with Equivalence relations now. As we progress further, we'll hopefully run into more concrete problems to continue the discussion.