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:

yes you can use the other `relation`

from `CRelation`

, which is in `Type`

instead of `Prop`

.

Li-yao said:

yes you can use the other

`relation`

from`CRelation`

, which is in`Type`

instead of`Prop`

.

Is there a `csetoid`

?

Wait, is there a `setoid`

?

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

@Li-yao has CRelation been tested

In anger, I mean

ugh, a bundled typeclass? that sounds a bad idea

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

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.
```

that should be `:>`

I guess, but I’d just use `Equivalence`

, or a notation for it?

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.

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`

?

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.

(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: Jun 23 2024 at 23:01 UTC