graph theory

Stream: maths

[Jakob von Raumer]

Have there been any useful attempts to make a good library on graph theory? Any students of yours, @Kevin Buzzard ? There's a student here who's considering formalising some planar graph theory as part of their bachelor's thesis.

[Johan Commelin]

@Jakob von Raumer There's a #graph theory stream!

[Johan Commelin]

There's been quite some activity in fact, see also https://github.com/leanprover-community/mathlib/tree/master/src/combinatorics

[Kevin Buzzard]

funnily enough I was thinking about this yesterday, and basically I have no idea what "good" means. It seems to me that graph theory is taught very early on to CS students, with applications to networks, algorithms etc. We don't have a graph theory course in the maths department at Imperial, and the one I sat through as an UG in Cambridge comprised a hotch-potch of unrelated results like Hall's Marriage theorem and the 5 colour theorem (and even the 7 colour theorem for maps on a torus) with no underlying story and no other courses relying on the results (mathematically, this is often the case in combinatorics-based courses, they tend to teach general principles as opposed to important theorems like the fundamental theorem of Galois theory which is used everywhere). So I am probably not the best person to ask! @Bhavik Mehta what does a "good" graph theory library contain?

[Jakob von Raumer]

Ah, thank you! Forgot to check the list of streams :)

[Jakob von Raumer]

@Kevin Buzzard The graph theory course at KIT at the math dept contains, if my memory serves me right, a lot of Ramsey theory style results

[Kevin Buzzard]

I think we probably had one lecture on "R(3,3)=6, proof by induction that R(m,n) is finite" and that was it for Ramsey theory.

[Bhavik Mehta]

Kevin Buzzard said:

funnily enough I was thinking about this yesterday, and basically I have no idea what "good" means. It seems to me that graph theory is taught very early on to CS students, with applications to networks, algorithms etc. We don't have a graph theory course in the maths department at Imperial, and the one I sat through as an UG in Cambridge comprised a hotch-potch of unrelated results like Hall's Marriage theorem and the 5 colour theorem (and even the 7 colour theorem for maps on a torus) with no underlying story and no other courses relying on the results (mathematically, this is often the case in combinatorics-based courses, they tend to teach general principles as opposed to important theorems like the fundamental theorem of Galois theory which is used everywhere). So I am probably not the best person to ask! Bhavik Mehta what does a "good" graph theory library contain?

I agree it's a tricky question. The two main things I'd like to see in a "good" library are definitions (of course with API) of all the basic concepts of graphs: planarity, colouring, extremal number, diameter etc with the standard results about them eg Brooks' theorem, Hall's theorem; and a collection of tools in order to make proving new results easy, for example results like Erdos-Stone, Szemeredi's regularity lemma and a clean API for probabilistic graph theory and expander graphs.

[Bhavik Mehta]

Some of these are much harder than others, but I think the resulting library has the same goal as any other maths library: to provide enough definitions and results to make proving "actual" graph theory results (ie active research things) convenient.

[Bhavik Mehta]

As for the existing Cambridge graph theory courses, my undergrad graph theory notes are here: https://github.com/b-mehta/maths-notes/blob/master/ii/mich/graph_theory.pdf, you can basically see a summary from the contents page. The Ramsey theory covered was basically what Kevin says, plus a proof of multicolour and infinite Ramsey; but there was also a Part III (MSc-level) Ramsey theory course syllabus here which went into more detail, @David Wärn is proving some of the combinatorial results from it eg Hales-Jewett and Rado's theorem. There was also a Part III Extremal Graph Theory course which was more in-depth, there are some notes from a 2017 version of this course here: https://dec41.user.srcf.net/notes/III_M/extremal_graph_theory.pdf

[Hunter Monroe]

@Bhavik Mehta do you mind if I update your Ramsey Theory files to the latest mathlib and submit?

[Bhavik Mehta]

Feel free to make the PRs, but the main reason I haven't is that I'm not certain they're ready for PR yet, there's the whole crec business and it's pretty ugly... That said, the actual result is (I think) formulated nicely so maybe it's not hugely important that the proof is ugly

[Patrick Massot]

Kevin Buzzard said:

We don't have a graph theory course in the maths department at Imperial, and the one I sat through as an UG in Cambridge comprised a hotch-potch of unrelated results like Hall's Marriage theorem and the 5 colour theorem (and even the 7 colour theorem for maps on a torus) with no underlying story and no other courses relying on the results (mathematically, this is often the case in combinatorics-based courses, they tend to teach general principles as opposed to important theorems like the fundamental theorem of Galois theory which is used everywhere).

In France a standard undergrad math curriculum features no graph theory at all. This is why graph theory doesn't appear at all on our undergrad math page. Some students may still encounter graphs in some random optional first year course on recreational mathematics.

[Arthur Paulino]

Question: why is simple_graph under combinatorics? Would it fit better under data?

Idea: data > graph > [simple_graph, directed_graph, weighted_graph etc]

What do you think?

[Dima Pasechnik]

normally speaking, "graphs" of "data (science)" are rather different from graphs as combinatorial structures.

[Yaël Dillies]

It would make me even sadder that there's so little under combinatorics :sad:

[Scott Morrison]

The data is more of a historical hodge podge of things people didn't find better homes for at the time. :-) I think in the long term we would like to rearrange things so data comes to mean "data structures" in the programming sense. I would encourage moving anything "mathmetical" out of data, rather than the reverse.

[Scott Morrison]

Indeed, after the transition to Lean4 I think we're hoping for a separate "standard library" that comes before mathlib, and perhaps we will actually aspire to emptying the data directory: everything about data structures per se will be in the standard library, and whatever remains can be categorised by mathematical topic in mathlib.

[Arthur Paulino]

@Kyle Miller thanks for the return! I think we can move on to this thread now

[Arthur Paulino]

Looking at how far that branch already is, I thought of the following subareas:

• shortest path theorems
• minimum cut
• maximum flow
• arriving at minimum cut and maximum flow duality

Of course, you might have a clearer idea on the next steps since you've been doing such a fine job on this branch for quite a while already. I want to try something but I'm all ears.

[Kyle Miller]

Regarding the location of graphs in the library -- given your topic about complexity theory, maybe you're interested in formalizing algorithms about graphs? I sort of think about the combinatorics graphs as being like the abstract interface (in the Java sense), where they don't have a concrete implementation. The data of a simple_graph is just a relation without any promise of computability (unless you have [decidable_rel G.adj]). You'd probably want reasonably efficient ways to represent a simple_graph for questions about complexity, and those might more on the data side of things.

[Arthur Paulino]

Hm, I guess I'd like to follow the flow of proving theorems with definitions without having to implement the mechanics of the algorithms just yet. Where do you see the simple_graph project moving towards?

[Kyle Miller]

Those all seem like interesting things to work on! Maybe for now feel free to use the walks_and_trees branch, adding some new files.

[Arthur Paulino]

Alright, just wanted to know. I will try a few things locally first before requesting the permission to write on branches. I wanna make sure I can lift some weights beforehand.

[Kyle Miller]

For simple_graph, one goal has been trying to implement all the basic stuff from the first few pages of Bollobas's textbook on graph theory, and trying to do so with an eye toward avoiding too much code duplication between, for example, simple graphs, multigraphs, labeled multigraphs, etc.

[Kyle Miller]

For flows of a simple graph, this might be a reasonable starting definition:

structure preflow {V : Type*} (G : simple_graph V) (α : Type*) [has_zero α] [has_neg α] :=
(weight : V → V → α)
(adj_of_nonzero : ∀ v w, weight v w ≠ 0 → G.adj v w)
(neg : ∀ v w, -weight v w = weight w v)

This supports having $A$-flows for any abelian group $A$. It's just missing conditions about what ∑ (w : V), weight v w is.

[Arthur Paulino]

Hm, maybe talking about shortest paths wrt non-weighted graphs would be a closer next step?

[Arthur Paulino]

Not sure if such theorems are very (re)usable tho.

[Kyle Miller]

Maybe directed graphs would be better for things about flows, but here's a definition for flows in an undirected graph:

import combinatorics.simple_graph.basic
import algebra.big_operators.basic
import data.real.basic

open_locale big_operators

structure flow {V : Type*} [fintype V]
  (G : simple_graph V) (cap : sym2 V → ℝ) (s t : V) :=
(weight : V → V → ℝ)
(adj_of_ne : ∀ v w, weight v w ≠ 0 → G.adj v w)
(neg : ∀ v w, -weight v w = weight w v)
(conserve : ∀ v, v ≠ s → v ≠ t → ∑ (w : V), weight v w = 0)
(cap_constraint : ∀ v w, abs (weight v w) ≤ cap ⟦(v, w)⟧)

Each edge has a capacity, and the flow for that edge can go in either direction so long as it's within the capacity.

This is also an option, allowing the capacity to be different for flows in each direction:

structure flow {V : Type*} [fintype V]
  (G : simple_graph V) (cap : V → V → ℝ) (s t : V) :=
(weight : V → V → ℝ)
(for_edges : ∀ v w, weight v w ≠ 0 → G.adj v w)
(neg : ∀ v w, -weight v w = weight w v)
(conserve : ∀ v, v ≠ s → v ≠ t → ∑ (w : V), weight v w = 0)
(cap_constraint : ∀ v w, weight v w ≤ cap v w)

[Kyle Miller]

Arthur Paulino said:

Not sure if such theorems are very (re)usable tho.

If anything, you'd probably create useful supporting lemmas along the way.

[Arthur Paulino]

Now I understood what you meant by "avoiding too much code duplication". You're using the simple_graph structure to extend onto other structures

[Arthur Paulino]

I will let you know of any updates :+1:

[Kyle Miller]

It might also be nice splitting up the definition into the "relative 1-cycle" part (i.e., the part having to do with Kirkhoff's law for currents where certain nodes are allowed to be current sources/sinks) and the capacity part. This can also be generalized to infinite graphs, so long as every vertex has only finitely many neighbors (i.e., it's locally finite).

/-- A relative 1-cycle with coefficients in an abelian group. -/
structure rel_cycle {V : Type*} (G : simple_graph V) [G.locally_finite] (W : set V)
  (α : Type*) [add_comm_group α] :=
(weight : V → V → α)
(adj_if : ∀ v w, weight v w ≠ 0 → G.adj v w)
(neg : ∀ v w, -weight v w = weight w v)
(conserve : ∀ v, ¬v ∈ W → ∑ w in G.neighbor_finset v, weight v w = 0)

/-- A real-valued relative 1-cycle with bounded weights with only two boundary vertices. -/
structure flow {V : Type*} (G : simple_graph V) [G.locally_finite]
  (cap : V → V → ℝ) (s t : V) extends rel_cycle G {s, t} ℝ :=
(cap_constraint : ∀ v w, weight v w ≤ cap v w)

[Kyle Miller]

