matchings

Stream: graph theory

[Alena Gusakov]

Is there anything else I need to do to get #5156 approved? There were two suggestions that I put aside for later, should I just implement them now?

[Alena Gusakov]

Don't know where to ask this - do people typically keep working from a branch after a PR from it has been approved?

[Mario Carneiro]

github prefers that you don't

[Alena Gusakov]

gotcha

[Mario Carneiro]

the UI gets a little wonky if you try to reopen a PR or reuse a PR branch

[Alena Gusakov]

i was just thinking that it feels a bit wasteful to keep making new branches for PRs

[Mario Carneiro]

you can delete the old ones, you know

[Alena Gusakov]

this is true, but does that delete the comment history?

[Mario Carneiro]

no

[Alena Gusakov]

ah okay, then that works lol

[Alena Gusakov]

thanks

[Mario Carneiro]

although it may make it harder to track down the commits they are attached to

[Mario Carneiro]

but if they have been squash merged in it's not particularly important to retain them

[Alena Gusakov]

gotcha

[Eric Wieser]

Bors deletes merged branches anyway, doesn't it?

[Alena Gusakov]

https://github.com/leanprover-community/mathlib/tree/simple_graph_matching

[Alena Gusakov]

this one's still up

[Mario Carneiro]

what's the PR?

[Alena Gusakov]

without realizing it i committed Eric's suggestion at the bottom, and that seems to have done something weird

[Eric Wieser]

You sure you didn't put it back up after bors deleted it?

[Alena Gusakov]

I honestly have no clue

[Mario Carneiro]

20 commits ahead and 25 behind master sounds like a bad sign

[Alena Gusakov]

Maybe I did some weird branching or something

[Alena Gusakov]

the original commit is still good

[Alena Gusakov]

https://github.com/leanprover-community/mathlib/pull/5156

[Alena Gusakov]

here's the PR

[Eric Wieser]

I find the bors way of rebasing all PRs at merge time makes it really hard to work with branches that build on top of multiple open PRs, as you then have no easy way to merge in master when the PRs you depend on get in

[Alena Gusakov]

Nevermind, it wasn't the commit. I genuinely have no idea what happened there

[Alena Gusakov]

I might've just done something wrong accidentally because I was jumping back and forth between the two PRs I had open

[Alena Gusakov]

I can delete the branch maybe?

[Mario Carneiro]

you can delete it, but make sure you have everything you want to keep from it first

[Alena Gusakov]

Actually I think it's okay - it looks like the PR keeps the comment history

[Alena Gusakov]

To delete I mean

[Kyle Miller]

There's some stuff about matchings here: https://github.com/leanprover-community/mathlib/blob/simple_graph_matching/src/combinatorics/simple_graph/matching.lean

For a perfect matching, it occurred to me that it might be useful to have an equivalence with this type:

