Stream: Coq users

Topic: Setoid rewrite with non-reflexive relations

view this post on Zulip 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.
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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Aug 05 2020 at 14:01):

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

view this post on Zulip Paolo Giarrusso (Aug 05 2020 at 14:03):

hm; that should actually follow from Transitive eqv

view this post on Zulip Paolo Giarrusso (Aug 05 2020 at 14:11):

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

view this post on Zulip 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)?

view this post on Zulip Paolo Giarrusso (Aug 05 2020 at 14:19):

yes, I was agreeing with you

view this post on Zulip Benjamin Salling Hvass (Aug 05 2020 at 14:19):

Ah sorry, read that wrong.

view this post on Zulip Paolo Giarrusso (Aug 05 2020 at 14:20):

sorry, I wasn't clear :-)

view this post on Zulip 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

view this post on Zulip Bas Spitters (Aug 05 2020 at 15:01):

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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Aug 06 2020 at 19:14):

Argh: not for Hint Extern.

view this post on Zulip Paolo Giarrusso (Aug 06 2020 at 19:15):

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

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Aug 06 2020 at 19:17):

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

view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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: Oct 13 2024 at 01:02 UTC