Andrew Appel (Jan 12 2023 at 19:46): Andrew Appel (Jan 12 2023 at 19:46):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" ?
Gaëtan Gilbert (Jan 12 2023 at 20:38):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
Andrew Appel (Jan 12 2023 at 23:17):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.
Jason Gross (Jan 13 2023 at 04:12):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.
Paolo Giarrusso (Jan 13 2023 at 07:17):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)
Paolo Giarrusso (Jan 13 2023 at 07:20):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.
Paolo Giarrusso (Jan 13 2023 at 07:26):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?
Andrew Appel (Jan 17 2023 at 17:47):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.
Andrew Appel (Jan 17 2023 at 17:55):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.
Andrew Appel (Jan 17 2023 at 17:56):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.
Paolo Giarrusso (Jan 17 2023 at 17:57):The testcase above is sufficient right? I can try later
Paolo Giarrusso (Jan 17 2023 at 17:59):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)
Andrew Appel (Jan 17 2023 at 18:04):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".
Paolo Giarrusso (Jan 17 2023 at 18:09):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)
Paolo Giarrusso (Jan 17 2023 at 18:11):okay, that makes some sense since Jason's gives goal (strict_eqv y ?y)
Andrew Appel (Jan 17 2023 at 18:12):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?
Andrew Appel (Jan 17 2023 at 18:21):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:
Paolo Giarrusso (Jan 17 2023 at 18:25):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 ...
Paolo Giarrusso (Jan 17 2023 at 18:39):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
Paolo Giarrusso (Jan 17 2023 at 18:46):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.
Andrew Appel (Jan 17 2023 at 23:02):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") ?
Paolo Giarrusso (Jan 18 2023 at 00:56):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?
Paolo Giarrusso (Jan 18 2023 at 01:13):but I could well be missing something, and I'm used to very different developments :-)
Matthieu Sozeau (Jan 19 2023 at 10:01):As you guessed the design space is so large and performance implications so hard to predict that we didn't add anything
Matthieu Sozeau (Jan 19 2023 at 10:02):But indeed, the doc should reflect that, and should give at least one solution
Andrew Appel (Jan 19 2023 at 15:50):@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".
Matthieu Sozeau (Jan 19 2023 at 16:01):That’s possible as well and it would be welcome ;)
Last updated: Oct 04 2023 at 23:01 UTC