Patrick Nicodemus (Oct 14 2022 at 20:23): Patrick Nicodemus (Oct 14 2022 at 20:23):I am interested in what the potential pathologies are that may arise from axiomatically adding quotient types to Coq. The way it's currently implemented in the coq-HoTT library using private modules and adjoining new computation rules seems sensible to me. This also seems to be the solution favored by @Gaëtan Gilbert in this discussion - https://github.com/coq/coq/issues/10871
Are there any problems that arise with this implementation? I guess it should break canonicity (?) because you're axiomatically asserting the existence of proofs of equality between two elements other than refl.
Are there any other reasonable implementations that would come with their own problems / tradeoffs?
In the above github discussion, Pierre-Marie Pédrot says that Lean's implementation of quotient types breaks subject reduction, then Mario Carneiro later arrives and says that this is a superficial problem with the quotient types rather than a fundamental one (it comes from the design choice that a quotient of a definitionally proof-irrelevant proposition is again definitionally proof-irrelevant; if one chose instead that quotients were proof-relevant types, this problem would not occur.)
Removing proof-irrelevance from the equation, is there a real risk of breaking subject reduction by adding quotient types?
Gaëtan Gilbert (Oct 14 2022 at 20:38):The way it's currently implemented in the coq-HoTT library using private modules
private inductives not modules
Are there any problems that arise with this implementation? I guess it should break canonicity (?) because you're axiomatically asserting the existence of proofs of equality between two elements other than refl.
yes, and also private inductives are a hack which provide no guarantees in the kernel
ie if you have a plugin which implements eg something like destruct and forgets to check that it's only run on non private inductives, the kernel won't complain
using ltac2 Constr.Unsafe probably works to ignore privacy too
Last updated: Apr 19 2024 at 12:02 UTC