[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[PVS] Re: defining functions on equivalence classes

Hi Larry,

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

| What does the package do exactly? Once you have proved that a  function
| respects the equivalence classes, the proofs are very simple.

Speaking for my HOL Light package (and the older HOL version described in
my PhD thesis), it simply automates the routine business of transferring
definitions and theorems from the underlying set based on an equivalence
relation R to results in the quotient type where "R" is replaced by
equality and so on. It only works for values bound by first-order
quantifiers; the extension to higher orders seems non-trivial. Of course
the proofs are indeed simple; most of the work is done just by
higher-order rewriting with the following theorem, which after
instantiation and proof of the antecedent, will appropriately transform
the starting theorem.

  |- (!x:Repty. R x x) /\
     (!x y. R x y = R y x) /\                                             
     (!x y z. R x y /\ R y z ==> R x z) /\                                
     (!a. mk(dest a) = a) /\                                              
     (!r. (?x. r = R x) = (dest(mk r) = r))                               
     ==> (!x y. R x y = (mk(R x) = mk(R y))) /\                           
         (!P. (!x. P(mk(R x))) = (!x. P x)) /\                            
         (!P. (?x. P(mk(R x))) = (?x. P x)) /\                            
         (!x:Absty. mk(R((@)(dest x))) = x)