max-flow min-cut help

Stream: graph theory

[Aleksandar Milchev]

Hey, I am trying to implement the max-flow min-cut theorem in my branch in mathlib https://github.com/leanprover-community/mathlib/blob/max_flow_min_cut/src/combinatorics/quiver/max_flow_min_cut.lean, but I need some help.
In the lemmas flow_value_global_ver and weak_duality there are commands, which I believe should work, but they don't. The commands, which I am talking about are all commented out after a sorry or give a direct error (like lines 374 and 468). All of the commented-out code in these two lemmas apart from lines 392 and 394, where I am still struggling to sum over pairs, I believe should be very close to what is needed to make the code work. Unfortunately, I don't know how to fix these errors (mentioning meta-variables, asking for types and not recognising finset.sum_le_sum), so I would be very grateful if you can help me. If necessary, I can show the error messages on different pieces of code.
Last, but not least, there is a strange error on line 1022 because of an up arrow arriving in front of a real number. Everything else is the same, but because of the arrow the code doesn't work and I don't even know why it is arriving (I haven't used it anywhere). This really should be a minor mistake, but I don't have a clue how to fix it.
Any help will be appreciated! The only lemma, which is logically not ready is no_augm_path, I am currently working on it, but I believe the others should be made to work easily by people proficient in working with Lean. I am open to any other advice as well! Thank you in advance for the help!

[Shreyas Srinivas]

Hi @Aleksandar Milchev : I am working on lean4 version of your proof. This is still a WIP. See this repository : https://gitlab.com/Shreyas941/maxflowmincutlean4

I am trying to following the same structure as yours with some convenient defintion changes and I was able to golf down many of your proofs. Thus far I have reached the theorem you call set_flow_conservation.

[Shreyas Srinivas]

For good measure I started with basic lemmas to get a grip on Finsets, hence the first hundred or so lines are about the degree sum result for digraphs. But as you go down further, to set_flow_conservation,(roughly around line 200), the proofs seem significantly shorter.

[Mathieu Guay-Paquet]

@Aleksandar Milchev
One general comment is that several times you have the pattern

have ... : ... := by {exact some_term},

But you can shorten it to just:

have ... : ... := some_term,

The tactic have expects a term after :=, and by {...}is a way to construct a term using tactics, and exact ... is the tactic which supplies a term directly. So you can skip the by {...} and exact ..., and just give the term directly.

This saves you some typing, but also sometimes works better. For example, on line 374, this gives me an error:

have union: {s} ∪ {t} = {s,t} := by {exact set.singleton_union},  -- error

The error makes me think that Lean is unable to infer some implicit argument of set.singleton_union, possibly because of the interaction with by {...} and exact .... And indeed, if I use @ notation and give the arguments explicitly, the proof works:

have union: {s} ∪ {t} = {s,t} := by {exact @set.singleton_union V s {t}},  -- ok

But Lean is able to infer all the implicit arguments if you give the term directly:

have union: {s} ∪ {t} = {s,t} := set.singleton_union, -- ok

[Shreyas Srinivas]

Also, I am not quite sure why you have a separate structure for Cut. This adds a few extra steps and theorems.

[Mathieu Guay-Paquet]

For line 343, I think I see some of your confusion between set and finset. The current line is an error:

-- "meta" errors occur, how is finset handled?
have hS: {s} ⊆ S := by {exact (set.singleton_subset_iff).2 sInS},

(Incidentally, on my computer the main error I get is invalid type ascription, and the error about meta is later in the list of errors.)
But in this context, S is a finset V rather than a set V. Thankfully, the finset type has a similar lemma to the set type, and this works:

have hS: {s} ⊆ S := by {exact (finset.singleton_subset_iff).2 sInS},

[Mathieu Guay-Paquet]

I think possibly for several of your proofs, you could get through the set versus finset difficulties by looking at the section on finset-to-set coercion. In particular, the lemma finset.mem_coe says that the elements of a finset (on the right-hand side) are the same as the elements of the underlying not-necessarily-finite set (on the left-hand side).

[Mathieu Guay-Paquet]

Also, possibly part of the confusion is that for literal set notation, like {a} and {a, b}, the notation works to specify a set, or a finset, or any type which implements has_singleton and has_insert (I think). Unless you specify it somehow, Lean will guess whether you mean set or finset, and it will look fine, until you come to use it, if it turns out that you wanted the other one.

[Mathieu Guay-Paquet]

Similarly, the ∈ notation "works" for set and for finset, but means something different, and you have to be careful which one you want.

[Shreyas Srinivas]

About this:

/- The next two equalities use sum over two elements, so I am not sure how to resolve them. -/
  have sum1: mk_out afn.f {s} + mk_out afn.f (S \ {s})  = mk_out afn.f S :=
  by sorry, -- {unfold mk_out, rw finset.sum_sdiff hS},
  have sum2: mk_in afn.f (S \ {s}) + mk_in afn.f {s} = mk_in afn.f S :=
  by sorry, -- {unfold mk_in, rw finset.sum_sdiff hS},

You can't prove them because they are not true. mk_out afn.f {s} counts the flow on those edges which leave {s} into the rest of the graph, including S \ {s}. The flow of these internal edges don't get counted in mk_out afn.f S. Same problem with sum2. For context for other readers here's the definition of mk_out:

noncomputable
def mk_out {V : Type* } [inst : fintype V]
  (f : V -> V -> ℝ) (s : finset V) : ℝ := ∑ x in s, ∑ y in finset.univ \ s, f x y

I am writing this at 1:45 am in the morning, so I apologise if I am missing something.

[Aleksandar Milchev]

Shreyas Srinivas said:

About this:

/- The next two equalities use sum over two elements, so I am not sure how to resolve them. -/
  have sum1: mk_out afn.f {s} + mk_out afn.f (S \ {s})  = mk_out afn.f S :=
  by sorry, -- {unfold mk_out, rw finset.sum_sdiff hS},
  have sum2: mk_in afn.f (S \ {s}) + mk_in afn.f {s} = mk_in afn.f S :=
  by sorry, -- {unfold mk_in, rw finset.sum_sdiff hS},

You can't prove them because they are not true. mk_out afn.f {s} counts the flow on those edges which leave {s} into the rest of the graph, including S \ {s}. The flow of these internal edges don't get counted in mk_out afn.f S. Same problem with sum2. For context for other readers here's the definition of mk_out:

noncomputable
def mk_out {V : Type* } [inst : fintype V]
  (f : V -> V -> ℝ) (s : finset V) : ℝ := ∑ x in s, ∑ y in finset.univ \ s, f x y

I am writing this at 1:45 am in the morning, so I apologise if I am missing something.

Thank you for that, I found that out myself, and I proved the correct one yesterday. I was missing ∑ x in {s}, ∑ y in S \ {s}, (f x y + f y x).

[Aleksandar Milchev]

Shreyas Srinivas said:

Hi Aleksandar Milchev : I am working on lean4 version of your proof. This is still a WIP. See this repository : https://gitlab.com/Shreyas941/maxflowmincutlean4

I am trying to following the same structure as yours with some convenient defintion changes and I was able to golf down many of your proofs. Thus far I have reached the theorem you call set_flow_conservation.

Thank you very much for sending that over! Maybe we can work together on proving the rest of the theorem, I am currently stuck on aug_path. I believe that my other errors shouldn't be too hard to fix. I will follow your progress on that, I have my own repo, which usually has the most updated code.

[Shreyas Srinivas]

Aleksandar Milchev said:

Shreyas Srinivas said:

Hi Aleksandar Milchev : I am working on lean4 version of your proof. This is still a WIP. See this repository : https://gitlab.com/Shreyas941/maxflowmincutlean4

I am trying to following the same structure as yours with some convenient defintion changes and I was able to golf down many of your proofs. Thus far I have reached the theorem you call set_flow_conservation.

Thank you very much for sending that over! Maybe we can work together on proving the rest of the theorem, I am currently stuck on aug_path. I believe that my other errors shouldn't be too hard to fix. I will follow your progress on that, I have my own repo, which usually has the most updated code.

This sounds good to me. We can work on this. A quick observation : many of the intermediate steps you are using in the (net cut flow = net source flow) theorem seem to be useful otherwise. Basically these are flow versions of various finset properties about partitioning and combining and rearranging sums. It might be useful to have them as separate lemmas.

[Aleksandar Milchev]

Shreyas Srinivas said:

Aleksandar Milchev said:

Shreyas Srinivas said:

Hi Aleksandar Milchev : I am working on lean4 version of your proof. This is still a WIP. See this repository : https://gitlab.com/Shreyas941/maxflowmincutlean4

I am trying to following the same structure as yours with some convenient defintion changes and I was able to golf down many of your proofs. Thus far I have reached the theorem you call set_flow_conservation.

Thank you very much for sending that over! Maybe we can work together on proving the rest of the theorem, I am currently stuck on aug_path. I believe that my other errors shouldn't be too hard to fix. I will follow your progress on that, I have my own repo, which usually has the most updated code.

This sounds good to me. We can work on this. A quick observation : many of the intermediate steps you are using in the (net cut flow = net source flow) theorem seem to be useful otherwise. Basically these are flow versions of various finset properties about partitioning and combining and rearranging sums. It might be useful to have them as separate lemmas.

Nice! As for the intermediate sums, I see what you mean. I will consider which one can be used later and probably put them in separate lemmas.

[Shreyas Srinivas]

Aleksandar Milchev said:

Nice! As for the intermediate sums, I see what you mean. I will consider which one can be used later and probably put them in separate lemmas.

Flows are very basic in theoretical CS. Many graph problems can be treated as flow problems in disguise. So being able to perform basic reasoning about flows is a crucial building block for many algorithmic verification tasks.

[Shreyas Srinivas]

For example, being able to split the flows from S to V \ S, into S to T and V\S\T (for T \subset V \ S) is a trivial but frequent stepping stone for many algorithmic solutions. I am working on my side on some of these theorems. I'll see how far I get by tomorrow night.

[Aleksandar Milchev]

Mathieu Guay-Paquet said:

Aleksandar Milchev
One general comment is that several times you have the pattern

have ... : ... := by {exact some_term},

But you can shorten it to just:

have ... : ... := some_term,

The tactic have expects a term after :=, and by {...}is a way to construct a term using tactics, and exact ... is the tactic which supplies a term directly. So you can skip the by {...} and exact ..., and just give the term directly.

This saves you some typing, but also sometimes works better. For example, on line 374, this gives me an error:

have union: {s} ∪ {t} = {s,t} := by {exact set.singleton_union},  -- error

The error makes me think that Lean is unable to infer some implicit argument of set.singleton_union, possibly because of the interaction with by {...} and exact .... And indeed, if I use @ notation and give the arguments explicitly, the proof works:

have union: {s} ∪ {t} = {s,t} := by {exact @set.singleton_union V s {t}},  -- ok

But Lean is able to infer all the implicit arguments if you give the term directly:

have union: {s} ∪ {t} = {s,t} := set.singleton_union, -- ok

Mathieu Guay-Paquet said:

For line 343, I think I see some of your confusion between set and finset. The current line is an error:

-- "meta" errors occur, how is finset handled?
have hS: {s} ⊆ S := by {exact (set.singleton_subset_iff).2 sInS},

(Incidentally, on my computer the main error I get is invalid type ascription, and the error about meta is later in the list of errors.)
But in this context, S is a finset V rather than a set V. Thankfully, the finset type has a similar lemma to the set type, and this works:

have hS: {s} ⊆ S := by {exact (finset.singleton_subset_iff).2 sInS},

Thank you very much! Both of your comments were very very useful! I managed to implement everything apart from proving {s} ∪ {t} = {s,t}. I have to use finset.cons, and I can't prove that finset.cons t {s} h = {s,t}. Also, when I write {t}.disj_union {s} h it gives me the error message:

invalid field notation, type is not of the form (C ...) where C is a constant
{t}
has type
?m_1

Otherwise, if I just use set.singleton_union, I get a typo error on line 515 because it treats {s,t} as a set, instead of finset.
Do you have any ideas about what should I do? Thank you in advance!

[Shreyas Srinivas]

have you tried to_finset?

[Shreyas Srinivas]

In mathlib4 there is a Set.toFinset. Following naming conventions there should be something like set.to_finset in mathlib

[Kevin Buzzard]

I managed to implement everything apart from proving {s} ∪ {t} = {s,t}.

The best way to ask a question on this site is to make a #mwe . So, in your file, make a new lemma stating precisely what you want, sorry the proof, and check that you can apply the lemma in your example to solve your problem. Then make a new file containing only that lemma, make sure it compiles, and post the fully working code and ask for help. This is a really efficient way to get a solution.

[Yaël Dillies]

That specific equality should be refl.

[Aleksandar Milchev]

Yaël Dillies said:

That specific equality should be refl.

I just tried it, and it gives the error message:

invalid apply tactic, failed to unify
{s} ∪ {t} = {s, t}
with
?m_8 = ?m_8

[Kevin Buzzard]

Then post the #mwe and we'll debug from there.

[Yakov Pechersky]

ext; simp will also do it

[Aleksandar Milchev]

Kevin Buzzard said:

Then post the #mwe and we'll debug from there.

It should be:

import data.finset.basic

universe u

variable (V : Type u)

open finset

lemma union : ∀ (s t : V), {s} ∪ {t} = {s,t} := by sorry,

However, I get an error message saying: 'don't know how to synthesize placeholder context' and don't know why. I tried to fix it, but I can't, apologies for that.

[Alex J. Best]

import data.finset.basic

universe u

variable (V : Type u)

open finset
.
open_locale classical
lemma union : ∀ (s t : V), ({s} : finset V) ∪ {t} = {s,t} := by sorry

[Alex J. Best]

Indeed refl works here, how are you dealing with decidability in your original problem?
Do you have open locale classical or some explicit decidability hypotheses?

[Aleksandar Milchev]

Alex J. Best said:

import data.finset.basic

universe u

variable (V : Type u)

open finset
.
open_locale classical
lemma union : ∀ (s t : V), ({s} : finset V) ∪ {t} = {s,t} := by sorry

Thank you very much for that, could you tell me how you put code in your message, please?
As for decidability, I have open_locale classical.

[Alex J. Best]

#backticks for the code

[Alex J. Best]

Something else must be different between your example and this one then, by intros s t; refl works here

[Alex J. Best]

Aleksandar Milchev said:

Yaël Dillies said:

That specific equality should be refl.

I just tried it, and it gives the error message:

invalid apply tactic, failed to unify
{s} ∪ {t} = {s, t}
with
?m_8 = ?m_8

what happens here with set_option pp.all true turned on (before the lemma)

[Eric Wieser]

I would guess that one side of the equality uses classical decidability and the other doesn't

[Aleksandar Milchev]

Alex J. Best said:

Aleksandar Milchev said:

Yaël Dillies said:

That specific equality should be refl.

I just tried it, and it gives the error message:

invalid apply tactic, failed to unify
{s} ∪ {t} = {s, t}
with
?m_8 = ?m_8

what happens here with set_option pp.all true turned on (before the lemma)

I managed to fix it by writing ({s} : finset V) instead of {s}. refl works now, thank you very much!

[Aleksandar Milchev]

Hello there! I am currently trying to implement the no_aug_path theorem, but I need to take the minimum flow, which can be pushed in the residual network. For that purpose, I need somehow to have all flow values in the augmenting path (the flow in the residual network between x and y is f' x y) in order to take the minimum one. I have all vertices in the residual network in a set called 'vertices', and I tried

set flows := { (rsn.f' x y) | ∀ x y :V, (x ∈ vertices ∧ y ∈ vertices ∧ exists_path.in x y) }

but I have an error saying: 'invalid binder, '(', '{', '[', '{{', '⦃' or identifier expected' when I hover on forall and then unknown identifiers for x,y, vertices and exists_path (defined to be an augmenting path). Can that be fixed or can you please suggest other ways I can construct a set with all flows in the augmenting path.

[Yaël Dillies]

I'm not sure what you mean your set to be, to be quite honest. You have x and y on the left of the |, then you introduce two other x and y with the forall.

[Yaël Dillies]

Am I right in thinking you didn't mean the forall to introduce new variables and your set can be written as function.uncurry rsn.f' '' {xy \in vertices \times\^s vertices | exists_path.in xy.1 xy.2}?

[Aleksandar Milchev]

Yaël Dillies said:

Am I right in thinking you didn't mean the forall to introduce new variables and your set can be written as function.uncurry rsn.f' '' {xy \in vertices \times\^s vertices | exists_path.in xy.1 xy.2}?

You are right, I don't actually want to introduce new variables with the forall (it's actually not needed).
Thank you very much for the code, it seems to work, but I am confused with '\times\^s', what does that stand for?

[Kyle Miller]

In Lean 3, you should be able to do { (rsn.f' x y) | (x y : V), (x ∈ vertices ∧ y ∈ vertices ∧ exists_path.in x y) } without the forall, if I got the syntax right.

[Kyle Miller]

It's {(expression in parentheses) | binders, condition}

[Eric Wieser]

I had no idea that there was a , condition term

[Kyle Miller]

@Eric Wieser No, unfortunately I misremembered, and I just had the opportunity to check. The way you encode this is that you add an extra binder. Simpler example:

def s (α β : Type*) (f : α → β) (p : α → Prop) : set β :=
{(f x) | (x : α) (h : p x)}

[Kyle Miller]

In principle you could have an extra , condition term, but in the current implementation it's just {(expression in parentheses) | binders}.

[Aleksandar Milchev]

Yaël Dillies said:

Am I right in thinking you didn't mean the forall to introduce new variables and your set can be written as function.uncurry rsn.f' '' {xy \in vertices \times\^s vertices | exists_path.in xy.1 xy.2}?

Thank you very much, I defined the set that way but had to use set.to_finset because I it is more convenient for the whole structure of the code and I needed that it is nonempty after. However, I have issues proving it, I am not sure how to prove that vertices are in this set. I was searching for more information in the documentation on how to use properties of sets, defined that way and the minimality of d, but couldn't find any. That is why, I need help with proving the theorems below, they shouldn't be really hard. I am currently working on proving that if the flow is maximal, there isn't an augmenting path in the residual network, so g can be treated as a function showing if (u,v) is an edge in the augmenting path (assuming one exists) and f is the flow in the residual network (always bigger than zero, that is why the lemma 'fact' can be used directly). Later on, I have two bigger problems, one is picking the edge going out of the source in the augmenting path and using it to prove that if an augmenting path exists, then a better flow can be created, and proving the flow conservation for a vertex v in the set vertices. I am feeling that I am really close to proving the theorem as these are the final issues, anything else works, but I need to resolve the small issues below first, and the two major issues later. I will be grateful if someone is keen to help me with that and at least resolves the lemmas, but please message me if you want to know more about the other two issues. My code can be found in this repository.

import data.real.basic
import data.set.basic
import tactic
import data.finset.basic
import tactic.induction
import algebra.big_operators.order

universe u

variable (V : Type u)

open finset

open_locale classical

lemma test (g : V → V → Prop) (f : V → V → ℝ) (t : V) : true :=
begin
  have fact: ∀ x y : V, f x y > 0 := by sorry, -- can be used as a fact
  set vertices := set.to_finset ({t} ∪ { x | (∃ y: V, g x y) }), --all vertices in the augmenting path
  -- set of all flow values in the augmenting path
  set flows := set.to_finset (function.uncurry f '' {xy ∈ vertices ×ˢ vertices | g xy.1 xy.2}),
  have nonemp: flows.nonempty := by sorry, -- has to be proven!
  set d := flows.min' nonemp, -- the minimum flow in the augmenting path
  have pos: 0 < d := by sorry, -- has to be proven!
  have noPath: ∀ v:V, v∉ vertices →
  (∀ u : V, ¬exists_path.in u v) ∧ (∀ w : V, ¬exists_path.in v w) := by sorry, -- has to be proven!
  have minimality: ∀ u v : V, g u v → d ≤ f u v := by sorry, -- has to be proven!
end

[Yaël Dillies]

Aren't you missing some finiteness assumption on V?

[Aleksandar Milchev]

Yaël Dillies said:

Aren't you missing some finiteness assumption on V?

Yes, I am, sorry, so the code should be:

import data.real.basic
import data.set.basic
import tactic
import data.finset.basic
import tactic.induction
import algebra.big_operators.order

universe u

variable (V : Type u)

open finset

open_locale classical

lemma test {V : Type u} [inst' : fintype V] (g : V → V → Prop) (f : V → V → ℝ) (t : V) : true :=
begin
  have fact: ∀ x y : V, f x y > 0 := by sorry, -- can be used as a fact
  set vertices := set.to_finset ({t} ∪ { x | (∃ y: V, g x y) }), --all vertices in the augmenting path
  -- set of all flow values in the augmenting path
  set flows := set.to_finset (function.uncurry f '' {xy ∈ vertices ×ˢ vertices | g xy.1 xy.2}),
  have nonemp: flows.nonempty := by sorry, -- has to be proven!
  set d := flows.min' nonemp, -- the minimum flow in the augmenting path
  have pos: 0 < d := by sorry, -- has to be proven!
  have noPath: ∀ v:V, v∉ vertices →
  (∀ u : V, ¬g u v) ∧ (∀ w : V, ¬g v w) := by sorry, -- has to be proven!
  have minimality: ∀ u v : V, g u v → d ≤ f u v := by sorry, -- has to be proven!
  sorry, -- just elliminates true
end

[Aleksandar Milchev]

Hello everyone! I am still working on the implementation of the max-flow min-cut theorem in Lean 3 and I have a good progress. Currently, I need help with the following MWE:

import data.real.basic
import data.set.basic
import tactic
import data.finset.basic
import tactic.induction
import algebra.big_operators.order

universe u

variable (V : Type u)

open finset

open_locale classical

lemma test {V : Type u} [inst' : fintype V] (p : V → V → Prop) (f : V → V → ℝ) (t : V) : true :=
begin
  have fact: ∀ x y : V, f x y > 0 := by sorry, -- can be used as a fact
  set vertices := set.to_finset ({t} ∪ { x | (∃ y: V, p x y) }), --all vertices in the augmenting path
  -- set of all flow values in the augmenting path
  set flows := set.to_finset (function.uncurry f '' {xy ∈ vertices ×ˢ vertices | p xy.1 xy.2}),

  have foo: ∀ u v : V, (u ∈ vertices ∧ v ∈ vertices) → f u v ∈ flows := by sorry, -- has to be proven!

  have nonemp: flows.nonempty := by sorry, -- can be used as a fact, can be proven directly using foo
  set d := flows.min' nonemp, -- the minimum flow in the augmenting path

  have bar: ∀ x : ℝ, x ∈ flows → x > 0 := by sorry,

  sorry, -- just elliminates true
end

I will appreciate it if someone can help me resolve the lemmas foo and bar above. Moreover, I will be really grateful if someone has a better look at my code and helps me to resolve the issues on lines 865 (another lemma with the name bar), 1031-1040 (should follow my proof, 1047 (lemma ancestor) and 1147 (just need to pick the edge (s,v) in the augmenting path. I believe that all issues apart from 1031-1040 should be resolved relatively quickly. Please let me know if someone decides to have a better look at my code and if any questions arise.

[Yaël Dillies]

Sorry, I wish I had time, but my finals are in a month!

[Aleksandar Milchev]

Yaël Dillies said:

Sorry, I wish I had time, but my finals are in a month!

Wish you good luck with that! My project deadline is the end of this week, but I believe I will continue with the implementation after because I want to finish the proof, it has been fascinating working so far.

[Alex J. Best]

I did the first one, there is some really weird behavior with cases being slow though, the second I got a bit confused by what happens if the vertices are equal, it seems path.in allows this but I'm not sure what happens to f then https://gist.github.com/alexjbest/d2adba680b8e20540874ad77b2aebb4a

[Aleksandar Milchev]

Alex J. Best said:

I did the first one, there is some really weird behavior with cases being slow though, the second I got a bit confused by what happens if the vertices are equal, it seems path.in allows this but I'm not sure what happens to f then https://gist.github.com/alexjbest/d2adba680b8e20540874ad77b2aebb4a

Hey, Alex! The first solution is working, thank you very much! As for your question, the non-symmetric property implies that there are no self-loops in the initial graph. Afterwards, the flow in the residual network is zero if there is no edge between two vertices in the initial graph, which is the case if the vertices are equal. I will have a look as well, but hope that helps!