Ssreflect Users Discussion List

[Felipe Cerqueira <>]

Hello,

I've looked further into the issue and decided to re-implement the linear
extension for boolean relations. I tried using fingraph.v for implementing the
transitive closure, but the existing definitions do not seem to suffice.

The documentation states that connect implements the transitive closure,

    connect e == the transitive closure of e (computed by dfs),

but that's incorrect. What it implements is actually the reflexive transitive closure,
as shown in this lemma:

    Lemma connect0 x : connect x x.

Does anyone know the easiest way to obtain a non-reflexive version of connect?
Would the DFS function have to be changed?

Thanks,
Felipe


On 9/19/16 11:23 AM, Felipe Cerqueira wrote:

Hi everyone,

In my development I have a "<=" relation over a finite type that is total but not antisymmetric,
so when I restrict it to the strict order "<", it is no longer total.
I need to create an extension of < that preserves totality.

I already have an implementation for Prop relations, but it's not compatible with
Mathematical Components.
Does anyone know of an existing implementation for such a partial order extension?

In case I need to implement it myself, it seems that the definitions of transitive closure
are the ones in the graph library, right? I haven't worked with that library so far.

Thanks,
Felipe