{ g : V → V // (∀ v, G.adj v (g v)) ∧ involutive g }

(or rather, given a perfect matching, have a definition for the V → V function and a lemma for the property it satisfies).
I think there are some partial versions of this in there already.

Tutte's theorem might be a good to prove to develop the matchings part of the library, if someone wants a graph theory project.

[Alena Gusakov]

oh true, i forgot about tutte's theorem

[Alena Gusakov]

that was gonna be my next goal

[Kyle Miller]

I've stated it at https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/some.20newbie.20questions.20about.20following.20progress/near/243549319 but it needs the "right" definitions of connected components in terms of walks, I think.

[Alena Gusakov]

oh neat, okay

[Kyle Miller]

Ok, I hereby declare that @Alena Gusakov has claimed the theorem

[Yaël Dillies]

Is there any generalisation of matchings we might want to consider?

[Eric Rodriguez]

Alena, there's an ancient PR of yours I reviewed (what feels like) centuries ago. Are you still interested in that or should I just fix it up ^^

[Mario Krenn]

I am very interested in understanding and playing with perfect matchings - mainly because I want to see how a proof like this (https://mathoverflow.net/questions/267002/graphs-with-only-disjoint-perfect-matchings) would be formalized.

The reason behind is, that a generalization of this statement to weighted graph is an open question, and has important relevance in quantum mechanics (and it looks simple enough to be a good starting point to Lean). Do you think it is a reasonably simple project as a beginner of Lean? Curious about your thoughts. Thanks :)

[Kyle Miller]

@Yaël Dillies I'm not sure of any real uses of it, but there's a weakened version of a perfect matching that you might call a function carried by a graph. It's a subgraph of the graph that contains every vertex and which has been given an orientation such that each vertex has exactly one outgoing edge. You can represent it by this type:

{ g : V → V // (∀ v, G.adj v (g v)) ∧ injective (λ v, ⟦(v, g v)⟧) }

Theorem 3.5.1

Here it is formalized for current mathlib:

import data.finset
import data.fintype.basic
import combinatorics.simple_graph.basic
import combinatorics.hall

open function
open simple_graph

/-- A necessary and sufficient condition for there to be a "function carried by a graph" is that
the set of edges incident to each finite subset of k vertices has at least k edges, for each k. -/
theorem exists_carried_fun_iff {V : Type*} [fintype V] [decidable_eq V]
  (G : simple_graph V) [decidable_rel G.adj] :
  (∀ (U : finset V), U.card ≤ (U.bUnion (λ u, G.incidence_finset u)).card)
  ↔ (∃ (g : V → V), (∀ v, G.adj v (g v)) ∧ injective (λ v, ⟦(v, g v)⟧)) :=
begin
  convert finset.all_card_le_bUnion_card_iff_exists_injective (λ v, G.incidence_finset v) using 1,
  ext,
  split,
  { rintro ⟨g, ha, hinj⟩,
    use λ v, ⟦(v, g v)⟧,
    use hinj,
    simpa using ha, },
  { rintro ⟨f, hinj, hi⟩,
    simp only [mem_incidence_finset] at hi,
    use λ v, (hi v).2.other,
    split,
    { intro v,
      have h := (hi v).1,
      rw ←sym2.mem_other_spec (hi v).2 at h,
      rwa mem_edge_set at h, },
    { simp only [hinj, sym2.mem_other_spec] }, },
end

[Kyle Miller]

This also works for infinite graphs so long as the graph is locally finite, using the infinite version of Hall's theorem (infinite Hall is currently in a PR)

[Yaël Dillies]

Oh nice!

[Yaël Dillies]

Note that Bhavik and Alena's paper is a bit unclear about whether it's true for all functions or whether we choose it.

[Yaël Dillies]

Also I think this is exactly stating that G has a 2-factor. A perfect matching is a 1-factor.

[Kyle Miller]

Mario Krenn said:

I want to see how a proof like this (https://mathoverflow.net/questions/267002/graphs-with-only-disjoint-perfect-matchings) would be formalized. [...] Do you think it is a reasonably simple project as a beginner of Lean?

I think the usual advice is that beginners should prove things involving objects that are already defined -- making good definitions for formalization is tricky. Also, combinatorics seems to be particularly tricky to formalize because proofs tend to appeal to intuition.

Right now the simple graph library lacks walks, paths, cycles, and Hamiltonian cycles (and their supporting lemmas). If you feel up to it, you can try your hand at these things and get help along the way here on Zulip. In a way it shouldn't be hard, but I'm not sure it'll be a simple project.

[Kyle Miller]

Yaël Dillies said:

unclear about whether it's true for all functions or whether we choose it.

It should have also said "a graph carries a function if there exists a function $f$ that the graph carries." This is my fault.

I don't think a graph carrying a function is equivalent to it having a 2-factor. It's whether there's a spanning subgraph such that each component has exactly one cycle. So, cycles with trees growing out of them.

[Yaël Dillies]

Ah I see

[Yaël Dillies]

Mario Krenn said:

Do you think it is a reasonably simple project as a beginner of Lean? Curious about your thoughts. Thanks :)

My advice for you is to not work alone. Get someone to help you along the way. Stick yourself to an existing project you already understand mathematically.

[Kyle Miller]

@Mario Krenn By the way, in case it's useful, here's a potential formalization of the theorem statement:

import combinatorics.simple_graph.basic
import combinatorics.simple_graph.matching

open_locale classical
noncomputable theory

open fintype

-- https://mathoverflow.net/questions/267002/graphs-with-only-disjoint-perfect-matchings

lemma k4_if_three_disjoint_perfect_matchings {V : Type*} [fintype V]
  (G : simple_graph V)
  (m₁ m₂ m₃ : G.matching)
  (h₁ : m₁.is_perfect) (h₂ : m₂.is_perfect) (h₃ : m₃.is_perfect)
  (d₁₂ : disjoint m₁.edges m₂.edges) (d₁₃ : disjoint m₁.edges m₃.edges) (d₂₃ : disjoint m₂.edges m₃.edges) :
  card V = 4 ∧ G = complete_graph V :=
sorry

[Kyle Miller]

I must not have understood the theorem, because this is a counterexample to the formalized statement:
image.png

You can get such a counterexample from any face 3-coloring of a 3-regular graph cellularly embedded on a surface. (In this case, a cube graph on a plane/sphere.)

[Kyle Miller]

Actually, any 3-regular graph that's edge 3-colorable works as a counterexample. Each set of edges of the same color forms a perfect matching, and these sets are disjoint.

[Alena Gusakov]

@Eric Rodriguez sorry about that, i'll try to circle back to that PR this week or something

[Alena Gusakov]

i've just completely forgotten about it cause i started a class

[Kyle Miller]

I think I've understood it now. Corrected:

import combinatorics.simple_graph.basic
import combinatorics.simple_graph.matching

open_locale classical
noncomputable theory

open fintype

instance {V : Type*} [fintype V] (G : simple_graph V) : fintype G.matching := sorry

-- https://mathoverflow.net/questions/267002/graphs-with-only-disjoint-perfect-matchings
lemma k4_if_perfect_matchings_disjoint {V : Type*} [fintype V]
  (G : simple_graph V)
  (hc : card {m : G.matching | m.is_perfect} ≥ 3)
  (hd : ∀ (m m' : G.matching), m.is_perfect → m'.is_perfect → m ≠ m' → disjoint m.edges m'.edges) :
  card V = 4 ∧ G = complete_graph V :=
sorry

[Kyle Miller]

I think this corrected theorem is still not correct, though, because there's another counterexample:
image.png

This is the generalized Petersen graph G(9,2), which is uniquely edge 3-colorable (meaning, up to permutation of colors, there is only one edge 3-coloring).

If you have a graph such that all its perfect matchings are disjoint, then you can take the subgraph consisting of edges that are members of one of the perfect matchings. If there are at least three perfect matchings, then choose three of the perfect matchings and throw the rest of the edges out. If you take each perfect matching as a distinct color, then you are left with an edge 3-coloring. Conversely, given an edge 3-coloring you get three disjoint perfect matchings on the original graph.

[Yaël Dillies]

Their argument is to form a cycle from two matchings. What does it give here?

[Kyle Miller]

Matsumoto, "Conjectures on uniquely 3-edge colorable graphs" in Contributions to Discrete Mathematics (2016) lists some conjectures. Fiorini and Wilson conjecture that every nonplanar 3-regular uniquely edge 3-colorable graph is related to G(9,2) by a sequence of delta-wye moves, and that every planar 3-regular uniquely edge 3-colorable graph is related to K_4 by a sequence of delta-wye moves.

[Yaël Dillies]

Oh wow! That was quite a quick digging up

[Kyle Miller]

I think I've made a silly mistake though. Just because a graph is uniquely edge 3-colorable doesn't mean there are only three perfect matchings. It's worth checking G(9,2) just to be sure...

[Kevin Buzzard]

Did you see the recent AI graph counterexample paper?

[Yaël Dillies]

Oh what's that?

[Kevin Buzzard]

Gowers tweeted about it a few weeks ago and it was discussed here too, maybe in one of the ML streams

[Mario Krenn]

Kyle Miller said:

I must not have understood the theorem, because this is a counterexample to the formalized statement:
image.png

You can get such a counterexample from any face 3-coloring of a 3-regular graph cellularly embedded on a surface. (In this case, a cube graph on a plane/sphere.)

Thanks for the examples. However, this graph has more than 3 perfect matchings. grafik.png -- and thus not all PMs are disjoint sets of edges.

[Kyle Miller]

@Mario Krenn I also just counted the number of perfect matchings for G(9,2): 22

[Mario Krenn]

@Kyle Miller Ah ok good. If you find a counter example, send me your bank account. I announced a 3000Euro prize for a counter example (or proof) of the generalization :D (see https://mariokrenn.wordpress.com/graph-theory-question/ or https://mathoverflow.net/questions/311325/vertex-coloring-inherited-from-perfect-matchings-motivated-by-quantum-physics)

[Kyle Miller]

The cube example was from when I thought it was whether there existed three disjoint perfect matchings, and G(9,2) was when I mistakenly thought having three simultaneously disjoint perfect matchings in a cubic graph meant there couldn't be more perfect matchings. The second formalized theorem statement seems to be correct so far.

[Mario Krenn]

Kyle Miller said:

Mario Krenn By the way, in case it's useful, here's a potential formalization of the theorem statement:

Wow thats so cool, thanks a lot, will try to go through it tomorrow in detail! thanks :)

[Eric Rodriguez]

Alena Gusakov said:

Eric Rodriguez sorry about that, i'll try to circle back to that PR this week or something

No worries, hadn't seen you around in forever so just wanted to remind you ^^ hope the class went well

[Mario Krenn]

Kevin Buzzard said:

Did you see the recent AI graph counterexample paper?

Do you mean this one: https://arxiv.org/abs/2104.14516 ?

[Kevin Buzzard]

Yes that was it. Thanks for finding it -- was about to plough through Twitter to try and find the URL again!

[Mario Krenn]

Kevin Buzzard said:

Yes that was it. Thanks for finding it -- was about to plough through Twitter to try and find the URL again!

I just had a call with an AI expert (who works with Christian S.) about Lean and formal AI provers, he mentioned it, funny that 10mins later you mention it :D

[Yaël Dillies]

Mario Krenn said:

Do you mean this one: https://arxiv.org/abs/2104.14516 ?

I just read it. This is insane!

[Yaël Dillies]

Maybe one day we will routinely use this kind of approach to check conjectures even before publishing.

[Kevin Buzzard]

Not if they're conjectures about infinite-dimensional Banach spaces...

[Patrick Massot]

Yaël Dillies said:

Maybe one day we will routinely use this kind of approach to check conjectures even before publishing.

As Kevin hinted at, the proportion of mathematics that could be treated like this is infinitesimal, although it gets a huge popular science press coverage because it's so much easier to talk about.

[Kyle Miller]

Rob Kirby once suggested using AI to generate candidate exotic $S^4$'s, which is not implausible because compact smooth 4-manifolds can be represented by, essentially, a graph -- a Kirby diagram. I've been skeptical, though, because it's unclear how you'd train something like this if there are no examples.

The great thing about extremal graph theory for this seems to be that questions come with a natural choice of objective/reward function. It would be cool if 4-manifolds had similar (computable) functions that measured how close to being an $S^4$ a diagram is and how exotic the manifold is. Maybe, at least, an AI could learn how to simplify Kirby diagrams, since diagrams have a natural measure of complexity.

[Adam Topaz]

I also remember seeing some papers doing something with Calabi Yau varieties using ML.

[Bryan Gin-ge Chen]

I remember hearing about this paper which seems relevant. @Scott Morrison isn't subscribed to this stream though (and I'm not sure if I should forcibly subscribe him).

[Kyle Miller]

@Bryan Gin-ge Chen My understanding is that the current state-of-the-art in Kirby diagram simplification is Bob Gompf himself

[Bryan Gin-ge Chen]

That could well be the case. I do remember being shown some papers of Akbulut with really amazing sequences of Kirby diagrams too.

[Patrick Massot]

Kyle Miller said:

My understanding is that the current state-of-the-art in Kirby diagram simplification is Bob Gompf himself

Don't you mean Akbulut?

[Patrick Massot]

When I read your first message I immediately thought: OMG, he wants a artifical Akbulut...

[Kevin Buzzard]

The Calabi Yau ML stuff is guessing data from equations and when the guy spoke about it at Imperial I asked a bunch of questions about the nature of the data (eg he's claiming that his AI can predict the dimension of some cohomology space with 90% accuracy and I asked whether the answer was 0 90% of the time and he said he never checked).

[Arthur Paulino]

I need help on this one: https://github.com/leanprover-community/mathlib/pull/10210
I was able to prove the is_perfect_iff lemma (thanks @Kyle Miller for the help with the right implication). But now I got stuck on the is_perfect_then_even_card_vertices lemma (and on the one above it).

[Arthur Paulino]

I decided to make the PR smaller and just do the refactoring, defining matchings as subgraphs. It's ready for review!

[Yaël Dillies]

I would like to know what people think of defining matchings vs having them as a special case of k-factors.

[Arthur Paulino]

Technically there's no definition of a matching, but rather a characterization of subgraphs that are matchings (according to the approach suggested by Kyle)

[Yaël Dillies]

Sure, take my question as "Should we spell it G.is_matching H or G.is_factor 1 H?"

[Arthur Paulino]

We can have both of them and a lemma that proves their equivalence, wdyt?

[Yaël Dillies]

Or we can just not have is_matching.<insert Kyle's opinion here>

[Arthur Paulino]

I am usually in favor of API richness that helps with usability. Ppl usually do study matchings in UG CS courses and thinking of them as 2-factors is not as straightforward

[Arthur Paulino]

The more general we make the API, the more alien it will look to outcomers... it's a thin trade-off :thinking:

I'm not sure where to draw the line, but it's something to keep in mind

[Kevin Buzzard]

Each definition comes with a cost (the API), and each definition is one more thing for Lean to unfold, so there needs to be some sort of balance, but it's a bit of an art working out where it is. I was very frustrated over the weekend not being able to say is_singleton and instead having to keep asking for non-empty subsingletons, but I persevered because I didn't want to make a robust API for something which "we have already" in some sense.

[Arthur Paulino]

If the primary goal is to have everything as efficiently formalized as possible, then I am all in favor of dropping matchings. But if we're also targeting people without as much mathematical maturity and even less "Lean maturity", then it becomes a concern (not only for matchings, but for more general use cases of mathlib)

[Kyle Miller]

I'm not sure how many theorems about factors will apply to matchings, so it likely won't be a bad kind of API duplication. Also, it seems very likely to me that, should it come to it, we can define G.is_matching in terms of G.is_factor without too much additional work, given how things are looking right now, so my opinion right now is to carry on.

(I'll try to take more of a look at this matching PR later today.)

[Kyle Miller]

Regarding alien definitions: one thing to keep in mind is that once you have a definition, you can build out interfaces to it that look more normal. This can be justified if the definition is more powerful somehow, or if it reduces maintenance costs for the relatively small team that develops mathlib. (Defining colorings to be homomorphisms is an example of this -- this isn't an uncommon way for mathematicians to study colorings anyway, and it lets us reuse a bunch of machinery that had already been written (and it helped me notice that there are some missing things about homomorphisms). Also, we could create an API for it that looked like the obvious translation.)

[Kyle Miller]

(Even graph homomorphisms are defined in terms of docs#rel_hom, which is essentially the definition of a homomorphism for an undirected graph allowing self-loops.)

[Arthur Paulino]

This is true. The PR that characterizes matchings as subgraphs ended up enriching the subgraph API

[Patrick Massot]

Arthur Paulino said:

If the primary goal is to have everything as efficiently formalized as possible, then I am all in favor of dropping matchings. But if we're also targeting people without as much mathematical maturity and even less "Lean maturity", then it becomes a concern (not only for matchings, but for more general use cases of mathlib)

We have a very clear answer to this. mathlib tries to be a comprehensive library for professional mathematicians and computer scientists. Then you can build a teaching library out of it if you want. This is done in the tutorial project which uses a custom definition for limits of sequences of real numbers but then secretly hooks into mathlib behind the scene when it needs to use without proof the Bolzano-Weirstrass theorem.

[Mauricio Collares]

Yaël Dillies said:

Sure, take my question as "Should we spell it G.is_matching H or G.is_factor 1 H?"

Typically a "factor" of G is defined to be a spanning subgraph of G, and a k-factor of G is defined to be a k-regular factor of G. With this terminology, 1-factors correspond to perfect matchings only.

If I understand correctly, the notion of is_factor proposed here says that the subgraph H, when coerced to a graph, is regular (but not necessarily spanning). If so, would adding is_regular and a coercion be enough?

[Mauricio Collares]

For a fixed graph H and a host graph G, a common definition is to say a graph G' is an H-factor of G if G' is a spanning subgraph of G isomorphic to a bunch of disjoint copies of H, as in https://arxiv.org/abs/0803.3406 for example. This generalizes 1-factors (which are K_2-factors). It does not generalize k-factors as is, but it's easy to find a common generalization by replacing H by a family $\mathcal{H}$ of graphs (which you could take as the family of $k$-regular graphs, say). I don't think it's useful to state it like this in mathlib right now, but it's certainly a concept people care about: as an indication, the aforementioned paper won the 2012 Fulkerson Prize.

[Arthur Paulino]

@Mauricio Collares How would you organize the API to accommodate such generalization accounting for the fact that "_-factor" is used with _ replaced by an integer or by the name of a graph?

[Mauricio Collares]

No idea, I guess another name would be necessary. But I wouldn't worry about the more general concept until someone decides to prove a result that uses it; I just couldn't resist mentioning it. Don't let that message interrupt you :) My main point was the first message (that is, I think "factor" usually implies "spanning" while "matching" doesn't)

[Kyle Miller]

@Mauricio Collares That's a good point that factors are spanning subgraphs. Maybe the following seems reasonable then if it's formalized as a relation:

def simple_graph.is_factor_of (k : ℕ) (G G' : simple_graph V) := G ≤ G' ∧ G.is_regular_of_degree k

Then you can write G.is_factor_of 1 G' for G being a perfect matching of G'.

[Kyle Miller]

(the order on simple_graph V is "spanning subgraph of")

[Kyle Miller]

(I'm very ignorant about k-factors beyond perfect matchings.)

[Arthur Paulino]

Another possibility, maybe a bit awkward but shorter, is being able to state H.factors G ("factors" as a verb)

[Yaël Dillies]

I think it's nice to access the factor number, so that you can tell "is a 1-factor"

[Yaël Dillies]

What do you think of my current definition at branch#quantum_graph

[Arthur Paulino]

Shortcut url: https://github.com/leanprover-community/mathlib/blob/539d402cf61a48d4be60360930016d7e67fe827f/src/combinatorics/quantum/factor.lean#L18

[Arthur Paulino]

It's nice even though it's tightly related to k-regular graphs. As Mauricio said, if we need something more generic we can come up with it in the future

[Arthur Paulino]

@Kyle Miller On the lemma that you proposed on the PR:

lemma is_matching_iff : M.is_matching ↔ ∀ (v ∈ M.support), ∃! (w ∈ M.support), M.adj v w`

I think it needs to be:

lemma is_matching_iff : M.is_matching ↔ ∀ (v ∈ M.verts), v ∈ M.support ∧ ∃! (w ∈ M.support), M.adj v w

[Kyle Miller]

There's a lemma you could add, which is that M.support is a subset of M.verts

[Arthur Paulino]

That's not the issue. The problem I'm experiencing is when I have to prove that there exists a w such that M.adj v w but I don't have the guarantee that v ∈ M.support (no guarantee that v has a neighbor)

[Arthur Paulino]

The only guarantee that I have is that v ∈ M.verts

[Arthur Paulino]

This is the problematic state:

V: Type u
G: simple_graph V
M: G.subgraph
v: V
h: ∀ (v : V), v ∈ M.support → (∃ (x : V), (x ∈ M.support ∧ M.adj v x) ∧ ∀ (y : V), y ∈ M.support → M.adj v y → y = x)
hv: ∀ (v : V), v ∈ M.verts
⊢ ∃ (x : V), M.adj v x ∧ ∀ (y : V), M.adj v y → y = x

[Arthur Paulino]

(Notice that I've strengthen the right side of the Iff on my modified lemma)

[Arthur Paulino]

(Also I'm not proving is_matching_iff right now. I'm using it to prove is_perfect_iff)

[Kyle Miller]

Oh, right. Maybe this is the true theorem:

lemma is_matching_iff : M.is_matching ↔ ∀ (v ∈ M.verts), ∃! w, M.adj v w`

I think I confused support with verts

[Arthur Paulino]

That should work, yeah

[Kyle Miller]

Actually, let's make this (∀ {{v}}, v ∈ M.verts -> ∃! w, M.adj v w) be the definition of is_matching, and then make the two properties in the structure I suggested be lemmas.

[Kyle Miller]

I guess eq_of_adj is unnecessary since it's that's part of exists-unique, but M.verts = M.support takes a little proof.

[Arthur Paulino]

Alright let me dig into that

[Arthur Paulino]

What does {{v}} mean?

[Yaël Dillies]

It means "implicit but left explicit in the type signature so long as the next explicit argument isn't fed in"

[Eric Rodriguez]

I used to dislike them but they've strongly grown on me

[Yaël Dillies]

I do think they're great.

[Arthur Paulino]

@Kyle Miller I got the definitions and lemmas you proposed to work:
https://github.com/leanprover-community/mathlib/pull/10210

[Arthur Paulino]

I think I noticed something we could benefit from: lemmas that prove that edges sets and incidence sets are finite if the vertices are finite

[Arthur Paulino]

This would free us from the necessity of placing multiple [fintype _] restrictions when we could just derive them from [fintype V]

[Kyle Miller]

Those exist, and they just depend on having enough decidable instances. [decidable_rel G.adj] and potentially [decidable_eq V]

[Kyle Miller]

Technically it's better for lemmas to use the most generic typeclass arguments, though, since they're easier to apply, rather ones derived from others. (Even though it's a pain to write lemmas this way.)

[Arthur Paulino]

Ah, you mean this:

instance edges_fintype [decidable_eq V] [fintype V] [decidable_rel G.adj] :
  fintype G.edge_set := subtype.fintype _

[Arthur Paulino]

And we have those for subgraphs too. Nice :D

[Kyle Miller]

This is an example of how it's difficult to discover how to get wanted typeclass instances.

It would be nice if there were a way to query the typeclass inference system while telling it the kind of typeclasses you're interested in (maybe decidable for example), and then it searches like usual, but whenever it's going to fail it looks at the list of wanted typeclasses, and if it's there it pretends it was satisfied. Then for each instance it obtains at the end, it can give you the list of typeclasses you need to satisfy.

[Arthur Paulino]

Do you mean something like library_search or something more interactive in the Lean infoview?

[Kyle Miller]

Maybe a version of this can be implemented by temporarily introducing priority-0 instances implemented by sorry for the ones you're interested in, and then walking through the instance's term at the end to discover which of these instances were used.

[Kyle Miller]

I'd imagine an interface like library_search/suggest or a command like #find

[Kyle Miller]

This sorry version doesn't give you all instances though, just the first that might match.

(The point of the having a kinds of typeclasses you're interested in is to keep this from having too many results.)

[Arthur Paulino]

Ah, I forgot to say it explicitly: this PR is ready for review: https://github.com/leanprover-community/mathlib/pull/10210

[Arthur Paulino]

Oops https://github.com/leanprover-community/mathlib/pull/10210#discussion_r757640946

[Arthur Paulino]

@Yaël Dillies It was merged after I removed it from the to do list

[Yaël Dillies]

Ah, whoops!

[Yaël Dillies]

My bad. You can just put it back in your next PR to this file

[Arthur Paulino]

I will just do it right away

[Arthur Paulino]

I decided to try to tackle some of the todo's regarding graph matchings and I'm not being able to state this lemma:

lemma is_matching_iff {M : subgraph G} :
  M.is_matching ↔ ∀ (v : V), M.degree v ≤ 1 :=
begin
  sorry
end

Lean says:

failed to synthesize type class instance for
V : Type u,
G : simple_graph V,
M : G.subgraph,
v : V
⊢ fintype ↥(M.neighbor_set v)

But how can I add a []-like implicit parameter that suffices this need for every v : V?

[Yaël Dillies]

If you look at docs#simple_graph.neighbor_set_fintype, you see that you need [fintype V] [decidable_rel G.adj]

[Yaël Dillies]

Theoretically, you only need docs#simple_graph.locally_finite. But I guess we haven't quite worked out how to granularly require finiteness.

[Arthur Paulino]

Hmm, locally_finite would do the trick if we had something equivalent for subgraphs. I'm going to add it

[Yaël Dillies]

All this duplication between simple_graph, simple_graph.subgraph, and soon weighted graphs (see branch#quantum_graph) is getting annoying... I'll pull out a plan to refactor the graph library in the next few days.

[Arthur Paulino]

An option is to require that G is locally finite and prove that every subgraph of G must be locally finite. Another option is to define locally finiteness for subgraphs specifically and only require that

[Yaël Dillies]

Given the current state of things, I'd advise you against adding a specific predicate for subgraphs.

[Arthur Paulino]

Alright, to avoid unnecessary work (given your refactoring intent), I'm just going to get it going with [fintype V] [decidable_rel M.adj]

[Arthur Paulino]

Because it's less restrictive than requiring locally finiteness for the entire supergraph G

[Arthur Paulino]

Also please let me know if/when you start the refactoring. I want to see it closely :eyes:

[Yaël Dillies]

I will! I already started prototyping yesterday.

[Arthur Paulino]

huh, wait. the lemma is wrong

[Arthur Paulino]

This is the lemma:

lemma is_matching_iff {M : subgraph G} [fintype V] [decidable_rel M.adj] :
  M.is_matching ↔ ∀ (v : V), M.degree v = 1 := sorry

[Arthur Paulino]

(not ≤ 1... but = 1)

[Kyle Miller]

Yaël Dillies said:

Theoretically, you only need docs#simple_graph.locally_finite. But I guess we haven't quite worked out how to granularly require finiteness.

It's a reducible definition for Π (v : V), fintype (G.neighbor_set v), mostly as a convenience for when you actually need every vertex to have finite degree.

[Kyle Miller]

@Arthur Paulino All you need is [Π (v : V), fintype (G'.neighbor_set v)] as a hypothesis.

[Kyle Miller]

Arthur Paulino said:

(not ≤ 1... but = 1)

Oh, I see, it's still not right with = 1, though. The subgraph.degree interface is defined so that vertices outside the subgraph have degree 0. ∀ (v : V), v \in M.verts -> M.degree v = 1 should do it.

[Arthur Paulino]

:octopus: Thanks!

[Kyle Miller]

@Yaël Dillies For weighted graphs, did you consider with_bot instead of option?

@[ext] structure weighted_graph (α : Type*) (W : Type*) :=
(weight : α → α → option W)
(weight_self (a : α) : weight a a = none)
(weight_comm (a b : α) : weight a b = weight b a)

Also, to cut down on all this code duplication, I strongly suggest renaming weighted_graph.to_simple_graph to weighted_graph.coe or something equally short and then using G.coe.adj instead of ever defining G.adj.

[Kyle Miller]

The reason simple_graph.subgraph has some seemingly duplicated API is that they're giving forms of definitions and lemmas in terms of the underlying graph's V type (so for example allowing garbage values on vertices outside the subgraph). The intent I had was that for things where avoiding subtypes isn't useful, you'd do G'.coe.whatever.

[Yaël Dillies]

I have a better idea than all of that, which would also apply to subgraphs. But I want to get a shiny prototype before showing it to you.

[Yaël Dillies]

Kyle Miller said:

For weighted graphs, did you consider with_bot instead of option?

I actually did, and thought it would be a better choice given that the weight order come from lifting everything from W to option W to α → option W to α → α → option W.

[Kyle Miller]

Yaël Dillies said:

I have a better idea than all of that, which would also apply to subgraphs. But I want to get a shiny prototype before showing it to you.

How mysterious. Can you describe the idea at least?

[Yaël Dillies]

Holds in two words, eleven letters: hom refactor.

[Arthur Paulino]

My proof came down to proving this:

lemma degree_eq_one_of_unique_adj {G' : subgraph G} {v : V} [fintype (G'.neighbor_set v)] :
  G'.degree v = 1 ↔ ∃! (w : V), G'.adj v w

But I'm kinda lost dealing with the definition of degree. Any hints?

[Kyle Miller]

@Yaël Dillies Ok, if I understand you, that's roughly one of the original designs I had for graphs, but there were complexities that weren't clear were worth it so kept things with the simpler design until we had a combinatorial explosion of combinatorial objects.

Were you thinking something roughly like this https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Typeclasses.20for.20morphisms/near/258738465 ?

There are some ergonomics problems, and I find it to be a bit sad that you lose G.adj v w dot notation syntax, but it's worth looking into again.

[Yaël Dillies]

Yes, but not quite. I'm really thinking along the lines of #9888

[Kyle Miller]

Anyway, it seems like we're roughly on the same page. At some point I was going to try having a has_adj class along with is_adj_loopless and is_adj_symm property classes.

[Arthur Paulino]

Arthur Paulino said:

My proof came down to proving this:

lemma degree_eq_one_of_unique_adj {G' : subgraph G} {v : V} [fintype (G'.neighbor_set v)] :
  G'.degree v = 1 ↔ ∃! (w : V), G'.adj v w

But I'm kinda lost dealing with the definition of degree. Any hints?

ping :big_smile:

[Kyle Miller]

@Arthur Paulino You need a lemma that the degree is 1 iff the neighbor_set is a singleton, I think. This lemma doesn't seem to exist for either simple_graph or subgraph yet.

[Kyle Miller]

I'm not immediately finding a mathlib theorem that fintype s = 1 <-> exists x, s = {x}

[Eric Rodriguez]

Do you mean finset there, Kyle? I'm fairly sure it exists

[Arthur Paulino]

Ah then it's not as straightforward as I expected (given the lemmas we currently have)

[Kyle Miller]

@Eric Rodriguez I think degree is defined using fintype.card (G'.neighbor_set v)

[Kyle Miller]

@Arthur Paulino It's fairly straightforward, and you can patch together a few lemmas. One is to turn this into (G'.neighbor_set v).to_finset.card using some lemmas from data.set.finite

[Kyle Miller]

Another seems to be docs#finset.card_le_one_iff_subset_singleton

[Yaël Dillies]

Kyle Miller said:

Anyway, it seems like we're roughly on the same page. At some point I was going to try having a has_adj class along with is_adj_loopless and is_adj_symm property classes.

Okay great! What I'm doing now is finding a way to clear up a few arrows in the instance graph that don't commute.

[Kyle Miller]

Oh, never mind, this is better: docs#finset.card_eq_one

[Arthur Paulino]

It's a bit funny because it's done the exact opposite for simple_graph:

/--
`G.degree v` is the number of vertices adjacent to `v`.
-/
def degree : ℕ := (G.neighbor_finset v).card

@[simp]
lemma card_neighbor_set_eq_degree : fintype.card (G.neighbor_set v) = G.degree v :=
(set.to_finset_card _).symm

[Arthur Paulino]

I mean, starting with finset.card and then turning it into fintype.card

[Arthur Paulino]

Is there something strange here or is my intuition fooling me?

[Kyle Miller]

@Arthur Paulino I've argued for removing G.neighbor_finset v before since it's just (G.neighbor_set v).to_finset, but I've done absolutely nothing about it. Perhaps simple_graph.subgraph.degree should be defined as (G.neighbor_set v).to_finset.degree to match up with simple_graph better.

[Arthur Paulino]

I'll leave things as they are for now because there's a hope Yael's refactor might kill these

[Kyle Miller]

On the other hand, maybe with these typeclasses Yael is talking about we'll be able to have neighbor_finset at lower cost. The problem is that, even with the typeclasses, you need lemmas for both neighbor_set and neighbor_finset.

[Arthur Paulino]

Isn't it possible to design neighbor_set and neighbor_finset such that everything that works for neighbor_set works for neighbor_finset?

[Arthur Paulino]

And then just have more lemmas for neighbor_finset because it's more restricted

[Arthur Paulino]

Anyways, I'll try to get it going with your tips and what we have for now :+1:

[Kyle Miller]

This seems to be the main sort of use of neighbor_finset: https://github.com/leanprover-community/mathlib/blob/master/src/combinatorics/simple_graph/adj_matrix.lean#L187 (it makes summation nicer looking). Ideally, we could sum over set too. Might be a use for a finset_like typeclass?

Unfortunately you can't really have things work for both, since one is a set and one is a finset.

[Arthur Paulino]

Kyle Miller said:

Arthur Paulino You need a lemma that the degree is 1 iff the neighbor_set is a singleton, I think. This lemma doesn't seem to exist for either simple_graph or subgraph yet.

Hm, I don't think the iff works because of the "at most" part:

/-- A set `s` is a `subsingleton`, if it has at most one element. -/
protected def subsingleton (s : set α) : Prop :=
∀ ⦃x⦄ (hx : x ∈ s) ⦃y⦄ (hy : y ∈ s), x = y

[Kyle Miller]

@Arthur Paulino What's the problem you're running into? Are you still dealing with degree = 1? (Be careful about difference between singleton and subsingleton, if that's helpful.)

[Arthur Paulino]

I indeed confused those

[Arthur Paulino]

Alright, I got it!

lemma card_neighbor_finset_eq_degree {G' : subgraph G} {v : V} [fintype (G'.neighbor_set v)] :
  (G'.neighbor_set v).to_finset.card = G'.degree v := by rw [degree, set.to_finset_card]

lemma degree_eq_one_of_unique_adj {G' : subgraph G} {v : V} [fintype (G'.neighbor_set v)] :
  G'.degree v = 1 ↔ ∃! (w : V), G'.adj v w :=
begin
  rw [← card_neighbor_finset_eq_degree, finset.card_eq_one, finset.singleton_iff_unique_mem],
  simp only [set.mem_to_finset, mem_neighbor_set],
end

lemma is_matching_iff {M : subgraph G} [Π (v : V), fintype (M.neighbor_set v)] :
  M.is_matching ↔ ∀ (v : V), v ∈ M.verts → M.degree v = 1 :=
begin
  split,
  { intros h v hvm,
    exact degree_eq_one_of_unique_adj.mpr (h hvm),},
  { intros hv v hvm,
    exact degree_eq_one_of_unique_adj.mp (hv v hvm), },
end

[Arthur Paulino]

Ideas on how to golf is_matching_iff further?

[Kevin Buzzard]

You could just write it in term mode with pointy brackets

[Yaël Dillies]

You should get something like that in the end. Golfed enough to my standards

⟨λ h v hvm, degree_eq_one_of_unique_adj.2 $ h hvm,
  λ hv v hvm, degree_eq_one_of_unique_adj.1 $ hv v hvm⟩

[Kevin Buzzard]

Does simp [degree_eq_one_of_unique_adj] work?

[Arthur Paulino]

Kevin Buzzard said:

Does simp [degree_eq_one_of_unique_adj] work?

nope :/

[Kyle Miller]

Definitely does, you just need to refl it at the end :smile:

simpa does that for you:

lemma is_matching_iff {M : subgraph G} [Π (v : V), fintype (M.neighbor_set v)] :
  M.is_matching ↔ ∀ (v : V), v ∈ M.verts → M.degree v = 1 :=
by simpa [degree_eq_one_of_unique_adj]

[Arthur Paulino]

Wow!

[Arthur Paulino]

PR: #10864

[Arthur Paulino]

How could we prove that a matching is 2-colorable? Are these the only options?

• Redefine coloring for subgraphs
• Coerce the subgraph into a graph and state the lemma for the graph instead?

I think both options are uneasy :thinking:
I'm starting to crave for a refactor that would allow us to say that a graph is a subgraph of another graph with a Prop :eyes:

[Kyle Miller]

@Arthur Paulino The second option is how I imagined it going.

I started implementing it, but I can't keep working on it right now. The idea here is that matchings have a function to their edge set, and then using the axiom of choice (via docs#function.surj_inv) you can choose a vertex for each edge. The bool-valued coloring is whether or not the vertex was the chosen vertex.

/-- Given a vertex, give the unique edge of the matching it is incident to. -/
noncomputable
def is_matching.to_edge {M : subgraph G} (h : M.is_matching)
  (v : M.verts) : M.edge_set :=
⟨⟦(v, (h v.property).some)⟧, (h v.property).some_spec.1⟩

lemma is_matching.to_edge.surjective {M : subgraph G} (h : M.is_matching) :
  function.surjective h.to_edge :=
begin
  rintro ⟨e, he⟩,
  refine sym2.ind (λ x y he, _) e he,
  use ⟨x, M.edge_vert he⟩,
  simp only [is_matching.to_edge, subtype.mk_eq_mk, subtype.coe_mk, sym2.congr_right],
  exact ((h (M.edge_vert he)).some_spec.2 y he).symm,
end

lemma is_matching.eq_to_edge_of_adj {M : subgraph G} (h : M.is_matching)
  {v w : V} (hv : v ∈ M.verts) (hw : w ∈ M.verts) (ha : M.adj v w) :
  h.to_edge ⟨v, hv⟩ = h.to_edge ⟨w, hw⟩ :=
begin
  simp only [is_matching.to_edge, subtype.mk_eq_mk, subtype.coe_mk],
  rw [sym2.eq_swap],
  congr,
  exact ((h (M.edge_vert ha)).some_spec.2 w ha).symm,
  exact ((h (M.edge_vert (M.symm ha))).some_spec.2 v (M.symm ha)),
end

lemma loopless (G' : subgraph G) (v : V) (h : G'.adj v v) : false :=
G.loopless v (G'.adj_sub h)

noncomputable
def bicoloring_of_matching {M : subgraph G} (h : M.is_matching) :
  M.coe.coloring bool :=
begin
  let f := function.surj_inv (is_matching.to_edge.surjective h),
  classical,
  let c : M.verts → bool := λ v, f (h.to_edge v) = v,
  fsplit,
  use c,
  rintros ⟨v, hv⟩ ⟨w, hw⟩,
  simp,
  intros ha h',
  by_cases hc : f (h.to_edge ⟨v, hv⟩) = ⟨v, hv⟩,
  { rw h.eq_to_edge_of_adj hw hv (M.symm ha) at h',
    simp only [hc, true_iff, eq_self_iff_true, subtype.mk_eq_mk] at h',
    subst h',
    exact M.loopless _ ha, },
  { simp [hc] at h',
    rw h.eq_to_edge_of_adj hv hw ha at hc,
    sorry, },
end

[Arthur Paulino]

@Kyle Miller wanna start the PR and I can try to take over?

[Arthur Paulino]

I'm trying to take another TODO item down but I'm quite sure I'm doing something strange here.
I'm trying to prove that the existence of a perfect matching on a graph implies that the cardinality of the number of vertices is even. For that, I'm telling lean "use the number of edges in the matching", but the proof follows quite strangely from there.

Here's the file with my current attempt. Help is much appreciated :pray:

[Kyle Miller]

I suggest using docs#simple_graph.is_perfect_matching_iff and docs#Exist.some to define a function simple_graph.is_perfect_matching.other : V -> V, then prove it's docs#function.involutive and without fixed points (not sure if a predicate exists for that), then use some lemma (that you might need to write, maybe something in docs#simple_graph.dart gives a hint) to show fintype.card V is even.

[Kyle Miller]

Maybe the idea is that you get a map to_edge : V -> M.edge_set that's 2-to-1, with simple_graph.is_perfect_matching.other being the map whose orbits partition V into the fibers of the to_edge map.

[Kyle Miller]

so you should be able to take things rather directly from the module for simple_graph.dart

[Arthur Paulino]

What do you mean by "without fixed points"?

[Kyle Miller]

@Arthur Paulino By the way, a more streamlined argument is to apply docs#simple_graph.even_card_odd_degree_vertices to M.spanning_coe

[Kyle Miller]

using an is_perfect_matching analogue of docs#simple_graph.subgraph.is_matching_iff_forall_degree (one without the v ∈ M.verts hypothesis)

[Kyle Miller]

This is the kind of thing I mean by without fixed points: docs#simple_graph.dart.rev_ne

[Kyle Miller]

It would still be nice to have simple_graph.is_perfect_matching.other and to prove some properties about it.

[Kyle Miller]

For example, prove that dart.fst defines an equivalence between M.spanning_coe.dart and V, and that dart.fst is an isomorphism in the sense that dart.fst d.rev = h.other (dart.fst d) (where h : M.is_perfect_matching).

[Yaël Dillies]

@Arthur Paulino, do you mind if I work on this branch? I have an idea of how the proof could go (and I think I'm gonna need the API surrounding that result very soon)

[Arthur Paulino]

Yaël Dillies said:

Arthur Paulino, do you mind if I work on this branch? I have an idea of how the proof could go (and I think I'm gonna need the API surrounding that result very soon)

Not at all, you can go for it.
If you don't take Kyle's suggestion as your route (defining simple_graph.is_perfect_matching.other and proving those results for it), you can also add it as a TODO and we can deal with it later :+1:

[Yaël Dillies]

I'm first gonna prove the slightly more general result that the support of a matching is even.

[Kyle Miller]

Are you going to use even_card_odd_degree_vertices? That seems potentially the most straightforward (though it would be for M.coe rather than M.spanning_coe)

[Yaël Dillies]

Given that this result is basically the handshaking lemma, I should probably use the handshaking lemma in the proof :grinning: But I'm not excluding finding a more convenient generalization/variation of even_card_odd_degree_vertices first.

[Bhavik Mehta]

It could be helpful to have a function is_perfect_matching.get_edge : V -> sym2 V which is guaranteed to have other and the given vertex, and to be an edge of the graph. (And probably the non-perfect generalisation)

[Arthur Paulino]

I thought the proof would go smooth with sum_degrees_eq_twice_card_edges. I still don't understand why it didn't work :sweat_smile:

[Arthur Paulino]

Bhavik Mehta said:

It could be helpful to have a function is_perfect_matching.get_edge : V -> sym2 V which is guaranteed to have other and the given vertex, and to be an edge of the graph. (And probably the non-perfect generalisation)

Yeah that function seemed to be the start of Kyle's reasoning here.

[Arthur Paulino]

BTW, while the simple_graph vs subgraph definitions don't get refactored, some instances that carry some assumptions down from the simple graph to its subgraphs would be very useful. E.g.: locally finiteness of neighbors on a vertex, rel decidability of subgraph.adj etc

[Arthur Paulino]

Actually this one is already contemplated:

instance finite_at {G' : subgraph G} (v : G'.verts) [decidable_rel G'.adj]
   [fintype (G.neighbor_set v)] : fintype (G'.neighbor_set v) :=
set.fintype_subset (G.neighbor_set v) (G'.neighbor_set_subset v)

[Kyle Miller]

For what it's worth, here's how to use sum_degrees_eq_twice_card_edges:

lemma is_perfect_matching_iff_forall_degree {M : subgraph G}
  [Π (v : V), fintype (M.neighbor_set v)] :
  M.is_perfect_matching ↔ ∀ (v : V), M.degree v = 1 :=
by simp [degree_eq_one_iff_unique_adj, is_perfect_matching_iff]

@[simp]
lemma spanning_coe_degree {G' : G.subgraph} (v : V)
  [fintype (G'.neighbor_set v)] [fintype (G'.spanning_coe.neighbor_set v)] :
  G'.spanning_coe.degree v = G'.degree v :=
begin
  rw [← card_neighbor_set_eq_degree, subgraph.degree],
  congr,
end

lemma even_card_vertices_of_perfect_matching {M : subgraph G}
  [fintype V] [decidable_eq V] [decidable_rel G.adj]
    (h : M.is_perfect_matching) : even (fintype.card V) :=
begin
  classical,
  rw is_perfect_matching_iff_forall_degree at h,
  have := M.spanning_coe.sum_degrees_eq_twice_card_edges,
  simp [h] at this,
  exact ⟨_, this⟩,
end

[Kyle Miller]

(I'd like the first two lemmas in the library somewhere anyway.)

[Arthur Paulino]

Oh it's done :rofl:

[Arthur Paulino]

@Yaël Dillies I can just push those proofs that Kyle already did

[Kyle Miller]

That doesn't have the more general one, though.

[Bhavik Mehta]

I wonder if this can be used to prove the more general one - given a matching it is perfect on itself, so it has an even number of vertices

[Yaël Dillies]

Dang, just went to have a glass a water and here comes the proof :rofl:

[Arthur Paulino]

It's true tho. I think having the more general one and this one following it would be nicer

[Kyle Miller]

I wonder if it's worth generalizing this lemma:

lemma is_matching_iff_forall_degree {M : subgraph G} [Π (v : V), fintype (M.neighbor_set v)] :
  M.is_matching ↔ ∀ (v : V), v ∈ M.verts → M.degree v = 1

We don't need a fintype instance for every vertex, just the ones in the support.

[Yaël Dillies]

We currently handle finiteness quite badly, so I would be eager for a full rethink on how to do it.

[Arthur Paulino]

@Yaël Dillies I'm going to push the proofs Kyle wrote and then you can improve it, okay?

[Kyle Miller]

It's funny, being able to have varying finiteness at different vertices is something I think we managed to actually pull off, vs the alternative (which was only finite graphs).

[Kyle Miller]

Maybe it's obvious in retrospect, since we have this API

[Yaël Dillies]

With all the kerfuffle of switching between finsets and sets? I saw Alena in pain writing the SRG branch back in March, and my medication was "Take more finsets".

[Kyle Miller]

(I'm happy to hear constructive criticism about what could be improved, but general comments about API being "bad" I don't find to be particularly helpful.)

[Yaël Dillies]

I'm trying to come up with something :smile:

[Yaël Dillies]

And sorry, I should stop insulting your APIs.

[Arthur Paulino]

okay @Yaël Dillies you can go for it. in the meantime I'm going to define the V -> edge function that Bhavik and Kyle were talking about

[Kevin Buzzard]

Never use finsets at all and do everything with set.finite :-)

[Arthur Paulino]

Since the topic of graph API came up, I'm going to take the chance and make a question that I've been longing to ask for a while now :D

[Yaël Dillies]

Kevin, the finsect outcast :grinning:

[Bhavik Mehta]

Kyle Miller said:

It's funny, being able to have varying finiteness at different vertices is something I think we managed to actually pull off, vs the alternative (which was only finite graphs).

I agree, but here's a particular thing which I think is missing?

instance {V : Type*} (G : simple_graph V) (G' : subgraph G) [fintype V] (v : V) :
  fintype (G'.neighbor_set v) := by apply_instance

[Yaël Dillies]

lol I was writing that instance just now

[Bhavik Mehta]

Oh actually it's already there, never mind!

[Yaël Dillies]

The one I'm interested in takes fintype M.support instead.

[Kyle Miller]

There are definitely some decidability instances missing for subgraph

[Kyle Miller]

instance [decidable_pred (∈ M.support)] [fintype V] : fintype M.support := set_fintype _

[Kyle Miller]

Yaël Dillies said:

The one I'm interested in takes fintype M.support instead.

I was too :smile:

[Kyle Miller]

I'm not sure the decidability instance needed, but I'd started on this one:

instance support_decidable_pred [decidable_rel G.adj] : decidable_pred (∈ M.support) :=
begin

end

(I doubt I have the right hypotheses.)

[Yaël Dillies]

You also need fintype V I'm afraid, because ∈ M.support is an existential.

[Arthur Paulino]

@Yaël Dillies do you want to push to that branch or open a PR into it?

[Yaël Dillies]

I'll just push I think

[Arthur Paulino]

Alright (just wanted to check so we don't step on each other's toes)

[Kyle Miller]

(I'm not working on this anymore -- just wanted to show how to use the lemma. No more toe stepping from me :footprints:)

[Arthur Paulino]

Kyle do you mind if I push the is_matching.to_edge function and the following two lemmas that you proved about it here?

[Kyle Miller]

Nope!

[Yaël Dillies]

Okay, got the instance.

[Arthur Paulino]

I'm also adding the loopless lemma into the subgraph API, but I changed it slightly:

protected lemma loopless {v : V} (G' : subgraph G) : ¬G'.adj v v :=
by {by_contra h, exact G.loopless v (G'.adj_sub h) }

[Kyle Miller]

One thing we need to fix for the simple graph API is that many lemma statements use derived decidability and fintype instances, rather than having everything be taken as instance arguments. This is a Known Bug that causes some random problems.

(A way I've wanted to solve this is to change how computability works in mathlib in general, but it would be nice if someone fixed these things sooner than whenever that might happen :wink:)

[Yaël Dillies]

Arthur Paulino said:

I'm also adding the loopless lemma into the subgraph API, but I changed it slightly:

protected lemma loopless {v : V} (G' : subgraph G) : ¬G'.adj v v :=
by {by_contra h, exact G.loopless v (G'.adj_sub h) }

adj_irrefl!

[Yaël Dillies]

Kyle Miller said:

(A way I've wanted to solve this is to change how computability works in mathlib in general, but it would be nice if someone fixed these things sooner than whenever that might happen :wink:)

I'm gonna ask the protocolary question: Will it change in Lean 4?

[Arthur Paulino]

Yaël Dillies said:

Arthur Paulino said:

I'm also adding the loopless lemma into the subgraph API, but I changed it slightly:

protected lemma loopless {v : V} (G' : subgraph G) : ¬G'.adj v v :=
by {by_contra h, exact G.loopless v (G'.adj_sub h) }

adj_irrefl!

lemma adj_irrefl {v : V} (G' : subgraph G) : ¬G'.adj v v :=
by { by_contra h, exact G.loopless v (G'.adj_sub h) }

[Yaël Dillies]

Because yeah clearly decidability management is a pain and shouldn't have to be dealt with. After all, why not a system which puts in the correct decidability assumptions on each lemma, unless it yucks in which case you do it by hand?

[Kyle Miller]

Regarding loopless and adj_irrefl -- should we change simple_graph.loopless to simple_graph.adj_irrefl and add simple_graph.loopless as an alias?

[Yaël Dillies]

Yes please, that would be much more in line with the rest of mathlib :smiling_face:

[Kyle Miller]

At some level I feel like this is caving in to viewing simple graphs as just being relations.

[Yaël Dillies]

Exactly

[Yaël Dillies]

And #11000 gives up on those custom names altogether.

[Arthur Paulino]

Yeah I've been thinking about this idea of being able to have graphs of whatever (not limiting the type of a vertex)

[Kyle Miller]

Anyway, so long as it's still simple_graph.loopless, I think it ought to be called simple_graph.subgraph.loopless. I'm very open to adj_irrefl being an alias in both cases for now.

[Kyle Miller]

@Arthur Paulino If I understand you, the intent there is to use sigma types when you want graphs with any vertex type

[Yaël Dillies]

The next step is of course to drop the subgraph.adj spelling and only use the dot-less graph.adj

[Arthur Paulino]

Kyle Miller said:

Anyway, so long as it's still simple_graph.loopless, I think it ought to be called simple_graph.subgraph.loopless. I'm very open to adj_irrefl being an alias in both cases for now.

Can I just do a full refactor and stick to adj_irrefl all the way through?

[Yaël Dillies]

with dot notatable lemmas like graph.adj.symm

[Kyle Miller]

@Yaël Dillies That's not an "of course" -- I really think we don't have to compromise and lose dot notation.

[Yaël Dillies]

Reread my message :grinning:

[Yaël Dillies]

It's a matter of shifting what we're dot notating on.

[Kyle Miller]

I know, and I mean I think we can still have dot notation on the object itself.

[Yaël Dillies]

But yeah, the dot notation on concrete structures has to be lost for the general lemmas. With the current state of things, this is what refactoring to a typeclass hierarchy entails.

[Kyle Miller]

(It might take some small modifications to Lean, but I still need to make sure it can't be done without that.)

[Yaël Dillies]

If you're willing to dig into Lean itself, then yeah I'm sure you can fix that. But I don't think this is that important. And in particular we shouldn't delay the refactor because of loss of dot notation IMO

[Arthur Paulino]

@Yaël Dillies I saw that you just pushed a commit. I'm gonna push a commit on top of it okay?

[Arthur Paulino]

(so you can pull before continuing)

[Yaël Dillies]

Go ahead. I'm off for the day

[Bhavik Mehta]

Yaël Dillies said:

Yes please, that would be much more in line with the rest of mathlib :smiling_face:

This isn't actually true, there is exactly one relation which uses _irrefl, namely lt, and exactly one instance of less to describe a property. The mathlib pattern is actually to use irrefl or irrefl_of together with the irreflexivity typeclass.

[Arthur Paulino]

Btw, today's brainstorming session was fun. Thanks! :D

[Arthur Paulino]

This is the current state of the PR: #11083 (after hopefully everything we've discussed here)

[Arthur Paulino]

@Kyle Miller almost at the same time you posted on the PR, I finished Yael's proof

[Arthur Paulino]

It doesn't require any of the assumptions you mentioned on your comment.
Neither [∀ v, fintype (M.neighbor_set v)] nor [∀ v, fintype (M.coe.neighbor_set v)]

[Arthur Paulino]

I have committed your suggestions as well as your alternative proof. Feel free to commit directly to the branch if you want to adjust details manually before we mark the PR as ready for review :+1:

[Arthur Paulino]

(or just comment here or on the PR and I can commit the adjustments)

[Kyle Miller]

@Arthur Paulino Oh right, not sure what I was thinking, those are definitely not necessary.

noncomputable instance (G' : subgraph G) [fintype G'.verts] (a : V) : fintype (G'.neighbor_set a) :=
fintype.of_injective (λ (v : G'.neighbor_set a), (⟨v, G'.edge_vert (G'.adj_symm v.2)⟩ : G'.verts))
(λ v w h, by { ext, convert congr_arg subtype.val h })

lemma is_matching.even_card {M : subgraph G} [hM : fintype M.verts] [decidable_eq V]
  [decidable_rel G.adj] (h : M.is_matching) :
  even (M.verts.to_finset.card) :=
begin
  classical,
  rw is_matching_iff_forall_degree at h,
  have := M.coe.sum_degrees_eq_twice_card_edges, simp [h] at this,
  use M.coe.edge_finset.card,
  rw [← this, set.to_finset_card],
  refl,
end

[Arthur Paulino]

So we leave the two proofs?

[Arthur Paulino]

hmm, actually we have this lemma:
lemma is_matching.support_eq_verts {M : subgraph G} (h : M.is_matching) : M.support = M.verts

[Kyle Miller]

Exactly -- even M.verts.to_finset.card seems to me to be more basic than even M.support.to_finset.card.

[Kyle Miller]

The proofs are basically the same, but when using M.verts you don't need the unfreezingI business.

[Arthur Paulino]

And now is_perfect_matching.even_card should be even simpler right?

[Arthur Paulino]

The PR is looking good for now. We can just golf it from here

[Arthur Paulino]

I've marked it as ready for review

[Yaël Dillies]

Kyle Miller said:

The proofs are basically the same, but when using M.verts you don't need the unfreezingI business.

I used M.support precisely because some lemmas were already using it instead of verts and I didn't want to introduce disparity.

[Kyle Miller]

@Yaël Dillies Are you proposing to use M.support instead of M.verts? If you're instead explaining what led you to choose it, for what it's worth I forgot what "the point" of docs#simple_graph.subgraph.is_matching.support_eq_verts was until I looked at all the code hours later (I, too, had started writing an M.support version to see what might be challenging, but you finished that one first).

[Arthur Paulino]

IIRC, Yael's motivation was because he would need this result in a near future, but I think he was referring to is_perfect_matching.even_card

[Arthur Paulino]

I am now trying to prove it this way:

lemma is_perfect_matching.even_card' {M : subgraph G} [fintype V] (h : M.is_perfect_matching) :
  even (fintype.card V) :=
begin
  have := is_matching.even_card h.1,
  rw card_verts_eq_of_spanning h.2 at this,
  exact this,
end

But now I need to prove these:

instance [fintype V] {G' : subgraph G} : fintype G'.verts := sorry

lemma card_verts_eq_of_spanning [fintype V] {G' : subgraph G}
  (h : G'.is_spanning) : G'.verts.to_finset.card = fintype.card V := sorry

[Arthur Paulino]

lemma card_verts_eq_of_spanning [fintype V] {G' : subgraph G}
  (h : G'.is_spanning) : G'.verts.to_finset.card = fintype.card V :=
by { congr, ext1, simp at *, solve_by_elim }

[Kyle Miller]

For writing the lemma, it's better to include fintype instances for everything in sight:

lemma card_verts_eq_of_spanning [fintype V] {G' : subgraph G} [fintype G'.verts]
  (h : G'.is_spanning) : G'.verts.to_finset.card = fintype.card V :=
by { rw is_spanning_iff at h, congr, convert set.to_finset_univ }

(Removed the non-terminal simp and used an existing lemma. There's a bit of magic here with convert; I think it runs assumption automatically?)

[Kyle Miller]

There's already an instance fintype G'.verts from fintype V if you have the right decidability instances:

instance [fintype V] {G' : subgraph G} [decidable_pred (∈ G'.verts)]: fintype G'.verts :=
by apply_instance

[Kyle Miller]

So you can get even_card' working by starting it with the classical tactic.

[Arthur Paulino]

Kyle Miller said:

For writing the lemma, it's better to include fintype instances for everything in sight

Doesn't that make the lemma more restrictive?

[Kyle Miller]

Then a little bit of golfing:

lemma is_perfect_matching.even_card' {M : subgraph G} [fintype V] (h : M.is_perfect_matching) :
  even (fintype.card V) :=
by { classical, simpa [card_verts_eq_of_spanning h.2] using is_matching.even_card h.1 }

[Kyle Miller]

Arthur Paulino said:

Kyle Miller said:

For writing the lemma, it's better to include fintype instances for everything in sight

Doesn't that make the lemma more restrictive?

It's the opposite: it makes sure you can apply it no matter which instances show up in the expression

[Kyle Miller]

"Be permissive in what you accept": all the instances in the goal are universally quantified here

set_option pp.implicit true
#check @card_verts_eq_of_spanning
/-
∀ {V : Type u_1} {G : simple_graph V} [_inst_1 : fintype V] {G' : G.subgraph} [_inst_2 : fintype ↥(G'.verts)],
G'.is_spanning → (@set.to_finset V G'.verts _inst_2).card = @fintype.card V _inst_1
-/

[Arthur Paulino]

Now I'm confused :upside_down:

[Arthur Paulino]

I thought that adding more [] parameters to my lemmas would restrict their usage

[Kyle Miller]

Compare it to this:

lemma card_verts_eq_of_spanning [fintype V] {G' : subgraph G} [decidable_pred (∈ G'.verts)]
  (h : G'.is_spanning) : G'.verts.to_finset.card = fintype.card V := sorry

set_option pp.implicit true
#check @card_verts_eq_of_spanning
/-
∀ {V : Type u_1} {G : simple_graph V} [_inst_1 : fintype V] {G' : G.subgraph} [_inst_2 : @decidable_pred V (λ (_x : V), _x ∈ G'.verts)],
G'.is_spanning → (@set.to_finset V G'.verts (@verts.fintype V G _inst_1 G' (λ (a : V), _inst_2 a))).card = @fintype.card V _inst_1
-/

[Kyle Miller]

This only applies to the case when the set.to_finset expression's fintype instance is created using set.fintype.

[Kyle Miller]

When we get this wrong, this is why we need convert sometimes.

[Arthur Paulino]

I will need to chew on this a little longer. Either way, this is the PR now: #11083

[Kyle Miller]

@Arthur Paulino The situation is analogous to the difference between these lemmas:

lemma foo {α : Sort*} (x : unit) (y z : α) : x = () := subsingleton.elim _ _
lemma foo' {α : Sort*} (y z : α) : () = () := rfl

The first lemma is more general than the second.

[Kyle Miller]

fintype is also a subsingleton -- even though all fintype instances for the same type are equal, they're not definitionally equal, so it's better to let them be additional arguments.

[Arthur Paulino]

That's probably why I hit this wall

[Kyle Miller]

If I remember correctly, that's a different issue (that I also ran into). I think one was finset.univ : finset V and the other was finset.univ : finset (set.univ : set V).

[Kyle Miller]

(In the second case, set.univ is being coerced to a type.)

[Kyle Miller]

It would probably be useful having a lemma in mathlib that these have the same cardinality if one doesn't already exist.

[Kyle Miller]

example {α : Type*} [fintype α] :
  (finset.univ : finset (set.univ : set α)).card = (finset.univ : finset α).card := sorry

[Arthur Paulino]

Would it make card_verts_eq_of_spanning trivial?

[Arthur Paulino]

(just to make sure I'm following)

[Kyle Miller]

Ok, good, got the types right and it's true:

example {α : Type*} [fintype α] :
  (finset.univ : finset (set.univ : set α)).card = (finset.univ : finset α).card :=
begin
  classical,
  rw ← finset.card_image_of_injective finset.univ subtype.coe_injective,
  congr,
  ext,
  simp,
  apply_instance,
end

[Kyle Miller]

Arthur Paulino said:

Would it make card_verts_eq_of_spanning trivial?

I don't know. It seems your proof of that lemma avoided this. I'm not completely sure if it's what you ran into yesterday, but it's definitely something I ran into.

[Arthur Paulino]

I'm going to post #11083 on #PR reviews okay?

[Yaël Dillies]

My reasoning is just that M.support was already used while M.verts wasn't and M.verts is in general stronger than M.support.

[Arthur Paulino]

Kyle Miller said:

Ok, good, got the types right and it's true:

example {α : Type*} [fintype α] :
  (finset.univ : finset (set.univ : set α)).card = (finset.univ : finset α).card :=
begin
  classical,
  rw ← finset.card_image_of_injective finset.univ subtype.coe_injective,
  congr,
  ext,
  simp,
  apply_instance,
end

Do you think this should go somewhere?