## 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: Jul 25 2024 at 15:02 UTC