graph theory walks

Stream: new members

[Christopher Schmidt]

Hello everyone!
I am an undergraduate and very new to LEAN. I want to use it for graph theory. Looking in the scource code there are certain things I do not understand yet. Lets start with the following, the code is mostly copied from simple_graph/connectivity.lean

'''
universe u

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

@[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
'''

First of all, I do not quite undertsand the definition of a "walk". I do not see, how this is "a finite sequence of adjacent vertices".
Secondly, should "nil" and "cons" be seen as attrributes of the "walk" ? Or how is "|" supposed to be read ?

Any help is appreciated.

[Shreyas Srinivas]

Christopher Schmidt said:

Hello everyone!
I am an undergraduate and very new to LEAN. I want to use it for graph theory. Looking in the scource code there are certain things I do not understand yet. Lets start with the following, the code is mostly copied from simple_graph/connectivity.lean

'''
universe u

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

@[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
'''

First of all, I do not quite undertsand the definition of a "walk". I do not see, how this is "a finite sequence of adjacent vertices".
Secondly, should "nil" and "cons" be seen as attrributes of the "walk" ? Or how is "|" supposed to be read ?

Any help is appreciated.

The definition is inductive. It says that walk is either:
i) A trivial walk which, given a vertex u, goes from a vertex u to itself. Therefore a walk of zero length.
ii) Or built up inductively by concatenating a vertex u to a walk from v to w, provided you have proof that u is adjacent to v and a walk from v to w.

[Shreyas Srinivas]

| can be basically read as or. You have a bunch of ways to construct a walk. You can either use the nil constructor to construct the empty walk "or" construct a walk using cons constructor, from an existing walk and a proof that the next vertex you tack on is connected to one of the ends of the walk.

[Christopher Schmidt]

Ah okay got it, thank you!

[Yaël Dillies]

Also, you can click this link :point_right: #backticks to see how to correctly format your message :smile:

[Christopher Schmidt]

Now the following code should be properly shown.

@[pattern] abbreviation nil' (u : V) : G.walk u u := walk.nil

@[pattern] abbreviation cons' (u v w : V) (h : G.adj u v) (p : G.walk v w) : G.walk u w :=
walk.cons h p

Reguarding that, I just wanted to know what "@[pattern] abbreviation" is used for? Where precisely is the difference of those abbreviations to the definition ?