Ssreflect Users Discussion List

[Emilio Jesús Gallego Arias <>]

Hi Florent,

Florent Hivert 
<>
 writes:

> Therefore, I find it easier to use a third encoding:
>
> - r : {set T * T}
>
> Aside from the full finset possibilities, this encoding has the advantage of
> being fully extensional. Indeed, one can use r1 = r2 and r1 == r2 in place 
> of
> e1 =2 e2... From r, one can easily recover e by
>
>   e = prod_curry (mem r)
>
> It could even be made a coercion {set T * T} -> rel T
>
> Is there anyone else using the same trick ? Do you think it is a good way to
> do ? Is there a problem with such a coercion ?  Should fingraph.v be 
> extended
> accordingly ? Any suggestion ?

Indeed we used that encoding in:

https://github.com/VerDILog/VerDILog/blob/iclp-2018/vup.v#L876

I guess it seemed natural both to extract to an OCaml set implementation
[which is a natural fit for that algoritmm] and to get some nicer
extensions [such as labelled graphs] in an easier way.

But AFAICT, revisiting the choice was still on our minds [as the
comments in the file point out :)] , so I am not sure if we can
contribute any insight other than the above code.

E.