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.

makes sense to me

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?

I don't think there is any way to get the `seq T`

generally for an `eqType`

, maybe `countType`

?

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?

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

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 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)

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