[Merged by Bors] - feat(combinatorics/simple_graph/connectivity): add functions to split walks and to create paths #11095
Conversation
|
I see many repeated blocks of tactics across different proofs (usually after |
| end | ||
|
|
||
| lemma support_take_until_subset {u v w : V} (p : G.walk v w) (h : u ∈ p.support) : | ||
| (p.take_until u h).support ⊆ p.support := |
There was a problem hiding this comment.
Do we have notions of sub-walk? Should we? (It's entirely possible the answer is no!)
There was a problem hiding this comment.
Not yet, and I don't immediately have any plans for them.
The closest we have at the moment is that we can give an explicit append expression: (p.take_until u h).append (p.drop_until u h) = p
| namespace walk | ||
| variables {G} [decidable_eq V] | ||
|
|
||
| /-- Given a walk, produces a walk with the same endpoints and no repeated vertices. -/ |
There was a problem hiding this comment.
It would be nice here to say that the new walk is a path, and that this is shown below. I can imagine cases where I want to "de-dup" a walk and carry around the property, rather than work in the subtype; perhaps that means this has a better name?
There was a problem hiding this comment.
I changed it to bypass since it creates a walk that bypasses the subwalks between duplicate vertices. Maybe that's a reasonable name?
jcommelin
added
awaiting-author
kmill
changed the title
kmill
added
awaiting-review
There was a problem hiding this comment.
This looks reasonable to me, but hopefully someone more familiar with the graph theory library can confirm (@b-mehta ?)!
|
Sorry for not checking this sooner! LGTM bors merge |
… walks and to create paths (#11095) This is chunk 3 of #8737. Introduces `take_until` and `drop_until` to split walks at a vertex, `rotate` to rotate cycles, and `to_path` to remove internal redundancy from a walk to create a path with the same endpoints. This also defines a bundled `path` type for `is_path` since `G.path u v` is a useful type.
github-actions
bot
added
ready-to-merge
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
This is chunk 3 of #8737. Introduces
take_untilanddrop_untilto split walks at a vertex,rotateto rotate cycles, andto_pathto remove internal redundancy from a walk to create a path with the same endpoints.This also defines a bundled
pathtype foris_pathsinceG.path u vis a useful type.