concrete simple graph

Stream: graph theory

[Alexandre Rademaker]

I am trying to understand how can I use the simple_graph to introduce some basic concepts of graph theory in my course on discrete math. In particular, I am trying to construct a concrete simple graph but I got a type error:

import combinatorics.simple_graph
open nat

def e1 : ℕ → ℕ → Prop
 | 1 2 := true
 | 2 1 := true
 | 2 3 := true
 | 3 2 := true
 | _ _ := false

def g1 := simple_graph.mk e1

What am I doing wrong?

[Bryan Gin-ge Chen]

docs#simple_graph is a structure with 3 fields, the first is an edge relation, which you've provided with e1. The second and third are proofs that the edge relation is symmetric and irreflexive, respectively. If you don't provide them, the . obviously syntax in the definition means that Lean will try using docs#obviously (I think this just calls tactic#tidy) to provide proofs. The error message says that obviously isn't able to prove those goals, so you'll most likely have to provide proofs yourself.

[Chris B]

^^ What he said.

def g1 : simple_graph nat :=
  have h1 : symmetric e1, from sorry,
  have h2 : irreflexive e1, from sorry,
  simple_graph.mk e1 h1 h2

[Alexandre Rademaker]

Nice! Thank you, looks like I need a better definition for the edges, these proofs are not trivial for my definition of e1.

[Alexandre Rademaker]

Ok, that is the complete boring step-by-step. I am probably missing some magic way to simplify the proof over finite data.

import combinatorics.simple_graph

inductive node : Type
 | a : node
 | b : node
 | c : node

open node

def e1 : node → node → Prop
 | a b := true
 | b a := true
 | a c := true
 | c a := true
 | _ _ := false

def g1 : simple_graph node :=
 have h1 : symmetric e1, from
 begin
  intros n m,
  apply node.cases_on n,
  apply node.cases_on m,
  rw e1, trivial,
  rw e1, intro, trivial,
  rw e1, intro, trivial,

  apply node.cases_on m,
  rw [e1, e1], intro, trivial,
  rw e1, trivial,
  rw [e1, e1], trivial,

  apply node.cases_on m,
  rw [e1,e1], intro, trivial,
  rw e1, trivial,
  rw e1, trivial,
 end,
 have h2 : irreflexive e1, from
 begin
  intro n,
  apply node.cases_on n,
  rw e1, trivial,
  rw e1, trivial,
  rw e1, trivial,
 end,
 simple_graph.mk e1 h1 h2

I could simplify to

def g1 : simple_graph node :=
 have h1 : symmetric e1, from
 begin
  intros n m,
  cases n,
  repeat {
      cases m,
      repeat {repeat {rw e1}, try {intro}, trivial}
  },
 end,
 have h2 : irreflexive e1, from
 begin
  intro n,
  cases n,
  repeat { rw e1, trivial },
 end,
 simple_graph.mk e1 h1 h2

[Alex J. Best]

you can use ; to apply to all created goals instead of repeat.

def g1 : simple_graph node :=
 have h1 : symmetric e1, from
 begin
   intros x y h,
   cases x;
   cases y; exact h,
 end,
 have h2 : irreflexive e1, from
 begin
  intro n,
  cases n; rw e1; trivial,
 end,
 simple_graph.mk e1 h1 h2

[Alexandre Rademaker]

thank you.

[Mario Carneiro]

It's much easier to work with an inductive:

inductive e1 : node → node → Prop
| ab : e1 a b
| ba : e1 b a
| ac : e1 a c
| ca : e1 c a

theorem e1.symm {x y} (h : e1 x y) : e1 y x := by cases h; constructor
theorem e1.irrefl (x) : ¬ e1 x x := λ h, by cases h

def g1 : simple_graph node := simple_graph.mk e1 @e1.symm e1.irrefl

[Mario Carneiro]

