## Stream: Coq users

### Topic: Setoid rewrite with non-reflexive relations

#### Benjamin Salling Hvass (Aug 05 2020 at 08:34):

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.

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.

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?

#### Paolo Giarrusso (Aug 05 2020 at 14:00):

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

#### Paolo Giarrusso (Aug 05 2020 at 14:01):

the goal `Proper (eqv ==> ?r0 ==> ?r) div` in `?X39` should be solvable by `div_proper`, so you know that `r0 = eq0` and `r = eqv`

#### Paolo Giarrusso (Aug 05 2020 at 14:01):

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

#### Paolo Giarrusso (Aug 05 2020 at 14:03):

hm; that should actually follow from `Transitive eqv`

#### Paolo Giarrusso (Aug 05 2020 at 14:11):

Sorry, scratch all that. Postulating `Reflexive eq0.` does fix your example.

#### Benjamin Salling Hvass (Aug 05 2020 at 14:16):

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)?

#### Paolo Giarrusso (Aug 05 2020 at 14:19):

yes, I was agreeing with you

#### Paolo Giarrusso (Aug 05 2020 at 14:20):

sorry, I wasn't clear :-)

#### Paolo Giarrusso (Aug 05 2020 at 14:20):

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

#### Bas Spitters (Aug 05 2020 at 15:01):

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

#### Yannick Zakowski (Aug 05 2020 at 22:46):

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?

#### Paolo Giarrusso (Aug 06 2020 at 19:12):

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

#### Paolo Giarrusso (Aug 06 2020 at 19:13):

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

#### Paolo Giarrusso (Aug 06 2020 at 19:14):

Argh: not for Hint Extern.

#### Paolo Giarrusso (Aug 06 2020 at 19:15):

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

#### Yannick Zakowski (Aug 06 2020 at 19:16):

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

#### Paolo Giarrusso (Aug 06 2020 at 19:17):

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

#### Paolo Giarrusso (Aug 06 2020 at 19:17):

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?

#### Matthieu Sozeau (Aug 09 2020 at 11:21):

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)

#### Paolo Giarrusso (Aug 09 2020 at 19:46):

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

#### Yannick Zakowski (Aug 09 2020 at 20:40):

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