Flow networks and flow equivalent forest

Stream: graph theory

[Niklas Mohrin]

Hi all! Over the last couple of months, we have been working on proving one side of the characterization of flow matrices in Lean 4. As of Wednesday, we are done with no sorries left! If anyone is interested, the code can be found at https://github.com/niklasmohrin/lean-seminar-2023 . The theorem we proved is the following: Given an undirected flow network G, we define its flow matrix to be the Matrix M with M[u, v] = "max flow in G from u to v". Then, for any Matrix, it holds that M is the flow matrix of some network G if and only if M is symmetrical and forall u, v, w we have min{M[u,v], M[v,w]} <= M[u,w]. One implication follows directly from MinCutMaxFlow theorem, the other one is more interesting, because it turns out that not only is it possible to construct a flow network from a matrix (for which the assumptions hold) with said matrix as its flow matrix, but we can even construct a network whose only non-null capacity edges form a forest! (This is the motivation for the Gomory-Hu-Tree algorithm, which computes such a flow equivalent tree efficiently). We will maybe try to upstream some of the useful stuff into mathlib, but most of our definitions would probably need some work first before being able to be merged into mathlib (for example flows taking values in the natural numbers turns out to be cause more pain than joy - a type parameter would be better).

[Yaël Dillies]

The first PR is #13685. I think it looks very good, but I am not an expert in network flows and have a hard time deciding whether the setup is general enough, eg #13685 currently doesn't apply to multigraphs.

[Yaël Dillies]

Could people who know more about it than me comment on the PR? Maybe @Apurva Nakade, @Martin Dvořák, @Kyle Miller?

[Shreyas Srinivas]

There is another PR to add directed graphs. Couldn't that definition be extended to provide the definition of Networks?

[Yaël Dillies]

You mean #14091 ?

[Shreyas Srinivas]

yes

[Shreyas Srinivas]

Could lead to API clutter if not harmonised

[Yaël Dillies]

@Niklas Mohrin, see the discussion above

[Shreyas Srinivas]

About multigraphs. The max flow min cut theorem trivially extends to (at least finite) multigraphs. Just clump all the multi-edges into one edge while adding their flows and capacities.

[Shreyas Srinivas]

the Ford Fulkerson method would still apply.

[Shreyas Srinivas]

That being said, encoding multigraphs in matrices is definitely more painful.

[Shreyas Srinivas]

To be precise there is the incidence matrix which applies as is, but not sure how the others are used.

[Shreyas Srinivas]

The convex optimisation folks do use the flow incidence matrix. See chapter 1 of https://convex-optimization.github.io/ (There is a free but password protected pdf with the password on this webpage, which is why I am not linking to the PDF).

[Shreyas Srinivas]

So, I don't see any obvious way or reason to generalise this work to multigraphs. It seems fine to me as is.

[Shreyas Srinivas]

What I would suggest is to call the Flow matrices FlowAdjMatrices

[Niklas Mohrin]

As far as generalization goes, I think that multigraphs could only become interesting if we add more parameters to each edge, for example if we wanted to model flows with costs associated with each edge (which is not too uncommon). For everything else, just summing the capacities of each edge from u to v and merging it into one edge should be equivalent.