you can also use a symmetric closure to cut down on the number of cases (although in this example it's not a very big deal, in a larger inductive it might be worth it)

import combinatorics.simple_graph

namespace relation
variables {α : Type*} (r : α → α → Prop)

def symm_gen (x y : α) : Prop := r x y ∨ r y x

variable {r}
theorem symm_gen.symm : symmetric (symm_gen r) := λ _ _, or.symm
theorem symm_gen.irrefl (H : irreflexive r) : irreflexive (symm_gen r) :=
by rintro _ (h|h); exact H _ h

end relation

inductive node : Type
| a : node
| b : node
| c : node

open node

inductive e1 : node → node → Prop
| ab : e1 a b
| ac : e1 a c

def g1 : simple_graph node :=
{ adj := relation.symm_gen e1,
  sym := relation.symm_gen.symm,
  loopless := relation.symm_gen.irrefl $ by rintro _ ⟨⟩ }

[Alexandre Rademaker]

Thank you @Mario Carneiro, I will try more tomorrow. It is a new world for me! I am trying to understand many things that I haven't played yet in Lean. It took me 30 min to understand how to obtain the neighbors of a node with #reduce (simple_graph.neighbor_set g2 c) that reduces to e1 c.

[Mario Carneiro]

I don't know that much about this graph library, but if you want to enumerate the values of x such that e1 c x you can do cases (h : e1 c x)

[Kyle Miller]

It's not particularly well developed, but you can create graphs from edge sets:

import combinatorics.simple_graph

def simple_graph.from_edges {α : Type*}
  (edges : set (sym2 α)) (loopless : ∀ e ∈ edges, ¬sym2.is_diag e) :
  simple_graph α :=
{ adj := λ v w, ⟦(v, w)⟧ ∈ edges,
  sym := by { intros v w, simp [sym2.eq_swap] },
  loopless := by { intros v h, have h' := loopless _ h, simpa using h' } }

open simple_graph

def my_edges : set (sym2 ℕ) :=
{ ⟦(1, 2)⟧,
  ⟦(2, 3)⟧ }

def my_graph : simple_graph ℕ :=
simple_graph.from_edges my_edges (by { dunfold my_edges, finish })

[Kyle Miller]

Part of it is that data.sym2 is missing the inverse to from_rel, which would take a set of unordered pairs and produce a relation. It should also have a lemma that if the set of unordered pairs has no diagonal elements, then the relation is irreflexive.

[Kyle Miller]

If anyone wants to add from_edges to the simple graph library, here's an additional lemma:

@[simp]
lemma edge_set_from_edges {α : Type*}
  {edges : set (sym2 α)} {loopless : ∀ e ∈ edges, ¬sym2.is_diag e} :
  (simple_graph.from_edges edges loopless).edge_set = edges :=
by tidy

(Maybe it would be better to be called from_edge_set rather than from_edges.)

[Alexandre Rademaker]

Hi @Kyle Miller , this is very interesting. The use of sym2 instead of a function simplified the definition of the edges and the proofs necessary to construct the graph. I also learned about dunfold that I have never seen before.

But thinking broadly, maybe I need to change my mindset to use lean to present basic graph theory. I am trying to compute with graphs as data structures and maybe the library as not developed with that purpose.

[Alexandre Rademaker]

Mario Carneiro said:

I don't know that much about this graph library, but if you want to enumerate the values of x such that e1 c x you can do cases (h : e1 c x)

Hum, that would be an alternative to my tentative #reduce command. But I would need to create a context to use this tactic..

[Kyle Miller]

@Alexandre Rademaker The graph library isn't designed to be used for data structures directly, and I think of it more as an abstract interface to graphs: you might create specialty data structures for computation along with a function to simple_graph to prove things (though this idea hasn't been tested yet). The library tries to make things decidable, at least, if the underlying relation is, though you have to implement fintype instances to get it to be able to #reduce the degree of a vertex, for example. Instances like these are where you supply your own algorithms that depend on the specific data structure.

[Alexandre Rademaker]

Thank you @Kyle Miller, but I didn't get the point about the abstract interface to graphs. Now that I know how to construct a particular graph, I am back to see how Lean can help me in the introduction to graph theory.

The majority of the courses/books about introduction to graphs have isomorphism as one of its first topics. It seems that providing examples like the ones described in https://www.youtube.com/watch?v=z-GfKbzvtBA&feature=youtu.be (possible following also the ideas of https://math.stackexchange.com/questions/2486944/how-to-tell-whether-two-graphs-are-isomorphic would be nice.

[Kyle Miller]

In an experimental branch, we have graph isomorphisms https://github.com/leanprover-community/mathlib/blob/simple_graphs2/src/combinatorics/simple_graph/hom.lean#L137 (though no real examples except for the one on line 200). An isomorphism of simple graphs is a bijection on vertex sets that preserves the adjacency relation in both directions.

[Alexandre Rademaker]

