The Coq mailing list

[Xavier MONTILLET <xavierm02.net AT gmail.com>]

I had already tried that but it hadn't worked, probably because I was exiting the section just after that.

Anyway, "Global Existing Instance R_compat" (apparently) does exacly what I wanted.

Thank you :)

On Thu, Jun 19, 2014 at 1:34 PM, Arnaud Spiwack <aspiwack AT lix.polytechnique.fr> wrote:

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