Induced subgraphs

Stream: Is there code for X?

[Dustin Mixon]

I would like to pass to the induced subgraph of a graph. The following example attempts to take the subgraph of a triangle induced by two vertices:

import combinatorics.simple_graph.subgraph

def K3 : simple_graph (fin 3) :=
{
  adj := λ x y, x ≠ y,
  symm := by finish,
  loopless := by finish,
}

#check (simple_graph.subgraph.top : K3.subgraph)
#check simple_graph.subgraph.induce (simple_graph.subgraph.top : K3.subgraph) (fin 2)

The final #check results in the error unknown identifier 'simple_graph.subgraph.induce'. What am I missing here?

[Kyle Miller]

First, two simplifications:

import combinatorics.simple_graph.subgraph

def K3 : simple_graph (fin 3) := ⊤

#check (⊤ : K3.subgraph)

The definition of ⊤ : simple_graph (fin 3) is the complete graph on the given vertex type, and ⊤ : K3.subgraph is the graph as a subgraph of itself (the documentation for docs#simple_graph.subgraph.top ought to mention that this is the preferred way to write it).

[Kyle Miller]

I'm getting a different error from unknown identifier 'simple_graph.subgraph.induce'. Maybe you have an older mathlib? This was added a week or two ago.

[Dustin Mixon]

Heh, I downloaded mathlib on Monday or Tuesday. Is it easy to update?

[Kyle Miller]

The error I'm getting is from the fact that fin 2 is a type, not a set (fin 3). One way to do what I think you want is the following:

#check simple_graph.subgraph.induce (⊤ : K3.subgraph) {0, 1}

[Kyle Miller]

This {0, 1} ends up being a set (fin 3)

[Kyle Miller]

That's weird that you have this error if you got mathlib last week -- it was added on July 7th (#14034)

[Dustin Mixon]

Yeah, I get the same error with your #check simple_graph.subgraph.induce (⊤ : K3.subgraph) {0, 1}

[Kyle Miller]

By the way, you probably don't want it, but I just thought I'd mention that another way to do induced graphs, if you want to get a simple_graph rather than a subgraph, is

#check K3.induce ({0, 1} : set (fin 3))

(I'm not quite sure why it needs the set (fin 3) type ascription hint here. Edit: oh, it's probably the argument order for simple_graph.induce)

[Kyle Miller]

Dustin Mixon said:

Heh, I downloaded mathlib on Monday or Tuesday. Is it easy to update?

Did you create a project using leanproject? I think you can do leanproject upgrade-mathlib.

[Dustin Mixon]

I just upgraded, and I'm getting the same errors. Here's the error I get for your simple_graph alternative:

invalid field notation, 'induce' is not a valid "field" because environment does not contain 'simple_graph.induce'
  K3
which has type
  simple_graph (fin 3)

[Kyle Miller]

Anyway, once you get mathlib working, you can make use of dot notation for simple_graph.subgraph.induce and write

#check (⊤ : K3.subgraph).induce {0, 1}

for short. This is the way it was intended to be written, but you don't have to.

[Kyle Miller]

@Dustin Mixon When you upgrade mathlib, do you see this line?

mathlib: trying to update _target/deps/mathlib to revision 87fc68283f9b2139606540086d135bd5ab95b8ad

Does it have the same revision as this?

[Kyle Miller]

Oh, another thing, after you upgraded, did you restart Lean in VS Code or whatever editor you're using?

[Dustin Mixon]

I don't see any line like that. I just put leanproject upgrade-mathlib in the terminal, and it downloaded (and installed) a component called 'lean' and then gave me some warnings:

info: downloading component 'lean'
info: installing component 'lean'
configuring _user_local_packages 1
WARNING: leanpkg configurations not specifying `path = "src"` are deprecated.
configuring _user_local_packages 1
WARNING: leanpkg configurations not specifying `path = "src"` are deprecated.
configuring _user_local_packages 1
WARNING: leanpkg configurations not specifying `path = "src"` are deprecated.
/Users/dustin.mixon/.lean/_target/deps/mathlib

I also restarted VS Code. I don't know how to restart Lean in VS Code.

[Kyle Miller]

Stepping back (it's something I should have asked), how did you create your Lean project?

[Kyle Miller]

(To restart Lean without restarting VS Code, you can do ctrl-shift-P, then "Lean: Restart", but restarting VS Code is sufficient.)

[Dustin Mixon]

Not sure what you mean by a Lean project. To write the above lean code, I opened VS Code, made a new file, and saved it as a .lean file in /Users/dustin.mixon/my_project/src.

[Dustin Mixon]

I just restarted Lean as you suggested, and I'm still getting the same errors.

[Dustin Mixon]

Hmm, maybe you're asking how I installed everything in the first place. I just followed these instructions: https://leanprover-community.github.io/install/macos.html#m1-macs--apple-silicon

[Kyle Miller]

Dustin Mixon said:

Not sure what you mean by a Lean project. To write the above lean code, I opened VS Code, made a new file, and saved it as a .lean file in /Users/dustin.mixon/my_project/src.

If I understand you correctly, you created the folder my_project yourself and just put a .lean file there, right? You need to create a lean project with some additional support files. https://leanprover-community.github.io/install/project.html

[Kyle Miller]

If you do leanproject new my_project when you're in /Users/dustin.mixon, it will create the my_project folder for you, then you can open that folder in VS Code

[Dustin Mixon]

It works!! Thanks so much!

[Dustin Mixon]

Do I really need to prove that an induced subgraph is induced, or is the proof already lurking somewhere? Here's what I'm up against:

import combinatorics.simple_graph.subgraph

def K3 : simple_graph (fin 3) := ⊤
def K2 := (⊤ : K3.subgraph).induce {0, 1}

lemma silly : K2.is_induced :=
begin
  sorry,
end

[Johan Commelin]

cc @Kyle Miller

[Kyle Miller]

@Dustin Mixon That seems to be a glaring oversight :smile:

[Kyle Miller]

Feel free to open a PR with this:

@[simp] lemma induce_top_is_induced : ((⊤ : G.subgraph).induce s).is_induced :=
by { intros v w, simp { contextual := tt } }

You can put it at the end of the induce section in combinatorics/simple_graph/subgraph.lean.

[Dustin Mixon]

I'm confused. I checked your proof:

import combinatorics.simple_graph.subgraph

def K3 : simple_graph (fin 3) := ⊤
def K2 := (⊤ : K3.subgraph).induce {0, 1}

lemma silly : K2.is_induced :=
begin
  intros v w,
  simp { contextual := tt },
end

and got the error simplify tactic failed to simplify. Am I doing something wrong?

[Kyle Miller]

Yes, it's because simp won't unfold the definition of K2 for you. You probably could fix it using simp [K2] { contextual := tt } or by adding @[reducible] to the definition of K2.

Another way is to use the lemma directly:

lemma silly : K2.is_induced :=
by { apply simple_graph.subgraph.induce_top_is_induced }

(I'm not completely certain why the apply is needed here. It's getting around some elaboration oddity.)

[Kyle Miller]

Here's another lemma that would be useful to add:

lemma induce_is_induced_of_is_induced (hi : G'.is_induced) (hs : s ⊆ G'.verts) :
  (G'.induce s).is_induced :=
begin
  intros v w,
  simp only [induce_verts, induce_adj, true_and] { contextual := tt },
  intros hv hw ha,
  exact hi (hs hv) (hs hw) ha,
end