Stream: Coq users

Topic: Generalized rewriting in predicates?


view this post on Zulip 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?

view this post on Zulip 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 (->).

view this post on Zulip 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?

view this post on Zulip Shea Levy (Oct 31 2020 at 19:07):

Sorry, Proper (R ==> iff) P

view this post on Zulip Li-yao (Oct 31 2020 at 19:13):

Exactly :)

view this post on Zulip Shea Levy (Oct 31 2020 at 19:28):

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

view this post on Zulip Li-yao (Oct 31 2020 at 19:30):

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

view this post on Zulip Shea Levy (Oct 31 2020 at 19:31):

Thanks!

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Oct 31 2020 at 20:10):

but this isn’t transport, is it?

view this post on Zulip Paolo Giarrusso (Oct 31 2020 at 20:10):

let me try an example

view this post on Zulip Paolo Giarrusso (Oct 31 2020 at 20:10):

suppose your goal is P x <-> P z

view this post on Zulip Paolo Giarrusso (Oct 31 2020 at 20:10):

and you know that H : R x y

view this post on Zulip Paolo Giarrusso (Oct 31 2020 at 20:11):

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

view this post on Zulip Shea Levy (Oct 31 2020 at 20:11):

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

view this post on Zulip Shea Levy (Oct 31 2020 at 20:11):

Ah :)

view this post on Zulip Paolo Giarrusso (Oct 31 2020 at 20:11):

“use the proper proof”?

view this post on Zulip Paolo Giarrusso (Oct 31 2020 at 20:11):

the question is what rewrite H will do

view this post on Zulip Shea Levy (Oct 31 2020 at 20:12):

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

view this post on Zulip Paolo Giarrusso (Oct 31 2020 at 20:12):

yes

view this post on Zulip Paolo Giarrusso (Oct 31 2020 at 20:12):

because P x occurs invariantly, that instance is not enough

view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip Paolo Giarrusso (Oct 31 2020 at 20:13):

until now I’m assuming R isn’t symmetric

view this post on Zulip Paolo Giarrusso (Oct 31 2020 at 20:13):

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

view this post on Zulip Paolo Giarrusso (Oct 31 2020 at 20:14):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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: Jan 31 2023 at 14:03 UTC