Stream: Coq users

Topic: Generalized rewriting in predicates?

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

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?

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

Predicates are functions ... -> Prop. Respectful predicates are respectful functions, where the relation in Prop is iff (<->) or sometimes impl (->).

Shea Levy (Oct 31 2020 at 19:05):

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?

Shea Levy (Oct 31 2020 at 19:07):

Sorry, Proper (R ==> iff) P

Li-yao (Oct 31 2020 at 19:13):

Exactly :)

Shea Levy (Oct 31 2020 at 19:28):

And I guess if R is symmetric I can use impl just as well?

Li-yao (Oct 31 2020 at 19:30):

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

Shea Levy (Oct 31 2020 at 19:31):

Thanks!

Paolo Giarrusso (Oct 31 2020 at 20:07):

@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

Paolo Giarrusso (Oct 31 2020 at 20:09):

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.

Shea Levy (Oct 31 2020 at 20:09):

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

Paolo Giarrusso (Oct 31 2020 at 20:10):

but this isn’t transport, is it?

Paolo Giarrusso (Oct 31 2020 at 20:10):

let me try an example

Paolo Giarrusso (Oct 31 2020 at 20:10):

suppose your goal is P x <-> P z

Paolo Giarrusso (Oct 31 2020 at 20:10):

and you know that H : R x y

Paolo Giarrusso (Oct 31 2020 at 20:11):

(let’s ignore for a second that R is symmetric)

Shea Levy (Oct 31 2020 at 20:11):

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

Shea Levy (Oct 31 2020 at 20:11):

Ah :)

Paolo Giarrusso (Oct 31 2020 at 20:11):

“use the proper proof”?

Paolo Giarrusso (Oct 31 2020 at 20:11):

the question is what rewrite H will do

Shea Levy (Oct 31 2020 at 20:12):

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

Paolo Giarrusso (Oct 31 2020 at 20:12):

yes

Paolo Giarrusso (Oct 31 2020 at 20:12):

because P x occurs invariantly, that instance is not enough

Shea Levy (Oct 31 2020 at 20:13):

Ah, so rewrite won't try sym. I guess that would probably be too expensive most of the time?

Paolo Giarrusso (Oct 31 2020 at 20:13):

basically, because the instance for iff is Proper (iff ==> iff) iff, not Proper (impl ==> impl) iff (IIUC)

Paolo Giarrusso (Oct 31 2020 at 20:13):

until now I’m assuming R isn’t symmetric

Paolo Giarrusso (Oct 31 2020 at 20:13):

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

Paolo Giarrusso (Oct 31 2020 at 20:14):

now, if R is symmetric, can the needed instance be derived?

Paolo Giarrusso (Oct 31 2020 at 20:14):

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

Paolo Giarrusso (Oct 31 2020 at 20:15):

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.

Paolo Giarrusso (Oct 31 2020 at 20:17):

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: Oct 03 2023 at 21:01 UTC