The Coq mailing list

[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.''