Skip to content

feat(Combinatorics/SimpleGraph/Clique): use IsContained instead of an explicit embedding from top#35613

Open
SnirBroshi wants to merge 13 commits intoleanprover-community:masterfrom
SnirBroshi:feature/simple-graph/clique-refactor-is-contained
Open

feat(Combinatorics/SimpleGraph/Clique): use IsContained instead of an explicit embedding from top#35613
SnirBroshi wants to merge 13 commits intoleanprover-community:masterfrom
SnirBroshi:feature/simple-graph/clique-refactor-is-contained

Conversation

@SnirBroshi
Copy link
Copy Markdown
Collaborator

@SnirBroshi SnirBroshi commented Feb 21, 2026 •
edited
Loading

This makes theorems require only a proof that a Copy exists rather than provide an explicit Embedding.

Also tag monotonicity lemmas with @[gcongr], and add Copy.isContained / Embedding.isIndContained / Embedding.isContained / Iso.isContained'.

This isn't a generalization per-se since one could use choice plus Copy.topEmbedding to upgrade the IsContained to an embedding, but IsContained makes more sense in theorems.

Open in Gitpod

@github-actions github-actions bot added the t-combinatorics Combinatorics label Feb 21, 2026
@github-actions
Copy link
Copy Markdown

github-actions bot commented Feb 21, 2026 •
edited
Loading

PR summary 4fea51b80c

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ Copy.isContained
+ Embedding.isContained
+ Embedding.isIndContained
+ IsContained.not_cliqueFree
+ IsContained.not_cliqueFree_card
+ Iso.isContained'
+ not_cliqueFree_iff_top_isContained

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).

YaelDillies
YaelDillies reviewed Mar 15, 2026
View reviewed changes
@YaelDillies YaelDillies added the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 15, 2026
@SnirBroshi SnirBroshi removed the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 19, 2026
@SnirBroshi SnirBroshi requested a review from YaelDillies March 19, 2026 07:38
YaelDillies
YaelDillies reviewed Mar 21, 2026
View reviewed changes
@YaelDillies YaelDillies added the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 21, 2026
@SnirBroshi SnirBroshi removed the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 23, 2026
@SnirBroshi SnirBroshi requested a review from YaelDillies March 23, 2026 05:18
YaelDillies
YaelDillies reviewed Mar 23, 2026
View reviewed changes
Mathlib/Combinatorics/SimpleGraph/Clique.lean Outdated
Comment on lines +356 to +357
noncomputable def completeGraphEmbeddingOfNotCliqueFree {n : ℕ} (h : ¬G.CliqueFree n) :
completeGraph (Fin n) ↪g G := by
Copy link
Copy Markdown
Contributor

@YaelDillies YaelDillies Mar 23, 2026

Choose a reason for hiding this comment

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

I don't see the point of renaming this

Suggested change
noncomputable def completeGraphEmbeddingOfNotCliqueFree {n : ℕ} (h : ¬G.CliqueFree n) :
completeGraph (Fin n) ↪g G := by
noncomputable def topEmbeddingOfNotCliqueFree {n : ℕ} (h : ¬G.CliqueFree n) :
completeGraph (Fin n) ↪g G := by

Copy link
Copy Markdown
Collaborator Author

@SnirBroshi SnirBroshi Mar 23, 2026 •
edited
Loading

Choose a reason for hiding this comment

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

The convention can't be to use completeGraph but then to name things with "top". This doesn't align with Mathlib's conventions. If this remains "top", then I can revert the completeGraph change.
The same applies to the other comment.

Copy link
Copy Markdown
Contributor

@YaelDillies YaelDillies Mar 23, 2026

Choose a reason for hiding this comment

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

Yet unfolding abbrevs that are there for discoverability when naming a lemma is the convention. See also typeLT vs type_lt for another example

Copy link
Copy Markdown
Collaborator Author

@SnirBroshi SnirBroshi Mar 23, 2026

Choose a reason for hiding this comment

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

typeLT is notation, not abbrev

Copy link
Copy Markdown
Contributor

@YaelDillies YaelDillies Mar 23, 2026

Choose a reason for hiding this comment

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

I know, I know, but this is an implementation detail

Copy link
Copy Markdown
Collaborator Author

@SnirBroshi SnirBroshi Mar 29, 2026

Choose a reason for hiding this comment

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

What about WellFoundedLT which is an abbrev for WellFounded?
Almost all lemmas that reference it are named with wellFoundedLT and not wellFounded_lt.

@YaelDillies YaelDillies added the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 23, 2026
@SnirBroshi SnirBroshi removed the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 23, 2026
@SnirBroshi SnirBroshi requested a review from YaelDillies March 23, 2026 13:33
YaelDillies
YaelDillies approved these changes Mar 23, 2026
View reviewed changes
Copy link
Copy Markdown
Contributor

@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.

Thanks! 🚀

maintainer merge

@github-actions
Copy link
Copy Markdown

github-actions bot commented Mar 23, 2026

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

pull_request_review, wf_run

@mathlib-triage mathlib-triage bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Mar 23, 2026
@YaelDillies YaelDillies removed their assignment Mar 23, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@YaelDillies YaelDillies YaelDillies approved these changes

Assignees

@awainverse awainverse

Labels

maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. t-combinatorics Combinatorics

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@SnirBroshi @YaelDillies @awainverse