# Zulip Chat Archive

## Stream: graph theory

### Topic: concrete simple graph

#### Alexandre Rademaker (Nov 12 2020 at 01:16):

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 (Nov 12 2020 at 01:27):

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 (Nov 12 2020 at 01:29):

^^ 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 (Nov 12 2020 at 01:41):

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 (Nov 12 2020 at 02:22):

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 (Nov 12 2020 at 02:50):

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 (Nov 12 2020 at 02:53):

thank you.

#### Mario Carneiro (Nov 12 2020 at 02:54):

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 (Nov 12 2020 at 03:02):

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 (Nov 12 2020 at 03:12):

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 (Nov 12 2020 at 03:14):

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 (Nov 12 2020 at 04:40):

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 (Nov 12 2020 at 04:44):

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 (Nov 12 2020 at 04:53):

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 (Nov 12 2020 at 12:56):

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 (Nov 12 2020 at 17:17):

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 (Nov 12 2020 at 18:41):

@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 (Nov 17 2020 at 04:51):

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 (Nov 17 2020 at 05:07):

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 (Nov 17 2020 at 22:48):

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 (Nov 17 2020 at 22:53):

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 (Nov 17 2020 at 22:58):

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 (Nov 17 2020 at 23:15):

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 (Nov 17 2020 at 23:18):

(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 (Nov 18 2020 at 00:39):

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 (Nov 18 2020 at 06:10):

@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 (Nov 18 2020 at 06:11):

this is way more expensive than the first version

#### Mario Carneiro (Nov 18 2020 at 06:12):

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

#### Mario Carneiro (Nov 18 2020 at 06:12):

it's also noncomputable

#### Kyle Miller (Nov 18 2020 at 06:16):

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 (Nov 18 2020 at 07:23):

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

?

#### Mario Carneiro (Nov 18 2020 at 07:30):

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 (Nov 22 2020 at 15:22):

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 (Nov 22 2020 at 16:48):

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

#### Aaron Anderson (Nov 22 2020 at 16:49):

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 (Nov 22 2020 at 16:52):

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 (Nov 23 2020 at 15:14):

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

#### Jalex Stark (Nov 24 2020 at 22:48):

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

#### Alexandre Rademaker (Nov 26 2020 at 13:58):

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 (Nov 26 2020 at 16:18):

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 (Nov 26 2020 at 16:20):

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 (Nov 26 2020 at 16:21):

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

#### Jalex Stark (Nov 26 2020 at 16:22):

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 (Nov 26 2020 at 16:22):

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 (Nov 26 2020 at 16:36):

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 (Nov 26 2020 at 16:38):

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 (Nov 26 2020 at 16:39):

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 (Nov 26 2020 at 16:43):

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

#### Aaron Anderson (Nov 26 2020 at 16:43):

forget about the `. obviously`

, and prove the two conditions by hand (what you've done)

#### Aaron Anderson (Nov 26 2020 at 16:44):

or try an abbreviated form.

#### Aaron Anderson (Nov 26 2020 at 16:44):

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 (Nov 26 2020 at 16:45):

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 (Nov 26 2020 at 16:46):

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

#### Aaron Anderson (Nov 26 2020 at 16:46):

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

#### Aaron Anderson (Nov 26 2020 at 16:49):

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 (Nov 29 2020 at 21:49):

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 (Nov 30 2020 at 21:42):

@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 (Dec 01 2020 at 04:07):

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 (Dec 01 2020 at 05:29):

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 (Dec 01 2020 at 05:36):

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' }
```

Last updated: May 08 2021 at 22:13 UTC