The Coq mailing list

[Paul Jackson <pbj AT inf.ed.ac.uk>]

Lawrence Paulson 
<lp15 AT cam.ac.uk>
 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? Also, are there any
> publications describing such proofs?

Larry,

here is some info on quotients in Nuprl and PVS.

 - Paul.

---------------------------------------------------------------------
Paul Jackson                e-mail: 
pbj AT inf.ed.ac.uk

School of Informatics       www:    http://www.dcs.ed.ac.uk/home/pbj
Edinburgh University        Phone:  [+44] (0)131 650 5131 / 650 2720
King's Buildings            Fax:    [+44] (0)131 667 7209
Edinburgh EH9 3JZ, UK      


--------------------------------------------------------------------------
1. Quotients in Nuprl.
--------------------------------------------------------------------------

The Nuprl type theory has a quotient-type type constructor.  If T is a
type and E is an equivalence relation on T, the type T//E consists of
the *same* elements as T, but the equality relation on T//E is E, not
that of T. (Every type in Nuprl has an associated equality relation.
This relation can be made arbitrarily coarse: it's not necessary that
equality correspond with some notion of computational equivalence.)
All functions must respect the equality of their domain types.  So a
function of type T//E -> A must return equal elements in type A for
E-equal elements of T.  By requiring T//E have the same elements as T,
one never explicitly forms equivalence classes when injecting from T to
T//E and so never has the possibly non-constructive problem of choosing
an equivalence class element when going from T//E to T.

I used Nuprl's quotient type to construct finite multisets and
finite sets from lists.
E.g. see:

http://www.cs.cornell.edu/Info/People/jackson/nuprl/theories/mset.html

These finite sets and multisets were in turn used in work in my PhD
thesis on verifying properties of operators for multivariate polynomial
arithmetic. 

The Nuprl quotient type has also been used for the quotient construction
in a proof of the Myhill-Nerode theorem on the minimisation of automata.
See the "Finite Automata" book in the "Nuprl Math Library" at:
http://www.cs.cornell.edu/Info/Projects/NuPrl/Nuprl4.2/Libraries/Welcome.html

The proof of this theorem is also written up in:

@InCollection{Constable&97:auto,
  author =       {Robert L. Constable and Paul B. Jackson
                  and Pavel Naumov and Juan Uribe},
  title =        {Constructively Formalizing Automata Theory},
  booktitle =    {Proof, Language and Interaction: 
                  Essays in Honour of Robin Milner},
  publisher =    {{MIT} Press},
  year =         2000,
  editor =       {Gordon Plotkin and Colin Stirling and Mads Tofte}
}

Alexei Nogin has done some more recent work on quotient types in Nuprl.
See his TPHOLs 2002 paper:

http://mojave.cs.caltech.edu/nogin/papers/quotients.html

If one is keen on being able to compute with functions involving quotient
types, it is important that equivalence classes be represented by single
elements of the equivalence classes - as is done in Nuprl or alternatively
using a simple wrapper constructor for each element.  One can't compute
with a predicate set (a function of type T->bool representing a set of 
elements of T) representing an equivalence class.  However, if working
in the executable fragment of a classical HOL (such as supported
in Isabelle/HOL or PVS) I don't see how one can have both such an approach
*and* have such class representatives be members of quotient types, because
constructors are always injective.  E.g. if doing the integers mod 6, 
one wants [1] = [7] with wrapper constructor [_].  But the injectivity of
[_] doesn't let one have this equality.

The closest one could get might be somehow to do all one's proofs with
quotient types, but then rewrite to more constructive operators as a
last step.  Alternatively, one never explicitly forms quotient types and
simply has to support rewriting with respect to arbitrary equivalence
relations, not just the built in ones.  I'm not sure, but I think
this is supported in Isabelle/HOL and HOL. It certainly is in Nuprl and
understand ACL2 supports it too.





--------------------------------------------------------------------------
2. Quotients in PVS
--------------------------------------------------------------------------

Quotient types are straightforward to define in PVS.  I've experimented
with them a few times:

- in the construction of integers as pairs of naturals, 
- in the essence of the first isomorphism theorem for groups,
- in a proof of the Myhill Nerode theorem.  

