The Coq mailing list

[Rob Arthan <rda AT lemma-one.com>]

On Monday 22 Mar 2004 11:14 am, Lawrence Paulson wrote:
> How frequently are quotient constructions used in formal proofs? I
> think John Harrison used one to construct the rationals, and there are
> a couple in Isabelle, but are there others?

In ProofPower-HOL, at the moment, the only quotient constructions in building 
the theory library are to construct the integers (as equivalence classes of 
pairs of natural numbers) and the reals (as equivalence classes of Dedekind 
cuts).

If you wanted to develop a theory of infinite cardinals in HOL, then it would 
be natural to define the infinite cardinals, in type 'a, to be the 
equivalence classes of sets of 'a modulo equinumerosity.

On Thursday 25 Mar 2004 6:00 pm, John R Harrison wrote:
>...
>
> In HOL Light, there are two quotient constructions involved in the
> construction of the reals, one to factor the space of nearly-additive
> functions N->N to yield the positive reals R+, the other to factor
> R+^2 as usual to yield signed reals.
>
> The only other instance of a quotient construction I have is in a port
> of Anthony Fox's ARM spec, where they're used to define a type of words,
> as Konrad mentioned.
>
> So a survey of my proofs supports what I guess to be your hypothesis, that
> quotient constructions are not used routinely.

I think that's true in the HOL world, but isn't that because (a) much of the 
work on pure mathematics in the various implementations of HOL has 
concentrated on analysis, and (b), in practical applications, the data is 
typically sufficiently concrete to let you work with canonical 
representatives rather than equivalence classes?

If you start trying to do much algebra or topology, you are much more likely 
to need quotient constructions.

For example, I've been playing with the beginnings of a ProofPower-HOL theory 
of elementary algebraic topology recently. Quotient constructions (or more 
accurately subquotient constructions) are endemic in this. E.g., I can think 
of no way of defining the fundamental group of a topological space other than 
as a set of equivalence classes of continuous functions from a circle to the 
space.

Similar thiings would apply if you wanted to develop group theory or ring 
theory - the three isomorphism theorems are amongst the most important basic 
tools in these theories and they all involve quotients. 

So, maybe Larry would get a very different answer if he asked this question 
in 
the Mizar world.

Regards,

Rob.