Some textbooks define networks as a graph combined with a capacity function c: E -> N (or similar), however, this did not seem appropriate at the time of writing since we wanted to be able to write N.cap u v directly (and would need an extra implication not Adj -> cap = 0, when really the network does just fine without tying it to graphs.

If you want to take a look at some more involved theorems, take a look at the ring branch of the github repository linked above, this is where I worked on replacing Nat (and Int) with rings like in my PR. This also contains one half of Min Cut Max Flow - I got stuck proofing the other direction (i.e. implementing some max-flow algorithm, see the maxflow branch for my last status)

[Niklas Mohrin]

Directed graphs in mathlib would be great (if all of the Walk and Path stuff is ported to them). For our seminar theorem, we came up with UndirectedNetwork.asSimpleGraph where Adj u v = 0 < cap u v. This had the disadvantage that this only forms a simple graph for undirected networks and all the decomposition theorems also only held for undirected networks because they used N.asSImpleGraph.Walk frequently. Later, when I generalized everything, I also changed the decomposition to use (fullGraph V).Walk instead and this worked to generalize to undirected networks too. I still find the first version more intuitive though, so having directed graphs would make this a lot nicer

[Niklas Mohrin]

So the design goal would be to not redefine any graph related stuff, but to have a conversion to graphs and frequently talk about objects related to this conversion, just like for example the bottleneck along a path of a graph is currently defined in the seminar repository as

def UndirectedNetwork.bottleneck
    {N : UndirectedNetwork V}
    (P : N.asSimpleGraph.NonemptyPath s t) : ℤ
  := ...

[Shreyas Srinivas]

About the mathlib direct graph API : Currently it is still in PR. I suggest that the two PRs be coordinated in some way since we probably do not benefit from duplicate API. About max flow min cut: I would suggest picking the Edmonds karp algorithm since there is already a formalisation in Isabelle for guidance: https://www.isa-afp.org/entries/EdmondsKarp_Maxflow.html

[Niklas Mohrin]

Shreyas Srinivas said:

What I would suggest is to call the Flow matrices FlowAdjMatrices

Are you referring to the "flow matrix" mentioned in the seminar repository and the theorem there, or is this about my open PR and the definitions from there? If it is the former, I think Adj is not really appropriate in there, because the matrix cells refer to max flow values between vertices that may only be connected through multiple edges (or not at all). If you mean the latter, I am not sure I understand what definition is meant that needs renaming - can you clarify?

[Shreyas Srinivas]

Shreyas Srinivas said:

About the mathlib direct graph API : Currently it is still in PR. I suggest that the two PRs be coordinated in some way since we probably do not benefit from duplicate API. About max flow min cut: I would suggest picking the Edmonds karp algorithm since there is already a formalisation in Isabelle for guidance: https://www.isa-afp.org/entries/EdmondsKarp_Maxflow.html

Do take into consideration that you don't need to prove the complexity bound like they do. Implementing the algorithm as noncomputable lean functions is sufficient for proof purposes.

[Niklas Mohrin]

Shreyas Srinivas said:

About the mathlib direct graph API : Currently it is still in PR. I suggest that the two PRs be coordinated in some way since we probably do not benefit from duplicate API. About max flow min cut: I would suggest picking the Edmonds karp algorithm since there is already a formalisation in Isabelle for guidance: https://www.isa-afp.org/entries/EdmondsKarp_Maxflow.html

Ah, very cool! I was trying for quite some time to prove termination of Dinitz Algorithm, but failed as all proofs I know are reasoning about the changes made throughout multiple phases - and I didn't want to track the phases in the algorithm, but rather iterate like I would when implementing in another language. I considered Edmonds Karp too, but the argument seemed even more difficult to me, since also here we talk about increase of a function over a handful of iterations. I didn't really know how to formalize this argument cleanly and ultimately lost interest

[Shreyas Srinivas]

Niklas Mohrin said:

Shreyas Srinivas said:

What I would suggest is to call the Flow matrices FlowAdjMatrices

Are you referring to the "flow matrix" mentioned in the seminar repository and the theorem there, or is this about my open PR and the definitions from there? If it is the former, I think Adj is not really appropriate in there, because the matrix cells refer to max flow values between vertices that may only be connected through multiple edges (or not at all). If you mean the latter, I am not sure I understand what definition is meant that needs renaming - can you clarify?

It is not quite an adjacency matrix but flow constraints can be represented using incidence matrices. I am suggesting that these be distinguished somehow. Maybe calling Vertex Flow matrices helps

[Niklas Mohrin]

Shreyas Srinivas said:

Shreyas Srinivas said:

About the mathlib direct graph API : Currently it is still in PR. I suggest that the two PRs be coordinated in some way since we probably do not benefit from duplicate API. About max flow min cut: I would suggest picking the Edmonds karp algorithm since there is already a formalisation in Isabelle for guidance: https://www.isa-afp.org/entries/EdmondsKarp_Maxflow.html

Do take into consideration that you don't need to prove the complexity bound like they do. Implementing the algorithm as noncomputable lean functions is sufficient for proof purposes.

But we need some kind of upper bound, otherwise the termination checker will not accept our definition, right?

[Shreyas Srinivas]

Niklas Mohrin said:

Shreyas Srinivas said:

About the mathlib direct graph API : Currently it is still in PR. I suggest that the two PRs be coordinated in some way since we probably do not benefit from duplicate API. About max flow min cut: I would suggest picking the Edmonds karp algorithm since there is already a formalisation in Isabelle for guidance: https://www.isa-afp.org/entries/EdmondsKarp_Maxflow.html

Ah, very cool! I was trying for quite some time to prove termination of Dinitz Algorithm, but failed as all proofs I know are reasoning about the changes made throughout multiple phases - and I didn't want to track the phases in the algorithm, but rather iterate like I would when implementing in another language. I considered Edmonds Karp too, but the argument seemed even more difficult to me, since also here we talk about increase of a function over a handful of iterations. I didn't really know how to formalize this argument cleanly and ultimately lost interest

Well founded recursion

[Shreyas Srinivas]

The answer to your other question is also well founded recursion

[Shreyas Srinivas]

I am not saying it will be an easy proof.

[Niklas Mohrin]

Well, yes, but I couldn't find a way to prove the decreasing relation, because the argument I found was arguing about the change over multiple phases

[Niklas Mohrin]

In particular for Dinitz, the distance in the residual network between s and t increases in every phase up until |V|, but I failed to prove it so far

[Niklas Mohrin]

Or do you think it will be easier to construct another well founded relation that does not follow the usual upper bound for running time? I feel that every "easy" relation, for example the sum of values the flow function takes or the sum of distances in the residual network, either doesn't work because R might is not well ordered or because the relation is not strictly increasing / decreasing

[Shreyas Srinivas]

you could try "every iteration, the number of unsaturated edges strictly decreases"

[Niklas Mohrin]

I will probably look back into this when I find time, around September, Edmonds Karp proof in Isabelle seems like a very good resource for sure :+1:

[Shreyas Srinivas]

you can probably save a lot of effort by using noncomputable and not implementing the algorithm the way they do. They have to reinvent WF iirc if they work in their DSL for algorithms

[Shreyas Srinivas]

Making heavy use of sets, finsets etc

[Niklas Mohrin]

The question for my PR remains, whether we want to design it with Min-Cost-Max-Flow _with multiple edges, with different costs_ already, or whether that makes the normal definition too annoying to work with in the case of just working on flows

[Shreyas Srinivas]

My personal opinion is that modulo the name change for Flow matrices (some disambiguation to clarify that it is vertex to vertex flow), I personally don't see the point of going down the min cost flow rabbit hole

[Shreyas Srinivas]

These are meaningfully different problems

[Niklas Mohrin]

Shreyas Srinivas said:

you can probably save a lot of effort by using noncomputable and not implementing the algorithm the way they do. They have to reinvent WF iirc if they work in their DSL for algorithms

Yeah, for sure we also want to use Classical.choice to choose which augmenting path to use. We could later change it to allow supplying a computable choice function, but it is irrelevant for proving stuff

[Shreyas Srinivas]

Exactly

[Shreyas Srinivas]

You do need to prove the relevant choice theorem.

[Niklas Mohrin]

Shreyas Srinivas said:

These are meaningfully different problems

Fair enough :+1:

[Niklas Mohrin]

Shreyas Srinivas said:

You do need to prove the relevant choice theorem.

What do you mean?

[Shreyas Srinivas]

that there is a path to choose

[Shreyas Srinivas]

for the PR I think you already distinguish between a flow and its matrix. So that should be sufficient generality for adding min cost flow later if someone wants to

[Niklas Mohrin]

Shreyas Srinivas said:

that there is a path to choose

The way that worked in my previous attempts was that the I branch on h : Nonempty F.residualNetwork.Path s t and augment and iterate, if it exists, or terminate otherwise

[Shreyas Srinivas]

oh okay

[Niklas Mohrin]

Shreyas Srinivas said:

for the PR I think you already distinguish between a flow and its matrix. So that should be sufficient generality for adding min cost flow later if someone wants to

Okay, so what exactly should be renamed then?

I am having a hard time understanding the definition from the convex optimization book and I have never seen it defined like this - I am not much into convex optimization either though. Do you think we will ever make use of the terminology from this definition, and if so, shouldn't we lean more into it or mention it in the file documentation? In my opinion, I would rather steer clear of it unless we intend to include some theory around it. Do you think that people will be confused by the definition of the PR, if there is no clarification in regards to the alternative definition from the book?

[Shreyas Srinivas]

A lot of names in texts are simplified because they are understood from context. When added to a general library like Mathlib, the names must be appropriately qualified. Whether Mathlib will ever include any convex optimisation math is a different story.

[Niklas Mohrin]

Another idea that might be worth to investigate: We could also make more fine-grained definitions already, for example

@[ext]
structure PseudoFlow (Pr : FlowProblem N) where
  f : V → V → R
  nonneg : ∀ u v, 0 ≤ f u v
  capacity : ∀ u v, f u v ≤ N.cap u v

@[ext]
structure PreFlow (Pr : FlowProblem N) extends PseudoFlow Pr where
  excess : ∀ v, v ≠ Pr.s ∧ v ≠ Pr.t → flowOut f v ≤ flowIn f v

@[ext]
structure Flow (Pr : FlowProblem N) extends PseudoFlow Pr where
  conservation : ∀ v, v ≠ Pr.s ∧ v ≠ Pr.t → flowOut f v = flowIn f v

We probably don't need PreFlow for now, but it could be nice to already have the split if someone one day wants to work on the PushRelabel algorithm. One uncertainty I have with this definition is that Flow should probably extend PreFlow, but that would make the definition a bit uglier since conservation implies excess. What do you all think?

[Niklas Mohrin]

@Shreyas Srinivas could you look over #13685 and make a suggestion on how to mention the convex optimization vocabulary? I am not sure where exactly it would best fit in

[Shreyas Srinivas]

I don't see why, in your PR, you would mention convex optimisation. There they use different matrices

[Shreyas Srinivas]

My only suggestion is to use an unambiguous name like "FlowVertexMatrix" or something you might find more suitable.

[Niklas Mohrin]

But use the name for what? Do you mean to rename Flow -> FlowVertexMatrix?

[Shreyas Srinivas]

Oh I see. You haven't included the flow matrices from your repo in this PR. Seems fine to me.

[Niklas Mohrin]

Alright then

[Shreyas Srinivas]

I wouldn't mention something that hasn't come up yet.

[Niklas Mohrin]

I agree, I just thought that you were talking about something from the PR. It will be some time until the "flow matrices" from the seminar repository could make it into mathlib, there is lots of stuff to do before

[Shreyas Srinivas]

Another thing about your PR.

[Shreyas Srinivas]

It seems what you call a Network is a Digraph. That DiGraph API was just merged into Mathlib.

[Shreyas Srinivas]

Your definition of Network could extend Digraph

[Shreyas Srinivas]

Currently it is simply treating the network as a complete graph with 0 capacity presumably indicating non-edges

[Shreyas Srinivas]

I would recommend extending DiGraph and adding a property for the cap function that makes this explicit.

[Shreyas Srinivas]

Also @Yaël Dillies , since you are a mathlib maintainer for combi and active on this thread: It seems this PR creates a fourth graph theory related folder under the Combinatorics folder . The existing ones are SimpleGraph, DiGraph, and Quiver. Do you think the Flow file created by this PR belongs under Digraph instead of a separate Flow folder?

[Yaël Dillies]

*reviewer

[Yaël Dillies]

I have in the past argued that we should rename the SimpleGraph folder to Graph.Simple the day mathlib acquires another kind of graphs. Seems like this day has happened

[Shreyas Srinivas]

I would suggest creating a Graph Theory folder and subsuming the purely graph theory related folders into it

[Shreyas Srinivas]

Yaël Dillies said:

I have in the past argued that we should rename the SimpleGraph folder to Graph.Simple the day mathlib acquires another kind of graphs. Seems like this day has happened

Right that message just appeared. Agreed.

[Niklas Mohrin]

We considered basing the Network type on SimpleGraph when we first defined it in our seminar. In fact, in the literature, flow networks are sometimes defined as a function $c : E -> R$ where $E$ are the edges of some underlying graph. However, we felt that there is not much benefit, while there is the disadvantage of making the Network (and Flow) interface less ergonomic with something like cap : Adj u v -> R. Instead, we added asSimpleGraph to convert the network to a graph to make statements about the underlying structure.

If I understand your suggestion correctly, you would not alter the definition of cap, but instead add another field with 0 < cap u v -> Adj u v. This sounds indeed nicer than the cap : Adj u v -> R version, but I am still not sure whether the change is worth it. The obvious benefit would be that there is no need for N.asDiGraph.Path u v anymore and it would just be N.Path u v (or something like N.asSimpleGraph.IsAcyclic from our seminar code would just be N.IsAcyclic). The downside is that we have the potentially unnecessary complication of having to choose a graph when defining a network. I suppose we could provide True as a default value for Adj (and also one for this new condition)?

[Shreyas Srinivas]

Two things:

1. What I am suggesting is cap : V -> V -> \R with cap_non_edge : \forall v w : V, \neg G.Adj v w -> cap v w = 0
2. Not integrating the flow stuff with digraphs means we effectively have a parallel API for flows. Flow problems are fundamental enough to be primitives elsewhere in graph theory. Think of finding a maximum bipartite matching in a graph by turning into a flow problem for example. Not doing this step of deriving from Digraph means Mathlib doesn't get a well-integrated API. Just my two cents. Maybe @Yaël Dillies can chip in.

[Niklas Mohrin]

I don't think there would be a parallel API, because any graph-y statements would be made through asSimpleGraph / asDiGraph. The question is whether we prefer the Network extends DiGraph or the Network.asDiGraph design

[Shreyas Srinivas]

How do you go from Graph to Network?

[Niklas Mohrin]

I would say you just have to define a network with the capacities you want. I don't see how extends DiGraph would make this more ergonomic

[Shreyas Srinivas]

It would define the network for the graph with cap_non_edge

[Niklas Mohrin]

But what capacity do you choose?

[Shreyas Srinivas]

that's beside the point. A network of flows makes little sense without being consistent with a graph structure. In Mathlib we are only proving theorems anyway

[Shreyas Srinivas]

It is upto users to instantiate the capacity function such that cap_non_edge holds.

[Niklas Mohrin]

I am not sure I agree; although flows are of course tightly related to graphs, we have evidence that the definition of networks that does not include graphs in the definition can work in the seminar repository. I don't see how only having theorems should influence our design, in fact, I think we should strive to allow usage of these types for downstream projects that _do_ want to run the code. As far as I see it, the decision boils down to opinion on which interface we think is nicer

[Niklas Mohrin]

I actually think that using Network extends DiGraph to allow for N.Path u v is a very fair reason to go with this design, I am just curious whether it will make for awkward usages later

[Shreyas Srinivas]

The seminar repository doesn't have to integrate with the rest of Mathlib. A mathlib flow library must be usable for graph flows without excess effort.

[Shreyas Srinivas]

Also my impression of mathlib is that computing is a tertiary or quaternary concern. Usability for proofs and connecting with other relevant parts of the library matters much more.

[Niklas Mohrin]

Okay, but what excess effort do you predict we will have?

[Shreyas Srinivas]

Anyway, these design decisions are upto the official reviewers and maintainers. My opinion is that Mathlib's flow library must integrate with digraphs

[Niklas Mohrin]

Just to clarify my point from earlier, for the bipartite matching example that was mentioned, I would expect the definition to be something like the following

inductive Ends where
| source
| sink

def Network.maxFlow (N : Network V ℤ) (u v : V) : ℤ := sorry

def maxCardinalityMatching {V W : Type} [Fintype V] [Fintype W] (G : SimpleGraph (V ⊕ W)) : ℤ :=
  let N : Network (V ⊕ W ⊕ Ends) ℤ := {
    cap := sorry
    nonneg := sorry
    loopless := sorry
  }
  N.maxFlow (.inr <| .inr Ends.source) (.inr <| .inr Ends.sink)

in the current version. Using Network extends DiGraph, the only change I can see is that the definition of N would change to the following (with all sorrys containing the same code as before):

let N : Network (V ⊕ W ⊕ Ends) ℤ := { G with -- <-- change here
  cap := sorry
  nonneg := sorry
  loopless := sorry
  cap_non_edge := sorry -- <-- change here
}

... or the definition would stay the same and implicitly use completeGraph V as the underlying graph.

[Niklas Mohrin]

Anyways, I agree that it must integrate with digraphs in some way and I suppose that fixing a graph with the Network extends DiGraph approach can be nice to for example keep this graph consistent between transformations of the network and to have all of the graph connectivity definitions directly available on Network. I just don't think there are many more reasons than these two

[Shreyas Srinivas]

What will change is that when writing theorems that involve graphs and their network, cap_non_edge will exist where it should.

[Shreyas Srinivas]

Indeed you do want to keep your network consistent with the graph in theorem statements by default

[Shreyas Srinivas]

I think this PR #13685 is technically sound. I haven't checked docstrings and other stuff so far. This PR introduces a new folder under Combinatorics. But I think this folder structure management is something for a future PR to handle

[Shreyas Srinivas]

Is it still the convention to require multi-line docstrings to start on a new line after the /--?

[Yaël Dillies]

It's rather the convention not to

[Yaël Dillies]

Overall, we are undecided

[Shreyas Srinivas]

Also, I read the discussion about the subset notation. In many areas that I deal with it would be most unnatural to mix up order and subset notation.

[Shreyas Srinivas]

In fact for substructure orders, we use subset notation much more than the order notation. Either way, I wonder whether your comment means there won't be a normal subset/subseteq notation from Mathlib in the future for Finsets and Sets.

[Yaël Dillies]

Yes, the plan is to scrape it off. It's somewhat challenging to the extent that we would like to keep it showing as ⊆/⊂ but have it be ≤/< underneath

[Shreyas Srinivas]

Okay, this is a big deal in math that comes from TCS like game theory stuff.

[Shreyas Srinivas]

One of the nice things about math in lean is being able to use familiar notation

[Shreyas Srinivas]

what effort is required to keep it in? Why is it being removed (probably needs a separate thread)?

[Yaël Dillies]

I mean, the plan is to keep ⊆/⊂, but make it be notation for ≤/<. Nothing should change visually

[Shreyas Srinivas]

so all the subset theorems work as is?

[Yaël Dillies]

That's the plan, at least

[Shreyas Srinivas]

As long as the user facing API doesn't change I have no worries. TCS folks are a very siloed lot. So unless someone actively works with lattices, orders, or domain theory, they are unlikely to be comfortable with them anymore than many math people will be with type theory. Having to work with Order theorems and notation will be confusing when they are working with finite sets.

[Rida Hamadani]

Shreyas Srinivas said:

Is it still the convention to require multi-line docstrings to start on a new line after the /--?

related topic: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/style.20guide.20for.20comments.3F

[Peter Nelson]

I haven't followed this whole conversation in detail - but does the solution eventually arrived at involve multigraphs?

The 'merge edges to stop it being a multigraph' solution is really just a band-aid. Edges in flow problems can be combinatorially significant (for example, two paralllel edges could correspond to different roads) and there are natural variants of flow problems that will be impossible to state if only single edges are allowed between a given pair.

[Shreyas Srinivas]

I think for describing max flow and min cut, this API is sufficient. Multigraphs become relevant in min cost flow like problems. My opinion is that this current API should be kept as is, for the same reason we treat Simplegraphs separatelyz rather than a special digraph

[Shreyas Srinivas]

It keeps the API uncluttered

[Peter Nelson]

Uncluttered, but it also encourages continued development and accrual of technical debt at the wrong level of generality.

The relationship between simple and non-simple graphs is complicated, and I think what is appropriate should be carefully considered in each given setting. It's not correct to just do absolutely everything for multigraphs, but I also worry that 'do it for simple graphs, and worry about the generalization later' is setting things up for disaster.

[Shreyas Srinivas]

Imho, flow problems on a simple digraphs are a sufficiently interesting in their own right to merit a separate and simple API

[Shreyas Srinivas]

Further, in this case, the flow vertex matrix doesn't naturally generalise to multigraphs

[Shreyas Srinivas]

Which I think is the end goal for this PR and the ones to come

[Niklas Mohrin]

I already posted this on github a while back, but no one has responded to it yet, so I will pick your brains over here:

[...] One might want a network to refer to a more specialized version of Digraph, which I think is not possible in the Network extends Digraph design.

I suppose the most flexible design to have all kinds of networks carry along all kinds of graphs would be structure Network (G : Digraph V) (R : Type u_R). However, this would defeat the main purpose for the move to the Network extends Digraph design :thinking:

Any opinions?

[Shreyas Srinivas]

I don't have any opinions on this.

[Niklas Mohrin]

Some time has passed, so I want to ramp up the discussion about my PR #13685 again: I think the biggest question still is how Networks should interact with Digraphs and SimpleGraphs. I have pushed a handful of commits that each present a different formalization. The main question is whether Network should be nested under Digraph or be a parallel thing. I think that having Network extend Digraph would be unneeded for a lot of theory on flows. On the other hand, it should be easy to formulate flow theorems for special classes of networks. On the current version of my branch, I added a structure NetworkOn (G : Digraph V) extends Network V R which takes some digraph as a parameter for the type.

We could also dismiss any connection to graphs for now and just add the plain Network. This would suffice to get started with flows in mathlib. What do you all think?