chore(Combinatorics/SimpleGraph/Copy): rename _bot lemmas to _emptyGraph#39303
Closed
FordUniver wants to merge 4 commits into
Closed
chore(Combinatorics/SimpleGraph/Copy): rename _bot lemmas to _emptyGraph#39303FordUniver wants to merge 4 commits into
_bot lemmas to _emptyGraph#39303FordUniver wants to merge 4 commits into
Conversation
…ce `Sub` subtype
Aligns the labelled/unlabelled naming in `Copy.lean` so that the type `Copy G H`
(labelled, injective hom from `G` into `H`) is paired with the count
`H.copyCount G` (labelled count, host-first per mathlib op convention) and the
new type `Sub G H` (subgraphs of `H` isomorphic to `G`) is paired with the
count `H.subCount G`. Also unifies the graph-variable letters: the `A B C` set
that was local to `Copy.lean` is dropped in favour of mathlib's wider `G H I`
convention, with `α β γ` → `V W X` correspondingly. Within the new convention
`G` is the guest (pattern, contained side) and `H` is the host (container),
matching `G ⊑ H` and the hom direction `G →g H`.
Types are pattern-first (`Copy G H`, `Sub G H`); operations are host-first via
dot notation (`H.copyCount G`, `H.subCount G`, `H.killCopies G`). This matches
the existing mathlib convention split (hom types use source-first, host-side
operations use the host as the dot-notation receiver).
Changes:
* Rename `labelledCopyCount → copyCount` (with British `@[deprecated]` alias
`labelledCopyCount`). The previous `copyCount → subCount` rename has no
alias — `copyCount` is reassigned to mean the labelled count.
* Add `abbrev Sub G H := {H' : H.Subgraph // Nonempty (G ≃g H'.coe)}`;
redefine `subCount` as `Fintype.card (G.Sub H)` (was the inline filter-set).
* Add `instance uniqueSubBot : Unique ((⊥ : SimpleGraph W).Sub H)` factoring
the singleton-empty-subgraph fact out of `subCount_bot`.
* Drop `copyCount_eq_card_image_copyToSubgraph` (legacy filter-form bridge,
unused after the type-form refactor).
* Unify `A B C / α β γ` to `G H I / V W X` throughout. Variable block follows
the mathlib convention (cf. `SimpleGraph/Maps.lean`): subscripted names
(`G₁ G₂ G₃`) for same-vertex-type variants used in `≤` chains and `ofLE`;
primed names (`G'`, `H'`) on independent universes (`V'`, `W'`) for the
cross-universe variants used in `isContained_congr` / `free_congr` (and
their `_left` / `_right` partial-iso forms). This preserves the universe
polymorphism the old `A B C / α β γ` block provided implicitly and that
`Extremal/Basic.lean` (line 96, `← free_congr .refl (.map e G)`) relies
on.
* Fix the docstring direction on `IsContained.trans` and `.trans'`: the
previous wording ("`G` contains `H`") read the relation backwards relative
to the lemma signature (`G ⊑ H` means `G` is contained in `H`).
* Update module docstring (`Sub`/`subCount` bullets, logical-flow ordering,
`SimpleGraph.Subgraph` cross-references); add TODOs for `homCount` and
the three densities.
…th selective exposure
Replace `@[expose] public section` with a plain `public section` and
restore selective `@[expose]` on only the declarations that need
cross-module reduction:
* `Copy.toEmbedding`, `Copy.id`, `Copy.ofLE`, `Copy.topEmbedding` — the
small constructive copy `def`s, kept transparent so consumers can
elaborate against them by reducing.
* `copyCount`, `subCount` — the noncomputable counts. These need to be
exposed so downstream files (e.g. the upcoming `InducedCopy.lean` in
feat/ind-copy-count) can prove bridging inequalities like
`embCount_le_copyCount` and `indSubCount_le_subCount` directly via
`Nat.card_le_card_of_injective`.
Also:
* Inline the `@[simps!]` projections of `Copy.topEmbedding` into a manual
`@[simp] lemma topEmbedding_apply` (and similarly for `Copy.toEmbedding`).
The auto-generated `simps` form attached to `@[simps!]` was opaque to
cross-module simp; the manual form is small enough to ship as a one-line
named lemma. The body of `topEmbedding` is also tightened from
`fun {v w} ↦ ⟨fun h ↦ by simpa using h.ne, _⟩` to
`fun {_ _} ↦ ⟨fun h ↦ f.injective.ne_iff.mp h.ne, _⟩`.
* `IsIndContained` switches from `def` to `abbrev`, since the body
`Nonempty (G ↪g H)` is small and downstream Lean elaboration benefits
from automatic unfolding here.
…Nat.card * `copyCount` and `subCount` redefined via `Nat.card` instead of `Fintype.card`. * `Fintype` hypotheses weakened to `Finite` throughout (`copyCount_eq_zero`, `copyCount_pos`, `subCount_eq_zero`, `subCount_pos`, `subCount_le_copyCount`, `uniqueSubBot`, `subCount_bot`, `subCount_of_isEmpty`, `bot_isContained_iff_card_le`, `le_card_edgeFinset_killCopies`, `le_card_edgeFinset_killCopies_add_subCount`). * `bot_isContained_iff_card_le`: `Fintype.card → Nat.card`. * New `Finite (G.Copy H)` instance (sibling to the existing `Fintype` instance). * New `Nonempty (Copy G H)` instance for `[IsEmpty V]`, used to give a one-line `copyCount_of_isEmpty` proof via `Nat.card_unique`. * New `subCount_eq_nat_card_range_toSubgraph` lemma exposing the link to `Copy.toSubgraph`'s range, used in `subCount_le_copyCount`. * New private `subgraph_iso_bot` lemma extracting the singleton-subgraph fact for `uniqueSubBot`, replacing the previous `Fintype.card_congr` / `set_fintype_card_eq_univ_iff` reasoning. * `le_card_edgeFinset_killCopies` proof avoids the `Fintype.ofFinite` round-trip via `Set.finite_range` + `Set.Finite.toFinset`.
…yGraph` Renames `subCount_bot → subCount_emptyGraph`, `uniqueSubBot → uniqueSubEmptyGraph`, and the private helper `subgraph_iso_bot → subgraph_iso_emptyGraph`, aligning with the `emptyGraph` / `completeGraph` naming convention introduced in leanprover-community#23838 and already adopted in `AdjMatrix.lean`. Deprecated `@[deprecated] alias`es preserve the public-facing names for downstream callers (where the statement shape is unchanged). Statement-level generalization (`H.subCount (⊥ : SimpleGraph V) = (Nat.card W).choose (Nat.card V)` for cross-universe `V`, subsuming `subCount_of_isEmpty` and the diagonal `V = W` case) is deferred — see the new TODO. The `subCount_completeGraph` analogue (clique count) naturally lives in `Clique.lean`, which already imports `Copy.lean`.
github-actions
Bot
added
the
large-import
PR summary defda893c0Import changes exceeding 2%
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Combinatorics.SimpleGraph.Copy | 588 | 768 | +180 (+30.61%) |
Import changes for all files
| Files | Import difference |
|---|---|
10 filesMathlib.Combinatorics.SimpleGraph.Circulant Mathlib.Combinatorics.SimpleGraph.Clique Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring Mathlib.Combinatorics.SimpleGraph.Hasse Mathlib.Combinatorics.SimpleGraph.Partition Mathlib.Combinatorics.SimpleGraph.Prod Mathlib.Combinatorics.SimpleGraph.Sum Mathlib.Combinatorics.SimpleGraph.Triangle.Basic Mathlib.Combinatorics.SimpleGraph.Triangle.Counting Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite |
1 |
Mathlib.Combinatorics.SimpleGraph.UnitDistance.Basic |
59 |
Mathlib.Combinatorics.SimpleGraph.Extremal.Basic |
100 |
Mathlib.Combinatorics.SimpleGraph.Copy Mathlib.Combinatorics.SimpleGraph.LineGraph |
180 |
Declarations diff
+ Sub
+ instance : FunLike (Copy G H) V W
+ instance : IsPreorder (SimpleGraph V) IsContained
+ instance : IsPreorder (SimpleGraph V) IsIndContained
+ instance [Finite V] [Finite W] : Finite (G.Copy H)
+ instance [IsEmpty V] : Nonempty (Copy G H) := IsContained.of_isEmpty
+ le_card_edgeFinset_killCopies_add_subCount
+ subCount
+ subCount_bot
+ subCount_emptyGraph
+ subCount_eq_nat_card_range_toSubgraph
+ subCount_eq_zero
+ subCount_le_copyCount
+ subCount_of_isEmpty
+ subCount_pos
+ subgraph_iso_emptyGraph
+ toEmbedding_apply
+ topEmbedding_apply
+ uniqueSubBot
+ uniqueSubEmptyGraph
- copyCount_bot
- copyCount_eq_card_image_copyToSubgraph
- copyCount_le_labelledCopyCount
- instance : FunLike (Copy A B) α β
- instance : IsPreorder (SimpleGraph α) IsContained
- instance : IsPreorder (SimpleGraph α) IsIndContained
- le_card_edgeFinset_killCopies_add_copyCount
You can run this locally as follows
## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>
## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.
No changes to strong technical debt.
No changes to weak technical debt.
2 tasks
FordUniver
added
the
blocked-by-other-PR
Collaborator
|
Can you explain why this rename makes sense? I'm not a fan of it |
Collaborator
Author
|
Closing — the rename (subCount_bot → subCount_emptyGraph etc.) will instead be folded into #38745 where it can ship without intermediate deprecated aliases for names that only briefly existed in unmerged form. |
Collaborator
What do you mean by this? |
Collaborator
Author
Sorry ignore that, should not have closed the PR by phone. |
1 task
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Renames
subCount_bottosubCount_emptyGraph,uniqueSubBottouniqueSubEmptyGraph, and the private helpersubgraph_iso_bottosubgraph_iso_emptyGraph, aligning with theemptyGraph/completeGraphnaming convention introduced in #23838 and already adopted inAdjMatrix.lean. Deprecated@[deprecated] aliases preserve the public-facing names for downstream callers — statement shapes are unchanged.CLOSED
Was planned to be part of the #38631 stack to align
Copy.leanwith #23838, but I think this needs some discussion first.