I am trying to do setoid rewriting in the presence of a partial equivalence relation, and it's not quite working.

Consider a function (g: T -> T -> bool),

such that Proper (eqv ==> strict_eqv ==> eq) g.

That is, on the first argument of g I should be able to rewrite by the equivalence relation "eqv", but on the second argument I require a partial equivalence relation "strict_eqv".

The lemma "test" demonstrates the exact situation:

```
Lemma test:
forall (T : Set) (eqv strict_eqv : relation T)
(g: T -> T -> bool) (x x' y : T)
(H: Equivalence eqv)
(H0: RelationClasses.PER strict_eqv)
(H1: RewriteRelation eqv)
(H2: RewriteRelation strict_eqv)
(H3: Proper (eqv ==> strict_eqv ==> @eq bool) g)
(H4: strict_eqv y y)
(H5: eqv x x')
(H6: g x y = false),
g x' y = false.
Proof.
intros.
Fail rewrite H5 in H6.
change (Proper strict_eqv y) in H4.
rewrite H5 in H6. (* succeeds *)
```

What you see is that if the hypothesis `strict_eqv y y`

is above the line, then the rewrite fails, but if it is converted to `Proper strict_eqv y`

then it succeeds.

I consider this to be a bug in the setoid-rewrite system (or in its libraries). I should not have to express `y==y`

using `Proper`

in this way.

I tried to patch the problem by adding a typeclass instance as follows:

```
Lemma PER_refl: forall (A: Type) (f: relation A) ,
RelationClasses.PER f ->
forall x, f x x -> Proper f x.
Proof. auto.
Qed.
Hint Resolve PER_refl : typeclass_instances.
```

but it didn't help.

So, am I doing something wrong, or is there a better way to do this, or is it really a "bug" ?

setoid rewrite uses typeclasses eauto to solve its Proper constraints

typeclasses eauto is guided by the syntactic shape of the terms, so `Proper R x`

does not match `R x x`

in its view

It does not recurse on non typeclass goals, if they can't be solved by unification while solving other goals they lead to resolution failures. For your instance the `f`

argument is non dependent so won't be unified and always fails.

you can try running

```
#[export]
Hint Extern 100 (Proper ?R ?x) =>
match goal with H : R x x |- _ => exact H end
: typeclass_instances.
```

I don't know how well that works in general though

Thank you. Based on your suggestion, I have done something even more aggressive:

```
#[export] Hint Extern 100 (Proper ?R ?x) =>
(red; auto with typeclass_instances) : typeclass_instances.
```

and it seems to work just fine. Now my question is, wouldn't *anyone* doing rewriting in the presence of PERs want this? And the presence of PERs is not so crazy or unusual, since it's explicitly mentioned in the Coq reference manual chapter on generalized rewriting.

Seems reasonable to me, though I worry a bit about performance.

```
Lemma PER_valid_l {A} {R : relation A} {HS : Symmetric R} {HT : Transitive R} x y (H : R x y) : Proper R x.
Proof. hnf; etransitivity; eassumption || symmetry; eassumption. Qed.
Lemma PER_valid_r {A} {R : relation A} {HS : Symmetric R} {HT : Transitive R} x y (H : R x y) : Proper R y.
Proof. hnf; etransitivity; eassumption || symmetry; eassumption. Qed.
Global Hint Extern 10 (Proper ?R ?x) => simple eapply (@PER_valid_l _ R); [ | | solve [ auto with nocore ] ] : typeclass_instances.
Global Hint Extern 10 (Proper ?R ?x) => simple eapply (@PER_valid_r _ R); [ | | solve [ auto with nocore ] ] : typeclass_instances.
```

which is, I think, a bit more general.

