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

*To*: Lawrence Paulson <lp15@cam.ac.uk>*Subject*: [PVS] Re: defining functions on equivalence classes*From*: John R Harrison <johnh@ichips.intel.com>*Date*: Thu, 25 Mar 2004 10:00:43 -0800*Cc*: John Harrison <johnh@ichips.intel.com>, isabelle-users@cl.cam.ac.uk, hol-info@lists.sourceforge.net, pvs@csl.sri.com, coq-club@pauillac.inria.fr*In-Reply-To*: Your message of "Mon, 22 Mar 2004 11:14:30 GMT."<16DA2C32-7BF2-11D8-B830-00039384D4B8@cam.ac.uk>*List-Help*: <mailto:pvs-request@csl.sri.com?subject=help>*List-Id*: PVS <pvs.csl.sri.com>*List-Post*: <mailto:pvs@csl.sri.com>*List-Subscribe*: <http://lists.csl.sri.com/mailman/listinfo/pvs>,<mailto:pvs-request@csl.sri.com?subject=subscribe>*List-Unsubscribe*: <http://lists.csl.sri.com/mailman/listinfo/pvs>,<mailto:pvs-request@csl.sri.com?subject=unsubscribe>*Sender*: pvs-bounces+archive=csl.sri.com@csl.sri.com

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

- Prev by Date:
**ProofLite Package for PVS 3.1** - Next by Date:
**[PVS] Re: [Hol-info] defining functions on equivalence classes** - Prev by thread:
**ProofLite Package for PVS 3.1** - Next by thread:
**[PVS] Re: [Hol-info] defining functions on equivalence classes** - Index(es):