Zulip Chat Archive

Stream: Is there code for X?

Topic: simple_graph.subgraph has Sups and Infs

Rémi Bottinelli (Feb 17 2023 at 11:59):

Any reason this isn't included already?

Kyle Miller (Feb 17 2023 at 12:06):

I don't think so, beyond no one getting to it yet.

I have a definition for Sup in this branch. We'd need to upgrade the lattice instance to complete_lattice, which takes proofs in addition to adding Sup (and Inf).

Rémi Bottinelli (Feb 17 2023 at 12:08):

Thanks! I might need it for the connectivity PR, maybe it's worth doing it.

Yaël Dillies (Feb 17 2023 at 14:07):

I have an open PR for it!

Yaël Dillies (Feb 17 2023 at 14:08):

#18285

Yaël Dillies (Feb 17 2023 at 14:09):

Actually, I see you want it for G.subgraph, not simple_graph α, but it's basically the same thing. Let me add it to the PR quick.

Yaël Dillies (Feb 17 2023 at 14:19):

cc @Rémi Bottinelli before you end up duplicating work

Rémi Bottinelli (Feb 17 2023 at 14:24):

too late

Rémi Bottinelli (Feb 17 2023 at 14:25):

I'll take it as a learning exercise :) and actually, it being not merged is a good excuse to shorten my PR a bit

Yaël Dillies (Feb 17 2023 at 14:26):

Feel free to share your code, in case you found something shorter than me

Rémi Bottinelli (Feb 17 2023 at 14:28):

I'd be surprised it is https://github.com/leanprover-community/mathlib/blob/8f23379261d38e32df19e5559ec779608a19df66/src/combinatorics/simple_graph/subgraph.lean

Rémi Bottinelli (Feb 17 2023 at 14:34):

I think infi/supr don't really play well with relations as of now, which means you kind of have to simp/split by hand

Rémi Bottinelli (Feb 17 2023 at 14:35):

mmh, I see you're building the adj by hand rather than as Inf/Sup. Why is that?

Yaël Dillies (Feb 17 2023 at 14:56):

To get better definitional equalities, and because it wasn't much harder(/actually easier?).

Rémi Bottinelli (Feb 17 2023 at 15:00):

I see, yeah, it's much easier: but doesn't that mean the API is not there yet and that's what should be done?

Yaël Dillies (Feb 17 2023 at 15:01):

Do you mean docs#Prop.supr_eq, docs#Prop.infi_eq?

Rémi Bottinelli (Feb 17 2023 at 15:04):

I don't mean anything specific.

Rémi Bottinelli (Feb 17 2023 at 15:30):

I've updated my PR and the definitions of Inf/Sup: https://github.com/leanprover-community/mathlib/blob/d0b649cb52f6af152365094d209b7ed50d298148/src/combinatorics/simple_graph/subgraph.lean but will probably remove them since you're taking care of it.

Yaël Dillies (Feb 17 2023 at 17:44):

@Rémi Bottinelli, it's updated! Feel free to drop a review :wink:

Last updated: Dec 20 2023 at 11:08 UTC