The Coq mailing list

[roconnor AT theorem.ca]

On Wed, 9 Nov 2011, Carlos Simpson wrote:

> Dear Russell,
>  It seems to me that your problem is more with the choice function
> than with the quotient types.

Well, I guess I find it hard to disentagle issues about quotients from 
issues about choice.

> What about having a quotient type
> with an induction principle saying that in order to
> define a function X/R -> Y it suffices to define a function X-> Y
> compatible with R? One can write something similar
> for sections of dependent types.
>  This would allow us to define your "squash" and hence to have access
> to proof-irrelevance even if we don't suppose it for Prop's. It
> also seems to allow for creating subtypes.

Well, this is pretty much the "proper" quotient system that I beleive 
Thorsten would advocate.  The problems I have with it stem from my two 
examples: if real numbers are defined via a quotient then you cannot 
construct any non-constent function from the reals to the rationals, and 
you cannot extend a normal vector in R^3 to an orthonormal basis, even 
though both these can be constructed using representatives of R and R^3.

>  By the way, Daniel Schepler points out that we get quotient types using
> the Ensembles.Extensionality axiom which is in the standard library;
> what exactly are the properties of those? i.e. do they satisfy the
> induction principle?

Browsing 
http://coq.inria.fr/pylons/contribs/files/ZornsLemma/v8.3/ZornsLemma.Quotients.html 
shows that

Lemma quotient_projection_surjective: forall xbar:quotient,
  exists x:A, quotient_projection x = xbar.

depends on proof_irrelevence.  This means that Schepler's use of "exists" 
is effectively a squashed dependent sum.  Coq's rule that propositions 
cannot eliminate over prevents us from building a theorem of choice over 
propositional existential, so Schepler uses yet another axiom, 
constructive_definite_description, in his definition of induced_function 
to get around this restriction.  At this point we have now thrown out any 
computational interpreation of the non-Prop universe.  Computation in Coq 
can and will get stuck at the constructive_definite_description, even if 
you try extracting code.  (Is it possible in some way to give a 
computational intepretation of constructive_definite_description?  It 
would at the very least require a complete overhaul of the extraction 
mechanism.)

I'm not sure why Schepler suggested that he only used the
Ensembles.Extensionality axiom.  This doesn't appear to be the case to me. 
I may be misunderstanding something here.

> ---Carlos
>
>
> Selon 
> roconnor AT theorem.ca:
>
> > > I am studying Coq and maybe now may attempt a practical exercise of writing
> > some theories.
> > > I noticed that the Coq approach is to use setoids. In my opinion, it is
> > silly and contrary to what we do in informal mathematics.
> >
> > From my experience, using setoids isn't particularly silly.  The same work
> > we do to prove functions respect equivalence relations is exactly the same
> > work that a traditional mathematician does to prove their function defined
> > on a quotient is well-defined.
> >
> > Furthermore, removing quotients has some nice consequences.  Specifically
> > the extensional axiom of choice is distinct from the intensional theorem
> > of choice (see <http://r6.ca/blog/20050604T143800Z.html>).
> >
> > If you deal with quotients in the traditional way, then the theorem of
> > choice will imply excluded middle, making the system non-constructive:
> >
> > Proof.
> >
> > Let P be any proposition.
> >
> > Consider the relation R (a b: Bool) := {a = b} + {P}.  We can prove R is
> > an equivalence relation.  Suppose we could make the quotient type Bool/R.
> > We can traditionally prove (*) forall a : Bool/R, {b : Bool | a = [b]/R}
> > where [x]/R is the injection from x : Bool into Bool/R.
> >
> > Thus from the theorem of choice we can conclude
> > we can conclude {f : Bool/R -> Bool | forall a:Bool/R, a = [f a]/R}.
> >
> > We have forall x y : Bool, {x = y} + {~ x = y}, because boolean equality
> > is decidable and thus {f [True]/R = f [False]/R} + {~ f [True]/R = f
> > [False]/R}.
> > However (f [True]/R = f [False]/R) <-> P
> >
> >   (proof, Suppose P, then R True False holds.  Thus [True]/R = [False]/R.
> >    on the other hand, if f [True]/R = f [False]/R, then we
> >    have [True]/R = [f [True]/R]/R = [f [False]/R]/R = [False]/R and thus
> >    R True False, and thus P holds.)
> >
> > Therefore {P} + {~P}.
> >
> > Qed.
> >
> > Now, Thorsten would argue that this traditional approach to
> > quotients is wrong (and I would agree).  Doing quotients properly
> > in type theory would disallow step (*) and instead only admit
> >
> > forall a : Bool/R, [[{b : Bool | a = [b]/R}]] where [[P]] is a squash
> > type, which is the type P quotiented so that all values are identified.
> > Now the theorem of choice won't apply.
> >
> > The problem with quotients done properly is that you can never escape from
> > them to choose a representative.  Now you might think that this is exactly
> > the point of using quotients; however such strict adherence to quotients
> > severely limits your ability to compute.
> >
> > Example (1) If you define the real numbers as a quotient you can never
> > approximate a real number by a rational number because all computable
> > functions from real numbers to rational numbers have to be continuous,
> > which means constant in this case.  Thus you could never display any
> > results of real number computation.  By using setoids you still have the
> > option to write disrespectful functions that allow you to pick an rational
> > approximation that depends on the particular representative and thus
> > allowing you to display decimal approximations.
> >
> > Example (2) If you define the real numbers as a quotient then you cannot
> > extend a unit vector in R^3 to an orthonormal basis in R^3 that includes
> > it.  Again, with proper quotients, all constructive functions from R^3 to
> > an orthonormal basis would have to be continuous.  By the
> > no-hairy-ball-can-be-combed-smooth theorem, such a continuous function is
> > impossible.  Again, if we use setoids we have an option of breaking free
> > of the equivalence relation and create a disrespectful function from R^3
> > to an orthonormal basis that includes it.  The construction of such a
> > basis will depend on the choice of representative, but the construction
> > can be carried out.
> >
> > From these examples (and I'm sure there are many more), I conclude that
> > using setoids is the most flexible approach.  Using traditional quotients
> > makes your system non-constructive, and using proper quotients limits your
> > ability to compute.
> >
> > --
> > Russell O'Connor                                      <http://r6.ca/>
> > ``All talk about `theft,''' the general counsel of the American Graphophone
> > Company wrote, ``is the merest claptrap, for there exists no property in
> > ideas musical, literary or artistic, except as defined by statute.''
>
>
> ------ ------ ------ ------ ------ ------ ------ ------ ------ ------ ------
>
> Carlos T. Simpson
> C.N.R.S., Laboratoire J. A. Dieudonne, Universite de Nice-Sophia Antipolis
>
> "Homotopy Theory of Higher Categories" now published!
>
> Cambridge University Press, October 2011
>
> http://www.cambridge.org/gb/knowledge/isbn/item6172978/
>
> ------ ------ ------ ------ ------ ------ ------ ------ ------ ------ ------

--
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''