The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

Record relationA := mkRelationA {
  R : relation A;
  R_compat : Proper (eqA ==> eqA ==> iff) R
}.

Existing Instance R_compat.

If you insist on using classes, have a look at the Arguments command (especially with clear_implicits).

On 19 June 2014 13:12, Xavier Montillet <xavierm02.net AT gmail.com> wrote:

Hi,

Since I have/want to use relations over quotient sets, I defined

Class relationA := mkRelationA {
  R : relation A;
  R_compat :> Proper (eqA ==> eqA ==> iff) R
}.

I currently use "RA.(@R)" to get the "relation A" from the "relationA" but I'd
prefer to force the arguments of the projections to be explicit because weird
things happen.

For example, given two variables:

Variable RA1 : relationA.
Varaible RA2 : relationA.

You can try to prove that their R-projections are equal:

Lemma wut : RA1.(@) = RA2.(@).

And the goal will be "R = R".

Obviously, "reflexivity" doesn't work and one can use "unfold R" to change the
goal to "(let (R0, _) := RA1 in R0) = (let (R0, _) := RA2 in R0)". But I'd
rather not have two different things with the same name in the first place...

So my questions are:

- Is it possible to force the arguments of the projections to be explicit?
- If it is, how?
- If it isn't, would it be possible to use a Record instead but still have
R_compat be "magically registered" so that I can use "rewrite" instead of
"apply R_compat"?

Thank you in advance for your answers.

Respectfully,

Xavier Montillet