coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Adam Chlipala <adam AT chlipala.net>
- To: quanta AT sdf.lonestar.org
- Cc: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Defining types from equivalence relations.
- Date: Tue, 14 Dec 2010 08:31:02 -0500
quanta AT sdf.lonestar.org
wrote:
I have a type T : Set and equivalence relation R : T -> T -> Prop and I
would
like to form the new type T/R : Set. I could not find any way to form this new
type. I need this type to define a lot of objects, but one example is
fractions. Thank you for any advice on this topic possible.
Many people complain that Coq doesn't provide good support for quotient types, which is the usual term for the feature you ask about. I'll leave it to others to give their favorite workarounds.
Your particular example of fractions is a good one, because there is a pretty straightforward implementation that doesn't bring in quotient types. A (positive, to keep this simple) rational number can be represented as a conceptually infinite vector, with each position standing for one of the complete set of prime numbers. Each position encodes the integer exponent for that prime, in the unique prime decomposition of the rational number. The vector doesn't actually need to be infinite because all exponents are 0 after some point. The usual equality has the expected behavior over this implementation.
- [Coq-Club] Defining types from equivalence relations., quanta
- Re: [Coq-Club] Defining types from equivalence relations., Adam Chlipala
- <Possible follow-ups>
- Re: Re: [Coq-Club] Defining types from equivalence relations., quanta
Archive powered by MhonArc 2.6.16.