[Merged by Bors] - feat(combinatorics/simple_graph): degree lemmas #5966
Conversation
b-mehta
added
the
awaiting-review
| def min_degree (G : simple_graph V) [nonempty V] [decidable_rel G.adj] : ℕ := | ||
| finset.min' (univ.image (λ (v : V), G.degree v)) (nonempty.image univ_nonempty _) | ||
| def min_degree [decidable_rel G.adj] : ℕ := | ||
| option.get_or_else (univ.image (λ v, G.degree v)).min 0 |
There was a problem hiding this comment.
What's the advantage of this definition over min'? The lemmas below look like they should all be obvious statements about min' whose lemmas belong in the finset API.
There was a problem hiding this comment.
Those statements about min' are already in the finset API, except with additional assumptions. The advantage of this definition is that it doesn't require V to be nonempty - following the usual mathlib pattern of definitions having minimal assumptions, and having assumptions on the lemmas.
There was a problem hiding this comment.
Ah, I missed the removal of nonempty V. My point still stands though - none of your proofs are anything to do with graphs, and are essentially just stating properties of a general finset.min_or_zero function:
[nonempty V] → ∃ v, f v = min_or_zero f∀ v, min_or_zero f ≤ f v[nonempty V] → ∀ k, (∀ v, k ≤ f v) → k ≤ min_or_zero f
I'd be tempted to either:
- Add an API like this to finset
- Work out why no one has needed this API yet, and use what the other code is already using.
This comment was marked as outdated.
This comment was marked as outdated.
Sorry, something went wrong.
There was a problem hiding this comment.
They're stating properties of your hypothetical finset.min_or_zero function, which applies to finsets and functions on them to the naturals - that is, it's just a composition of finset.image, finset.min and option.get_or_else. Are you suggesting we make an API for this particular composition rather than using the existing APIs for each of those?
There was a problem hiding this comment.
I don't think I understand your point here - what's special about this particular composition of three existing functions that means it deserves a special API? That is, we already have good APIs for the three individual functions, which is why there has been no need to make a special one for this combination - has something changed?
There was a problem hiding this comment.
I guess my objection comes in two parts:
- I'm not convinced the
0default is actually a helpful API. An alternative would be to usewith_top ℕ- the proofs in this PR remain essentially the same after adding twowith_top.coe_le_coe.mprs. - If you did use
with_top ℕ, you could redefinemin_degreeasuniv.inf (λ v, G.degree v), and then most of the proofs in this PR are actually missing API aboutinfonlinear_order, which would be great to have directly on finset.
There was a problem hiding this comment.
Since this takes a hypothesis of [fintype V], my gut reaction is that with_top nat doesn't feel right.
I think the new defs added here should include "finite" where appropriate, and we may need to add them to older doc strings in this file as well (in a followup PR?).
There was a problem hiding this comment.
The idea behind with_top was just to give the minimum of an empty set a well-behaved meaning - not to represent vertices of infinite degree.
I've added the missing inf lemma on linear_order in #6103.
There was a problem hiding this comment.
My reason for avoiding with_top nat is because in practice proving things in graph theory, it's much more helpful to return 0 than change the return type - again, this is the usual mathlib pattern, see eg real.sqrt.
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
| The maximum degree of all vertices (and `0` if there are no vertices). | ||
| -/ | ||
| def max_degree [decidable_rel G.adj] : ℕ := | ||
| option.get_or_else (univ.image (λ v, G.degree v)).max 0 |
There was a problem hiding this comment.
Had you given any thought to using finset.sup?
def max_degree [decidable_rel G.adj] : ℕ :=
univ.sup (λ v, G.degree v)It doesn't seem to be as well-developed for getting an existential out of it, but I thought I'd ask.
There was a problem hiding this comment.
I made a PR that adds that existential, #6103 (exists_mem_eq_inf)
Note that sup needs with_top N, but you could cast back down to N after applying sup.
There was a problem hiding this comment.
Had you given any thought to using
finset.sup?def max_degree [decidable_rel G.adj] : ℕ := univ.sup (λ v, G.degree v)It doesn't seem to be as well-developed for getting an existential out of it, but I thought I'd ask.
Yeah - my original version of this used finset.sup and inf, but it's just more awkward to prove things in practice that way, which is why I went with this approach!
There was a problem hiding this comment.
You seem to have proved all the lemmas that completely define min_degree and max_degree (at least for nonempty V) so I'm happy with however they're implemented. It might be worth mentioning in the docstrings the names of the lemmas (I think it's three lemmas each) that define them, so people aren't tempted to unfold the definitions.
There was a problem hiding this comment.
That's a good point, thanks!
There was a problem hiding this comment.
I had a go at defining this using sup, but there're some currently-broken typeclass instances that conflict: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/complete_lattice.20%28with_top.20.E2.84.95%29/near/226163944. The definition I tried was:
def max_degree [decidable_rel G.adj] : ℕ :=
option.get_or_else (univ.sup (λ v, foo v) : with_top ℕ) 0
|
I've switched this back to |
semorrison
added
awaiting-author
b-mehta
removed
the
awaiting-author
b-mehta
added
the
awaiting-review
|
✌️ b-mehta can now approve this pull request. To approve and merge a pull request, simply reply with |
bryangingechen
added
the
delegated
|
If Kyle's happy with this then I am too. bors r+ |
Proves some lemmas about the minimum/maximum degree of vertices in a graph - also weakens the assumptions for the definitions, following the usual mathlib pattern of defining total functions.
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
Proves some lemmas about the minimum/maximum degree of vertices in a graph - also weakens the assumptions for the definitions, following the usual mathlib pattern of defining total functions.
YaelDillies
removed
the
awaiting-review
Proves some lemmas about the minimum/maximum degree of vertices in a graph - also weakens the assumptions for the definitions, following the usual mathlib pattern of defining total functions.