[Merged by Bors] - feat(Combinatorics/SimpleGraph/Walk): add `penultimate` and `snd` by Command-Master · Pull Request #16769 · leanprover-community/mathlib4

Command-Master · 2024-09-13T14:40:09Z

Here are some reasons for it:

We want to add penultimate, as p.getVert (p.length - 1) duplicates p, and snd should exist for symmetry.
In some cases it makes sense to consider the vertices of a walk without the first/last one, and then this is the walk version of List.head/List.last, not l[1]/l[l.size-2]
In walks the first/last node and adjacency are a lot more important than they usually are in lists, so it makes more sense to have a special term for the node adjacent to the first/last node.
Walks always have a sensible default, so there's no need for the "take a proof/default value/panic/return an option" duplication which lists have and so this doesn't require much API.

github-actions · 2024-09-13T14:40:55Z

PR summary bd757c1549

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ adj_penultimate
+ adj_snd
+ edge_lastDart
+ getVert_nil
+ lastDart
+ penultimate
+ penultimate_concat
+ penultimate_cons_cons
+ penultimate_cons_nil
+ penultimate_cons_of_not_nil
+ snd
+ snd_cons
+ tail_nil
- adj_getVert_one
- getVert_cons_one

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

pimotte

There's still a getVert 1 in WalkCounting.lean, other than that, looks good to me:)

YaelDillies

List.snd doesn' exist. How do you justify Walk.snd?

Command-Master · 2024-11-02T16:53:02Z

Here are a few reasons for it:

I want to add penultimate, as p.getVert (p.length - 1) duplicates p, so snd should exist for symmetry.
In some cases it makes sense to consider the vertices of a walk without the first one, and then this is the walk version of List.head, not l[1]
In walks the first node and adjacency are a lot more important than they usually are in lists, so it makes more sense to have a special term for the node adjacent to the first node.
Walks always have a sensible default, so there's no need for the "take a proof/default value/panic/return an option" duplication which lists have and this doesn't require much API.

YaelDillies

Okay great! Can you make this comment be your PR description?

maintainer delegate

Command-Master · 2024-11-10T10:34:28Z

Updated

Command-Master · 2024-11-10T14:04:21Z

maintainer merge

Command-Master · 2024-11-10T14:05:57Z

@YaelDillies it doesn't seem to be active yet - could you maintainer merge please?

YaelDillies · 2024-11-10T14:56:35Z

Hmm, interesting

maintainer merge

github-actions · 2024-11-10T14:56:53Z

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

kim-em · 2024-11-29T01:15:05Z

To be honest I remain a little skeptical even about adding this level of synonyms.

It seems the simplifications that are achieved in this PR come from dropping some unused proof obligations, which it seems could be done separately without introducing snd and penultimate.

Another suggestion would be to set up a GetElem instance, and write w[1] instead of w.getVert 1.

(One might even experiment with adding a GetElem instance that takes an Int, and then one could write w[-1] instead of penultimate. I wonder if anyone has already experimented with this for List/Array...)

Command-Master · 2024-11-29T03:26:31Z

The simplifications here aren't the point — my main reason for this is use in #16382 and further work I haven't PRd yet. A GetElem with an int could work, but I don't think it would be good — I feel like it would just force many lemmas to take positivity conditions

b-mehta · 2024-12-15T18:25:44Z

I think these look somewhat reasonable - snd and penultimate are natural operations, and have more of a reason to exist for walks than they do for list. But I'd still like more detail on what these will be used for - it looks like #16382 doesn't have much of a mathematical justification for these. Can you say more about what your application of the new declarations is?

Command-Master · 2024-12-19T05:24:22Z

I think these look somewhat reasonable - snd and penultimate are natural operations, and have more of a reason to exist for walks than they do for list. But I'd still like more detail on what these will be used for - it looks like #16382 doesn't have much of a mathematical justification for these. Can you say more about what your application of the new declarations is?

I use it to root a SimpleGraph.IsTree and get a Tree - the penultimate vertex of the path from the root gives the parent, in this case

b-mehta · 2025-01-06T14:48:21Z

Thanks!

bors merge

