Graphs in Lean

Stream: new members

[Simon Daniel]

Hello,
I want to model a network by a set of Nodes (String) and Edges between Nodes (a Subset of cartesian product of Nodes).
i tried

structure Network where
  nodes: List String
  edges: List (String × String)
  p: ∀ (l1 l2: String), edges.contains (l1, l2) -> (nodes.product nodes).contains (l1, l2)

def testNet: Network := Network.mk ["hello", "alice"] [("alice", "hello")] (by sorry)

but somehow i feel like there should be a nicer approach. Is using lists and ignoring duplicates even the way to go?

[Timo Carlin-Burns]

Are you looking to write efficient algorithms with this data structure? The problem of data structures to represent networks (AKA graphs) is a well-studied one in computer science

[Simon Daniel]

im effectively trying to write a directed graph where my nodes are a finite subset of String. Efficent algorithms are none of my concerns, i need to find (optional) paths from a to b and connected subgraphs.
But the Lean std does not provide a datatype for sets right? i only found https://leanprover-community.github.io/mathlib4_docs/Lean/Data/SSet.html which seems to be for a different purpose. Should i look into Set or FinSet of Mathlib?
or something like this with subtypes

def string_subtype := {s:String // ["alice", "bob", "eve"].contains s}
def node: string_subtype := ⟨"alice", by decide⟩

[Timo Carlin-Burns]

Mathlib has docs#SimpleGraph for an undirected graph

[Timo Carlin-Burns]

It represents edges with a predicate

[Timo Carlin-Burns]

You can also represent edges with a docs#Set

[Timo Carlin-Burns]

But predicates and Sets are computationally useless, so if you want to write an algorithm to find a path, you will need something else. If you just want to proof that some sequence of nodes is a path, then these approaches will work fine

[Simon Daniel]

could you elaborate why its useless? i guess because both represent possibly infinite Sets?
Im more used to Sets from other Programming languages that are a (finite) collection of unique items instead of a predicate on a type

[Matthew Ballard]

Predicates do not generate executable code by default

[Kyle Miller]

There are some computations done on SimpleGraph, but the way these work is that they make use of the Fintype and Decidable typeclasses to register computations for particular SimpleGraphs.

• DecidableRel G.Adj with Fintype V is essentially an adjacency matrix representation
• Fintype (G.neighborSet v) for all v gives you an adjacency list representation

In the Connectivity module, there are for example algorithms to compute whether a graph is connected. Horrible algorithms that you never want to evaluate, but they're technically still algorithms.

You may say you're not interested in efficient algorithms, but if you want to compute anything at all, I think you'll say you want an efficient algorithm (there's a difference between efficient and optimal after all).

[Kyle Miller]

Using Set in the definition of SimpleGraph is making SimpleGraph be a sort of abstract definition of a graph, with no concrete data structure, but every data structure for a simple graph can be converted to a SimpleGraph, and they can provide classes for various computations. In Mathlib, we don't have any concrete data structures for graphs.

There's an example data structure in the Königsberg bridge problem in the Archive here, where the graph is created from a list of adjacent vertex pairs.

[Simon Daniel]

thanks for the explanation, the example has been useful