You could search for PER instead... and probably should use class_apply / autoapply (yes, typeclasses eauto claims to be using simple eapply, but it isn't, as Janno IIRC documented on the bug tracker)

At least, that'd be the consistent choice. Or you could wrap R x y in a "ByAuto" class, solved by auto with nocore, and then PER_valid* could be instances.

OTOH, @Robbert Krebbers taught Iris folks to worry about performance for *failed* rewrites, which must explore an entire backtracking tree: these instances increase the branching factor there. Maybe the hints should be Extern, and filter out ==> in R?

I have tested @Jason Gross 's thing from fiat-crypto (but with Global changed to #[extern]), and it doesn't do the job. @Paolo Giarrusso , can you be more specific about what your suggestion would look like? I'm not a typeclasses expert.

Maybe @Jason Gross 's fiat-crypto version isn't working for me because I've explicitly declared my relation as a PER (without separately adding symmetric and transitive lemmas to a hint database), which is just a different interface than fiat-crypto is using, which relies separately on the lemmas but doesn't use a PER instance.

Scratch that, Jason's version *does* work for me if I change "auto with nocore" to "auto", which probably indicates some lack of hygiene on my part, elsewhere.

The testcase above is sufficient right? I can try later

Re PR vs symmetric/transitive, `PER`

's declaration adds hints to `typeclass_instances`

, which `typeclasses eauto`

should use in the subgoals generated by `Hint Extern`

(while e.g. `auto`

wouldn't). `Set Typeclasses Debug.`

can help confirm what happens (but won't affect `auto`

, only `typeclasses eauto`

)

Here's my latest version, with two improvements to make it more efficient: adopting Paulo's suggestion to reject ==>, and adding "nocore":

```
#[export] Hint Extern 100 (Proper ?R ?x) =>
(* See https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/rewriting.20with.20PERs *)
(lazymatch R with respectful _ _ => fail | _ => red; auto with nocore typeclass_instances end) : typeclass_instances.
```

It doesn't work for me if I replace "auto with nocore typeclass_instances" with "typeclasses eauto".

That works for me with `From Coq Require Import Relations RelationClasses Setoid Morphisms.`

, but Jason's doesn't work in the original case, unless I replace `auto`

with `eauto`

(with Coq 8.16)

okay, that makes some sense since Jason's gives goal `(strict_eqv y ?y)`

My original proposal was: since Matthieu's generalized-rewriting chapter in the Coq reference manual suggests that PERs should really work in setoid rewriting, we should propose a Coq PR or issue-report for the stdlib that adds a Hint that makes this actually work. It's too subtle for ordinary users (like me) to figure this out. Do you think my latest version is worth recommending for adding to the stdlib this way?

Just for the amusement of anyone who has read this far in the chat, I can explain the motivation behind all this PER stuff. Let eqv be an equivalence relation on Flocq floating-point numbers that treats all infinities and NaNs as equivalent, and treats negative-zero equivalent to positive-zero. And let strict_eqv be a PER that treats any finite number equivalent to itself, and negative-zero equivalent to positive-zero, but infinities and NaNs are not equivalent to anything (even themselves). Then it is the case that floating-point divide is `Proper (eqv ==> strict_eqv ==> eqv)`

but not `Proper (eqv ==> eqv ==> eqv)`

. :goblin:

your complaint is definitely valid and worth an issue, for all the reasons you've given.

Whether one of these proposals is fast enough to add to the stdlib, or even enable by default, could be trickier, especially since `Hint Extern`

can't be disabled and setoid rewriting already tends to have bad performance.

But the stdlib could add and document `Module PerRewriting. #[export] Hint Extern ...`

Okay, here's a conservative variant that suffices for the original test and seems rather safe. It's based on Jason Gross's idea, but asks for a `PER`

instance to limit applicability to existing code, uses `eassumption`

as leaf solver, and a custom `ByEassumption`

class to avoid needing `Hint Extern`

. The only downside is that it still applies to all `Proper`

searches:

https://gist.github.com/Blaisorblade/f8928e791dfd19c8df18c10679e51bd1

Forgot: the only hint extern is safe, since it only applies to searches for `ByEassumption`

.

```
Class ByEassumption (P : Prop) := { by_eassumption : P }.
#[global] Arguments by_eassumption : clear implicits.
#[global] Hint Extern 1 (ByEassumption ?P) => constructor; eassumption : typeclass_instances.
(* ... *)
#[export] Instance PER_valid_l {A} {R : relation A} `{!PER R} x y (H : ByEassumption (R x y)) : Proper R x.
(* ... Ditto for [PER_valid_r] *)
```

But at this point, I suspect it's a matter of sending a pull request, and trading expressivity and performance. The Coq benchmarks should have at least some coverage thanks to the Iris ecosystem, which uses setoid rewriting quite a bit. Not sure we have good tests on failing rewrites, but I hope that's enough.

I guess the design decision is: do we want to limit this to assumptions (as in my original example) or do we want to permit a more general search (such as my "auto with nocore typeclass_instances") ?

New idea: `strict_eqv`

probably warrants some search beyond my gist, but typeclass search can already help:

```
#[global] Instance: Proper strict_eqv (+0). ... Qed.
#[global] Instance: Proper strict_eqv (-0). ... Qed.
#[global] Instance: forall n, FiniteFloat n -> Proper strict_eqv n. ... Qed.
```

not that I ever knew `Proper R el`

made sense when `el`

isn't a function, but docs can fix that.

We could also replace/rename `ByEassumption`

by a more extensible `Related`

typeclass:

```
Class Related {A} (R : relation A) (x y : A) := { self_related : R x y }.
#[global] Arguments self_related : clear implicits.
#[global] Hint Mode Related + + ! - :typeclass_instances. (* Constrain search when inputs aren't known *)
#[global] Hint Mode Related + + - ! :typeclass_instances.
#[global] Hint Extern 1 (Related _ _ _) => constructor; eassumption : typeclass_instances.
```

You could even add `auto with nocore`

. Or `auto with nocore typeclass_instances`

, but that seems strange: `auto`

and `typeclasses eauto`

use hints very differently (`auto`

uses syntactic matching, TC search uses unification). And the relation is probably not a typeclass, so hints for it would usually not be in `typeclass_instances`

?

but I could well be missing something, and I'm used to very different developments :-)

As you guessed the design space is so large and performance implications so hard to predict that we didn't add anything

But indeed, the doc should reflect that, and should give at least one solution

@Matthieu Sozeau perhaps it is possible, after all this discussion, to find a recommended solution and add this to an existing module of stdlib; and if we are concerned about performance implications, encapsulate it in a submodule with #[export] scope, so the doc can just say "you should `Import PerRewriting`

to enable this feature".

That’s possible as well and it would be welcome ;)

Last updated: Oct 13 2024 at 01:02 UTC