…6769) Here are some reasons for it: - We want to add `penultimate`, as `p.getVert (p.length - 1)` duplicates `p`, and `snd` should exist for symmetry. - In some cases it makes sense to consider the vertices of a walk without the first/last one, and then this is the walk version of `List.head`/`List.last`, not `l[1]`/`l[l.size-2]` - In walks the first/last node and adjacency are a lot more important than they usually are in lists, so it makes more sense to have a special term for the node adjacent to the first/last node. - Walks always have a sensible default, so there's no need for the "take a proof/default value/panic/return an option" duplication which lists have and so this doesn't require much API. Co-authored-by: Daniel Weber <55664973+Command-Master@users.noreply.github.com>

mathlib-bors · 2025-01-06T14:57:45Z

Pull request successfully merged into master.

Build succeeded:

* origin/master: (189 commits) chore(Algebra): make more names consistent (#20449) feat: Polynomial FLT (#18882) feat: A disjoint union is finite iff all sets are finite, and all but finitely many are empty (#20457) fix: linkfix in 100.yaml (#20517) feat(1000): fill in more entries (#20470) feat(Combinatorics/SimpleGraph/Walk): add `penultimate` and `snd` (#16769) feat(ContinuousMultilinearMap): add lemmas about `.prod` (#20462) feat(RingTheory): classification of etale algebras over fields (#20324) fix: Allow multiple builds on staging branch (#20515) feat(CategoryTheory/Shift/Adjunction): properties of `Adjunction.CommShift` (#20337) chore(Data/Multiset/Basic): move the `sub`, `union`, `inter` sections lower (#19863) chore(Topology/UniformSpace/Completion): make coe' argument implicit (#20514) refactor(Algebra/Category/Grp/Colimits): change the construction of colimits in `AddCommGrp` (#20474) feat(Topology/Algebra/InfiniteSum/NatInt): Add pnat lems (#16544) chore(RingTheory/Finiteness): rename Module.Finite.out (#20506) refactor(CategoryTheory/Limits/Preserves/Ulift): simplify the proof that the universe lifting functor for types preserves all colimits (#20508) feat(CategoryTheory): products in the category of Ind-objects (#20507) chore: remove >9 month old deprecations (#20505) chore(FieldTheory/Galois): small cleanup (#20217) chore(LinearIndependent): generalize to semirings (#20480) chore(NumberTheory/NumberField/AdeleRing): refactor adele rings (#20500) chore: replace `aesop` with `simp` where possible (#20483) chore(1000): remove nonexistent fields (#20493) chore(CategoryTheory/Adjunction.Basic, CategoryTheory/Equivalence): change definition of `Adjunction.comp` and `Equivalence.trans` (#20490) feat(Asymptotics): add `Asymptotics.*.*Prod` lemmas (#20458) feat: a conditional kernel is almost everywhere a probability measure (#20430) feat: if `f` is a measurable group hom, then every point has a neighborhood `s` such that `f '' s` is bounded (#20304) feat: `Ico`, `Ioc`, and `Ioo` are not closed or compact (#20479) chore: drop redundant hypothesis in `Module.Dual.eq_of_preReflection_mapsTo` (#20492) feat(FaaDiBruno): derive `DecidableEq` (#20482) chore(SetTheory/Ordinal/Basic): `{x // x < y}` → `Iio y` (#20413) chore: generalize `FormalMultilinearSeries.ofScalars_norm` to `Seminormed` (#20351) chore(MvPolynomial/Localization): golf using TensorProduct (#20309) chore(Combinatorics/Enumerative/Partition): auto-derive DecidableEq (#20277) chore(CategoryTheory): make relevant parameters explicit in `Arrow.homMk`. (#20259) feat: add `IsStarNormal (↑x⁻¹ : R)` instance for `x : Rˣ` (#20091) fix: Stop cancelling builds of master (#20435) chore: update Mathlib dependencies 2025-01-05 (#20485) feat(SetTheory/Cardinal/Arithmetic): miscellaneous cardinality lemmas (#18933) chore: bump toolchain to v4.16.0-rc1, and merge bump/v4.16.0 (#20464) chore: bot validates lean-toolchain on bump/v4.X.0 branches (#20478) feat: shorthand lemmas for the L1 norm (#20383) chore: remove unnecessary adaptation notes (#20467) chore(Algebra/Category/MonCat/Colimits): remove smallness condition (#20473) chore(SetTheory/Ordinal/Arithmetic): `IsLeftCancelAdd Ordinal` (#19888) feat(Algebra): more on `OrthogonalIdempotents` (#18195) feat(Radical): `(radical a).natDegree ≤ a.natDegree` (#20468) feat(Polynomial): `(a^n)' = 0` iff `a' = 0` when `n` doesn't divide the characteristic (#20190) feat(Algebra/Lie): add Lie's theorem (#13480) chore(RingTheory/Generators): make algebra instance a def (#14265) ...

Command-Master added 7 commits September 6, 2024 06:25

Update

3f47258

Fix

a36e839

Fix

cacdb4a

feat(Combinatorics/SimpleGraph/Walk): add penultimate and snd

e9a4258

Add

3bc34ab

Update

18df849

Add lastDart

50b637c

Command-Master requested a review from pimotte September 13, 2024 14:40

Command-Master mentioned this pull request Sep 13, 2024

[Merged by Bors] - feat(Combinatorics/SimpleGraph/Walk): add dropLast #16382

Closed

2 tasks

Command-Master added the t-combinatorics Combinatorics label Sep 13, 2024

Command-Master changed the title ~~feat(Combinatorics/SimpleGraph/Walk): add penultimate and snd~~ feat(Combinatorics/SimpleGraph/Walk): add penultimate and snd Sep 14, 2024

pimotte reviewed Sep 14, 2024

View reviewed changes

Update

99cb33e

joneugster changed the title ~~feat(Combinatorics/SimpleGraph/Walk): add penultimate and snd~~ feat(Combinatorics/SimpleGraph/Walk): add penultimate and snd Sep 27, 2024

leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Oct 14, 2024

Merge branch 'master' into CM_penultsnd

fd28375

leanprover-community-bot-assistant removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Oct 16, 2024

YaelDillies reviewed Nov 2, 2024

View reviewed changes

Command-Master requested a review from YaelDillies November 7, 2024 13:58

YaelDillies approved these changes Nov 10, 2024

View reviewed changes

github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Nov 10, 2024

Command-Master requested a review from kim-em December 7, 2024 09:06

leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Dec 16, 2024

Merge branch 'master' into CM_penultsnd

bd757c1

leanprover-community-bot-assistant removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Dec 19, 2024

Command-Master requested a review from b-mehta January 6, 2025 14:42

ghost added the ready-to-merge This PR has been sent to bors. label Jan 6, 2025

mathlib-bors bot changed the title ~~feat(Combinatorics/SimpleGraph/Walk): add penultimate and snd~~ [Merged by Bors] - feat(Combinatorics/SimpleGraph/Walk): add penultimate and snd Jan 6, 2025

mathlib-bors bot closed this Jan 6, 2025

mathlib-bors bot deleted the CM_penultsnd branch January 6, 2025 14:57

SnirBroshi mentioned this pull request Nov 23, 2025

[Merged by Bors] - feat(Combinatorics/SimpleGraph): split Walk.lean into 5 files #31573

Closed

Conversation

Command-Master commented Sep 13, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Sep 13, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary bd757c1549

Import changes for modified files

Declarations diff

Uh oh!

pimotte left a comment

Choose a reason for hiding this comment

Uh oh!

YaelDillies left a comment

Choose a reason for hiding this comment

Uh oh!

Command-Master commented Nov 2, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

YaelDillies left a comment

Choose a reason for hiding this comment

Uh oh!

Command-Master commented Nov 10, 2024

Uh oh!

Command-Master commented Nov 10, 2024

Uh oh!

Command-Master commented Nov 10, 2024

Uh oh!

YaelDillies commented Nov 10, 2024

Uh oh!

github-actions bot commented Nov 10, 2024

Uh oh!

kim-em commented Nov 29, 2024

Uh oh!

Command-Master commented Nov 29, 2024

Uh oh!

b-mehta commented Dec 15, 2024

Uh oh!

Command-Master commented Dec 19, 2024

Uh oh!

b-mehta commented Jan 6, 2025

Uh oh!

mathlib-bors bot commented Jan 6, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

Command-Master commented Sep 13, 2024 •

edited

Loading

github-actions bot commented Sep 13, 2024 •

edited

Loading

Command-Master commented Nov 2, 2024 •

edited

Loading