The Coq mailing list

["Peter V. Homeier" <homeier AT saul.cis.upenn.edu>]

> 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? Also, are there any
> publications describing such proofs?
>
> Larry Paulson

I have been happy to do some work with quotients, and have composed
a package of tools to deal with them in HOL.

This package was applied to a proof of the Church-Rosser property
for the lambda calculus, based very closely on Barendregt's classic
presentation [1], but including Takahashi's triangle, for both beta
and eta reduction.  Of course, the package is not restricted to
this application, but supports quotients in general.

This work was described in a pair of posters presented at the
2001 TPHOLs in Edinburgh, just before the 9/11 attacks.

The two papers, and the associated code, may be downloaded from
http://www.cis.upenn.edu/~hol/lamcr/

Unfortunately I left out of the references of the Church-Rosser
paper far too many good related papers of other proofs, and I
apologize to those who were excluded.  In an attempt to show more
text within the page limit, I neglected many significant prior papers
in my references, to my sorrow.  I intend to correct this in the future.
Please do not take offense at the present if your name and your work
is not mentioned.

I have spoken with Dr. John Harrison of Intel about his related
quotients package, about possibly combining the two joining the
best of each, since each has features not found in the other.

I would tender the opinion that quotients would ease the treatment
of deep embeddings of all languages that have binding constructs,
where some analog of alpha equivalence appears.  The effect is
quite striking.  Although it takes some effort to raise the logical
structure of the language definition to the higher, quotiented level,
the ease of treatment at that higher level, where most of the proof
effort is focused, heartily commend this approach.

Peter Homeier

[1] H. P. Barendregt, The Lambda Calculus: Its Syntax and Semantics
    (Revised Edition), in Studies in Logic and the Foundations of
    Mathematics, Volume 103, 1984, Elsevier, especially sections
    2.1-2.1.17 and 3.1-3.3.10.

----------------------------------------------------------------------------
Peter Vincent Homeier         __     The above opinions are mine and not the
homeier AT saul.cis.upenn.edu
   <;_><   opinions of University of Pennsylvania.
Home Page:   http://www.cis.upenn.edu/~homeier/
"In Your majesty ride prosperously because of truth, humility, and
righteousness; and Your right hand shall teach You awesome things." (Ps 45:4)