Ssreflect Users Discussion List

[Erik Martin-Dorel <>]

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

-- 
Érik Martin-Dorel, PhD
Maître de Conférences, Lab. IRIT, Univ. Toulouse 3


https://www.irit.fr/~Erik.Martin-Dorel