refactor(Combinatorics/SimpleGraph/Copy): rename copy counts, align variable names, clean up docstring

[FordUniver]

Renames labelledCopyCount to copyCount and reassigns the previous copyCount to unlabeledCopyCount. Unifies graph-variable letters to the standard Guest / Host convention. Restructures and cleans up the module docstring.

Co-authored-by: Malte Jackisch 45597826+MaltyBlanket@users.noreply.github.com

---

Step 2/5 of the Copy / InducedCopy refactor-feat stack.

Originally motivated by a adiscussion in #38631 by @SnirBroshi that the British spelling of labelled is deprecated; see also discussion on Zulip (#general > SimpleGraph.Copy is labeled but copyCount is not). The addition of the new UnlabeledCopy type was separated into #39307 as a requirement to keep the diff somewhat readable.

On top of the Zulip discussion I also unified the argument naming to always follow the Guest / Host convention. This highlighted a discrepancy where we write Copy G H but copyCount H G. I left this untouched since small-first-big-later seems to be the type and big-first-small-later the ops norm in mathlib. I am happy to align them if someone has a strong opinion either way.

I also adjusted a ton of docstrings since the rename was already touching them, so it seemed sensible to use this opportunity for cleanup. Open to suggestions for what should be done differently.

I also considered replacing Bot/Top with EmptyGraph/CompleteGraph in args and statement names (@SnirBroshi that was the now-closed #39303 ) because I thought that was established with #23838 but it seems controversial, so I have reverted it.

notion	before	after
labelled copy / injective hom / monomorphism	Copy A B	Copy G H
count of labelled copies	G.labelledCopyCount H	H.copyCount G
count of unlabelled copies	G.copyCount H	H.unlabeledCopyCount G
killing operation	G.killCopies H	H.killCopies G
graph variables	mixed A B C / α β γ and G H I / V W X	uniform G H I / V W X (+ G'/H' on V'/W')

• depends on: feat(Combinatorics/SimpleGraph/Copy): introduce UnlabeledCopy carrier subtype #39307

Diff for the changes just in this PR over its predecessor: link

[github-actions]

Welcome new contributor!

Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests.

We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the awaiting-author tag, or another reason described in the Lifecycle of a PR. The review dashboard has a dedicated webpage which shows whether your PR is on the review queue, and (if not), why.

If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR.

Thank you again for joining our community.

[github-actions]

PR summary 4a320e882c

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff (regex)

+ UnlabeledCopy
+ instance : FunLike (Copy G H) V W
+ instance : IsPreorder (SimpleGraph V) IsContained
+ instance : IsPreorder (SimpleGraph V) IsIndContained
+ le_card_edgeFinset_killCopies_add_unlabeledCopyCount
+ uniqueUnlabeledCopyBot
+ unlabeledCopyCount
+ unlabeledCopyCount_bot
+ unlabeledCopyCount_eq_card_image_copyToSubgraph
+ unlabeledCopyCount_eq_zero
+ unlabeledCopyCount_le_copyCount
+ unlabeledCopyCount_of_isEmpty
+ unlabeledCopyCount_pos
- copyCount_bot
- 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.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 4a320e8).

• +10 new declarations
• −3 removed declarations

+SimpleGraph.UnlabeledCopy
-SimpleGraph.copyCount_bot
-SimpleGraph.copyCount_le_labelledCopyCount
-SimpleGraph.le_card_edgeFinset_killCopies_add_copyCount
+SimpleGraph.le_card_edgeFinset_killCopies_add_unlabeledCopyCount
+SimpleGraph.uniqueUnlabeledCopyBot
+SimpleGraph.unlabeledCopyCount
+SimpleGraph.unlabeledCopyCount_bot
+SimpleGraph.unlabeledCopyCount_eq_card_image_copyToSubgraph
+SimpleGraph.unlabeledCopyCount_eq_zero
+SimpleGraph.unlabeledCopyCount_le_copyCount
+SimpleGraph.unlabeledCopyCount_of_isEmpty
+SimpleGraph.unlabeledCopyCount_pos

---

No changes to strong technical debt.

No changes to weak technical debt.

Current commit 4a320e882c
Reference commit 47550252e7

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/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).

[FordUniver]

Labeled with awaiting-zulip based on #general>SimpleGraph.Copy is labeled but copyCount is not. The question is whether to enforce both labeled and unlabeled as a prefix for copyCount and deprecate the un-prefixed version. If so, this PR would probably be a natural place to do so.

[FordUniver]

Updated the PR per discussion on zulip, also aligned the variable names to follow Guest / Host convention after checking with @YaelDillies and cleaned up docstrings. Also split up the abbrev Sub into a prerequisite PR (#39307).

Ready to be reviewed again. Use this link for the diff over #39307.

[mitchell-horner]

I think this is a good idea. I sense Sub will be unpopular as a name (I personally don't mind it), but I agree with the shape of everything.

[mitchell-horner]

I actually would rather this the other way around. That H is the smaller contained graph and G is the larger graph.

The idea being that H.Free G looks like a predicate "is $G$ a $H$-free graph".

I understand this is purely cosmetic, but that is how it is written in extremal/*.lean and it would be nice to be consistent if we are going through rewriting variables, etc.

That is, H < G < I should be the order.

I had originally used A, B, C to be generic but that was a poor choice in retrospect. 😅

[FordUniver]

I am not quite sure I follow what convention you are suggesting? To use different variable letters or different variable order? There is three different things overall:

1. What letters do we use for SimpleGraph variables (G, H, I or A, B, C)?
2. Do we (try to) use consistent letters to highlight the "small" in relation to the "large" graphs?
3. In which order do "small" and "large" graph appear as arguments of any particular definition or statement.

I believe the file was previously inconsistent with respect to all three. Now it is only (somewhat) inconsistent with respect to (3): types (Copy) are big-first while ops (copyCount) are small first. This is somewhat in line with mathlib practices though I couldn't find any other examples where type and op are so closely linked in name as Copy and copyCount.

W.r.t. the order I don't have any particularly strong opinion, i.e., I can swap the order of both / either Copy and copyCount. If we wanted to avoid any confusion, we could have more verbose names FreeOf, FreeFrom, copyCountOf, copyCountIn, ...

But what I would find very confusing is to use G for the big graph and H for the smaller one or to just have an "alphabetic by argument order" convention, i.e., we would have copy G H and copyCount G H but the variable names do not align. I am not sure how common this convention is, but I have always liked the Guest / Host mnemonic.

[mathlib-merge-conflicts]

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

[mathlib-merge-conflicts]

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