I thought that isomorphism would be a proposition not a type ... I would like to be able to provide two simple graphs and construct a prove of their isomorphism. That is, given an f , show that it is bijective and preserves adjacent relations

[Kyle Miller]

Two graphs are isomorphic if there exists an isomorphism between them. The best way to show two graphs are isomorphic is to provide an explicit isomorphism, which gives the exact correspondence between vertices in each graph. If you want to turn it into a proposition, you could say nonempty (G ≃g G') (using the notation from that branch), but you'd only want to do that if for some reason you can't construct the isomorphism.

[Kyle Miller]

But maybe you're asking for Lean to compute whether two graphs are isomorphic? You could probably write a tactic to do this, if the graphs are presented suitably. (Or maybe use a Mario-style trick where you do logic programming at the typeclass level?)

[Kyle Miller]

I backported graph isomorphism from the experimental branch to what's currently in mathlib and then took the pair of isomorphic graphs from the beginning of the YouTube video and showed they're isomorphic by providing an explicit isomorphism (with inefficient proofs):

import combinatorics.simple_graph

universes u v

namespace simple_graph

def from_edges {α : Type*}
  (edges : set (sym2 α)) (loopless : ∀ e ∈ edges, ¬sym2.is_diag e) :
  simple_graph α :=
{ adj := λ v w, ⟦(v, w)⟧ ∈ edges,
  sym := by { intros v w, simp [sym2.eq_swap] },
  loopless := by { intros v h, have h' := loopless _ h, simpa using h' } }

lemma from_edges.edge_set {α : Type*}
  {edges : set (sym2 α)} {loopless : ∀ e ∈ edges, ¬sym2.is_diag e} :
  (simple_graph.from_edges edges loopless).edge_set = edges :=
by tidy

abbreviation iso {V : Type u} {V' : Type v} (G : simple_graph V) (G' : simple_graph V') : Type (max u v) :=
rel_iso G.adj G'.adj

infix ` ≃g ` : 50 := iso

end simple_graph

open simple_graph

inductive V1 | v1 | v2 | v3 | v4 | v5 | v6
inductive V2 | va | vb | vc | vd | ve | vf
open V1 V2

def G : simple_graph V1 :=
simple_graph.from_edges
{⟦(v1, v4)⟧,
 ⟦(v1, v5)⟧,
 ⟦(v1, v6)⟧,
 ⟦(v2, v4)⟧,
 ⟦(v2, v5)⟧,
 ⟦(v2, v6)⟧,
 ⟦(v3, v4)⟧,
 ⟦(v3, v5)⟧,
 ⟦(v3, v6)⟧,
}
(by finish)

def H : simple_graph V2 :=
simple_graph.from_edges
{⟦(va, vb)⟧,
 ⟦(va, vd)⟧,
 ⟦(va, vf)⟧,
 ⟦(vb, vc)⟧,
 ⟦(vb, ve)⟧,
 ⟦(vc, vd)⟧,
 ⟦(vc, vf)⟧,
 ⟦(vd, ve)⟧,
 ⟦(ve, vf)⟧,
}
(by finish)

def GtoH_verts : V1 → V2
| v1 := vb
| v2 := vd
| v3 := vf
| v4 := vc
| v5 := ve
| v6 := va

def HtoG_verts : V2 → V1
| vb := v1
| vd := v2
| vf := v3
| vc := v4
| ve := v5
| va := v6

def GisoH : G ≃g H :=
{ to_fun := GtoH_verts,
  inv_fun := HtoG_verts,
  left_inv := begin intro x, cases x; simp [GtoH_verts, HtoG_verts], end,
  right_inv := begin intro x, cases x; simp [GtoH_verts, HtoG_verts], end,
  map_rel_iff' := begin
    intros x y,
    dsimp [G, H, from_edges],
    simp only [set.mem_insert_iff, set.mem_singleton_iff, sym2.eq_iff],
    cases x; cases y; dsimp [GtoH_verts]; simp,
  end }

[Kyle Miller]

(There's probably some way to have HtoG_verts be automatically constructed from GtoH_verts since V1 and V2 are finite types, but I don't know how off the top of my head.)

[Mario Carneiro]

You can't construct HtoG_verts directly from GtoH_verts without leaving an important verification condition on the table: the goal is to show a bijection and if you just make a list of pairs you don't know it's bijective. Writing the functions in each direction ensures exhaustiveness, and checking that they are converses is easy (linear time)

[Kyle Miller]

@Mario Carneiro I was imagining something like this, but more automated (and also more computable since the types are decidable and finite).

import data.fintype.basic

open fintype

inductive V1 | v1 | v2 | v3 | v4 | v5 | v6
inductive V2 | va | vb | vc | vd | ve | vf
open V1 V2

instance : fintype V1 :=
begin use {v1, v2, v3, v4, v5, v6}, tidy, cases x; simp end

instance : fintype V2 :=
begin use {va, vb, vc, vd, ve, vf}, tidy, cases x; simp end

@[simp] lemma card_V1 : card V1 = 6 := by tidy
@[simp] lemma card_V2 : card V2 = 6 := by tidy

def f : V1 → V2
| v1 := vb
| v2 := vd
| v3 := vf
| v4 := vc
| v5 := ve
| v6 := va

lemma f_inj : function.injective f :=
by { intros x y, cases x; cases y; simp [f] }

lemma f_bij : function.bijective f :=
(bijective_iff_injective_and_card f).mpr ⟨f_inj, by simp⟩

noncomputable
def f_equiv : V1 ≃ V2 :=
equiv.of_bijective f f_bij

lemma f_equiv_to_fun : f_equiv.to_fun = f :=
by { ext x, simp [f_equiv] }

[Mario Carneiro]

this is way more expensive than the first version

[Mario Carneiro]

the injectivity check is O(n^2) while the back and forth check is O(n)

[Mario Carneiro]

it's also noncomputable

[Kyle Miller]

Technically it's all O(1) since there are only 6 elements, but in any case I'm only looking for mathematical convenience to define an explicit bijection and I don't care too much about running time of the resulting function.

How is this noncomputable? There are only 6^6 possible functions, and you can check all of them to see what would be the inverse in a computable way.

[Kevin Buzzard]

It's noncomputable in the sense that you wrote noncomputable?

[Mario Carneiro]

If you are looking for mathematical convenience, the example is too minimal. Almost all of the boilerplate can be removed but it needs to fit in some larger pattern of graph isomorphisms. This looks way too much like a toy example to draw general conclusions

[Alexandre Rademaker]

I was thinking about the current definition of simple graph. What is the motivation for this particular way to define graphs? In particular why carrying out the proofs as components of the structure?

[Aaron Anderson]

In part, in analogy to the way groups and such are defined.

[Aaron Anderson]

If you want to have a structure that has some data that follow some properties, the easiest way to do it seems to be to bundle together the data and the proofs of the properties.

[Aaron Anderson]

Another possible way to do it could have been by defining a set of edges, but if that was defined as say, a set of the type sym2, the symmetric square of the vertex type, then you’d still need to include a proof of the irreflexivity axiom.

[Alexandre Rademaker]

In what situations and how the proofs in the structure can or should be used?

[Jalex Stark]

for "how" to use the proofs in a structure, use dot notation?

[Alexandre Rademaker]

Thank you @Jalex Stark and sorry, I know that we can access fields in a structure with the dot notation. The how is not a question about Lean syntax, it is more about the purpose of having this term in the structure and contexts that it would be useful. See

def e1 : node → node → Prop
 | a b := true
 | b a := true
 | a c := true
 | c a := true
 | _ _ := false

def g2 : simple_graph node :=
 have h1 : symmetric e1, from
 begin
  intros n m,
  cases n,
  repeat {
      cases m,
      repeat {repeat {rw e1}, try {intro}, trivial}
  },
 end,
 have h2 : irreflexive e1, from
 begin
  intro n,
  cases n,
  repeat { rw e1, trivial },
 end,
 simple_graph.mk e1 h1 h2

#check g2.sym

This only reveals that g2.sym is a very unreadable term g2.sym : auto_param (symmetric g2.adj) (name.mk_string "obviously" name.anonymous) of type symmetric e1 I hope. But what is the benefits of carrying this proof with the structure?

[Jalex Stark]

hmm so my understanding is a bit shaky here, too. I think that the part matching auto_param (_) (_ "obviously" _) means that Lean did or will try to prove symmetric e1 using the obviously tactic, which is currently the same as trying to prove it with tidy

[Jalex Stark]

Before seeing your code I had the impression that g2.sym would be of type symmetric e1 or at least of some type that is defeq to symmetric e1.

[Jalex Stark]

Maybe @Kyle Miller or @Aaron Anderson or @Alena Gusakov can say something more helpful

[Jalex Stark]

Often in mathlib we manage to build up a lot of theory without being very good at producing concrete examples. Thank you for trying to do that !

[Jalex Stark]

When I first came to this server i was trying to prove any theorems about a certain finite group of cardinality $8$ and I found the experience pretty disheartening

[Aaron Anderson]

The goal of the definition

structure simple_graph (V : Type u) :=
(adj : V → V → Prop)
(sym : symmetric adj . obviously)
(loopless : irreflexive adj . obviously)

is to be functionally equivalent to the simpler definition

structure simple_graph (V : Type u) :=
(adj : V → V → Prop)
(sym : symmetric adj)
(loopless : irreflexive adj)

[Aaron Anderson]

To see what I mean by "functionally equivalent", check out the proofs that use G.sym and G.loopless.

lemma ne_of_adj {a b : V} (hab : G.adj a b) : a ≠ b :=
by { rintro rfl, exact G.loopless a hab }

uses G.loopless exactly as if it was of type irreflexive G.adj, and

lemma edge_symm (u v : V) : G.adj u v ↔ G.adj v u := ⟨λ x, G.sym x, λ x, G.sym x⟩

uses G.sym exactly as if it was of type symmetric G.adj.

[Aaron Anderson]

So when you are proving things using those properties, you can pretend it's just the simpler definition, and lean will make the necessary conversions for you.

[Aaron Anderson]

When you want to prove those properties, you have two choices:

[Aaron Anderson]

forget about the . obviously, and prove the two conditions by hand (what you've done)

[Aaron Anderson]

or try an abbreviated form.

[Aaron Anderson]

What I'd do in general is try what we did for the complete_graph:

def complete_graph (V : Type u) : simple_graph V :=
{ adj := ne }

except with adj := whatever your relation is.

[Aaron Anderson]

Then lean will complain at you and say if it's missing one or both of the proofs, which you then just have to do the old-fashioned way.

[Aaron Anderson]

As to the other question you could be asking is why have proofs as part of the structure at all?

[Aaron Anderson]

The answer I have to that is, if we didn't, objects of this type wouldn't be graphs!

[Aaron Anderson]

You could define it as

structure simple_graph (V : Type u) :=
(adj : V → V → Prop)

but then you couldn't prove basic theorems that are true of graphs, because you'll have counterexamples to symmetry and irreflexitivity.

[Alexandre Rademaker]

I see, thank you @Aaron Anderson for the detailed explanation. So the instantiation of a simple_graph forces you to carry the proofs that certificate that the instance is a simple graph. The lemmas you provided using the proofs in the structure field also makes thing clear.

[Kyle Miller]

@Alexandre Rademaker https://leanprover.github.io/reference/expressions.html#implicit-arguments explains all the kinds of arguments that Lean supports -- these can appear both in argument lists to functions and to fields for structures. The auto_param is an internal detail for the case of using a tactic to synthesize the optional argument (I think the documentation should say optional and not implicit in that last case)

[Kyle Miller]

This is how I might write that proof (just changing things a little without changing the tactics really):

inductive node | a | b | c
open node

def e1 : node → node → Prop
 | a b := true
 | b a := true
 | a c := true
 | c a := true
 | _ _ := false

def g2 : simple_graph node :=
{ adj := e1,
  sym := begin
    intros n m,
    cases n; cases m; { dunfold e1, intro, trivial },
  end,
  loopless := begin
    intro n,
    cases n; { dunfold e1, trivial },
  end }

[Kyle Miller]

The tidy tactic is able to prove it's a simple graph with a little help:

def g2 : simple_graph node :=
{ adj := e1,
  sym := λ n m, by cases n; cases m; tidy,
  loopless := λ n, by cases n; tidy }

What ; does is run the following tactics for each case generated by the first tactic. So, for example, cases n; cases m; tidy ends up running tidy for each possibility for n and m.

[Kyle Miller]

In the end, both proofs just do cases on each argument, so here's a way to compact it. This should work in general to prove that other adjacency relations defined in a similar way are graphs:

meta def cases' : tactic unit := `[intro h, cases h; { trivial <|> cases' }]

def g2 : simple_graph node :=
{ adj := e1,
  sym := by cases',
  loopless := by cases' }