Stream: Coq users

Topic: Generalized rewriting with custom 'relation' type?

Shea Levy (Oct 31 2020 at 17:58):

I'm reading about generalized rewriting now, and I see it's based on coq stdlib's relation type. I'm working with relations I may want to compute with, so I'm working in Type instead of Prop, can I use generalized rewriting there? If this is answered further in the docs feel free to RTFM at me :joy:

Li-yao (Oct 31 2020 at 18:10):

yes you can use the other relation from CRelation, which is in Type instead of Prop.

Shea Levy (Oct 31 2020 at 18:38):

Li-yao said:

yes you can use the other relation from CRelation, which is in Type instead of Prop.

Is there a csetoid?

Paolo Giarrusso (Oct 31 2020 at 18:52):

Wait, is there a setoid?

Shea Levy (Oct 31 2020 at 18:52):

https://coq.inria.fr/library/Coq.Classes.SetoidClass.html#Setoid

Paolo Giarrusso (Oct 31 2020 at 18:52):

@Li-yao has CRelation been tested

Paolo Giarrusso (Oct 31 2020 at 18:52):

In anger, I mean

Paolo Giarrusso (Oct 31 2020 at 18:53):

ugh, a bundled typeclass? that sounds a bad idea

Li-yao (Oct 31 2020 at 18:53):

I don't know. I haven't used it.

Shea Levy (Oct 31 2020 at 18:54):

Paolo Giarrusso said:

ugh, a bundled typeclass? that sounds a bad idea

Yeah, I just defined:

Class equivaluable T := equivalent : crelation T.

Notation "x ≡ y" := (equivalent x y) (at level 70, no associativity).
Notation "x ≢ y" := (complement equivalent x y) (at level 70, no associativity).

Class setoid T {T_equivaluable : equivaluable T} :=
  setoid_equivalence : Equivalence equivalent.

Paolo Giarrusso (Oct 31 2020 at 18:55):

that should be :> I guess, but I’d just use Equivalence, or a notation for it?

Shea Levy (Oct 31 2020 at 18:56):

Paolo Giarrusso said:

that should be :> I guess, but I’d just use Equivalence, or a notation for it?

This is a class over T, not the relation.

Paolo Giarrusso (Oct 31 2020 at 18:58):

okay, so it’s a notation for @Equivalence T (≡). I mean, it’s probably fine, but it’s not a no-op. OTOH, maybe you want a different Hint Mode?

Paolo Giarrusso (Oct 31 2020 at 18:59):

FWIW: my manual for setoid rewriting is stdpp, e.g. https://gitlab.mpi-sws.org/iris/stdpp/-/blob/master/theories/base.v#L277, but it doesn’t cover Type, and Robbert suggested there might be additional issues with that case. Unsure.

Paolo Giarrusso (Oct 31 2020 at 19:00):

(OTOH, stdpp changes some stdlib settings in https://gitlab.mpi-sws.org/iris/stdpp/-/blob/master/theories/base.v#L550 — those changes are usually for the better, but IIUC this particular one requires double the amount of Proper instances)

Last updated: Oct 04 2023 at 22:01 UTC