Incomplete work

Stream: PR reviews

[Aleksandar Milchev]

Hey! I have tried to implement the max-flow min-cut theorem in my branch in mathlib, but my work is incomplete. There are a few lemmas in the no_augm_path lemma which need to be proven. However, I am not sure if I will be able to resolve them soon, but I still want to contribute to mathlib. My code can be found also in my repository. Should I create a pull request and ask for a review or I should wait until advised so? Thank you!

[Alex J. Best]

Are there parts which can be naturally split out into separate PRs that are already complete? (as you have quite a number of lines unless it shrinks significantly during review I'd think that several PRs would be a natural way to get this included, rather than one big one that is hard to review, e.g. PR some defs and basic lemmas first, then some intermediate lemmas, then the big result separately at the end)
How hard do you think the remaining parts are?

You could always open a draft PR just so its a bit easier for people to look at your code and comment on it.

One of the first obvious things about your work is that you have many very long proofs, mathlib would almost definitely want those breaking down into sublemmas a bit more.
Also you should check out https://leanprover-community.github.io/contribute/style.html as a first step, and run the linters (style and code) on your work if you haven't already.
Getting code into mathlib state definitely does require quite a bit of work still.

[Alex J. Best]

Also worth mentioning that the transition from mathlib3 to mathlib4 is fast approaching, so unless this goes very quickly it's likely that at some point porting your work to mathlib4 (hopefully mostly automated) and PRing it there will be the way to go

[Aleksandar Milchev]

Alex J. Best said:

Are there parts which can be naturally split out into separate PRs that are already complete? (as you have quite a number of lines unless it shrinks significantly during review I'd think that several PRs would be a natural way to get this included, rather than one big one that is hard to review, e.g. PR some defs and basic lemmas first, then some intermediate lemmas, then the big result separately at the end)
How hard do you think the remaining parts are?

You could always open a draft PR just so its a bit easier for people to look at your code and comment on it.

One of the first obvious things about your work is that you have many very long proofs, mathlib would almost definitely want those breaking down into sublemmas a bit more.
Also you should check out https://leanprover-community.github.io/contribute/style.html as a first step, and run the linters (style and code) on your work if you haven't already.
Getting code into mathlib state definitely does require quite a bit of work still.

Thank you very much for your response. The weak duality of the theorem, i.e. the value of every flow is less than or equal to the capacity of every cut, can be separated as its proof of correctness is completed.
Also, the lint style says 'Error: ERR_TAC: Files in mathlib cannot import the whole tactic folder, nor tactic.omega or tactic.observe', saying several times 'Warning: WRN_BRC: Probable misformatting of curly braces' and then exits with code 123, I am not sure why.
In terms of style, I have followed the documentation guidance, so the style of the code should be okay.
As for mathlib4, this repository is based on my work, so once I complete my proof, the transition will be done soon.

[Alex J. Best]

I think exit code 123 just means the linter failed on some file (as we use xargs to pass the list of files). So its due to the "cannot import tactic". which is basically a rule that you shouldn't import tactic itself, but instead only the tactics you need (of course you will likely want to import tactic while working on a file but remove them before the file is added to mathlib).
As for the curly braces I'd recommend looking at a few files in mathlib to get a feel for the way we lay things out, apologies if worrying about braces seems a bit excessive but mathlib tries to stick to a very consistent style.
It looks like

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

are sufficient imports for your file

[Anne Baanen]

Or better yet:

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

:smile:

[Aleksandar Milchev]

Alex J. Best said:

I think exit code 123 just means the linter failed on some file (as we use xargs to pass the list of files). So its due to the "cannot import tactic". which is basically a rule that you shouldn't import tactic itself, but instead only the tactics you need (of course you will likely want to import tactic while working on a file but remove them before the file is added to mathlib).
As for the curly braces I'd recommend looking at a few files in mathlib to get a feel for the way we lay things out, apologies if worrying about braces seems a bit excessive but mathlib tries to stick to a very consistent style.
It looks like

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

are sufficient imports for your file

Thank you both for your replies! I changed that and reformated the brackets a little bit (I think following the format in other documents as well), but lint still exits with the same exit code, this time without displaying the error for the tactics import. It just says 'Warning: WRN_BRC: Probable misformatting of curly braces' like 10 times and then exits. I have no idea how to fix that.

[Eric Wieser]

If you create a PR, then it will leave a comment on each line where the braces are offensive

[Aleksandar Milchev]

Eric Wieser said:

If you create a PR, then it will leave a comment on each line where the braces are offensive

Thank you, I will do that. Should I make a PR for the whole code or just the proof of the weak duality as the code for the latter is complete?

[Eric Wieser]

One option is to do both, and mark the incomplete one as depending on the other one, and with the WIP label

[Scott Morrison]

Many small PRs is best. Reviewing happens fastest if each individual PR is easy. Ideally each PR will only modify/create one file (perhaps excepting adding a handful of lemmas to an earlier file). No file should ever have more than 1000 lines (just split as needed).

My preference (this is far from a rule, however), is that every declaration is either: at most ~10 lines long, or, is copiously commented explaining the entire structure of the proof in natural language as interspersed comments.

[Scott Morrison]

My first concern looking at your branch is that your theorem is about

structure strange_digraph (V : Type*) [inst : fintype V]  :=
  (is_edge : V → V → Prop)
  (hnonsymmetric : ∀ u v : V, ¬ ((is_edge u v) ∧ (is_edge v u)))

rather than about standard notions. Usual presentations of the max-cut-min-flow theorem don't need to say this "non-symmetric" condition, so I would hope a formalisation doesn't either.

(Aside: since [fintype V] is not needed to define this structure, it should probably be deferred. There is an "unused arguments" linter that will complain about this.)

I know that the combinatorics library in mathlib3 is a bit lacking, and we don't have directed graphs per se. One possibility would be to use quiver with hom := nnreal.

[Scott Morrison]

Finally, I see that your imports are all already ported to mathlib4. Given you already have a mathlib4 port written, could I suggest that you concentrate on PRing that directly? I'm not sure there's anything to gain by putting this into mathlib3 first.

[Aleksandar Milchev]

Eric Wieser said:

One option is to do both, and mark the incomplete one as depending on the other one, and with the WIP label

Done, thank you! I created a new branch called max_flow_min_cut_wip and made a PR from it with the work still in progress. The numbers of the two PRs are #18996 and #18998.