Stream: math-comp users

Topic: refinement between rel T and T -> seq T


view this post on Zulip Karl Palmskog (Oct 26 2021 at 09:08):

does it make sense to do CoqEAL style automated refinement between rel T and T -> seq T, for T : finType? I don't see any current machinery for this, but for low-level graph algorithm implementation and their correctness proofs, it seems to me one would often want to switch around, as was done here.

view this post on Zulip Cyril Cohen (Oct 26 2021 at 09:10):

makes sense to me

view this post on Zulip Evgeniy Moiseenko (Oct 26 2021 at 09:37):

Does T has to be finType though?
I often find myself doing the same juggling between rel T and T -> seq T in the context of rewrite systems & operational semantics,
where T represents states of the system and is not necessarily finite.
Perhaps eqType is sufficient?

view this post on Zulip Karl Palmskog (Oct 26 2021 at 09:44):

I don't think there is any way to get the seq T generally for an eqType, maybe countType?

view this post on Zulip Evgeniy Moiseenko (Oct 26 2021 at 09:50):

ah, sorry, you're right.
I was thinking only about conversion in one direction: from T -> seq T to rel T.
For the other direction we need choiceType, right?

view this post on Zulip Karl Palmskog (Oct 26 2021 at 10:00):

yeah, I guess one could do:

Probably there is already something close to this machinery in MathComp, and then some dotting of i's in CoqEAL is needed on top

view this post on Zulip Cyril Cohen (Oct 26 2021 at 10:50):

Actually, refinements do not need to be computable in CoqEAL, only the implem -> spec direction, which corresponds to (T -> seq T) -> rel T

view this post on Zulip Cyril Cohen (Oct 26 2021 at 10:51):

Cyril Cohen said:

Actually, refinements do not need to be computable in CoqEAL, only the implem -> spec direction, which corresponds to (T -> seq T) -> rel T

(actually, not even that, I think, but it makes things simpler)

view this post on Zulip Evgeniy Moiseenko (Oct 27 2021 at 08:37):

I realized that for rel T ==> T -> seq T direction we need more than just T : choiceType.
Also we need a finite-suffix constraint on relation r: forall x : T, exists ys : seq T, y \in ys <-> r x y.
It corresponds to finitely-branching rewrite systems, or locally-finite graphs.


Last updated: Feb 08 2023 at 04:04 UTC