Depth-first search on quivers, with proof

Stream: mathlib4

[Anand Rao Tadipatri]

I am considering implementing the depth-first search algorithm for finite quivers and proving a few related properties. This may be useful in graph theory or geometric group theory, where one may want to produce a spanning tree of a connected graph or decide whether two vertices of a graph are connected by a (directed) path. Ideally the implementation should run reasonably fast on small graphs to allow testing of examples, while also being transparent enough to allow proofs.

I am thinking of implementing something along the lines of the code snippet below (perhaps rewritten to avoid loops and mutable variables if that makes the proofs easier). I would like to know whether this kind of algorithm with proofs is suitable for Mathlib. I would also appreciate feedback on whether and in what form definitions and constructions such as Listable, Quiver.neighbourhood and the union of WideSubquivers should be integrated into Mathlib.

import Mathlib.Combinatorics.Quiver.Subquiver
import Mathlib.Data.Fintype.Basic

/-- A version of `Fintype α` which not only expresses the
  fact that the type is finite but also gives a way of enumerating the elements. -/
class Listable (α : Sort _) where
  elems : List α
  complete : ∀ x : α, x ∈ elems
  -- may be unnecessary
  nodup : elems.Nodup

notation "[" α "]ₗ" => (Listable.elems : List α)

instance {α : Sort _} [Listable α] : Fintype α :=
  ⟨⟨.mk' [α]ₗ, Listable.nodup⟩, Listable.complete⟩

instance {α : Sort _} [Fintype α] [Ord α] : Listable α := sorry

instance {α : Sort _} {β : α → Sort _}
  [Listable α] [∀ a : α, Listable (β a)] : Listable (Sigma β) :=
  { elems := .join <| [α]ₗ.map <| fun a => [β a]ₗ.map (Sigma.mk a),
    complete := sorry, nodup := sorry }

instance {α : Sort _} [Listable α] {P : α → Prop} [DecidablePred P] : Listable {a : α // P a} :=
  { elems := [α]ₗ.filterMap <| fun a =>
    if h : P a then some ⟨a, h⟩ else none
  , complete := sorry, nodup := sorry }


def Quiver.star [Q : Quiver V] (v : V) := Σ w : V, v ⟶ w

instance {V : Sort _} [Q : Quiver V] [Listable V] (v : V) [∀ w : V, Listable (v ⟶ w)] :
  Listable (Quiver.star(Q := Q) v) :=
  inferInstanceAs <| Listable <| Sigma _

namespace WideSubquiver

instance [Quiver V] : Union (WideSubquiver V) :=
  ⟨fun Q Q' v w => Q v w ∪ Q' v w⟩

def ofEdge [Quiver V] {v w : V} (e : v ⟶ w) : WideSubquiver V :=
  Quiver.wideSubquiverEquivSetTotal.invFun {⟨v, w, e⟩}

end WideSubquiver

variable {V : Type _} [Q : Quiver V] [Listable V] [∀ v w : V, Listable (v ⟶ w)] [DecidableEq V]

def depthFirstTraversal (root : V) (visited : List V) : List V × (WideSubquiver V) := Id.run do
  let mut discovered := root :: visited
  let mut Q : WideSubquiver V := ⊥
  for ⟨w, e⟩ in [Quiver.star root]ₗ do
    if w ∉ discovered then
      have : [V]ₗ.length - discovered.length < [V]ₗ.length - visited.length := sorry
      let (discovered', Q') := depthFirstTraversal w discovered
      Q := Q ∪ (WideSubquiver.ofEdge e) ∪ Q'
  return (discovered, Q)
termination_by _ => [V]ₗ.length - visited.length

theorem visited_of_edge {u v w : V} (e : v ⟶ w) : v ∈ (depthFirstTraversal u []).fst → w ∈ (depthFirstTraversal u []).fst := by
  unfold depthFirstTraversal
  sorry

[Rémi Bottinelli]

Not very important, but in PR 17828 we call your Neighborhood Star.

[Anand Rao Tadipatri]

Thanks, I think star sounds better. I've updated my code snippet.

[Shreyas Srinivas]

This is nice. May I ask why you would like to remove mutable variables? There is much to be gained from being able to reason about mutable variables in the algorithms world, at least complexity-theory-wise.

[Rémi Bottinelli]

How do you even reason about those (mutables) in lean? Is it translated to some monad?

[Shreyas Srinivas]

Rémi Bottinelli said:

How do you even reason about those (mutables) in lean? Is it translated to some monad?

I don't know yet. My idea was to use restricted mutations. But this is a slightly different context.

[Anand Rao Tadipatri]

Thanks. I believe the code in the Id monad is compiled down to fold and map internally. I prefer the mutable variable and loop syntax too, but I am not sure how easy it will be to analyse in a proof.

I am not having very good results trying to prove this test lemma about the depthFirstTraversal function:

theorem visited_of_edge {u v w : V} (e : v ⟶ w) : v ∈ (depthFirstTraversal u []).fst → w ∈ (depthFirstTraversal u []).fst := by
  unfold depthFirstTraversal
  sorry

[Shreyas Srinivas]

Am I correct to assume that you are not using this to make complexity claims? We will probably be doing something similar for complexity and algorithms. I am checking to avoid duplication of effort and names of defs

[Yuyang Zhao]

We recently found docs#fin_enum / docs4#FinEnum and no file import it, I think we should choose one between it and Listable to keep in mathlib (of course, maybe make some small changes).

[Anand Rao Tadipatri]

Yes, you're right - I am mainly concerned with using this implementation to perform small-scale computations with graphs and using it with proofs to automatically decide properties like connectedness and reachability. However I'd be happy to coordinate and work on implementing it in a way that's useful to both complexity analysis and decision procedures/proofs.

[Anand Rao Tadipatri]

Yuyang Zhao said:

We recently found docs#fin_enum / docs4#FinEnum and no file import it, I think we should choose one between it and Listable to keep in mathlib (of course, maybe make some small changes).

Thanks. FinEnum seems to already have a large number of useful lemmas and constructions associated with it. One thing that seems to be missing, but may be useful while trying out computations, is the for ... in notation through the ForIn typeclass.

[Yuyang Zhao]

(As an experienced competitive programmer I can't wait to use lean to write some algorithms (with correctness proofs), but I'm still trying to convince some Online Judge owners to add lean4 to their OJ :innocent: )

[Anand Rao Tadipatri]

(Indeed - with the Std4 library, competitive programming in Lean4 seems very much a possibility.)