completeGraph vs ⊤

Stream: mathlib4

[Eric Wieser]

This PR I think overall makes things a little better:

rss-bot said:

refactor(SimpleGraph): make completeGraph and emptyGraph abbrevs for ⊤ and ⊥ (mathlib4#23838)

define Top and Bot in-line for SimpleGraph and set completeGraph and emptyGraph as abbrev

Co-authored-by: FordUniver <61389961+FordUniver@users.noreply.github.com>

Authored-by: FordUniver (commit)

but should we just drop docs#SimpleGraph.completeGraph entirely? It's now an abbrev so it at least doesn't interfere with rw etc, but it still makes it confusing when naming lemmas.

[Bryan Gin-ge Chen]

I've admittedly not studied the graph theory part of mathlib much, but when looking over the diff of that PR, replacing the ⊤ and ⊥ with completeGraph and emptyGraph in theorem statements made them much easier for me to parse.

[Kyle Miller]

I'm a little surprised to see this changed. I'm pretty sure @Eric Wieser and @Yaël Dillies were both part of the discussion for the current design, where the point was to give some definitions for discoverability, and have the docstrings teach about top and bot.

A separate point is that there's a difference between semireducibility and instance reducibility, so having SimpleGraph.completeGraph defined first and then be used in the instance prevents it from being unnecessarily unfolded. It's like docs#SimpleGraph.IsSubgraph being a separate definition. (Pinging @Christoph Spiegel, since I see you asked about the seemingly backwards definition.) It's probably not a big deal in practice — and I can't say exactly what the difference will affect — but it was intentional.

It's not true that using an abbrev "doesn't interfere with rw" @Eric Wieser. The key matching means that for example you won't be able to rw [<- top_sup_eq] if the goal has completeGraph instead of \top. Maybe this will be relaxed this year if rw starts using discrimination trees.

[Eric Wieser]

Should we revert #23838 then?

[Bryan Gin-ge Chen]

It looks like #graph theory > bounded_lattice (simple_graph V) @ 💬 is the Zulip thread corresponding to !3#8330 which was the previous design. (It looks like I also put thumbs-up emojis agreeing with using top and bot instead of complete_graph and empty_graph...)

[Eric Wieser]

Kyle Miller said:

A separate point is that there's a difference between semireducibility and instance reducibility, so having SimpleGraph.completeGraph defined first and then be used in the instance prevents it from being unnecessarily unfolded.

I think we're pretty inconsistent about whether we do this; certainly, doing it leaves slightly confusing definitions around which confuse new users, sometimes to the point they feel urged to contribute and remove them!

[Eric Wieser]

(I agree there's a potential performance benefit)

[Bryan Gin-ge Chen]

Eric Wieser said:

Should we revert #23838 then?

If we do revert it, might I humbly request that someone expands the docstrings so that we don't end up changing it once again?