Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - feat(combinatorics/simple_graph/connectivity): walk.to_subgraph #17325

Closed
wants to merge 9 commits into from
Closed

[Merged by Bors] - feat(combinatorics/simple_graph/connectivity): walk.to_subgraph #17325

wants to merge 9 commits into from

Conversation

kmill
Copy link
Collaborator

@kmill kmill commented Nov 3, 2022

A construction for the subgraph consisting of the vertices and edges of a given walk.

Open in Gitpod

@kmill
feat(combinatorics/simple_graph/connectivity): walk.to_subgraph
d4ea34b 
A construction for the subgraph consisting of the vertices and edges of a given walk.
@kmill kmill added awaiting-review The author would like community review of the PR t-combinatorics Combinatorics labels Nov 3, 2022
@kmill kmill requested a review from a team as a code owner November 3, 2022 16:55
@bottine
Copy link
Collaborator

bottine commented Nov 4, 2022

Maybe lemmas relating the behaviours of subgraph.of_adj and simple_graph.adj.to_walk would be appropriate?

YaelDillies
YaelDillies reviewed Nov 20, 2022
View reviewed changes
Copy link
Collaborator

@YaelDillies YaelDillies left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Sorry, I had this review waiting around for ages.

src/combinatorics/simple_graph/connectivity.lean Outdated Show resolved Hide resolved
src/combinatorics/simple_graph/connectivity.lean Outdated Show resolved Hide resolved
@kmill
Copy link
Collaborator Author

kmill commented Dec 21, 2022

@YaelDillies Thanks, I somehow missed your review!

YaelDillies
YaelDillies reviewed Dec 25, 2022
View reviewed changes
Copy link
Collaborator

@YaelDillies YaelDillies left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

A few more simp suggestions.

src/combinatorics/simple_graph/connectivity.lean Outdated Show resolved Hide resolved
src/combinatorics/simple_graph/connectivity.lean Outdated Show resolved Hide resolved
src/combinatorics/simple_graph/connectivity.lean Outdated Show resolved Hide resolved
src/combinatorics/simple_graph/connectivity.lean Outdated Show resolved Hide resolved
src/combinatorics/simple_graph/connectivity.lean Outdated Show resolved Hide resolved
src/combinatorics/simple_graph/connectivity.lean Outdated Show resolved Hide resolved
YaelDillies
YaelDillies approved these changes Jan 7, 2023
View reviewed changes
Copy link
Collaborator

@YaelDillies YaelDillies left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Hopefully final comments!

src/combinatorics/simple_graph/subgraph.lean

@[simp] lemma verts_inf {H H' : G.subgraph} : (H ⊓ H').verts = H.verts ∩ H'.verts := rfl

lemma neighbor_set_sup {H H' : G.subgraph} (v : V) :
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
lemma neighbor_set_sup {H H' : G.subgraph} (v : V) :
@[simp] lemma neighbor_set_sup {H H' : G.subgraph} (v : V) :

src/combinatorics/simple_graph/subgraph.lean
(H ⊔ H').neighbor_set v = H.neighbor_set v ∪ H'.neighbor_set v :=
by { ext w, simp }

lemma neighbor_set_inf {H H' : G.subgraph} (v : V) :
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
lemma neighbor_set_inf {H H' : G.subgraph} (v : V) :
@[simp] lemma neighbor_set_inf {H H' : G.subgraph} (v : V) :

src/combinatorics/simple_graph/subgraph.lean
@@ -386,6 +398,23 @@ begin
exact ⟨_, _, h.2 ha, rfl, rfl⟩ }
end

lemma map_sup {G : simple_graph V} {G' : simple_graph W} (f : G →g G')
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
lemma map_sup {G : simple_graph V} {G' : simple_graph W} (f : G →g G')
@[simp] lemma map_sup {G : simple_graph V} {G' : simple_graph W} (f : G →g G')

@kmill
Copy link
Collaborator Author

kmill commented Jan 7, 2023

@YaelDillies I worry about having "non-affine" simp lemmas and usually try to avoid them. By an "affine" lemma I mean that each variable in the RHS appears at most as many times as in the LHS. Non-affine simp lemmas can have exponential term growth.

I'm not inclined to include these homomorphism-pushing lemmas as simp lemmas, but I'm sort of ambivalent. If you feel like we should definitely have these as simp lemmas before merging this PR, then I'll defer to you here. We can also decide to make these be simp lemmas later once we have applications of them. (Maybe @b-mehta has any thoughts?)

@YaelDillies
Copy link
Collaborator

I would tag these as simp by virtue of them being distributivity lemmas, for example filter.map_sup.

I don't think we need them to be simp before merging, but it's not very principled to make simp only half the distributivity lemmas you introduce (you are making verts_inf simp).

@kmill
Copy link
Collaborator Author

kmill commented Jan 7, 2023

verts_inf is affine, which is why I was fine with it. Really I only wanted verts_sup to be simp so that you could get confluence for verts of a path as a subgraph (vs taking support directly).

@YaelDillies
Copy link
Collaborator

I see what you mean, but I don't really buy it. Those lemmas are fine so long as we globally agree on a direction of pushing. At any rate, this is a minor issue.

maintainer merge

@github-actions
Copy link

github-actions bot commented Jan 7, 2023

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

@jcommelin
Copy link
Member

Thanks 🎉

bors merge

@github-actions github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Jan 7, 2023
bors bot pushed a commit that referenced this pull request Jan 7, 2023
@kmill
feat(combinatorics/simple_graph/connectivity): walk.to_subgraph (#1…
d6e84a0 
…7325)

A construction for the subgraph consisting of the vertices and edges of a given walk.
@bors
Copy link

bors bot commented Jan 7, 2023

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(combinatorics/simple_graph/connectivity): walk.to_subgraph [Merged by Bors] - feat(combinatorics/simple_graph/connectivity): walk.to_subgraph Jan 7, 2023
@bors bors bot closed this Jan 7, 2023
@bors bors bot deleted the kmill_walk_to_subgraph branch January 7, 2023 13:53
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@bottine bottine bottine approved these changes

@YaelDillies YaelDillies YaelDillies approved these changes

@b-mehta b-mehta Awaiting requested review from b-mehta

Assignees
No one assigned
Labels
ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) t-combinatorics Combinatorics
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
4 participants
@kmill @bottine @YaelDillies @jcommelin