Making a finite graph type in Lean - introduction rule

Question

I'm making a finite directed graph type in Lean. I know type theory from an abstract point of view, but I'm struggling to find the way Lean would produce a type playing the role of a "finite set", where we explicitly specify all of its constituents. I also need to define a type for the incidence preserving functions between different directed graphs. But since types aren't like sets in this way, I'm unsure of what plays this role in Lean.

The other thing I'm struggling with is notation. I'd like to be able to introduce a finite graph using something like this: {x, y, z, w, e : x -> y, f : y -> z}. But I'm not sure how flexible Lean's notation is.

Thanks so much for any help!

Answer 1

Here is how Lean defines undirected graphs (docs):

structure simple_graph (V : Type u) :=
(adj : V → V → Prop)
(symm : symmetric adj . obviously)
(loopless : irreflexive adj . obviously)

For notation, since this is a structure you could construct a graph using one of Lean's many notations for constructing structures, for example:

def my_graph : simple_graph int := { 
  adj := λ n m, 0 < n ∧ m = -n, 
  symm := sorry,    -- replace sorry with a proof that adj is symmetric
  loopless := sorry -- replace sorry with a proof that adj is non-reflexive
}

The idea of a directed and undirected graph are similar. A graph is a set of nodes with an edge relation. For an undirected graph, this relation is symmetric and non-reflexive. For a directed graph, you don't need these conditions so it is simpler. This is assuming you want at most one directed edge between nodes.

If you want to allow more than one edge between a pair of nodes, then there are a number of approaches. You could modify this example to make a structure depending on both type V of vertices and a type E of edges where there is a source and target map:

structure multi_edge_directed_graph (V : Type u) (E : Type u) :=
(source : E → V)
(target : E → V)

Now as for finite graphs, you just have to require that the type V (and E if a multi-edge graph) is also finite. This can be done with the typeclass fintype. For example this instance proves that if the vertex type is finite, then the graph is as well (docs). Since it is a typeclass instance, this can be derived automatically (if say I have a graph on bool, since Lean knows bool is a fintype, it also knows any graph on bool is by this instance).

noncomputable instance {V : Type u} [fintype V] : fintype (simple_graph V) :=
by { classical, exact fintype.of_injective simple_graph.adj simple_graph.ext }

Also, see the Lean docs for how to define other notations like graph homomorphisms. Note, it looks like this project is still a work in progress, so you may want to reach out to the authors for advice on contributing more types of graphs once you are comfortable with the tools.