I've just read through the generalized rewriting docs, and while it seems like there's good support for rewriting in respectful *functions*, it's not clear that there's anything for respectful *predicates* (e.g. some P such that P x and R x y implies P y). Did I miss that/is there some way to include those?

Predicates are functions `... -> Prop`

. Respectful predicates are respectful functions, where the relation in `Prop`

is `iff`

(`<->`

) or sometimes `impl`

(`->`

).

Li-yao said:

Predicates are functions

`... -> Prop`

. Respectful predicates are respectful functions, where the relation in`Prop`

is`iff`

(`<->`

) or sometimes`impl`

(`->`

).

So I want a proof of `Proper P R iff`

?

Sorry, `Proper (R ==> iff) P`

Exactly :)

And I guess if `R`

is symmetric I can use `impl`

just as well?

I believe that's technically a little weaker but it does work in simple cases.

Thanks!

@Shea Levy if `R`

is symmetric I’d use `iff`

, not `impl`

, but I have only tested this with stdpp (where you also need flipped instances), not with the stdlib alone

one way to try this out is to try rewriting in different settings. Also, measure performance — setoid rewriting can involve heavy backtracking during search for `Proper`

instances.

Paolo Giarrusso said:

Shea Levy if

`R`

is symmetric I’d use`iff`

, not`impl`

, but I have only tested this with stdpp (where you also need flipped instances), not with the stdlib alone

Can you explain why? We usually define e.g. `transport`

like `x = y -> P x -> P y`

, not `x = y -> P x <-> P y`

but this isn’t transport, is it?

let me try an example

suppose your goal is `P x <-> P z`

and you know that `H : R x y`

(let’s ignore for a second that `R`

is symmetric)

I can just use the proper proof on H and sym H

Ah :)

“use the proper proof”?

the question is what `rewrite H`

will do

If I know `Proper (R ==> impl) P`

yes

because `P x`

occurs invariantly, that instance is not enough

Ah, so `rewrite`

won't try `sym`

. I guess that would probably be too expensive most of the time?

basically, because the instance for `iff`

is `Proper (iff ==> iff) iff`

, not `Proper (impl ==> impl) iff`

(IIUC)

until now I’m assuming `R`

isn’t symmetric

TLDR: this rewrite must find `Proper (R ==> iff) P`

somehow.

now, if `R`

is symmetric, can the needed instance be derived?

answer: I don’t know and I don’t want to know, but given how slow rewriting often gets, I wouldn’t want to.

sadly, rewriting tends to do _too much_ backtracking, rather than too little. It’s usually very quick, but when it gets perceptibly slow, `Set Typeclass Debug`

before it will give you a pretty long trace.

however, I don’t fully understand the machinery, so I mostly have questions and scars. my rewrites work, but not all of them are as fast as they should :-(

Last updated: Jan 31 2023 at 14:03 UTC