I am unable to get the example under 'rewriting and non reflexive relations' in https://coq.inria.fr/refman/addendum/generalized-rewriting.html to work. As I read the example, you should be able to rewrite with `H0`

in the proof of `test`

and get an obligation to prove `eq0 n n`

in the following:

```
Require Import ZArith.
Require Import Setoid.
Require Import Morphisms.
Require Import micromega.Lia.
Local Open Scope Z.
Parameter T : Type.
Parameter eqv : relation T.
Parameter div : T -> Z -> T.
Instance eqv_eqv : Equivalence eqv.
Admitted.
Definition eq0 x y := x = y /\ x <> 0.
Instance eq0_sym : Symmetric eq0.
Proof. intros ?; unfold eq0; lia. Qed.
Instance eq0_trans : Transitive eq0.
Proof. intros ?; unfold eq0; lia. Qed.
Instance div_proper : Proper (eqv ==> eq0 ==> eqv) div.
Admitted.
Lemma test x y n : eq0 n n -> eqv x y -> eqv (div x n) (div y n).
Proof.
intros H H0. setoid_rewrite H0.
```

This however gives the error

```
Error: setoid rewrite failed: Unable to satisfy the following constraints:
UNDEFINED EVARS:
?X37==[x y n H H0 |- relation T] (internal placeholder) {?r}
?X38==[x y n H H0 |- relation Z] (internal placeholder) {?r0}
?X39==[x y n H H0 (do_subrelation:=do_subrelation) |- Proper (eqv ==> ?r0 ==> ?r) div] (internal placeholder) {?p}
?X40==[x y n H H0 |- ProperProxy ?r0 n] (internal placeholder) {?p0}
?X42==[x y n H H0 |- relation T] (internal placeholder) {?r1}
?X43==[x y n H H0 (do_subrelation:=do_subrelation) |- Proper (?r ==> ?r1 ==> Basics.flip Basics.impl) eqv]
(internal placeholder) {?p1}
?X44==[x y n H H0 |- ProperProxy ?r1 (div y n)] (internal placeholder) {?p2}
TYPECLASSES:?X37 ?X38 ?X39 ?X40 ?X42 ?X43 ?X44
```

What am I doing wrong?

You need an instance claiming that `eqv`

is proper over `eqv`

— that's what `Proper (?r ==> ?r1 ==> Basics.flip Basics.impl) eqv]`

is asking about

the goal `Proper (eqv ==> ?r0 ==> ?r) div`

in `?X39`

should be solvable by `div_proper`

, so you know that `r0 = eq0`

and `r = eqv`

hence, you need `Proper (eqv ==> ?r1 ==> flip impl) eqv`

hm; that should actually follow from `Transitive eqv`

Sorry, scratch all that. Postulating `Reflexive eq0.`

does fix your example.

Paolo Giarrusso said:

Sorry, scratch all that. Postulating

`Reflexive eq0.`

does fix your example.

But isn't the point of the example that it should work without `eq0`

being reflexive (which it isn't)?

yes, I was agreeing with you

Ah sorry, read that wrong.

sorry, I wasn't clear :-)

technically the problem seems to be affect the `ProperProxy`

instances — I don't know if you're missing some import defining more infrastructure *for* ProperProxy

Better error messages would be good: https://github.com/coq/coq/issues/6141

Fwiw, I do not think you are doing anything wrong @Benjamin Salling Hvass , and I would be interested in understanding why it fails as well.

First, notice that the rewrite should "morally" work, as the following should essentially mimic the expected high level justification of the rewrite:

```
transitivity (div y n).
eapply div_proper; [exact H0 | exact H].
```

One way to get a better understanding of what goes on, albeit a cumbersome one, is to set the debugging information (and add Fail, as actual failure flushes the buffer):

```
Typeclasses eauto := debug.
Fail setoid_rewrite H0.
```

We see that things start as expected: it looks for a justification for rewriting an `eqv`

equation under `div`

, i.e. for a `Proper (eqv ==> ?r0 ==> ?r) div`

and picks for it `div_proper`

as expected.

Now that entails that it unifies `?r0`

with `eq0`

, and must therefore be able to prove that `eq0 n n`

holds to make progress. This is expressed by looking for an instance to `ProperProxy eq0 n`

, which unfolds exactly to `eq0 n n`

.

And that's where things seem to get wrong: to prove this, typeclass resolution seem to only rely on instances, but do not check for its unfolded definition in the goal. And to this end, there are only three possibilities: it knows that it holds if the relation is `eq`

(see `eq_proper_proxy`

), it knows that it holds for reflexive relations (see `eq_proper_proxy`

), and it knows that it is a synonymous to `Proper`

.

As such, note that the rewrite works if you rewrite the lemma as:

```
Lemma test x y n : Proper eq0 n -> eqv x y -> eqv (div x n) (div y n).
```

or:

```
Lemma test x y n : ProperProxy eq0 n -> eqv x y -> eqv (div x n) (div y n).
```

But it is cumbersome and unintuitive, I would have expected things to work out in the original setup.

Maybe @Matthieu Sozeau have some insight into whether this is a bug/undesirable behavior, or if we are missing a good reason for it?

Typeclass resolution isn't going to use info from the context, but the manual implies that if searches for ProperProxy fail, that should result in extra goals

Sorry, I retract on the first part: I guess that's only true for instances, not for side conditions.

Argh: not for Hint Extern.

As a hack, can you add an Hint Extern that unfolds ProperProxy and uses assumption?

That's a bit unclear to me. It at least definitely use info from the context for hypotheses whose type is a class: see the fact that simply writing the precondition as `ProperProxy eq0 n`

works. It picks this hypothesis during typeclass resolution even if it's not a declared instance

Right, anything local counts as instance. The same works with let in terms.

On external hints, I am less sure how to get extra goals instead. Would shelve help, or is it the bad idea it sounds like?

Indeed typeclass resolution only considers hypothesis whose head is syntactically a class (for efficiency, in general it would otherwise require to unify all hypotheses to know if they can apply or not). However it should be fine to add a hint `Extern (ProperProxy _ _) => solve [red; assumption] : typeclass_instances`

(or anything more powerful)

That sounds like a bug — at least the manual requires updating (since it promises extra goals), and maybe some solution should be integrated

Thanks Matthieu! In relation with Paolo's remark: when you say "it should be fine to add(...)", do you mean that it would be fine to add this hint to the `Setoid`

module, and therefore that we should create a Issue/PR in this direction, or do you mean that it should be fine to add it locally as needed but would remain too pervasive to be there by default?

Last updated: Jun 23 2024 at 23:01 UTC