None of this is published, but if anyone is interested, I've put the PVS
theory files up at:

  http://www.dcs.ed.ac.uk/home/pbj/pvs/

I've also included explicitly below a PVS theory file sketch of this
work that hopefully gives the idea of how one can approach quotients in
PVS. 

Particular capabilities that one gains with PVS's type theory as
compared to that of HOL or Isabelle/HOL include:

- Since the PVS type theory includes subtypes, quotient types can be
  directly defined from predicate sets without the need for a typedef
  facility with abstraction and representation functions.

- It's useful that types can take value arguments. E.g. given a function
  f : A -> B, one can define a type Quot(f) which contains a set of 
  equivalence classes of A induced by the equivalence relation 
  E(x,y) = (f(x) = f(y)).  Another example is if you want to define a 
  type Mod(n) for the integers mod n.
  
If you are using HOL or Isabelle/HOL, I would guess you could get much
of these capabilities using something like Joe Hurd's predicate subtyping
approach. See his TPHOLs 2001 paper:

http://www.cl.cam.ac.uk/users/jeh1004/research/papers/subtypes.html


% Sketch of one way of doing quotients in PVS

% PVS notation:
%  set[A] = [A->bool]
%  equivalence?[A](R) says that R is an equivalence relation
%  If s : [T->bool], (s) is the type of all elements a of T for which s(a)
%   is true.

% PVS theories have parameters in [] at start of theory definition.
% These implicitly parameterise each definition introduced in the theory.
% When definitions are used, such parameters can often be automatically
% inferred, though they can also be explicitly supplied.
% Below, most of the theory switching is used to alter which 
% definition arguments are optional.

quot_demo_1 [A : TYPE+] : THEORY
  BEGIN

  x,y : VAR A
  E : VAR (equivalence?[A])    
  eclass(x,E) : set[A]  = {y | E(x,y)}   % e(quivalence) class of x

  Z : VAR set[A]
  Qset(E) :  set[set[A]] = {Z | Exists x : eclass(x,E) = Z}
  Qtype(E) : TYPE = (Qset(E))    % Qtype[A](E) is the quotient type A/E

  ecl(x,E) : Qtype(E) = eclass(x,E) 

% An example lemma for eliminating quantification over Qtype:

  qtype_forall_elim : LEMMA
    Forall (P : pred[Qtype(E)]) :
      (Forall (U :Qtype(E)) : P(U)) = (Forall (x : A) : P(ecl(x,E)))

% The indefinite choice operator `choose' selects out elements
% of equivalence classes.

  END quot_demo_1 

% Here we switch to theory with E as additional parameter, so E is 
% optional value argument to `rep' function.  (Both A and E args to
% rep should be inferrable from the type of its argument U)

quot_demo_2[A : TYPE+, E : (equivalence?[A]) ] : THEORY
  BEGIN
  IMPORTING quot_demo_1[A]

  U : VAR Qtype(E)
  rep(U) : A = choose(U) % rep(resentative) of U

% The following lemmas abstract away from any need for further 
% fiddly reasoning with choose.
  
  x : VAR A
  rep_ecl : LEMMA E(rep(ecl(x,E)), x)
  ecl_rep : LEMMA ecl(rep(U),E) = U


  END quot_demo_2

functions_1 [D,R : TYPE] : THEORY
 BEGIN
  x1,x2 : VAR D
  f : VAR [D->R]
  E : VAR (equivalence?[D]) 

  respects?(E)(f) : bool = Forall x1,x2 : E(x1,x2) => f(x1) = f(x2)

 END functions_1

% In some circumstances it is more elegant to extract
% elements using a `lifting' operator qlift that lifts E-respecting
% functions of type A->B to type (A/E)->B:

quot_demo_3 [A:TYPE+, E:(equivalence?[A]), B:TYPE] : THEORY
 BEGIN
  IMPORTING quot_demo_2[A,E], functions_1

  f : VAR [A->B]
  U : VAR Qtype(E)

  qlift(f)(U) : B = f(rep(U))

  x : VAR A
  qlift_elim : LEMMA 
    Forall (f:(respects?[A,B](E))) : qlift(f)(ecl(x,E)) = f(x) 


  END quot_demo_3