Ssreflect Users Discussion List

[Christian Doczkal <>]

Hello, 

I've been using the fingraph library quite extensively and there has only 
ever been one instance where I found myself needing the (non-reflexive) 
transitive closure. I ended up defining it roughly as follows: 

Definition trans_closure e x y := [exists z, e x z && connect e z y]

This allows properties like transitivity etc. pp. to be proved using the 
existing lemmas for connect.

Best,
Christian

On 05/18/2018 08:08 PM, Erik Martin-Dorel wrote:
> Dear MathComp developers,
> 
> We recently explored the fingraph.v formalization (for reusing its
> definition of transitive closure that comes for free with a
> decidability proof of the obtained order…), and we noticed after a
> while that this definition "connect" was reflexive (cf. the presence
> of the "connect0" lemma).
> 
> It seems to us that the usual definition of the transitive closure
> (such as the one that can be found in Wikipedia articles) does not
> perform the reflexive closure at the same time.
> 
> So our question is twofold:
> 
> 1. Would you agree to change the documentation of fingraph to account
> for that? basically by replacing [1] with
> (* connect e == the reflexive transitive closure of e (computed by dfs). *)
> 
> [1] 
> https://github.com/math-comp/math-comp/blob/mathcomp-1.7.0/mathcomp/ssreflect/fingraph.v#L17
> 
> 
> 2. Would it be interesting for some users to provide a separate
> definition of the usual transitive closure in that file?
> 
> (If yes, maybe we could also refactor the current lemmas about the
> reflexive-transitive closure to depend on the new definition? but of
> course that latter refactoring effort is maybe not worth it…)
> 
> I give below a tentative definition for the transitive closure that we
> have started exploring (proving a few lemmas that are ommitted here).
> 
> --8<---------------cut here---------------start------------->8---
> (* The transitive closure is defined by "strict_connect".
>    "dfs_excl" could be removed and inlined in this definition… *)
> 
> Definition dfs_excl' (g : T->seq T) (n:nat) (v:seq T) (x:T) :=
>   if x \in v then v else
>     match n with
>     | 0     => v
>     | n'.+1 => foldl (dfs g n') v (g x)
>     end.
> 
> Definition dfs_excl (g : T->seq T) (x:T) :=
>   dfs_excl' g (#|T|.+1) [::] x.
> 
> Definition strict_connect (e : rel T) : rel T :=
>   fun x y => y \in dfs_excl (rgraph e) x.
> --8<---------------cut here---------------end--------------->8---
> 
> Feel free to comment if you think that another definition would be
> more appropriate.
> 
> Kind regards,
> 
> Erik and Marc
>