Stream: math-comp users

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

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.

Cyril Cohen (Oct 26 2021 at 09:10):

makes sense to me

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?

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?

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?

Karl Palmskog (Oct 26 2021 at 10:00):

yeah, I guess one could do:

• T -> seq T ==> rel T for any T : eqType
• rel T ==> T -> seq T for any T : choiceType

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

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

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)

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: Apr 19 2024 at 15:02 UTC