Lean extends the Calculus of Inductive Constructions with quotient types, as discussed by Carneiro (2019, Sec 2.7.1). However, that and other choices break some metatheoretic properties of CIC (Carneiro, 2019, Sec. 3.1), properties that Coq developers care about; consistency is nevertheless preserved.
Coq does not add support for quotients; one must instead use setoids explicitly. By looking at Carneiro (2019), we can see the difference: unlike quotient A/R, a setoid (A, R) is not a standard type, and we must explicitly remember to use R instead of standard equality wherever needed.
Both with setoids and quotients, we must ensure that functions respect the equivalence on their domain. However, when using quotients A/R, that must only be checked for functions that use A/R's eliminator, while with setoids we need more work.
For example, take a function f : A/R -> B, and g : B -> C: we can write h : A/R -> C = fun x => g (f x) without incurring additional proof obligations.
With setoids as implemented in Coq, we can adapt this example and define f : A -> B, g : B -> C and h : A -> C = fun x => g (f x). We can then prove that f respects R (in Coq, that's exposed through an instance of the Proper typeclass). However, we don't get for free that h respects R — we must show it explicitly, even tho that can be automated in part.
What's more, Coq's standard library does not have great support for setoids. Robbert Krebbers stdpp library (2020) improves on that, by providing additional type classes and tactics; with such support, using setoids becomes realistic, tho it still involves quite some boilerplate, annoyances, and limitations.
Typeclass Equiv A represents setoid equivalence on A.
Tactic solve_proper can help showing that functions respect equivalences; in our example, it could prove h respects R for free; however, it is not complete.
Tactic f_equiv is an analogue of f_equal, but for setoids: from goal R (f x) (f y) it produces goal S x y if we have an instance of Proper (R ==> S) f — that is, f maps R related inputs to S-related outputs.
The Iris library uses setoids constantly, and it shows how to reduce further the associated boilerplate; but details are out of scope here.
Even when using stdpp, setoids are not for free:
- they involve additional boilerplate;
- stdpp tactics for setoids are not complete, and the workarounds needed for when they fail are not pretty;
- generally, Coq automation using typeclasses and/or canonical structures can become pretty delicate at scale.
Bibliography:
- Mario Carneiro, 2019, The Type Theory of Lean, M.Sc. Thesis, https://github.com/digama0/lean-type-theory/releases/download/v1.0/main.pdf.
- Robbert Krebbers and others, 2020, stdpp library, https://gitlab.mpi-sws.org/iris/stdpp, last accessed 2020, created a few years ago.