Ssreflect Users Discussion List

[Allyx FONTAINE <>]

Hello,

I'm interesting in graphs and I especially look at lemmas on DFS in fingraph. Is there some similar work about BFS?


More particularly, I defined BFS as (lv are the visited nodes, and lr those which need to be explored) :

Variables (T : finType) (e : rel T).

Fixpoint bfs (n: nat) (sv sr: seq T) {struct n} : seq T :=
  if n is n'.+1 then
     if sr is (t::q) then
         (t::  (bfs n'
                      (t::sv)
                      (q ++ ( enum [set x| (e t x) && (x \notin sv) && (x \notin sr)] ))))
     else nil
  else nil.

and I would like to prove the following:

Lemma bfsP x y :
  reflect (exists2 p, path e x p & y = last x p)
          (y \in bfs #|T| [::] [::x]).

Best regards,
Allyx