1-cycles themselves form an abelian group, the rank of which is an important invariant for graphs (it's the minimum number of edges you have to remove to get a forest).

[Yakov Pechersky]

Also, just because git status says your branch is up to date doesn't mean you don't have changes. By that I mean unsaved changes. Edited unsaved files earlier in the import tree still cause recompilation of themselves and dependent files.

[Yakov Pechersky]

If they are open in your vscode and your extension settings are the default ones.

[Arthur Paulino]

@Kyle Miller Lean is not accepting append_support'' nor append_support' on my machine (connectivity.lean lines 462 to 488).

lemma append_support'' {u v w : V} (p : G.walk u v) (p' : G.walk v w) :
  ((p.append p').support : multiset V) = {u} + p.support.tail + p'.support.tail :=
begin
  rw [append_support, ←multiset.coe_add],
  congr' 1,
  simp only [multiset.singleton_eq_singleton, multiset.cons_coe,
    zero_add, multiset.coe_eq_coe, multiset.cons_add],
  rw [←support_eq],
end

lemma append_support' [decidable_eq V] {u v w : V} (p : G.walk u v) (p' : G.walk v w) :
  ((p.append p').support : multiset V) = p.support + p'.support - {v} :=
begin
  rw append_support,
  cases p',
  { simp only [nil_support, list.tail_cons, list.append_nil],
    convert_to _ = (p.support + ([v] - {v}) : multiset V),
    { erw multiset.add_sub_cancel,
      simp, },
    { nth_rewrite 0 ←add_zero (p.support : multiset V),
      rw add_left_cancel_iff,
      simp, }, },
  { simp_rw [cons_support, list.tail_cons, ←multiset.cons_coe, ←multiset.singleton_add],
    rw [add_comm, add_assoc, add_comm],
    erw multiset.add_sub_cancel,
    rw [←multiset.coe_add, add_comm], },
end

On the former, it's failing to apply simp and on the later the second simp ends up with unsolved goals. Was this under your radar?

[Arthur Paulino]

Okay I fixed a few things. I wanna push to a different branch before merging so you can see my modifications first because these are my first changes to mathlib files.

[Arthur Paulino]

https://github.com/leanprover-community/mathlib/pull/9983 A PR to merge my branch into yours.
You said that I could push commits directly to your branch if I added new files. But in this case I made changes to files that you wrote so I'm more comfortable opening a PR into your branch this time around (I don't want to mess things up).

[Kyle Miller]

For those kinds of changes (fixing proofs, changing names, and the like), feel free to commit straight to the branch. (And thanks for finding a way to simplify one of the proofs! I wouldn't mind if you did that for more of the proofs; many still have things like non-terminal simps.)

I haven't seen using PRs targeting non-master branches before for mathlib, and I'm not sure how it will interact with the existing PR due to my lack of experience. Will squash-and-merge effectively just add a single commit to the walks_and_trees branch?

[Yaël Dillies]

Yeah, such PR are fine but pretty rare. People usually rather go through a PR-like process behind the scenes.

[Arthur Paulino]

Okay since you've already reviewed the changes and approved them (on this chat), I'm gonna accept the PR and merge my branch into yours

[Arthur Paulino]

Kyle Miller said:

I haven't seen using PRs targeting non-master branches before for mathlib, and I'm not sure how it will interact with the existing PR due to my lack of experience. Will squash-and-merge effectively just add a single commit to the walks_and_trees branch?

Yeah that's precisely it. It's just a way of coordinating collaboration so you know exactly what I'm changing instead of having to read it on a tight git diff terminal interface

[Arthur Paulino]

But sure, I can be more straightforward and commit directly on your branch :+1:

[Kyle Miller]

(I don't mind reviewing your changes if you prefer PRing.)

[Arthur Paulino]

Interesting, I've just found out about this GitHub feature: compare.
If you go to https://github.com/leanprover-community/mathlib/compare you can pick two branches as if you wanted to merge one into the other and the diff will be shown in a PR-styled way. Example: comparing walks_and_trees with master:
https://github.com/leanprover-community/mathlib/compare/master...walks_and_trees

But it doesn't allow commentaries etc, which make sense

[Arthur Paulino]

Kyle Miller said:

(I don't mind reviewing your changes if you prefer PRing.)

Thanks :big_smile:
Yeah I feel safer that way

[Arthur Paulino]

According to this definition, trees and spanning trees are the same for us, right?

/-- A *tree* is a connected acyclic graph. -/
def is_tree : Prop := G.connected ∧ G.is_acyclic

[Kyle Miller]

A spanning tree is a G' : subgraph G that satisfies G'.is_spanning and G'.coe.is_tree (docs#simple_graph.subgraph.coe to turn the subgraph into a graph.) It's probably more convenient to use G'.spanning_coe.is_tree, which doesn't introduce a subtype for the vertices.

Another way to formalize spanning trees, probably even more convenient, is as a G' : simple_graph V such that G' ≤ G and G'.is_tree. The type simple_graph V has a boolean algebra structure from comparing edge sets, and G' ≤ G means G' is a spanning subgraph of G.

[Arthur Paulino]

Ah, wait, I got confused. The concept of "Spanning tree" is that we can compute the spanning tree of a connected graph

[Kyle Miller]

This (or some variation on it) would be nice to have:

theorem exists_spanning_tree (G : simple_graph V) (h : G.connected) :
  ∃ G', G' ≤ G ∧ G'.is_tree :=
sorry

[Kyle Miller]

This is a noncomputable version, allowing for V to be infinite. The argument that comes to mind uses Zorn's lemma applied to acyclic graphs G' ≤ G.

[Arthur Paulino]

Nice. I'm trying to figure out a way to state that the number of edges of a finite tree is equal to the number of vertices minus 1

[Arthur Paulino]

But I'm not even being able to write it as a lemma and have Lean accept it

[Arthur Paulino]

This is not the right lemma, but I'm getting an error.

lemma asd : G.is_tree → G.edge_finset.card = 1 := sorry

The error is:

failed to synthesize type class instance for
V : Type u,
G : simple_graph V,
_inst_1 : decidable_eq V,
ᾰ : G.is_tree
⊢ fintype V

[Kyle Miller]

That's saying you don't have the assumption that V is finite. Add [fintype V] as an argument to asd.

[Kyle Miller]

I guess you need [decidable_eq V] [fintype V] [decidable_rel G.adj] to use G.edge_finset.

[Kyle Miller]

(This should be changed actually. G.edge_finset should just need [fintype G.edge_set]. Or maybe it should be removed, since all it does is make it a little easier to write G.edge_set.to_finset.)

[Arthur Paulino]

[fintype V] [decidable_rel G.adj] did the job, thanks!

Question: I see that some proofs use assumptions introduced with {...} and others use [...]. What's the difference?

[Kyle Miller]

https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/set.2Efinite.2Efintype/near/249577393

[Kyle Miller]

https://leanprover.github.io/reference/expressions.html#implicit-arguments

[Bryan Gin-ge Chen]

Chapter 10 of #tpil is a good reference on how type classes (related to the square brackets) work in Lean 3.

[Arthur Paulino]

lemma asd [fintype G.edge_set]: G.is_tree → G.edge_set.to_finset.card = 1 := sorry is accepted :+1:

[Arthur Paulino]

I will get back to the introduction of spanning trees once I figure this one out. Now I need to express the cardinality of V. Let me struggle a little

[Kyle Miller]

That's fintype.card V if you've got [fintype V]

[Kyle Miller]

(it's common to add an open fintype line so you can just write card V)

[Arthur Paulino]

Is this too astray?

open fintype

lemma is_tree_then_card_edges_le_card_vertices
  [fintype G.edge_set] [fintype V] : G.is_tree → card G.edge_set < card V :=
begin
  sorry
end

lemma is_tree_then_not_card_edges_le_card_vertices_minus_one
  [fintype G.edge_set] [fintype V] [nonempty V]: G.is_tree → ¬ card G.edge_set < card V - 1 :=
begin
  sorry
end

/-
the strategy is to use the lemmas above and nat.eq_of_lt_succ_of_not_lt in order to
achieve equality
-/
lemma is_tree_then_card_edges_eq_card_vertices_minus_one
  [fintype G.edge_set] [fintype V] [nonempty V] : G.is_tree → card G.edge_set = card V - 1 :=
begin
  intro h,
  have hle := is_tree_then_card_edges_le_card_vertices _ h,
  have hnle := is_tree_then_not_card_edges_le_card_vertices_minus_one _ h,
  sorry
end

[Arthur Paulino]

Maybe an induction on the number of vertices works better

[Kyle Miller]

It would be possible to prove it using an induction principle for trees (though I'm not sure exactly how I'd want to formulate it).

Another option is more direct. Given a tree, choose an arbitrary root $v$. Let $W=V\setminus v$. For every $w\in W$, there is a unique path from $w$ to $v$ (see tree_path); let $e(w)$ denote the first edge in this path. This function $e$ is surjective (given an edge, you should be able to use is_rootward_antisymm to show it's the image of one of its endpoints) and it is injective (same lemma or thereabouts). Since this is a bijection, we get an equality of the cardinalities of the edge set and of $W$.

[Arthur Paulino]

Will take a closer look at your approach tomorrow. I'm feeling a bit fried after some hours trying to translate my thoughts into Lean.

I've started this draft PR, also including some adjustments you requested on the previous PR that I couldn't see in time:
https://github.com/leanprover-community/mathlib/pull/9993

[Kyle Miller]

The coercions here are a bit hairy, but maybe you can try filling in the sorries (assuming I set things up right):

def next_edge : ∀ (v w : V) (h : v ≠ w) (p : G.walk v w), G.incidence_set v
| v w h walk.nil := (h rfl).elim
| v w h (@walk.cons _ _ _ u _ hvw _) := ⟨⟦(v, u)⟧, hvw, sym2.mk_has_mem _ _⟩

lemma is_tree_then_card_edges_eq_card_vertices_minus_one
  [fintype G.edge_set] [fintype V] [nonempty V] (h : G.is_tree) :
  card G.edge_set = card V - 1 :=
begin
  have root := classical.arbitrary V,
  rw ←set.card_ne_eq root,
  let f : {v | v ≠ root} → G.edge_set,
  { intro v,
    let a := next_edge (v : V) root v.property (G.tree_path h v root : G.walk v root),
    -- convert the term of incidence_set to an edge_set; there's probably a nicer way
    exact ⟨_, a.property.1⟩, },
  have fprop : ∀ (v : V) (hv : v ≠ root), ↑(f ⟨v, hv⟩) ∈ G.incidence_set v,
  { intros v hv,
    dsimp [f],
    generalize : next_edge _ _ _ _ = e,
    exact e.property, },
  have finj : function.injective f,
  { sorry, },
  have fsurj : function.surjective f,
  { sorry, },
  exact (card_of_bijective ⟨finj, fsurj⟩).symm,
end

(Small warning: I'm not sure how much more code is needed to fill them in.)

[Arthur Paulino]

It's not accepting v as an input of next_edge:

type mismatch at application
  next_edge ↑v
term
  ↑v
has type
  V : Type u
but is expected to have type
  simple_graph ?m_1 : Type ?

[Johan Commelin]

Do you need next_edge _ v? With an extra underscore?

[Johan Commelin]

Maybe simple_graph _ shouldn't be an explicit argument of next_edge?

[Arthur Paulino]

The extra underscore before v worked, but I don't understand what you meant by simple_graph _ being an argument of next_edge

[Kevin Buzzard]

@Arthur Paulino if you read the error message you can see it says "you know where you put v? I was expecting you to put a simple graph", and if you hover over next_edge you can see all the inputs it expects and in what order, so you can confirm that indeed the first input to that function is supposed to be a simple graph

[Kevin Buzzard]

Do you understand about () and {} inputs to functions? (Edit -- and [] inputs) That's what Johan is talking about

[Johan Commelin]

@Arthur Paulino I guess you have variables (foobar : simple_graph V) somewhere above the definition of next_edge. I don't know much about the graph theory library, but maybe that should be [simple_graph V].

[Arthur Paulino]

I'm gonna do some reading on that subject

[Kevin Buzzard]

The _ means "Lean please work out yourself what this input should be"

[Kevin Buzzard]

But a more cunning choice of brackets will mean that you don't even need to put the _

[Kevin Buzzard]

Inputs in () brackets are supplied by the user, unless the user gives lean _ which puts the ball back into its court. Inputs in {} brackets are supplied by lean's unification system so the user skips them, and inputs in [] brackets are supplied by lean's type class inference system so the user skips them too.

[Kevin Buzzard]

Right now your error was giving lean a vertex when it wanted a simple graph, the suggested fix was to give it _ but another fix would be to change the type of bracket

[Arthur Paulino]

Right now your error was giving lean a vertex when it wanted a simple graph

If that's the error, then I think it's not just about the brackets. There's a logical error because we want V to be the vertices of a simple_graph G. So elements of V, such as v, shouldn't be of type simple_graph

[Kevin Buzzard]

You can read the error, and it is what it is. I am not suggesting that v should have type simple_graph! I am however suggesting that Lean wanted something of type simple_graph where you put a v, and this is of your own making (because of your choice of brackets).

[Kevin Buzzard]

If you post a #mwe with the error I can try and explain my point more clearly (apart from the fact that I'm about to go to a meeting)

[Arthur Paulino]

Yeah I copied/pasted Kyle's code and now I'm trying to catch up with his line of thought :sweat_smile:. I'm still crawling in Lean so I don't think I can spot a MWE that manifests this error.
But you're not the first one that mentions the possibility of improving the way that the assumptions are denoted (implicitly/explicitly) so that's definitely something to take into consideration as an improvement.

[Kevin Buzzard]

I'm asking if you could simply paste your fully (almost) working file with the error, so I don't have to go back over the entire thread and cut and paste all the parts together.

[Arthur Paulino]

Let me try

[Arthur Paulino]

import combinatorics.simple_graph.basic

variables {V : Type u} (G : simple_graph V)

/-- A walk is a sequence of adjacent vertices.  For vertices `u v : V`,
the type `walk u v` consists of all walks starting at `u` and ending at `v`.

We say that a walk *visits* the vertices it contains.  The set of vertices a
walk visits is `simple_graph.walk.support`. -/
@[derive decidable_eq]
inductive walk : V → V → Type u
| nil {u : V} : walk u u
| cons {u v w: V} (h : G.adj u v) (p : walk v w) : walk u w

attribute [refl] walk.nil

def next_edge : ∀ (v w : V) (h : v ≠ w) (p : G.walk v w), G.incidence_set v
| v w h walk.nil := (h rfl).elim
| v w h (@walk.cons _ _ _ u _ hvw _) := ⟨⟦(v, u)⟧, hvw, sym2.mk_has_mem _ _⟩

lemma is_tree.card_edges_eq_card_vertices_sub_one'
  [fintype G.edge_set] [fintype V] [nonempty V] (h : G.is_tree) :
  card G.edge_set = card V - 1 :=
begin
  have root := classical.arbitrary V,
  rw ←set.card_ne_eq root,
  let f : {v | v ≠ root} → G.edge_set,
  { intro v,
    let a := next_edge (v : V) root v.property (G.tree_path h v root : G.walk v root),
    -- convert the term of incidence_set to an edge_set; there's probably a nicer way
    exact ⟨_, a.property.1⟩, },
  have fprop : ∀ (v : V) (hv : v ≠ root), ↑(f ⟨v, hv⟩) ∈ G.incidence_set v,
  { intros v hv,
    dsimp [f],
    generalize : next_edge _ _ _ _ = e,
    exact e.property, },
  have finj : function.injective f,
  { sorry, },
  have fsurj : function.surjective f,
  { sorry, },
  exact (card_of_bijective ⟨finj, fsurj⟩).symm,
end

[Kevin Buzzard]

This file doesn't work for me.

[Kevin Buzzard]

What branch of mathlib are you on? And there are universe issues.

[Arthur Paulino]

The branch is called more_on_trees. I've just pushed a commit. The file is src/combinatorics/simple_graph/connectivity.lean

[Arthur Paulino]

The lemma starts at line 1251

[Kevin Buzzard]

There are errors on that branch for me, in files imported by the file you're working on. This can cause unexpected issues.

[Kevin Buzzard]

But despite these issues I think I've seen enough to be able to say something coherent.

[Kevin Buzzard]

Unfortunately I can't get next_edge compiling either on your branch or on master.

[Kevin Buzzard]

But the definition mentions G and G is a variable which depends on V, so the actual type of next_edge will be something like next_edge : \forall {V : Type u} (G : simple_graph V), ∀ (v w : V) (h : v ≠ w) (p : G.walk v w), G.incidence_set

[Arthur Paulino]

Yeah Kyle introduced the definition of next_edge just today, here on Zulip

[Kevin Buzzard]

And the reason that V is in {} brackets and G is in () brackets is because of the variables {V : Type u} (G : simple_graph V) line

[Kevin Buzzard]

The brackets for the next_edge variables correspond to the brackets used in the variables command earlier.

[Kevin Buzzard]

So the first user-provided input for next_edge needs to be a term of type simple_graph V

[Kevin Buzzard]

and then the second and third inputs are two terms of type V etc etc

[Kevin Buzzard]

And so the error you get is correct, because of the choice of brackets in the variables line.

[Kevin Buzzard]

Johan suggested making them [] but it seems that simple_graph is a structure not a class, which means that the designers have left open the possibility that you might want to consider more than one structure of a simple graph on a fixed vertex type V. As a result the type class inference system does not know about simple_graph so [] brackets won't work.

[Kevin Buzzard]

The other possibility is that you change (G : simple_graph V) into {G : simple_graph V} and in this case you'll be asking the unification system to fill in the variable for you. This could well work, because now my guess for what next_edge will want to eat is first two elements v,w of V, then a proof that v!=w, and finally a term p of type G.walk v w, and once Lean sees this term it will be able to look at its type and guess what G was, as the term G is mentioned in the type of p, and this is exactly the sort of thing which the unification system does. So I suspect that changing (G : simple_graph V) to {G : simple_graph V} on the variables line (or, if this variables line is on line 10 of the code and you're looking at line 1000, writing a new line variable {G} just above the definition of next_edge) will be another way of fixing the error you were seeing (other than adding in the _).

[Arthur Paulino]

It worked :D
I'm learning the syntax slowly. For instance, it's not clear to me why the first parameter of next_edge is a simple_graph.
When I read

def next_edge : ∀ (v w : V) (h : v ≠ w) (p : G.walk v w), G.incidence_set v
| v w h walk.nil := (h rfl).elim
| v w h (@walk.cons _ _ _ u _ hvw _) := ⟨⟦(v, u)⟧, hvw, sym2.mk_has_mem _ _⟩

just by checking the matches I see four inputs (like v w h walk.nil)

[Kevin Buzzard]

Yes but you also see V and G, right? Where are they coming from?

[Kevin Buzzard]

That's what variables do for you -- they are automatically added as inputs to any function which mentions them by name.

[Kevin Buzzard]

They're not there when the function is defined, but when you use the function you have to supply them

[Kevin Buzzard]

The | magic is supplying them, but if you do #check @next_edge just after the definition, or hover over it in a place where it's used in a theorem, you'll see the extra inputs.

[Arthur Paulino]

Will Lean4 work like this too?

[Kevin Buzzard]

Yup

[Arthur Paulino]

Okay then I better get used to it. I think it's a bit hard on the reader but I see how it speeds up writing

[Kyle Miller]

Sorry for the confusion I've seemed to cause with the code I posted. I had written it at the end of src/combinatorics/simple_graph/connectivity.lean in the walks_and_trees branch right before the final end simple_graph, so the full context was variables {V : Type u} {G : simple_graph V} [decidable_eq V] in the simple_graph namespace.

[Kyle Miller]

It looks like errors in imports are from someone helpfully merging master to bring the branch up to date, but this introduced some small errors. (@Arthur Paulino if you want to fix them, in subgraph.lean look for the couple cases of sym := and replace them with symm :=. I think that's it.)

[Arthur Paulino]

Nice. I had replaced some occurrences of sym by symm but I seem to have overlooked two of them

[Anupam Nayak]

Declaring variables actually makes it easier for the reader too, if used properly. If you're working on something where you have 10 theorems, all about some 3 or 4 variables, then having to read the same arguments in each theorem is cumbersome. Separating out the common variables makes it clear to the reader that the next few theorems are all about these variables.

Even in maths we do this a lot when we say "let X, Y be topological spaces, f a continuous function from X to Y, yada yada, theorem 1... theorem n"

[Yaël Dillies]

That someone being me :exhausted:

[Arthur Paulino]

@Kyle Miller I was also trying to make this definition a bit clearer:

def next_edge : ∀ (v w : V) (h : v ≠ w) (p : G.walk v w), G.incidence_set v
| v w h walk.nil := (h rfl).elim
| v w h (@walk.cons _ _ _ u _ hvw _) := ⟨⟦(v, u)⟧, hvw, sym2.mk_has_mem _ _⟩

Do you think it's worth the effort?

[Arthur Paulino]

What does mem stand for?

[Kyle Miller]

next_edge would be better if G were an explicit argument, but it doesn't make the definition clearer. I'm not sure it could be made simpler.

By doubling the amount of code, you can split off the proof of incidence from the edge the function outputs:

def next_edge (G : simple_graph V) : ∀ (v w : V) (h : v ≠ w) (p : G.walk v w), sym2 V
| v w h walk.nil := (h rfl).elim
| v w h (@walk.cons _ _ _ u _ hvw _) := ⟦(v, u)⟧

lemma next_edge_mem_incidence_set (v w : V) (h : v ≠ w) (p : G.walk v w) :
  G.next_edge v w h p ∈ G.incidence_set v :=
begin
  cases p,
  { exact (h rfl).elim },
  { exact ⟨by assumption, sym2.mk_has_mem _ _⟩, }
end

[Kyle Miller]

mem is used in a name for ∈

[Arthur Paulino]

this is the current diff: https://github.com/leanprover-community/mathlib/pull/9993/files

[Arthur Paulino]

If I have e: ↥(G.edge_set), how to get the vertices that compose e?

[Yaël Dillies]

e.1 gives you an edge. From there it's a good exercise to define what you want. There are several ways to do it.

[Kevin Buzzard]

I guess e.val will have type sym2 V so look at the API for sym2 by right clicking on it

[Kevin Buzzard]

oh hmm it's a quotient. You could use quotient.out I guess

[Yaël Dillies]

If you don't find what you want, don't worry but do tell us. The API for sym2 is currently crap and we have plans to improve it.

[Arthur Paulino]

I think it's better to explain the strategy I'd apply if I were to prove it in a undergrad course, then I can use some help on translating my intent to Lean.

This is my current state:

V: Type u
G: simple_graph V
_inst_1: decidable_eq V
_inst_2: fintype ↥(G.edge_set)
_inst_3: fintype V
_inst_4: nonempty V
h: G.is_tree
root: V
f: ↥{v : V | v ≠ root} → ↥(G.edge_set) := λ (v : ↥{v : V | v ≠ root}), ⟨↑(next_edge ↑v root _ ↑(G.tree_path h ↑v root)), _⟩
fprop: ∀ (v : V) (hv : v ≠ root), ↑(f ⟨v, hv⟩) ∈ G.incidence_set v
finj: function.injective f
e: ↥(G.edge_set)
⊢ ∃ (a : ↥{v : V | v ≠ root}), f a = e

That is, I need to prove that given an edge e of a tree G and a root vertex root, I can retrieve a as the furthest vertex that composes e

[Arthur Paulino]

f is a function that returns the last edge on a path from root to a given vertex

[Arthur Paulino]

My intuition is to take e1 and e2 as the vertices that compose e and apply f to them. Either f(e1) or f(e2) will result in e

[Arthur Paulino]

The proof wouldn't be complete because I'd need to prove that last sentence. My struggle is to translate my thoughts into Lean

[Kyle Miller]

Yaël Dillies said:

The API for sym2 is currently crap and we have plans to improve it.

Where's this sentiment coming from? It certainly has everything necessary for this (though of course things can always be improved.)

[Yaël Dillies]

Doing SRL :stuck_out_tongue_closed_eyes:

[Yaël Dillies]

Bhavik identified two stupid lemmas which made our life much easier. But we still ended up not using sym2 anymore (well, except for the intrinsically simple_graphpart).

[Kyle Miller]

@Arthur Paulino One way to do this is this incantation: cases e with e he, refine quotient.ind (λ p, _) e, cases p with v w,

[Kyle Miller]

Oh, wait, that doesn't generalize a variable correctly.

[Kyle Miller]

Maybe cases e with e he, induction e using quotient.ind, cases e with v w,

[Kyle Miller]

I could have sworn there was a sym2.ind that we added, but I guess it was just sym2.lift

[Yaël Dillies]

We have sym2.ind in branch#szemeredi

[Arthur Paulino]

Now I need to take the furthest one (between v and w) from root

[Arthur Paulino]

I'm gonna spend a few hours here: https://leanprover.github.io/reference/tactics.html

[Bryan Gin-ge Chen]

Some info on that page might be out of date. I suspect you'd be better off reading the corresponding chapter of TPiL and referring to our tactic docs as needed.

[Kyle Miller]

Here's sort of what I was imagining for surjectivity:

def next_edge (G : simple_graph V) : ∀ (v w : V) (h : v ≠ w) (p : G.walk v w), G.incidence_set v
| v w h walk.nil := (h rfl).elim
| v w h (@walk.cons _ _ _ u _ hvw _) := ⟨⟦(v, u)⟧, hvw, sym2.mk_has_mem _ _⟩

lemma nonempty_path_not_loop {v : V} {e : sym2 V} (p : G.path v v)
  (h : e ∈ walk.edges (p : G.walk v v)) : false :=
begin
  cases p with p hp,
  cases p,
  { exact h, },
  { cases hp,
    simpa using hp_support_nodup, },
end

lemma eq_next_edge_if_mem_path {u v w : V}
  (hne : u ≠ v) (hinc : ⟦(u, w)⟧ ∈ G.incidence_set u)
  (p : G.path u v) (h : ⟦(u, w)⟧ ∈ (p : G.walk u v).edges) :
  G.next_edge u v hne p = ⟨⟦(u, w)⟧, hinc⟩ :=
begin
  cases p with p hp,
  cases p,
  { exact (hne rfl).elim },
  { cases hp,
    simp at hp_support_nodup,
    simp only [next_edge, subtype.mk_eq_mk, subtype.coe_mk],
    congr,
    simp only [list.mem_cons_iff, subtype.coe_mk, simple_graph.walk.cons_edges, sym2.eq_iff] at h,
    cases h,
    { obtain (⟨_,rfl⟩|⟨rfl,rfl⟩) := h; refl, },
    { have h := walk.mem_support_of_mem_edges _ h,
      exact (hp_support_nodup.1 h).elim, }, },
end

lemma is_tree_then_card_edges_eq_card_vertices_minus_one
  [fintype G.edge_set] [fintype V] [nonempty V] (h : G.is_tree) :
  card G.edge_set = card V - 1 :=
begin
  have root := classical.arbitrary V,
  rw ←set.card_ne_eq root,
  let f : {v | v ≠ root} → G.edge_set := λ v,
    ⟨G.next_edge v root v.property (G.tree_path h v root),
     G.incidence_set_subset _ (subtype.mem _)⟩,
  have fprop : ∀ (v : V) (hv : v ≠ root), ↑(f ⟨v, hv⟩) ∈ G.incidence_set v,
  { intros v hv,
    dsimp only [f, subtype.coe_mk],
    apply subtype.mem, },
  have finj : function.injective f,
  { sorry, },
  have fsurj : function.surjective f,
  { intro e,
    cases e with e he,
    induction e using quotient.ind,
    cases e with v w,
    cases is_rootward_or_reverse h root he with hr hr,
    { use v,
      rintro rfl, -- goal is equivalently v ≠ root; substitute v for root
      dsimp only [is_rootward] at hr,
      exact nonempty_path_not_loop _ hr.2,
      cases hr,
      simp only [f],
      erw eq_next_edge_if_mem_path _ ⟨he, _⟩ _ hr_right; simp, },
    { sorry, -- do the same thing again. use wlog?
    }, },
  exact (card_of_bijective ⟨finj, fsurj⟩).symm,
end

[Kyle Miller]

With the right lemmas, this could be a lot cleaner. I'm also not sure if going through is_rootward_or_reverse and using the definition of is_rootward is the best way, but at least it works.

[Arthur Paulino]

eq_next_edge_if_mem_path is not being accepted

[Arthur Paulino]

invalid field notation, function 'simple_graph.next_edge' does not have explicit argument with type (simple_graph ...)

[Kyle Miller]

Note that I changed the definition of next_edge to include G as an explicit argument

[Arthur Paulino]

Oh, ok
Now it failed to instantiate goal with v on the use tactic

[Arthur Paulino]

brb

[Arthur Paulino]

Alright, had to do some tweaks, but I was able to finish up surjection:

def next_edge (G : simple_graph V) : ∀ (v w : V) (h : v ≠ w) (p : G.walk v w), G.incidence_set v
| v w h walk.nil := (h rfl).elim
| v w h (@walk.cons _ _ _ u _ hvw _) := ⟨⟦(v, u)⟧, hvw, sym2.mk_has_mem _ _⟩

lemma nonempty_path_not_loop {v : V} {e : sym2 V} (p : G.path v v)
  (h : e ∈ walk.edges (p : G.walk v v)) : false :=
begin
  cases p with p hp,
  cases p,
  { exact h, },
  { cases hp,
    simpa using hp_support_nodup, },
end

lemma eq_next_edge_if_mem_path {u v w : V}
  (hne : u ≠ v) (hinc : ⟦(u, w)⟧ ∈ G.incidence_set u)
  (p : G.path u v) (h : ⟦(u, w)⟧ ∈ (p : G.walk u v).edges) :
  G.next_edge u v hne p = ⟨⟦(u, w)⟧, hinc⟩ :=
begin
  cases p with p hp,
  cases p,
  { exact (hne rfl).elim },
  { cases hp,
    simp at hp_support_nodup,
    simp only [next_edge, subtype.mk_eq_mk, subtype.coe_mk],
    congr,
    simp only [list.mem_cons_iff, subtype.coe_mk, simple_graph.walk.cons_edges, sym2.eq_iff] at h,
    cases h,
    { obtain (⟨_,rfl⟩|⟨rfl,rfl⟩) := h; refl, },
    { have h := walk.mem_support_of_mem_edges _ h,
      exact (hp_support_nodup.1 h).elim, }, },
end

lemma is_tree.card_edges_eq_card_vertices_sub_one
  [fintype G.edge_set] [fintype V] [nonempty V] (h : G.is_tree) :
  card G.edge_set = card V - 1 :=
begin
  have root := classical.arbitrary V,
  rw ←set.card_ne_eq root,
  let f : {v | v ≠ root} → G.edge_set := λ v,
    ⟨G.next_edge (v : V) root v.property (G.tree_path h v root : G.walk v root),
     G.incidence_set_subset _ (subtype.mem _)⟩,
  have fprop : ∀ (v : V) (hv : v ≠ root), ↑(f ⟨v, hv⟩) ∈ G.incidence_set v,
  { intros v hv,
    dsimp only [f, subtype.coe_mk],
    apply subtype.mem, },
  have finj : function.injective f,
  { intros v₁ v₂,

    sorry, },
  have fsurj : function.surjective f,
  { intro e,
    cases e with e he,
    induction e using quotient.ind,
    cases e with e₁ e₂,
    cases is_rootward_or_reverse h root he with hr hr,
    { use e₁,
      rintro rfl,
      dsimp only [is_rootward] at hr,
      exact nonempty_path_not_loop _ hr.2,
      cases hr,
      have key := eq_next_edge_if_mem_path _ _ _ hr_right,
      { simp only [f],
        erw key,
        simp [sym2.eq_swap]},
      { simpa [sym2.eq_swap]}, },
    { use e₂,
      rintro rfl,
      dsimp only [is_rootward] at hr,
      exact nonempty_path_not_loop _ hr.2,
      cases hr,
      have key := eq_next_edge_if_mem_path _ _ _ hr_right,
      { simp only [f],
        erw key,
        simp [sym2.eq_swap], },
      { simpa [he]}, }, },
  exact (card_of_bijective ⟨finj, fsurj⟩).symm,
end

[Kyle Miller]

Nice. By the way, I modified my comment shortly after posting it with some minor proof simplifications in the surjection proof

[Kyle Miller]

Any reason you changed it to cases e with e₁ e₂? This splits e into two vertices, so naming-wise either v w or v₁ v₂ seem potentially better.

[Arthur Paulino]

hm, I wanted to use something different than v. Maybe w suits better

[Arthur Paulino]

or u₁ u₂?

[Arthur Paulino]

I'm gonna try to use your optimized solution to prove it for the other vertex

[Kyle Miller]

There's also wlog since the two cases are basically the same except for permuting the vertices, but it gives a very slow proof:

  have fsurj : function.surjective f,
  { intro e,
    cases e with e he,
    induction e using quotient.ind,
    cases e with u₁ u₂,
    wlog := is_rootward_or_reverse h root he using [u₁ u₂],
    { use u₁,
      rintro rfl,
      dsimp only [is_rootward] at case,
      exact nonempty_path_not_loop _ case.2,
      cases case,
      simp only [f],
      erw eq_next_edge_if_mem_path _ ⟨he, _⟩ _ case_right; simp, },
    obtain ⟨p, hp⟩ := this (G.symm he),
    use p,
    simp [hp, sym2.eq_swap], },

[Arthur Paulino]

Slow in terms of processing? Like it's more time consuming?

[Arthur Paulino]

have fsurj : function.surjective f,
  { intro e,
    cases e with e he,
    induction e using quotient.ind,
    cases e with u₁ u₂,
    cases is_rootward_or_reverse h root he with hr hr,
    { use u₁,
      rintro rfl,
      dsimp only [is_rootward] at hr,
      exact nonempty_path_not_loop _ hr.2,
      cases hr,
      simp only [f],
      erw eq_next_edge_if_mem_path _ ⟨he, _⟩ _ hr_right; simp [he]},
    { use u₂,
      rintro rfl,
      dsimp only [is_rootward] at hr,
      exact nonempty_path_not_loop _ hr.2,
      cases hr,
      simp only [f],
      erw eq_next_edge_if_mem_path _ ⟨_ , _⟩ _ hr_right; simp [he, sym2.eq_swap], }, },

[Arthur Paulino]

okay I'm gonna push this version to my branch

[Arthur Paulino]

@Kyle Miller I was thinking yesterday about the function f you defined inside the proof and I realized that f being (or not) surjective and injective is closely related with the definition of trees. That is, if f is not surjective then there's a pair of vertices that are not reachable from the root. And if if is not injective, then there is a cycle in G. Do you think this approach could be clearer?
For the injection, at least, I'd want to try a proof by contradiction by finding a cycle. What do you think?

[Arthur Paulino]

Branch updated!
https://github.com/leanprover-community/mathlib/pull/9993
Please let me know what you think :rocket:

[Kyle Miller]

That approach would definitely work (for non-injectivity, it would be nice if there were a way to construct a cycle from f somewhat directly, by iteratively applying it to the opposite vertex across the output edge, but that would take some more work to develop).

Something I forgot to mention is that is_rootward_or_reverse and is_rootward_antisymm do these kinds of cycle argument already, and I figured it might save some work to use them. However, it would be a good exercise to not use them, for both you and for the library (to help see what's missing).

[Arthur Paulino]

Yeah I'm trying as hard as I can to translate the logic inside my mind into Lean. The proof by cycle construction seems to be going okay, unless I've set myself for some very hard intermediate proof that I can't see right now. From your perspective, do you see a trap like that in my code? I mean, is any of those sorrys that I inserted super hard for my current level?

[Arthur Paulino]

Okay, 1 sorry down. 1 sorry left

[Kyle Miller]

What you're doing seems doable (if perhaps all a bit of a trial by fire :smile: but you seem to be fine with that!).

I wanted to check my suggestion to use is_rootward_antisymm actually panned out, so I went ahead and proved injectivity with it. It'd be better if you kept going with your approach, so don't let this spoiler-tagged-code stop you.

Here's a utility lemma that may or may not be helpful to you:

lemma next_edge_mem_edges (G : simple_graph V) (v w : V) (h : v ≠ w) (p : G.walk v w) :
  (G.next_edge v w h p : sym2 V) ∈ p.edges :=
begin
  cases p with p hp,
  { exact (h rfl).elim },
  { simp only [next_edge, list.mem_cons_iff, walk.cons_edges, subtype.coe_mk],
    left,
    refl,},
end

lemma is_tree_then_card_edges_eq_card_vertices_minus_one
  [fintype G.edge_set] [fintype V] [nonempty V] (h : G.is_tree) :
  card G.edge_set = card V - 1 :=
begin
  have root := classical.arbitrary V,
  rw ←set.card_ne_eq root,
  let f : {v | v ≠ root} → G.edge_set := λ v,
    ⟨G.next_edge v root v.property (G.tree_path h v root),
     G.incidence_set_subset _ (subtype.mem _)⟩,
  have fprop : ∀ (v : V) (hv : v ≠ root), ↑(f ⟨v, hv⟩) ∈ G.incidence_set v,
  { intros v hv,
    dsimp only [f, subtype.coe_mk],
    apply subtype.mem, },
  have finj : function.injective f,
  { rintros ⟨u₁, h₁⟩ ⟨u₂, h₂⟩,
    by_cases hne : u₁ = u₂,
    { subst u₂,
      simp, },
    simp only [subtype.mk_eq_mk, subtype.coe_mk],
    generalize he₁ : G.next_edge _ _ _ _ = e₁,
    generalize he₂ : G.next_edge _ _ _ _ = e₂,
    cases e₁ with e₁ heu₁,
    cases e₂ with e₂ heu₂,
    simp only [subtype.coe_mk],
    rintro rfl,
    cases heu₁ with heu₁_edge heu₁_adj,
    cases heu₂ with heu₂_edge heu₂_adj,
    simp only [subtype.coe_mk] at heu₁_adj heu₂_adj,
    have e_is : e₁ = ⟦(u₁, u₂)⟧,
    { induction e₁ using quotient.ind,
      cases e₁ with v₁ w₁,
      simp only [sym2.mem_iff] at heu₁_adj heu₂_adj,
      obtain (rfl|rfl) := heu₁_adj;
      obtain (rfl|rfl) := heu₂_adj;
      try { exact (hne rfl).elim };
      simp [sym2.eq_swap], },
    subst e₁,
    apply is_rootward_antisymm h root,
    { split,
      exact heu₂_edge,
      convert G.next_edge_mem_edges _ _ h₁ _,
      simp, erw he₁, refl, },
    { split,
      exact G.symm heu₂_edge,
      convert G.next_edge_mem_edges _ _ h₂ _,
      simp, erw he₂, simp [sym2.eq_swap], }, },
  have fsurj : function.surjective f,
  { intro e,
    cases e with e he,
    induction e using quotient.ind,
    cases e with u₁ u₂,
    wlog := is_rootward_or_reverse h root he using [u₁ u₂],
    { use u₁,
      rintro rfl,
      dsimp only [is_rootward] at case,
      exact nonempty_path_not_loop _ case.2,
      cases case,
      simp only [f],
      erw eq_next_edge_if_mem_path _ ⟨he, _⟩ _ case_right; simp, },
    obtain ⟨p, hp⟩ := this (G.symm he),
    use p,
    simp [hp, sym2.eq_swap], },
  exact (card_of_bijective ⟨finj, fsurj⟩).symm,
end

[Kyle Miller]

Now that next_edge exists, it would probably be better to redefine next_edge and is_rootward so there's less of an impedance mismatch. Too much of the proof seems to be moving data around to put things into or out of a form that works for the definition of is_rootward.

[Kyle Miller]

(This part of the branch is much more experimental -- I'd wanted to see whether there was already enough stuff to be able to come up with some definition for is_rootward that satisfied lemmas is_rootward_antisymm and is_rootward_or_reverse.)

[Kyle Miller]

Another way this argument could have been organized is to define two functions parent child : G.edge_set -> V when given a root. These functions give the structure of the rooted tree, and e = ⟦(parent e, child e)⟧ for all e (modulo coercions). Then you'd show that child is injective, and its image is the set of non-root vertices. Taking cardinalities, you get the result.

[Arthur Paulino]

Hm, I got stuck on that part. I was able to build a circuit but I'm not seeing how I can prove that the graph is not acyclic

[Kyle Miller]

Maybe the proof of is_rootward_or_reverse might have some hint. walk.to_path is a way to turn a walk into a path, so that's a way to get a cycle from a circuit.

[Arthur Paulino]

I got the cycle but I don't know how to say "here's the cycle, G is not acyclic"

[Arthur Paulino]

have has_cycle : ¬G.is_acyclic,
let cycle := (walk.to_path circuit : G.walk u₁ u₁),

[Kyle Miller]

Oh, I led you down a bad path, sorry. That defines the empty path -- walk.to_path will delete everything since there's only one path from a vertex to itself.

[Kyle Miller]

It might be easier applying lemma is_acyclic_iff : G.is_acyclic ↔ ∀ (v w : V) (p q : G.path v w), p = q. If you intro your goal, you get a G.is_acyclic hypothesis, which you can rw with this lemma.

[Kyle Miller]

Then you can specialize it to the two paths you built your circuit from. I'm not sure if this is the best way, but you should be able to get that either u1 or u2 is equal to root, which is a contradiction.

[Arthur Paulino]

I'm not being able to break down g

u₁_root_u₂: G.walk u₁ u₂ := ↑(G.tree_path h u₁ root).append ↑(G.tree_path h u₂ root).reverse
u₁_u₂: G.path (u₁, u₂).fst (u₁, u₂).snd := path.singleton e_prop
u₂_u₁: G.path u₂ u₁
circuit: G.walk u₁ u₁ := u₁_root_u₂.append ↑u₂_u₁
g: u₁_root_u₂.to_path = u₁_u₂
⊢ false

[Arthur Paulino]

This is so close!

[Arthur Paulino]

Okay I need another cue :sweat_smile:
after this one I'm gonna go to the very basics. I'm sure I will understand a lot more

[Arthur Paulino]

Ah, I actually found an issue with my plan. Because of the way circuits are defined, a circuit can be something like u -> v -> w -> v -> u

[Arthur Paulino]

Which doesn't even contain a cycle

[Arthur Paulino]

@Kyle Miller feel free to hit the merge button if you think everything is okay:
https://github.com/leanprover-community/mathlib/pull/9993/files

[Arthur Paulino]

@Kyle Miller feel free to hit the merge button if you think everything is okay:
https://github.com/leanprover-community/mathlib/pull/9993/files

[Arthur Paulino]

There's something strange about our branches. A lot of things break when I merge master into them :thinking:

[Yaël Dillies]

What kind of stuff? Some of it might might my fault.

[Arthur Paulino]

Hm, we can go slowly. First, simple_graph/adj_matrix is not working on more_on_trees

[Arthur Paulino]

It doesn't work on walks_and_trees either. But this PR (walks_and_trees into master) is open and without broken tests:
https://github.com/leanprover-community/mathlib/pull/8737

[Arthur Paulino]

more_on_trees contains fixes for walks_and_trees. So if we can get more_on_trees it to work, this PR will fix walks_and_trees

[Arthur Paulino]

Long story short, can you help me fix more_on_walks? :smile:

[Yaël Dillies]

Let's have a look!

[Yaël Dillies]

Wait 10-15min, I'm onto something else right now.

[Arthur Paulino]

Np, I'm investigating these merges a little further

[Arthur Paulino]

2 months ago this line was added. but nowadays, R cannot be found anymore

[Arthur Paulino]

Back then, this was the line that introduced R (a semiring)

[Yaël Dillies]

Don't worry too much, this happens all the time. You write something, then someone comes along and changes the variables and bem your branch broke.

[Arthur Paulino]

But... how come can they merge something if their changes break other parts of the code?

[Arthur Paulino]

Shouldn't the build test fail?

[Yury G. Kudryashov]

CI ensures that master branch still compiles. It doesn't care about other branches.

[Yury G. Kudryashov]

So, if you work on a feature in a branch and merge master, then quite possibly your code will break.

[Arthur Paulino]

Ah, so it's really a matter of other branches becoming old/deprecated with time

[Yaël Dillies]

@Arthur Paulino, did you push all your changes? I can try to bump now.

[Arthur Paulino]

Yeap, more_on_trees is up to date on GitHub too

[Arthur Paulino]

after those fixes on adj_matrix.lean I'm gonna try to merge master into it

[Yaël Dillies]

I'm doing that now.

[Arthur Paulino]

Thanks!

[Kyle Miller]

If the way the PR to another branch works is that it does a squash merge, won't that make it very difficult to see what Arthur's changes were? Maybe the destination branch should be updated to master, too?

[Yaël Dillies]

Yeah, the best thing would have been to fix those problems while in walks_and_trees

[Arthur Paulino]

There's the "blame" visualization mode on GitHub. We can use that if we want to see who did what

[Kyle Miller]

Since it's a squash, I think everything that changes from merging master will be blamed on you, Arthur

[Arthur Paulino]

Oh, you mean on master

[Arthur Paulino]

On master it's gonna be blamed on you because I opened a PR into your branch

[Kyle Miller]

I mean on walks_and_trees. I like having somewhat nice commit histories on branches so that I can track what's changed while working.

[Kyle Miller]

If your PR is what updates walks_and_trees to master, then there will be this massive commit that mixes what you did with everything that's happened to mathlib, and it will list you as the author. (This doesn't matter for the history of master, since it will all be squashed again.)

[Arthur Paulino]

Makes sense. I should have started doing those fixes on walks_and_trees

[Kyle Miller]

I suspect all that needs to be done is to make sure to merge master on walks_and_trees, then merge walks_and_trees into more_on_trees, and then when the PR is merged, things will be OK.

[Arthur Paulino]

I can cherry pick changes from Yael and make small pushes on your branch if he's already started the merging process

[Arthur Paulino]

@Yaël Dillies have you?

[Kyle Miller]

I don't think you need to do that -- this merging plan should be sufficient, and it shouldn't create any conflicts.

[Yaël Dillies]

I'm doing exactly what Kyle just described.

[Arthur Paulino]

Perfect

[Arthur Paulino]

Next time I do fixes, I'm gonna do on the branch I branched out from and then merge it into mine afterwards

[Kyle Miller]

Perhaps a surprising thing about git is that every commit is actually a complete snapshot of the entire repository (along with pointers to the commits it's based on). All the diffs you see in the UI are just computed on the fly from these complete snapshots. I'm just trying to make sure there's a commit on walks_and_trees that already has a post-merge-master state so that when more_on_trees is merged, the diff that git computes will make more sense.

[Yaël Dillies]

I've fixed connectivity and adj_matrix. Is there any file file you noticed that was broken?

[Yaël Dillies]

All fixed!

[Kyle Miller]

You really threaded the needle there with all of your comma removal, somehow avoiding a merge conflict. :clap:

[Kyle Miller]

Do you know why adj_matrix_pow_apply_eq_card_walk needs semiring now?

[Yaël Dillies]

Yeah, I was expecting some horrendous thing going on!

[Yaël Dillies]

What did it need before?

[Yaël Dillies]

I suspect that what happened is that a variables [semiring R] got removed.

[Kyle Miller]

Oh right, adj_matrix was generalized to def adj_matrix [has_zero α] [has_one α]

[Kyle Miller]

Thanks @Arthur Paulino for getting this to happen

lemma is_tree.card_edges_eq_card_vertices_sub_one
  [fintype G.edge_set] [fintype V] [nonempty V] (h : G.is_tree) :
  card G.edge_set = card V - 1

[Arthur Paulino]

I kicked it off, but you were the one actually paving the way :D

[Arthur Paulino]

Thanks a lot Yaël for the merges!

[Kyle Miller]

Hopefully eventually we'll have the matrix-tree theorem, too, which at its core relates any $(n-1)\times(n-1)$ minor of the Laplacian matrix to the set of all tree-like functions f : {v | v ≠ root} → G.edge_set.

[Yaël Dillies]

This sounds like it should say

lemma is_tree.card_edges [fintype V] (h : G.is_tree) :
  G.edge_finset.card = card V - 1 :=

[Yaël Dillies]

[fintype G.edge_set] should come from [fintype V] and [nonempty V] is useless.

[Kyle Miller]

I sort of want to abolish G.edge_finset since it's just G.edge_set.to_finset.

The reason [fintype G.edge_set] is there is because, while it is derived from [fintype V], it's better to have it take an arbitrary proof of finiteness rather than requiring it to take the one derived from [fintype V].

[Yaël Dillies]

Ah yeah because it shows up in the statement.

[Kyle Miller]

It's true that nonempty V is not necessary because of truncating subtraction.

[Yaël Dillies]

I strongly disagree to removing edge_finset. It's very useful but I think it could be redefined.

[Yaël Dillies]

It's actually just a matter of changing.to_finset with univ.filter becaus you assume a fintype anyway.

[Kyle Miller]

edge_finset definitely should be redefined -- right now it requires [fintype V] which is very restrictive. The definition is using the instance that says [fintype G.edge_set] from [fintype V].

[Arthur Paulino]

This line requires [nonempty V], doesn't it?
have root := classical.arbitrary V,

[Yaël Dillies]

In SRL, we talk a lot about edge_finset (even if to be fair it's hidden under one definition so never actually see it).

[Yaël Dillies]

Arthur Paulino said:

This line requires [nonempty V], doesn't it?
have root := classical.arbitrary V,

My point is that the final statement doesn't require it. so you can case-split on is_empty V/nonempty V, prove the trivial stuff in the first case, and go on with your existing proof in the second case.

[Yaël Dillies]

And for SRGs, Alena definitely needed edge_finset.

[Kyle Miller]

I think the reason edge_finset exists is that we didn't realize we could write G.edge_set.to_finset, judging by its definition. It also makes summations over the edge set look nicer, but it's mostly cosmetic.

[Yaël Dillies]

Maybe we can change the assumptions to [fintype (G.neighbors_set u)] [fintype (G.neighbors_set v)]?

[Kyle Miller]

Here's a question: is the empty graph a tree? Right now the definition allows empty graphs to be trees, but that doesn't seem right.

[Kyle Miller]

@Arthur Paulino A good exercise would be to remove the [nonempty V] assumption, if you want to do that.

[Arthur Paulino]

Sure I'm gonna try it

[Kyle Miller]

docs#is_empty_or_nonempty

[Yaël Dillies]

Is there thing akin to docs#tactic.nontriviality which would automatically perform the cache update and the goal discharge?

[Kyle Miller]

You'll also have to figure out how to show the cardinality of the edge set is 0 if V is empty. Maybe write that as a separate lemma, like

lemma simple_graph.edge_set_empty_of_empty [is_empty V] : ¬G.edge_set.nonempty := sorry

[Arthur Paulino]

Yaël Dillies said:

Is there thing akin to docs#tactic.nontriviality which would automatically perform the cache update and the goal discharge?

Do you mean this one? https://leanprover-community.github.io/mathlib_docs/logic/nontrivial.html#tactic.interactive.nontriviality

[Kyle Miller]

@Yaël Dillies I think casesI would work?

[Arthur Paulino]

@Kyle Miller do you agree with this name change?

This sounds like it should say

lemma is_tree.card_edges [fintype V] (h : G.is_tree) :
  G.edge_finset.card = card V - 1 :=

[Arthur Paulino]

To me it sounds more like the name of a function that would return the cardinality of the set of edges of a tree :thinking:
But of course, my experience in this subject is super short

[Mauricio Collares]

Kyle Miller said:

Here's a question: is the empty graph a tree? Right now the definition allows empty graphs to be trees, but that doesn't seem right.

Of course this is debatable, but typically empty sets are not connected. For the graph case, this means the empty graph is not a tree (but it is a forest with zero trees, of course).

[Arthur Paulino]

Within my (shallow) understanding, making use of a subtraction that truncates at zero to prove such lemma for empty trees sounds a bit hacky. Because, semantically, the right side of the equality (n - 1) doesn't make sense to me

[Arthur Paulino]

Unless, of course, we have a reason (besides pure generality) to make it true for empty trees as well

[Kyle Miller]

is_tree.card_edge_finset would be a better name than is_tree.card_edges. I agree removing the nonempty V assumption is hacky, but if it's only a few extra lines in the proof it's nice when you can eliminate assumptions.

[Kyle Miller]

It also might not be a hack if G.is_tree comes with the fact that V is nonempty, for instance by modifying G.is_connected to include this hypothesis.

[Arthur Paulino]

Okay that makes sense to me. I'm gonna try and see if I can do it

[Arthur Paulino]

@Kyle Miller It took longer than I expected, but I got it to work!
https://github.com/leanprover-community/mathlib/pull/10053

[Arthur Paulino]

Also @Yaël Dillies :point_up:

[Arthur Paulino]

Hey @Yury G. Kudryashov, after your proposed changes this was the only proof I couldn't adjust:

lemma is_tree_iff : G.is_tree ↔ nonempty V ∧ ∀ (v w : V), ∃!(p : G.walk v w), p.is_path :=
begin
  simp only [is_tree, is_acyclic_iff],
  split,
  { rintro ⟨hc, hu, hne⟩,
    use hne,
    intros v w,
    let q := (hc v w).some.to_path,
    use q,
    simp only [true_and, path.path_is_path],
    intros p hp,
    specialize hu v w ⟨p, hp⟩ q,
    rw ←hu,
    refl, },
  { rintro ⟨hne, h⟩,
    refine ⟨_, _, hne⟩,
    { intros v w,
      obtain ⟨p, hp⟩ := h v w,
      use p, },
    { rintros v w ⟨p, hp⟩ ⟨q, hq⟩,
      simp only [p, hp, q, hq],
      exact unique_of_exists_unique (h v w) hp hq, }, },
end

[Arthur Paulino]

It's failing to apply the very first simp

[Eric Rodriguez]

the issue is that is_tree is now a structure, so it's not definitionally equal to the ands from before

[Eric Rodriguez]

here's a working version:

lemma is_tree_iff : G.is_tree ↔ nonempty V ∧ ∀ (v w : V), ∃!(p : G.walk v w), p.is_path :=
begin
  split,
  { rintro ⟨hc, hu, hne⟩,
    rw is_acyclic_iff at hu,
    refine ⟨hne, λ v w, _⟩,
    let q := (hc v w).some.to_path,
    use q,
    simp only [true_and, path.path_is_path],
    intros p hp,
    specialize hu v w ⟨p, hp⟩ q,
    rw ←hu,
    refl, },
  { rintro ⟨hne, h⟩,
    refine ⟨_, _, hne⟩,
    { intros v w,
      obtain ⟨p, hp⟩ := h v w,
      use p, },
    { rw is_acyclic_iff,
      rintros v w ⟨p, hp⟩ ⟨q, hq⟩,
      simp only [p, hp, q, hq],
      exact unique_of_exists_unique (h v w) hp hq, }, },
end

note that I changed the use/intros into a refine, which is a very nice tactic. it's also strictly stronger than split! (although annoyingly, it gets confused when you try to do a rintro in it... so for example refine ⟨λ ⟨hc, hu, hne⟩, _, λ ⟨hne, h⟩, _⟩ doesn't work, but if it did it'd be the sameas the split and the two rintros you do after

[Arthur Paulino]

Thank you very much!

[Arthur Paulino]

Another thing... The lint tests are failing. I tried to fix those but I couldn't figure it out.

[Eric Rodriguez]

don't worry about them, they're not in your part of the code

[Eric Rodriguez]

also, I know you've put in all this work on this, but it may be worth keeping the "weaker" empty option available (as mathematically boring as it is); I think this is common in mathlib, with things like docs#is_preconnected (so maybe is_pretree?) because a lot of results end up holding for the weaker class anyways

[Arthur Paulino]

Hm, I'd rather leave it for later decisions since we're not sure whether we need that generalization starting from a definition of "preconnectedness" in the context of graphs

[Arthur Paulino]

I'd say time will tell. Let's see how the need evolves

[Arthur Paulino]

Plus I'm not so sure how I'd go about that generalization with the definition of "pretrees". I gave it a little go and I ended up having to redefine a lot of things in terms of "pretree", like pretree_path and pretree_dist, which seemed very odd to me :thinking:

[Arthur Paulino]

What if we just allow empty trees and add the nonempty restrictions on lemmas that require such? In other words, simply ignore my most recent PR?

[Kevin Buzzard]

I think the idea of letting "pre-trees" be forests such that there's a path between any two vertices is fine, and then just define a tree to be a nonempty pretree.

[Kevin Buzzard]

there are a bunch of standard theorems about primes which are true for preprimes (i.e. primes and 1), e.g. p divides ab implies p divides a or p divides b

[Kyle Miller]

Right now, a forest is just an acyclic graph (and it has no definition of its own since G.is_acyclic exists), and a tree is a connected acyclic graph. The definition of G.is_connected is that there's a walk between every pair of vertices. If anything, it should be G.is_connected that should require that there be at least one vertex.

The way this probably should work is the definition of connected be changed to "there exists a vertex v such that for every vertex w there is a walk from v to w."

[Kyle Miller]

This is the same as saying that the quotient of V by the G.walk relation is a singleton.

[Arthur Paulino]

But then how would we structure it? Have the definition of trees that requires connectivity and define a forest as an union of trees?

[Kyle Miller]

I'm suggesting that the definition of connectivity be changed, and leave is_tree alone. A forest is just an acyclic graph, so there's nothing to change there.

[Kyle Miller]

Unfortunately, this makes the different theorems for what G.is_tree is equivalent to to be more awkward, but maybe they don't have to be equivalences.

[Arthur Paulino]

Today I merged master into walks_and_trees again and solved some lint errors

[Arthur Paulino]

@Kyle Miller Is this what you mean?
https://github.com/leanprover-community/mathlib/pull/10082

[Arthur Paulino]

Line 1244 is not working and I don't know how to proceed there. Probably related to what you've said about dropping the equivalence

[Kyle Miller]

Kyle Miller said:

The way this probably should work is the definition of connected be changed to "there exists a vertex v such that for every vertex w there is a walk from v to w."

def connected : Prop := ∃ (u : V), ∀ (v : V), G.reachable u v

[Kyle Miller]

and then something like

lemma connected_iff_nonempty_and_pairwise_reachable :
  G.connected ↔ nonempty V ∧ ∀ (u v : V), G.reachable u v :=
begin
  sorry
end

[Kyle Miller]

I haven't given much thought to the effects of this, though. The nonempty V ∧ ∀ (u v : V), G.reachable u v definition is potentially nicer (note that in the definition you gave, nonempty V is inside the forall).

[Arthur Paulino]

Oops, I better remove it from the forall.

[Arthur Paulino]

The definition I gave is more "symmetrical", I think

[Arthur Paulino]

And it changes less things

[Arthur Paulino]

Okay, I got some progress there

[Scott Morrison]

I think we already have at least 2 or 3 pairs of definitions is_preconnected and is_connected in mathlib, where is_connected is just is_preconnected + nonempty. You should do that too!

[Arthur Paulino]

Got the definition of preconnected in :+1:
@Kyle Miller I wasn't able to prove connected_of_edge_connected but everything else is working. Feel free to take over branch change-connectivity-def before accepting this PR (which merges change-connectivity-def into yours)

[Arthur Paulino]

And I'm closing this PR since we're going for the change of definition of connected instead

[Arthur Paulino]

@Kyle Miller I've updated https://github.com/leanprover-community/mathlib/pull/10082 with your ideas but I couldn't make connected_of_edge_connected work

[Arthur Paulino]

(the proof is written in a way that I can't understand at the moment)

[Yakov Pechersky]

Do you remember what the definition of connected used to be before?

[Arthur Paulino]

Yeah

def connected : Prop := ∀ (u v : V), G.reachable u v

[Yakov Pechersky]

It was an and. So I used and.imp_right, since connected was preconnected AND nontrivial V and edge_connected _ _ _ _ was connected _ , which was _ AND nontrivial V. So the right hand side of the assumption implies the right hand side of the goal. That's the and.imp_right shortcut.

[Yakov Pechersky]

Not exactly, that's what preconnected is.

[Yakov Pechersky]

Now that connected is a structure, and not a plain and conjunction, you can't use and.elim_right anymore.

[Yakov Pechersky]

With the new definition, here's a place to start:

lemma connected_of_edge_connected {k : ℕ} (hk : 0 < k) (h : G.edge_connected k) : G.connected :=
{ preconnected := _,
  nonempty := _ }

[Arthur Paulino]

I see, but I think it's the writing style (I've very new to Lean). So far I've only been able to understand steps explicitly separated by commas

[Kyle Miller]

I think the and.imp_right proof might be more obfuscated than just terse, so don't feel bad about not being able to follow it.

[Arthur Paulino]

begin
  split,
  rw preconnected,
  intros u v,
  rw reachable,
end

leaves me at

V: Type u
G: simple_graph V
k: ℕ
hk: 0 < k
h: G.edge_connected k
uv: V
⊢ nonempty (G.walk u v)
V: Type u
G: simple_graph V
k: ℕ
hk: 0 < k
h: G.edge_connected k
⊢ nonempty V

[Kyle Miller]

I'm having a hard time modifying the one-liner, but here's away to modify the original one:

lemma preconnected_of_edge_connected {k : ℕ} (hk : 0 < k) (h : G.edge_connected k) :
  G.preconnected :=
begin
  intros v w,
  have h' := (h ∅ (by simp) (by simp [hk])).preconnected v w,
  simp only [finset.coe_empty, subgraph.delete_edges_of_empty] at h',
  cases h',
  exact ⟨h'.map (subgraph.map_spanning_top _)⟩,
end

Have another lemma nonempty_of_edge_connected, then put them together for connected_of_edge_connected.

[Yakov Pechersky]

lemma connected_of_edge_connected {k : ℕ} (hk : 0 < k) (h : G.edge_connected k) : G.connected :=
let C' := h ∅ (by simp) (by simp [hk]) in
{ preconnected := by simpa using C'.preconnected,
  nonempty := C'.nonempty }

[Yakov Pechersky]

If you want to reuse the old proof. Really, there should be a connected.antimono or however you name it, saying that if a "supergraph" is connected, so is an induced subgraph.

[Yakov Pechersky]

The original proof was pretty terse too =), I just followed the style

[Arthur Paulino]

Alright, PR updated. I'm gonna spend a few hours tomorrow figuring out what you guys wrote. But feel free to merge it into walks_and_trees if you see fit :+1:
https://github.com/leanprover-community/mathlib/pull/10082

Or, of course, just push commits directly to change-connectivity-def

[Yakov Pechersky]

Right now I'm having issues extracting the reachable Prop out of the quot. I'm clumsy with that API. If I have the following state, what's the right quot API?

V: Type u
G: simple_graph V
_inst_1: unique G.connected_component
h: nonempty V
v: V
w: V
this: G.connected_component_of v = G.connected_component_of w
⊢ G.reachable v w

[Kyle Miller]

(preconnected_of_edge_connected is now unnecessary given Yakov's connected_of_edge_connected)

[Kyle Miller]

@Yakov Pechersky I'm not sure if you can apply it directly, but docs#quotient.eq should be a way to do something with this given reachable_is_equivalence/reachable_setoid

[Yakov Pechersky]

Ah, something with docs#quot.exact maybe?

[Kyle Miller]

The nice thing about the quotient ones (like docs#quotient.exact) is that they give it in terms of the original relation, rather than eqv_gen. Maybe this is a hole in the quot api? having variants for when you can supply an explicit setoid?

[Yakov Pechersky]

Right, but even quotient.* ask for the setoid to be an implicit arg

[Kyle Miller]

example [unique G.connected_component] [h : nonempty V] (v w : V)
  (this: G.connected_component_of v = G.connected_component_of w) :
  G.reachable v w :=
@quotient.exact _ G.reachable_setoid _ _ this

[Kyle Miller]

quotient seems to be designed around having a canonical setoid instance for a given type, but there are times when you want potentially many.

[Kyle Miller]

It would be nice if there were a quot.exact' or something that explicitly took this setoid instance, and then quotient.exact could be defined in terms of it.

[Yakov Pechersky]

@[simp] lemma equivalence.eqv_gen_iff {α : Type*} {r : α → α → Prop} (h : equivalence r) {x y : α} :
  eqv_gen r x y ↔ r x y :=
begin
  refine ⟨λ H, _, eqv_gen.rel _ _⟩,
  induction H,
  { assumption },
  { exact h.left _ },
  { exact h.right.left ‹_› },
  { exact h.right.right ‹_› ‹_› }
end

lemma connected_component_of.reachable_congr {v w : V}
  (h : G.connected_component_of v = G.connected_component_of w) : G.reachable v w :=
by simpa [reachable_is_equivalence] using quot.exact _ h

[Kyle Miller]

setoid might not be right since it bundles the relation -- rather, if quot.exact' took an equivalence proof.

[Yakov Pechersky]

Which gives the following too:

@[reducible]
def quot.is_empty {α : Type*} (p : α → α → Prop) [is_empty α] :
  is_empty (quot p) :=
⟨λ a, quot.induction_on a (λ a', is_empty_elim a')⟩

instance connected_component.is_empty_of_is_empty [is_empty V] :
  is_empty G.connected_component :=
quot.is_empty _

lemma connected_of_unique [unique G.connected_component] : G.connected :=
begin
  casesI is_empty_or_nonempty V,
  { exact is_empty_elim (default G.connected_component) },
  { exact ⟨λ _ _, connected_component_of.reachable_congr (subsingleton.elim _ _), ‹_›⟩ }
end

[Kyle Miller]

If eqv_gen is really the best interface to quot given an equivalence relation, I'd suggest

lemma _root_.eqv_gen.of_eqv {α : Type*} {r : α → α → Prop} (h : equivalence r) {x y : α}
  (H : eqv_gen r x y) : r x y :=
begin
 induction H,
 { assumption },
 { exact h.left _ },
 { exact h.right.left ‹_› },
 { exact h.right.right ‹_› ‹_› }
end

lemma connected_component_of.reachable_congr {v w : V}
  (h : G.connected_component_of v = G.connected_component_of w) : G.reachable v w :=
(quot.exact _ h).of_eqv G.reachable_is_equivalence

If namespaces worked out, it would also be nice with flipped arguments, so that the proof is G.reachable_is_equivalence.of_eqv_gen (quot.exact _ h)

[Kyle Miller]

eqv_gen_iff would be nice to have, too

[Kevin Buzzard]

Arthur Paulino said:

begin
  split,
  rw preconnected,
  intros u v,
  rw reachable,
end

leaves me at

V: Type u
G: simple_graph V
k: ℕ
hk: 0 < k
h: G.edge_connected k
u v: V
⊢ nonempty (G.walk u v)
V: Type u
G: simple_graph V
k: ℕ
hk: 0 < k
h: G.edge_connected k
⊢ nonempty V

@Arthur Paulino maybe you don't need this now, but here's how to do that nonempty goal from earlier: if you look at the definition of nonempty then you can see that the constructor is called nonempty.intro, so exact nonempty.intro u should do it.

[Arthur Paulino]

@Kevin Buzzard makes sense, thanks!

[Arthur Paulino]

@Kyle Miller do you think the PR needs more adjustments before merging?

[Arthur Paulino]

/-- The list of edges in a walk are all edges of the graph.
It is written in this form to avoid unsightly coercions. -/
lemma edges_subset_edge_set {u v : V} (p : G.walk u v) {e : sym2 V}
  (h : e ∈ p.edges) : e ∈ G.edge_set

Hm, this isn't really what we mean, is it? Wouldn't it be more like "Every edge in a walk is an edge of the graph"?

[Kyle Miller]

Are you talking about the comment? Less weird is "Every edge in a walk's edge list is an edge of the graph." The point of this comment is to remind the reader why it's not p.edges ⊆ G.edge_set, and that's because p.edges : list (sym2 V) rather than set (sym2 V).

[Arthur Paulino]

Yeah, about the comment

[Kyle Miller]

(Please feel free to clarify that comment in the source. You can delete it and start over.)

[Arthur Paulino]

Hi! I'm trying to prove the lemma that says that the existence of a perfect matching implies that the cardinality of the vertices set is even. I've come to this point:

V: Type u
G: simple_graph V
_inst_1: fintype V
M: G.matching
_inst_2: fintype ↥(M.edges)
h: ∀ (v : V), ∃ (e : sym2 V), e ∈ M.edges ∧ v ∈ e
⊢ card V = 2 * card ↥(M.edges)

[Yaël Dillies]

I'd advise you to go by double counting the finset (univ : V × sym2 V).filter (λ ve, ve.1 ∈ ve.2)

[Johan Commelin]

Can you define an equiv V ≃ Σ e : M.edges, {v : V // v ∈ e}?

[Yaël Dillies]

Yeah, that's another way. Not sure it goes smoothly, though.

[Arthur Paulino]

I thought about double counting too because a vertex is in exactly one edge and an edge has exactly two vertices ( verytypical informal proof)

[Johan Commelin]

I suggest choose e he1 he2 using h as next tactic step.

[Kyle Miller]

This should follow from the degree-sum formula, right? Perfect matchings are certain kinds of subgraphs (this coercion is not implemented) and then you apply docs#simple_graph.sum_degrees_eq_twice_card_edges and use the fact that all the degrees are 1 for this subgraph.

[Kyle Miller]

If you want to do it yourself, I'd suggest using the map V -> sym2 V for the perfect matching that gets the edge associated to a vertex, show the image is M.edges, and show the map is 2-1 onto each element of M.edges.

[Kyle Miller]

(Somewhere I shared a link to a branch that contains more things about perfect matchings, when @Yaël Dillies asked very recently. I think it has this V -> sym2 V map.)

[Kyle Miller]

Matchings were added to mathlib before subgraphs were. It might be reasonable to redesign them as a graph M : simple_graph V satisfying M \leq G such that whenever M.adj v w and M.adj v w' then w = w'. We could define simple_graph.support of a graph to be {v : V | \exists w, G.adj v w}, and then a perfect matching is an M such that M.support = set.univ.

[Yaël Dillies]

Do you think we even want a standalone definition if we have k-factors?

[Kyle Miller]

If there are k-factors, then it would be good to have an interface for 1-factors something like this

[Kyle Miller]

though it would instead actually be terms of G.subgraph instead of terms of simple_graph V that are subgraphs.

[Kyle Miller]

Maybe make sure k-factors work for non-locally-finite graphs; the definition of matchings I gave doesn't depend on that assumption.

[Kyle Miller]

@Arthur Paulino if you want a relatively small thing to try PRing to mathlib itself, it could be defining the support of a simple_graph, which I don't think exists already. Maybe its definition could be def simple_graph.support (G : simple_graph V) : set V := rel.image G.adj set.univ, and then you'd have a simp lemma simple_graph.mem_support that says a vertex v is an element of G.support iff there exists a vertex w with G.adj v w. One other useful lemma (a corollary) would be that if G.adj v w for (v w : V) then v is an element of G.support.

[Arthur Paulino]

Yeah, all of a sudden this matching lemma became a redesigning task which I'm not sure I can handle without bugging too many people :sweat_smile:

[Arthur Paulino]

At least not yet

[Johan Commelin]

What is left? That goal state that you posted above?

[Johan Commelin]

That shouldn't require any redesigning.

[Johan Commelin]

With that choose line that I posted, it should be quite straightforward to build the equiv.

[Johan Commelin]

And then you can use fintype.card_congr and fintype.card_sigma. By then you should be in pretty good shape.

[Yaël Dillies]

Arthur Paulino said:

Yeah, all of a sudden this matching lemma became a redesigning task which I'm not sure I can handle without bugging too many people :sweat_smile:

Don't worry! I happen to need k-factors myself.

[Arthur Paulino]

@Kyle Miller I was able to prove the lemma with:

@[simp] lemma mem_support {v : V} : v ∈ G.support ↔ ∃ w, G.adj v w :=
begin
  simp only [support, rel.image],
  split,
  { intro h,
    choose w h using h,
    use w,
    cases h with _ h,
    rw adj_comm at h,
    use h, },
  { intro h,
    choose w h using h,
    use w,
    simp [h, adj_comm], }
end

But I notice some repeated structure for each split. Is it possible to optimize this proof?

[Arthur Paulino]

better:

@[simp] lemma mem_support {v : V} : v ∈ G.support ↔ ∃ w, G.adj v w :=
begin
  simp only [support, rel.image, adj_comm],
  split,
  { intro h,
    choose w h using h,
    use w,
    cases h with _ h,
    use h, },
  { intro h,
    choose w h using h,
    use w,
    simp [h], }
end

[Kyle Miller]

I think you might be able to do it in one line with rw [support, rel.mem_image, adj_comm]

[Kyle Miller]

(maybe simp only instead of rw)

[Kyle Miller]

Oh, you'll need set.mem_univ and maybe a couple others.

[Arthur Paulino]

Is it slower to add many arguments to simp only?
Another question, what's the difference between simp [a, b, ...] and simp only [a, b, c, ...]?

[Kyle Miller]

Without only, it additionally uses all lemmas marked with the @[simp] attribute. https://leanprover-community.github.io/extras/simp.html

[Arthur Paulino]

About the redesign you mentioned, isn't it a bit strange to define a matching as a subgraph? I mean, it's a subgraph that always contain all the vertices of the full graph

[Arthur Paulino]

I think it's more common in the literature to understand a matching as a subset of edges

[Kyle Miller]

This theorem, by the way, is strangely resisting squeeze_simp and simp?

[Arthur Paulino]

What do you mean?

[Kyle Miller]

And regarding formalization vs literature: combinatorics is a very intuitive subject, so things tend to be very informal because the gaps can be filled in easily. But a computer needs everything to be represented very precisely. It seems like many of the ways we might use matchings are very subgraph-like, so we may as well just represent them as subgraphs, without needing to create coercions back and forth between different representations.

Yael seems to be on it to define what k-factors are, and he was thinking of defining them as being subgraphs.

[Kyle Miller]

Arthur Paulino said:

What do you mean?

Ok:

@[simp] lemma mem_support {v : V} : v ∈ G.support ↔ ∃ w, G.adj v w :=
begin
  simp [support, rel.mem_image, adj_comm, set.mem_univ],
end

Replacing simp with squeeze_simp suggests this simp only:

@[simp] lemma mem_support {v : V} : v ∈ G.support ↔ ∃ w, G.adj v w :=
begin
  simp only [support, rel.mem_image, adj_comm, set.mem_univ, set.mem_univ, iff_self, exists_true_left],
  -- goal not closed
end

[Arthur Paulino]

Yeah as soon as I said it, I realized that spanning trees also have this characteristic of containing all vertices of the bigger graph and we might as well define them as subgraphs

[Arthur Paulino]

Wow that's indeed a 1-liner

[Kyle Miller]

There's a complexity already with simple graphs that there are two notions of a subgraph: G.subgraph for arbitrary ones and simple_graph V for spanning ones (where we take only those that are $\leq$).

[Arthur Paulino]

@[simp] lemma mem_support {v : V} : v ∈ G.support ↔ ∃ w, G.adj v w :=
  by simp [support, rel.image, adj_comm]

closed the goal here

[Kyle Miller]

docs#simple_graph.subgraph.spanning_coe is an attempt to connect up with this latter notion, and I expect to use G.support at some point for restricting a graph to a G.subgraph by removing degree-0 vertices.

[Kyle Miller]

This would be a little better:

@[simp] lemma mem_support {v : V} : v ∈ G.support ↔ ∃ w, G.adj v w :=
by simp [support, rel.mem_image, adj_comm]

It's better to use the "API" for definitions rather than unfolding them. The point of mem_support is to define the API for G.support so future users don't have to unfold it.

[Kyle Miller]

Actually, I'm not sure this should be a @[simp] lemma. It doesn't hurt, but it's unclear to me right now whether it will help simplify things. I guess leave it unless anyone has a reason it shouldn't be one.

[Arthur Paulino]

I can add it without @[simp] and then you can make it so if you see fit later

[Yakov Pechersky]

You might have a support_mono lemma that says G <= G' -> G.support <= G'.support, right?

[Arthur Paulino]

lemme try to get that in

[Yakov Pechersky]

Something something forgetful functor to Set

[Arthur Paulino]

type mismatch at application
  G ≤ G'
term
  G'
has type
  simple_graph W : Type v
but is expected to have type
  simple_graph V : Type u

G' wasn't defined as a subgraph of G here :thinking:

[Arthur Paulino]

This should go inside subgraph right?

[Kyle Miller]

This would be for (G G' : simple_graph V)

[Kyle Miller]

There's an ordering on simple graphs with the same vertex type based on edge containment

[Kyle Miller]

@Arthur Paulino For your proof earlier, you don't need to use choose, but you can rather use cases, rcases, or obtain since the goal is a proposition. choose is mainly useful for when you need to "actually" get a value out of an existential

[Yaël Dillies]

I would even add when you need to swap an exists and a forall.

[Arthur Paulino]

Got this one

lemma support_mono (H: simple_graph V) : H ≤ G → H.support ≤ G.support :=
begin
  intros h v hv,
  simp only [←is_subgraph_eq_le, is_subgraph] at h,
  rw mem_support at hv,
  choose w hw using hv,
  use w,
  simp [hw, h, adj_comm],
end

[Kyle Miller]

Two things, other than that looks good (though of course someone will golf it, it's inevitable): make sure to put a space after H, and please swap the roles of H and G in the lemma statement -- if you #check @support_mono you'll see that the arguments are (G H : simple_graph V). Another option is to edit your lemma so it says (H G : simple_graph V) since this will override the variables

[Kyle Miller]

I forgot a third thing: put (h : H ≤ G) as an argument before the colon, since you're introing it anyway.

[Arthur Paulino]

like this?

lemma support_mono (G' : simple_graph V) (h : G ≤ G') : G.support ≤ G'.support :=
begin
  intros v hv,
  rw [←is_subgraph_eq_le, is_subgraph] at h,
  rw mem_support at hv,
  cases hv with w hw,
  use w,
  simp [hw, h, adj_comm],
end

[Mario Carneiro]

probably G and G' should be implicit

[Mario Carneiro]

also space before after the <- although enforcement on that rule is pretty low

[Kyle Miller]

@Arthur Paulino so use {G G' : simple_graph V} as the argument instead

[Kyle Miller]

What rule's that about <-?

[Mario Carneiro]

i.e. rw [← is_subgraph_eq_le, is_subgraph] at h,

[Arthur Paulino]

done: https://github.com/leanprover-community/mathlib/pull/10176

[Arthur Paulino]

PR updated :+1:

[Arthur Paulino]

I'm attempting to formalize vertex coloring. do you guys think this is a good design?

structure vertex_coloring :=
(color : V → ℕ)
(valid : ∀ (v w : V), G.adj v w → color v ≠ color w)

def vertex_colors (C : G.vertex_coloring) := ...

[Yaël Dillies]

We already thought about it quite a lot.

[Mario Carneiro]

I would make the codomain of color a parameter

[Yaël Dillies]

@David Wärn used them without explicitly defining them for docs#combinatorics.line.exists_mono_in_high_dimension

[Yaël Dillies]

and @Alena Gusakov has a definition on a branch

[Yaël Dillies]

Either way, you'll want to use docs#pairwise

[Mario Carneiro]

@Yaël Dillies I don't think your example is a vertex coloring in @Arthur Paulino 's sense, Hales-jewett does not have any constraints on colors of adjacent vertices

[Yaël Dillies]

No, it doesn't. This is more of a contextual idea.

[Mario Carneiro]

it does reveal some ambiguity of the terminology though

[Arthur Paulino]

@Mario Carneiro do you mean like this?

structure vertex_coloring (color_type : Type u) :=
(color : V → color_type)
(valid : ∀ (v w : V), G.adj v w → color v ≠ color w)

def vertex_colors (color_type : Type u) (C : G.vertex_coloring color_type) := ...

[Mario Carneiro]

yes

[Arthur Paulino]

That was my first go but I found it a bit annoying to carry color_type everywhere. What can I do about it?

[Yaël Dillies]

Call it α :stuck_out_tongue:

[Arthur Paulino]

Ah, then explain in a docstring

[Mario Carneiro]

The docstring of vertex_coloring needs to explain it anyway

[Arthur Paulino]

@Yaël Dillies how do you mean about pairwise?

[Mario Carneiro]

but it's also useful to be able to constrain the type to other things; even in the finite graph situation you might want to take the codomain to be fin k to get a k-coloring

[Mario Carneiro]

and in the infinite graph situation you might want it to be some other cardinal

[Mario Carneiro]

or even just use regular type operations on it like A ⊕ B when joining two graphs with disjoint colors

[Yaël Dillies]

Eh, it doesn't turn out that great.

[Yaël Dillies]

I was thinking of something like ∀ a, is_antichain G.adj (color '⁻¹ {a})

[Mario Carneiro]

or your "colors" could be other mathematical objects relevant to an application. This is the reason why docs#matrix lets you use arbitrary index types even though we usually just think of the fin n case

[Kyle Miller]

Mario Carneiro said:

it does reveal some ambiguity of the terminology though

These tend to be called "proper" colorings when there can be confusion.

@Arthur Paulino Another design is to consider homomorphisms to complete_graph α, which gives you a lot of power

[Kyle Miller]

abbreviation proper_coloring (α : Type*) := G →g complete_graph α

[Kyle Miller]

This is how @Aaron Anderson suggested doing it.

[Arthur Paulino]

I was thinking about defining vertex_coloring and edge_coloring

[Arthur Paulino]

Do you think it would be okay to prove the homomorphism after having that pair of more bare-bones definitions?

[Kyle Miller]

I think you should start with the homomorphism and turn the fields from the struct into a definition and a lemma. The first is from applying the homomorphism, and the second is what it means to be a homomorphism, so it should be 2-4 lines total

[Kyle Miller]

It takes a bit of definition unfolding to see it, but this homomorphism definition is basically identical to the struct you defined

[Arthur Paulino]

Alright, I'm gonna try to dig this approach

[Kyle Miller]

(@Yaël Dillies With your k-factors work, one thing to think about is how to go back and forth between edge colorings and coverings by disjoint maximal 1-factors (i.e., perfect matchings).)

[Arthur Paulino]

How do I say this?

lemma proper_coloring_is_valid (α : Type*) (C : G.proper_coloring α) :
 ∀ (v w : V), G.adj v w → ¬(C.adj v w) := sorry

[Arthur Paulino]

invalid field notation, 'adj' is not a valid "field" because environment does not contain 'simple_graph.proper_coloring.adj'
  C
which has type
  G.proper_coloring α

[Kyle Miller]

variables {V : Type u} (G : simple_graph V)

abbreviation proper_coloring (α : Type*) := G →g complete_graph α

variables {G} {α : Type*} (C : G.proper_coloring α)

def proper_coloring.color (v : V) : α := C v

lemma proper_coloring.valid (v w : V) (h : G.adj v w) :
  C.color v ≠ C.color w :=
C.map_rel h

[Kyle Miller]

Also,

def proper_coloring.mk (f : V → α) (h : ∀ {v w : V}, G.adj v w → f v ≠ f w) :
  G.proper_coloring α := ⟨f, @h⟩

for a constructor that looks recognizable.

[Kyle Miller]

One of the reasons for having this be a homomorphism is that if you have an injective map a -> b, then there is an induced graph homomorphism complete_graph a ->g complete_graph b (not written, but easy), which you can compose with a proper a-coloring to get a proper b-coloring (so you can extend the set of colors using already existing machinery).

[Kyle Miller]

Or, if you have a graph homomorphism G ->g G' and a proper a-coloring of G', then you can compose the homomorphisms to get a proper a-coloring of G. This can be used to show that subgraphs of a proper a-colorable graph are a-colorable.

[Arthur Paulino]

You can see a lot further than I can. I will do my best to catch up

[Yaël Dillies]

(Yaël Dillies With your k-factors work, one thing to think about is how to go back and forth between edge colorings and coverings by disjoint maximal 1-factors (i.e., perfect matchings).)

Does that mean you want k-factors to be subgraphs?

[Kyle Miller]

@Arthur Paulino Something I'm looking forward to is having the fact that if every finite subgraph of a graph has a proper a-coloring, then (noncomputably) the graph has a proper a-coloring. This can be done using the idea for how docs#finset.all_card_le_bUnion_card_iff_exists_injective is proved from docs#finset.all_card_le_bUnion_card_iff_exists_injective'

I guess there's a more general result, which is if G' is a finite graph and if every finite subgraph of G has a homomorphism to G', then there is a homomorphism from G to G'.

[Kyle Miller]

@Yaël Dillies How were you thinking about formalizing them?

[Arthur Paulino]

Kyle Miller said:

Arthur Paulino Something I'm looking forward to is having the fact that if every finite subgraph of a graph has a proper a-coloring, then (noncomputably) the graph has a proper a-coloring. This can be done using the idea for how docs#finset.all_card_le_bUnion_card_iff_exists_injective is proved from docs#finset.all_card_le_bUnion_card_iff_exists_injective'

Isn't that kind of trivial from our current definition of subgraph since a graph can be a subgraph of itself?

structure subgraph {V : Type u} (G : simple_graph V) :=
(verts : set V)
(adj : V → V → Prop)
(adj_sub : ∀ {v w : V}, adj v w → G.adj v w)
(edge_vert : ∀ {v w : V}, adj v w → v ∈ verts)
(symm : symmetric adj . obviously)

[Kyle Miller]

The graph can be infinite!

[Arthur Paulino]

Oh okay then, now that's interesting :rofl:

[Arthur Paulino]

I'm still in the process of struggling a bit with syntax. I will be chewing the idea of proper_coloring that you suggested

[Arthur Paulino]

def proper_coloring.mk (f : V → α) (h : ∀ {v w : V}, G.adj v w → f v ≠ f w) :
  G.proper_coloring α := ⟨f, @h⟩

what does @h mean?

[Kevin Buzzard]

it turns the {} brackets into () ones

[Kyle Miller]

The problem is that with just h, lean will fill in the v and w arguments with metavariables that it tries to solve for, but the second slot for the constructor is expecting a function that still takes those as arguments.

[Kevin Buzzard]

If you try it without the @ then presumably you get some error saying "I was expecting you to give me a function which starts by consuming two elements of V but this function h appears to start by eating a term of type G.adj _ _"

[Kyle Miller]

I guess there's really not a need for these to be implicit arguments for this h argument -- I was just following the types for rel_iso.mk, which is what those angle brackets actually mean in this context.

[Kyle Miller]

This is a kind of fun thing you can do with proper_coloring.mk, if you like pattern matching:

abbreviation proper_coloring (α : Type*) := G →g complete_graph α

variables {G} {α : Type*} (C : G.proper_coloring α)

@[pattern]
def proper_coloring.mk (f : V → α) (h : ∀ {v w : V}, G.adj v w → f v ≠ f w) :
  G.proper_coloring α := ⟨f, @h⟩

def proper_coloring.color : Π (C : G.proper_coloring α), V → α
| (proper_coloring.mk f valid) := f

def proper_coloring.valid : Π (C : G.proper_coloring α) {v w : V} (h : G.adj v w), C.color v ≠ C.color w
| (proper_coloring.mk f valid) v w h := valid h

(I'm not suggesting you implement color and valid this way. It's just an example of what @[pattern] can do and why it might be good to keep the arguments toh as implicit.)

[Arthur Paulino]

It's still not clear to me what mk is doing. It's a function that takes a coloring function and a hypothesis that this coloring function is a proper one and returns... what?

[Kyle Miller]

It's returning an "actual" proper coloring

[Kyle Miller]

which we defined to be a kind of graph homomorphism

[Kyle Miller]

Try looking at #check @vertex_coloring.mk for your original definition:

structure vertex_coloring (color_type : Type u) :=
(color : V → color_type)
(valid : ∀ (v w : V), G.adj v w → color v ≠ color w)

Every structure defines a .mk function (unless you override what it's called), which is the constructor.

[Kyle Miller]

An idea here is that what structure does is have Lean create a new type from scratch with all the desired properties -- all these properties are what the type is. What we can instead do is take a pre-existing type and implementing the same properties, so this type now is the structure defined by vertex_coloring. (There's one difference though, which is that record syntax doesn't work quite as well if you don't use structure directly.)

[Kyle Miller]

The way dot notation works also helps keep up the illusion. We can write C.color and it will look for proper_coloring.color C first.

[Arthur Paulino]

The question I asked here was because I'm trying to arrive at a definition of the chromatic number. I did this:

open fintype

def proper_coloring.colors : set α := set.range C.color

def proper_coloring.card [fintype C.colors] : ℕ := card C.colors

But I'm very unsure this will have good consequences

[Arthur Paulino]

Maybe I should focus on some lemmas first

[Kyle Miller]

It's easier to just use fintype.card α here, then later use some idea of restricting a coloring. It's ok if not all colors are used, since there's a smaller α where it does use all the colors.

[Arthur Paulino]

Maybe some trick similar to the rel.image from earlier?

[Kyle Miller]

A TODO in subgraph.lean says "Images of graph homomorphisms as subgraphs." If we had that implemented, then you could do C.image to get a subgraph, the vertex set of which is the set of used colors.

[Kyle Miller]

(The edges in the images represent colors that show up on endpoints of some edge in the original graph. If the image isn't a complete graph, you can merge colors whenever they're not adjacent, for example.)

[Arthur Paulino]

Got this so far:

import combinatorics.simple_graph.basic

universe u

namespace simple_graph
variables {V : Type u} (G : simple_graph V)

abbreviation proper_coloring (α : Type*) := G →g complete_graph α

variables {G} {α : Type*} (C : G.proper_coloring α)

def proper_coloring.color (v : V) : α := C v

lemma proper_coloring.valid (v w : V) (h : G.adj v w) : C.color v ≠ C.color w :=
  C.map_rel h

def proper_coloring.mk (color : V → α) (h : ∀ {v w : V}, G.adj v w → color v ≠ color w) :
  G.proper_coloring α := ⟨color, @h⟩

def proper_coloring.card [fintype α] : (G.proper_coloring α) → ℕ := fintype.card α

def proper_coloring.is_minimal [fintype α] : Prop :=
  ∀ C' : (G.proper_coloring α), C.card ≤ C'.card

end simple_graph

[Yaël Dillies]

Kyle Miller said:

Yaël Dillies How were you thinking about formalizing them?

I was thinking of defining them as graphs. But making them subgraphs does sound smart

[Arthur Paulino]

I found this: https://github.com/leanprover-community/mathlib/blob/simple_graph_coloring/src/combinatorics/simple_graph/coloring.lean

[Kyle Miller]

Maybe this would work:

import combinatorics.simple_graph.basic
import data.nat.lattice

universe u

namespace simple_graph
variables {V : Type u} (G : simple_graph V)

abbreviation proper_coloring (α : Type*) := G →g complete_graph α

variables {G} {α : Type*} (C : G.proper_coloring α)

def proper_coloring.color (v : V) : α := C v

lemma proper_coloring.valid (v w : V) (h : G.adj v w) : C.color v ≠ C.color w :=
  C.map_rel h

@[pattern]
def proper_coloring.mk (color : V → α) (h : ∀ {v w : V}, G.adj v w → color v ≠ color w) :
  G.proper_coloring α := ⟨color, @h⟩

/-- Whether a graph can be colored by at most `n` colors. -/
def colorable (G : simple_graph V) (n : ℕ) : Prop :=
∃ (α : Type*) [fintype α] (C : G.proper_coloring α),
by exactI fintype.card α ≤ n  -- the "by exactI" trick is a way to get Lean to notice the `fintype` instance

/-- If `G` isn't colorable with finitely many colors, this will be 0. -/
noncomputable
def chromatic_number (G : simple_graph V) := Inf { n : ℕ | G.colorable n }

end simple_graph

[Kyle Miller]

The definition of colorable is "There exists a finite color type of size at most n for which there is a proper coloring of G." The by exactI is a bit unfortunate; try removing it to see the error it's avoiding.

[Kyle Miller]

By the way, here's some code from a while back about graphs and colorings (from before mathlib had anything about simple graphs at all): https://github.com/kmill/lean-graphcoloring/blob/master/src/graph.lean

[Kyle Miller]

Arthur Paulino said:

I found this: https://github.com/leanprover-community/mathlib/blob/simple_graph_coloring/src/combinatorics/simple_graph/coloring.lean

This is the one that got more developed: https://github.com/leanprover-community/mathlib/blob/simple_graph_matching/src/combinatorics/simple_graph/coloring.lean

It has stuff about homomorphisms, but colorings weren't homomorphisms themselves.

[Kyle Miller]

It also has this interesting "dual" version of colorings, which an indexed family of subsets of vertices (one subset per color), which allows you to work with partial colorings since not every vertex needs a color:

/-- This is an indexed family of disjoint subsets of the vertex type of `G` such that vertices in
the same set are not adjacent.  This is similar to `subgraph.coloring`, however not every vertex
needs to be given a color. -/
@[ext]
structure coloring' {V : Type u} (G : simple_graph V) (β : Type v) :=
(color_set : β → set V)
(disjoint : ∀ (c c' : β), c ≠ c' → color_set c ∩ color_set c' = ∅)
(valid : ∀ (c : β) (v v' : V), v ∈ color_set c → v' ∈ color_set c → ¬G.adj v v')

[Arthur Paulino]

I found the idea of β-colorable (would be α-colorable in our case) pretty smart, which constrains the coloring by the elements of the codomain

[Joanna Choules]

Kyle Miller said:

I guess there's a more general result, which is if G' is a finite graph and if every finite subgraph of G has a homomorphism to G', then there is a homomorphism from G to G'.

Do you happen to know if this is already being worked on currently? I thought I would try the proof myself out of curiosity, and I've been making reasonable headway, but I'm conscious of not duplicating effort.

[Kyle Miller]

@Joanna Choules I'm not aware of anyone working on it. (Are you using docs#nonempty_sections_of_fintype_inverse_system? or do you have another approach for the compactness argument?)

[Kyle Miller]

@Arthur Paulino This is a proof that that definition of colorability I gave is "reasonable" (in that it is equivalent to something that's more concrete):

/-- Whether a graph can be colored by at most `n` colors. -/
def colorable (G : simple_graph V) (n : ℕ) : Prop :=
∃ (α : Type*) [fintype α] (C : G.proper_coloring α),
by exactI fintype.card α ≤ n  -- the "by exactI" trick is a way to get Lean to notice the `fintype` instance

def complete_graph.of_embedding {α β : Type*} (f : α ↪ β) : complete_graph α ↪g complete_graph β :=
{ to_fun := f,
  inj' := f.inj',
  map_rel_iff' := by simp }

lemma colorable_if_nonempty_fin_coloring (G : simple_graph V) (n : ℕ) :
  G.colorable n ↔ nonempty (G.proper_coloring (fin n)) :=
begin
  split,
  { rintro ⟨α, αf, C, h⟩,
    tactic.unfreeze_local_instances,
    let f := (fintype.equiv_fin α).to_embedding.trans (fin.cast_le h).to_embedding,
    exact ⟨(complete_graph.of_embedding f).to_hom.comp C⟩, },
  { rintro ⟨C⟩,
    exact ⟨ulift (fin n), by apply_instance,
      (complete_graph.of_embedding equiv.ulift.symm.to_embedding).to_hom.comp C, by simp⟩, },
end

There are some universe variable issues that the proof needs to deal with, and it needs tactic.unfreeze_local_instances to get Lean to notice the fintype instance, but other than these technicalities the proof amounts to composing some graph homomorphisms.

[Arthur Paulino]

it's not accepting this line: let f := (fintype.equiv_fin α).to_embedding.trans (fin.cast_le h).to_embedding,

[Arthur Paulino]

type mismatch at application
  (fintype.equiv_fin α).to_embedding.trans (fin.cast_le h).to_embedding
term
  (fin.cast_le h).to_embedding
has type
  fin C.card ↪ fin n : Type
but is expected to have type
  fin (fintype.card α) ↪ ?m_1 : Sort (max 1 (imax 1 ?))

[Arthur Paulino]

Something to do with this definition that I added:

def proper_coloring.card [fintype α] : (G.proper_coloring α) → ℕ := fintype.card α

[Joanna Choules]

@Kyle Miller I plan to use the inverse system approach, yeah. So far I've mainly been working on the scaffolding (establishing a directed_order, defining the system functor), but I think I know how I want the main thread of the proof to go through.

[Arthur Paulino]

@Kyle Miller do you think this can be useful?

lemma chromatic_number_is_minimal [fintype α] (h : C.is_minimal) :
  chromatic_number G = C.card :=
begin
  sorry
end

[Arthur Paulino]

def proper_coloring.is_minimal [fintype α] : Prop :=
  ∀ C' : (G.proper_coloring α), C.card ≤ C'.card

[Kyle Miller]

Is C.card defined to be card (set.range C.color)? I thought I saw you define it to be card α, and this theorem wouldn't be true for that. (Maybe name the set C.support and make the theorem be about card C.support?) There will be some decidable complaints from lean, so maybe add open_locale classical to avoid this for now.

[Arthur Paulino]

This is the definition:

def proper_coloring.card [fintype α] : (G.proper_coloring α) → ℕ := fintype.card α

[Kyle Miller]

Yeah, that's giving you the number of colors, not the number of used colors.

[Arthur Paulino]

Ah, right

[Kyle Miller]

I think these are true:

def proper_coloring.chromatic_number_le [fintype α] (C : G.proper_coloring α) :
  G.chromatic_number ≤ fintype.card α :=
sorry

def proper_coloring.zero_le_chromatic_number [nonempty V] [fintype α] (C : G.proper_coloring α) :
  0 < G.chromatic_number :=
sorry

def proper_coloring.chromatic_number_minimal [fintype α] (C : G.proper_coloring α)
  (h : ∀ (C' : G.proper_coloring α), set.range C'.color = set.univ) :
  G.chromatic_number = fintype.card α :=
sorry

[Arthur Paulino]

Why do you use def for these instead?

[Arthur Paulino]

@Kyle Miller I've uploaded everything to the branch graph-coloring-homomorphism

[Kyle Miller]

That was a mistake -- they were supposed to be lemmas

[Kyle Miller]

This is potentially a useful variation:

lemma colorable_if_nonempty_fin_coloring' (G : simple_graph V) (n : ℕ) :
  G.colorable n ↔ ∃ (C : G.proper_coloring ℕ), ∀ v, C.color v < n :=
begin
  rw colorable_if_nonempty_fin_coloring,
  split,
  { rintro ⟨C⟩,
    let f := complete_graph.of_embedding (fin.coe_embedding n).to_embedding,
    use f.to_hom.comp C,
    cases C with color valid,
    intro v,
    exact fin.is_lt (color v), },
  { rintro ⟨C, Cf⟩,
    refine ⟨⟨λ v, ⟨C.color v, Cf v⟩, _⟩⟩,
    rintro v w hvw,
    simp only [complete_graph_eq_top, top_adj, subtype.mk_eq_mk, ne.def],
    exact C.valid v w hvw, },
end

[Arthur Paulino]

I'm gonna include it in the branch too

[Arthur Paulino]

here: https://github.com/leanprover-community/mathlib/blob/graph-coloring-homomorphism/src/combinatorics/simple_graph/coloring.lean

[Arthur Paulino]

I'm gonna try to pick up that other task to redesign matchings as subgraphs. I think it's simpler :sweat_smile:

[Kevin Buzzard]

I'm quite happy for this discussion to be going on here but isn't there an entire graph theory stream where you can sort your ideas into different threads which perhaps will be helpful for later reference? Perhaps @Joanna Choules and @Arthur Paulino don't know about it -- it's hidden by default. It would be really great to see some more progress in this area, I think there's plenty to be done and I think we now understand basic design decisions (which held up graph theory for so long) much better so there's now a chance for the area to grow

[Joanna Choules]

Yeah, I just wanted to do a quick status check before ploughing on. If I run into any implementation questions I'll thread them separately.

[Arthur Paulino]

@Kevin Buzzard How to create different threads inside a stream? Do you mean we can have the following hierarchy:
maths > graph theory > coloring?

[Reid Barton]

There is a separate stream (same level as maths), see #graph theory

[Arthur Paulino]

Posting here too since not everyone has subscribed to #graph theory
It's open for reviews: https://github.com/leanprover-community/mathlib/pull/10210