Skip to content

refactor(SimpleGraph): change bridges not to require the edge to be present#32583

Open
MJ141592 wants to merge 2 commits intoleanprover-community:masterfrom
MJ141592:MJ_IsBridge_31690
Open

refactor(SimpleGraph): change bridges not to require the edge to be present#32583
MJ141592 wants to merge 2 commits intoleanprover-community:masterfrom
MJ141592:MJ_IsBridge_31690

Conversation

@MJ141592
Copy link
Copy Markdown

@MJ141592 MJ141592 commented Dec 8, 2025 •
edited by YaelDillies
Loading

Remove the requirement for edges to exist in definition of isBridge, and then change the related lemmas to adjust for this, by renaming, fixing the statements and fixing the proofs, including in Acyclic.

Closes #31690.

@github-actions github-actions bot added the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label Dec 8, 2025
@github-actions
Copy link
Copy Markdown

github-actions bot commented Dec 8, 2025 •
edited
Loading

PR summary 8a623d70b9

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ IsBridge.notMem_edges_of_isCycle
+ isAcyclic_iff_forall_isBridge
+ isBridge_iff_forall_cycle_notMem
+ isBridge_iff_forall_walk_mem_edges
+ isBridge_iff_not_isEdgeConnected_two
+ isBridge_sup_edge
- isAcyclic_iff_forall_adj_isBridge

You can run this locally as follows 
## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

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

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

No changes to technical debt.

You can run this locally as

./scripts/reporting/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).

@github-actions github-actions bot added the t-combinatorics Combinatorics label Dec 8, 2025
@YaelDillies YaelDillies changed the title feat(SimpleGraph): change bridges not to require the edge to be present refactor(SimpleGraph): change bridges not to require the edge to be present Dec 8, 2025
YaelDillies
YaelDillies reviewed Dec 8, 2025
View reviewed changes
@YaelDillies YaelDillies added the awaiting-author A reviewer has asked the author a question or requested changes. label Dec 8, 2025
SnirBroshi
SnirBroshi reviewed Dec 8, 2025
View reviewed changes
@mathlib4-merge-conflict-bot mathlib4-merge-conflict-bot 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 19, 2025
@mathlib4-merge-conflict-bot
Copy link
Copy Markdown
Collaborator

mathlib4-merge-conflict-bot commented Dec 19, 2025

This pull request has conflicts, please merge master and resolve them.

@YaelDillies YaelDillies mentioned this pull request Dec 22, 2025
Closed
2 tasks
@github-actions github-actions bot 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 24, 2025
YaelDillies
YaelDillies reviewed Dec 25, 2025
View reviewed changes
@SnirBroshi
Copy link
Copy Markdown
Collaborator

SnirBroshi commented Dec 26, 2025

Hello 👋
Please merge master (click "Update branch" below), there are 2 new lemmas about bridges from #32870 that would need adjusting for the new definition

@MJ141592
Copy link
Copy Markdown
Author

MJ141592 commented Jan 7, 2026

I'm unfortunately going to be unavailable in the next two weeks, so I've invited @SnirBroshi to my fork in case it's necessary to hurry this up. Sorry for being so slow with it so far - I'm still intending to complete this soon after these two weeks if you haven't needed to do so before then. Thank you both for the feedback so far!

@SnirBroshi
Copy link
Copy Markdown
Collaborator

SnirBroshi commented Jan 7, 2026

It's unfortunate, but I think there's no rush on this, unless I've missed some PR that needs this.
I was thinking of offering help, but if you're up to this and it helps you learn Lean then leaving it to you sounds good.

@b-mehta
Copy link
Copy Markdown
Contributor

b-mehta commented Feb 9, 2026

There's not a specific rush to get this one in, but it would be nice to have it off the queue, and allows future work about bridges (and connectivity in general) to be in a more secure place. @MJ141592 (or Snir) is there something we could do to help make this easier for you?

@MJ141592
Copy link
Copy Markdown
Author

MJ141592 commented Mar 3, 2026

There's not a specific rush to get this one in, but it would be nice to have it off the queue, and allows future work about bridges (and connectivity in general) to be in a more secure place. @MJ141592 (or Snir) is there something we could do to help make this easier for you?

I'm sorry for the delayed response - I will spend a few hours on this in the next couple of days, and see if I can get it complete. I'll view #36022 and coordinate with @SproutSeeds.

@github-actions github-actions bot added the large-import Automatically added label for PRs with a significant increase in transitive imports label Mar 16, 2026
@MJ141592
Copy link
Copy Markdown
Author

MJ141592 commented Mar 17, 2026

Thank you @YaelDillies for substantial offline help with this. All points previously discussed are resolved now, and there is a final problem Yael will fix very soon. Thank you both for the help!

@YaelDillies YaelDillies removed the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 18, 2026
@mathlib-dependent-issues mathlib-dependent-issues bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Mar 18, 2026
@mathlib-merge-conflicts mathlib-merge-conflicts bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Mar 18, 2026
@mathlib-merge-conflicts
Copy link
Copy Markdown

mathlib-merge-conflicts bot commented Mar 18, 2026

This pull request has conflicts, please merge master and resolve them.

@mathlib-dependent-issues mathlib-dependent-issues bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Apr 1, 2026
@mathlib-dependent-issues
Copy link
Copy Markdown

mathlib-dependent-issues bot commented Apr 1, 2026

This PR/issue depends on:

@YaelDillies YaelDillies mentioned this pull request Apr 2, 2026
Closed
@YaelDillies
refactor(SimpleGraph): change bridges not to require the edge to be p…
07a3c84 
…resent

Author: MJ141592 <[email protected]>
Date:   Tue Mar 17 15:59:50 2026 +0100
Co-authored-by: Yaël Dillies <[email protected]>
@github-actions github-actions bot removed merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) large-import Automatically added label for PRs with a significant increase in transitive imports labels Apr 2, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@YaelDillies YaelDillies YaelDillies left review comments

@Rida-Hamadani Rida-Hamadani Awaiting requested review from Rida-Hamadani

+1 more reviewer

@SnirBroshi SnirBroshi SnirBroshi left review comments

Reviewers whose approvals may not affect merge requirements

Assignees

No one assigned

Labels

new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-combinatorics Combinatorics

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

Change bridges not to require the edge to be present

5 participants

@MJ141592 @mathlib4-merge-conflict-bot @SnirBroshi @b-mehta @YaelDillies