Defining graphs in Lean

Stream: general

[Hoang Le Truong]

I definite a function on the certain domain as follow

def V: set ℕ := {1,2,3,4}

def g [has_one V][has_add V](e:V× V ): ℕ :=
match  e  with
|(1,2) :=2
|(2,1) :=2
|_     :=0
end

I received the following message

equation compiler failed (use 'set_option trace.eqn_compiler.elim_match true' for additional details)

and

invalid function application in pattern, it cannot be reduced to a constructor (possible solution, mark term as inaccessible using '.( )') 1

What is error?

[Kenny Lau]

V is not an inductive type.

[Kenny Lau]

you can't match it

[Kenny Lau]

you can't just "make it work" by using [has_one V] [has_add V]

[Hoang Le Truong]

I need make V as an inductive type, not is subset of \N

[Kenny Lau]

depends on your purpose

[Kenny Lau]

I would just use if-then-else

[Hoang Le Truong]

I need V is subset of \N

[Hoang Le Truong]

how are we use V is an inductive type and subset of \N

[Johan Commelin]

def g : V \times V \to nat := \lam x, if x.1 * x.2 = 2 then 2 else 0

[Johan Commelin]

Something like that?

[Kenny Lau]

inductive def V : \N \to Prop
| one : 1 \to V
| two : 2 \to V
| three : 3 \to V
| four : 4 \to V

[Hoang Le Truong]

@Johan Commelin It is ok but if I have function has domain is random and large. It is not good to make function when use if - then-else

[Kenny Lau]

maybe you should tell us what you want to do

[Hoang Le Truong]

I want to make function with card V=100 and valued is random

[Kenny Lau]

randomness doesn't exist

[Kevin Buzzard]

(in Lean)

[Kenny Lau]

randomness doesn't exist, period

[Johan Commelin]

What do you mean with "valued is random", do you mean that V is an arbitrary subset of \N?

[Kenny Lau]

a random variable is neither random nor a variable

[Kevin Buzzard]

(I guess the quantum mechanics course is next year Kenny, right?)

[Hoang Le Truong]

yes

[Kenny Lau]

alright

[Johan Commelin]

Kenny will choose not to follow QM...

[Kenny Lau]

lol

[Johan Commelin]

Hoang, ok, and what should your function do with V?

[Johan Commelin]

You want a function V \to \N, is that right?

[Hoang Le Truong]

yes is randomness doesn't exist
I want find example function g

[Hoang Le Truong]

def G (e:ℕ× ℕ ): ℕ :=
match  e  with
|(1,2) :=2
|(2,1) :=2
|(1,3) :=2
|(3,1) :=2
|(2,4) :=1
|(4,2) :=1
|(3,4) :=1
|(4,3) :=1
|_     :=0
end

[Hoang Le Truong]

it is ok but I want to certain domains V

[Kevin Buzzard]

Maybe you should define your function on all of nat x nat

[Kevin Buzzard]

and then just ignore its values on the elements you don't like

[Johan Commelin]

Ok, so define the function on \N \times \N, and then restrict to V

[Kenny Lau]

i'll say it isn't even a function

[Johan Commelin]

Kenny, did you read that translation of the article by Aristotle?

[Kevin Buzzard]

This is a standard trick in this game: for example the square root function in Lean is defined on all the reals, and returns the square root of x if x>=0 but just returns something random if x < 0

[Kenny Lau]

what about it

[Johan Commelin]

something random <-- Kevin

[Kevin Buzzard]

you are just making noise Kenny, not contributing, that's what about it

[Hoang Le Truong]

yes I want it

[Kevin Buzzard]

When I thought more like a mathematician, I really thought I wanted the square root function to be only defined on the non-negative reals

[Hoang Le Truong]

I want same as @Kevin Buzzard

[Kenny Lau]

I don't even know what function he wants to build. My understanding is that he wants some kind of a function defined on N x N, and then he just randomly gives some values in the two examples he gave us

[Kevin Buzzard]

but after building such a function myself, and then discovering how hard it was to use it, I started coming round to the methods which Mario and others were preaching.

[Kenny Lau]

he wants an arbitrary function N x N -> N, that's all I can make of it

[Kevin Buzzard]

right, so let's listen to him and find out more.

[Hoang Le Truong]

In fact, I have function with certain properties. I want example from such function

[Kenny Lau]

what properties?

[Kevin Buzzard]

What do you mean by "example"? You mean an example of the function, or example of a value, or example of a definition, or... ? When you say "I have function" -- you mean you have the definition of the function already? In Lean or on paper? Or you just have some properties which you want the function to satisfy?

[Kevin Buzzard]

We are still trying to understand your question.

[Sean Leather]

I think one property of the function Hoang wants is the type: ℕ × ℕ → ℕ.

[Sean Leather]

Or perhaps the type should have subsets of ℕ?

[Sean Leather]

{ns : ℕ × ℕ // p ns} → ℕ for some p : ℕ × ℕ → Prop?

[Hoang Le Truong]

graph is connected

[Hoang Le Truong]

I want check the definition of graph is correct

[Hoang Le Truong]

I think g is graph

[Kevin Buzzard]

What does this have to do with nat?

[Hoang Le Truong]

variables {α : Type }
variable graph: α × α → ℕ

[Hoang Le Truong]

I think functiongraph is graph

[Kevin Buzzard]

Is alpha the vertices of the graph? What is nat doing there?

[Hoang Le Truong]

yes

[Kevin Buzzard]

What is a graph? For me it is vertices and edges, and there is no ℕ

[Hoang Le Truong]

def G (e:ℕ× ℕ ): ℕ :=
match  e  with
|(1,2) :=2
|(2,1) :=2
|(1,3) :=2
|(3,1) :=2
|(2,4) :=1
|(4,2) :=1
|(3,4) :=1
|(4,3) :=1
|_     :=0
end

[Hoang Le Truong]

is example of graph

[Kevin Buzzard]

What is a graph for you?

[Hoang Le Truong]

vertices def V: set ℕ := {1,2,3,4}

[Kenny Lau]

so every graph is countable

[Hoang Le Truong]

I do not know

[Hoang Le Truong]

I have that definition of connected graph. I want check such definition in lean which I make is true or fail. I make an example of such definition

[Hoang Le Truong]

I make example of graph

def G (e:ℕ× ℕ ): ℕ :=
match  e  with
|(1,2) :=2
|(2,1) :=2
|(1,3) :=2
|(3,1) :=2
|(2,4) :=1
|(4,2) :=1
|(3,4) :=1
|(4,3) :=1
|_     :=0
end
````
it is ok. but

def V: set ℕ := {1,2,3,4}

def G (e:V× V ): ℕ :=
match e with
|(1,2) :=2
|(2,1) :=2
|(1,3) :=2
|(3,1) :=2
|(2,4) :=1
|(4,2) :=1
|(3,4) :=1
|(4,3) :=1
|_ :=0
end

is it not run

[Kevin Buzzard]

Aah

[Mario Carneiro]

this is the konigsberg graph?

[Kevin Buzzard]

rofl

[Hoang Le Truong]

yes

[Kevin Buzzard]

even more rofl

[Mario Carneiro]

I would use custom inductive types for all of it

[Hoang Le Truong]

no

[Mario Carneiro]

inductive vertices | north_shore | west_island | ...

[Kevin Buzzard]

@Hoang Le Truong -- he is saying that you should make your own type called graph

[Kevin Buzzard]

and I would definitely agree with him

[Mario Carneiro]

inductive edges : vertices -> vertices -> Type
| bridge1 : edges north_shore west_island
...

[Hoang Le Truong]

yes I agree

[Mario Carneiro]

It's self documenting and clear and unambiguous

[Kevin Buzzard]

and then you could formalise what it means for a graph to be connected

[Kevin Buzzard]

(for all vertices v1 and v2 there's a path from v1 to v2)

[Kevin Buzzard]

and then you could prove it in this case just by a case by case check

[Kevin Buzzard]

But for a big graph, it is not so clear that Lean is the tool for this.

[Mario Carneiro]

This gets complicated for large graphs, but you will want to switch to a different encoding anyway in that case

[Kevin Buzzard]

You might want to read about what algorithms are used to prove a graph is connected, and implement one of those, but probably you would not get good performance in comparison with a tool like python

[Mario Carneiro]

For fabs this is not a big problem

[Mario Carneiro]

If you were, say, trying to work with the graphs in the four color theorem this kind of encoding is far too dense

[Hoang Le Truong]

Yes I begin graph in general. after I restrict example

[Kevin Buzzard]

Mario I'm surprised you haven't implemented graphs in mathlib. It's just the sort of thing a computer scientist would like to do, I would have thought.

[Mario Carneiro]

The problem (which I have had also in metamath) is that "graph" means something different every time it is used

[Mario Carneiro]

and the different theories are hard to fit in the same framework

[Mario Carneiro]

even though everyone pretends it is easy

[Kevin Buzzard]

I wondered if this was why. You need directed and undirected graphs, graphs where you're allowed/not allowed to have an edge from v to v, graphs where you are/are not allowed to have more than one edge from v to w, and that's before we've even started worrying about whether all graphs are finite etc

[Hoang Le Truong]

Of course, I go this way.

[Hoang Le Truong]

Now I work only the above graph G

[Kevin Buzzard]

So maybe one way of proceeding is that you decide exactly what is a graph for you, and then make your own type, and then make a term of that type corresponding to Koenigsberg, and make a general definition for connected, and then prove that Koenigsberg is connected.

[Mario Carneiro]

And those "not allowed" things are not just constraints, they change the encoding completely, i.e. if there are no multiple edges you can have a relation instead of a set of edges with dom/cod; if it is undirected then maybe you want a function on unordered pairs, if you have hyperedges then maybe each edge maps to a set of vertices which may or may not have size 2, ...

[Mario Carneiro]

I agree that this is what Hoang should do, and it's what I did for Koenigsberg in Metamath

[Kevin Buzzard]

I can now envisage a 2500-line graph.lean which carefully does every single possibility ;-)

[Mario Carneiro]

just define things that make sense for undirected multigraphs

[Mario Carneiro]

and forget about all the other crazy stuff until the next project

[Hoang Le Truong]

I begin graph directed multiple degree have loop graph

[Hoang Le Truong]

After I restrict to undirected multiphaps
Now I only work on a above G. I have two way to define G. I want to known what is good.

[Johan Commelin]

Hoang, that was a bit of an XY problem: https://mywiki.wooledge.org/XyProblem

[Johan Commelin]

I suggest you start a new topic titled "Defining graphs in Lean"

[Johan Commelin]

It would have helped a lot if you had mentioned the word "graph" in the first few posts. Instead of just "function with properties"

[Hoang Le Truong]

How to change "function on certain domain " to Defining graphs in Lean

[Hoang Le Truong]

Ok I changed it

[Kevin Buzzard]

I have two way to define G. I want to known what is good.

I am a mathematician, and I find myself asking this question often in Lean. I think it is a very difficult and delicate question, and sometimes the computer scientist experts here answer things like "it depends on why you want this structure". My advice to you is to go ahead and formalise it in one way, and then post your actual working code and ask for comments.

[Hoang Le Truong]

I have two ways to define G. one is

inductive vertices
| a | b | c | d

def g (e:vertices× vertices ): ℕ :=
match  e  with
|(vertices.a,vertices.b) :=2
|(vertices.b,vertices.a) :=2
|(vertices.a,vertices.c) :=2
|(vertices.c,vertices.a) :=2
|(vertices.b,vertices.d) :=1
|(vertices.d,vertices.b) :=1
|(vertices.c,vertices.d) :=1
|(vertices.d,vertices.c) :=1
|_ :=0
end

and another is

def G (e:ℕ × ℕ  ): ℕ :=
match  e  with
|(1,2) :=2
|(2,1) :=2
|(1,3) :=2
|(3,1) :=2
|(2,4) :=1
|(4,2) :=1
|(3,4) :=1
|(4,3) :=1
|_     :=0
end

what is way in Lean good

[Johan Commelin]

No, that is not the definition of a graph

[Johan Commelin]

It is only 1 very specific example.

[Johan Commelin]

First you should decide if you want a general definition, or only the Koenigsberg example.

[Hoang Le Truong]

I want a general definition and after apply to example

[Johan Commelin]

So then, give a general definition, and not an example.

[Johan Commelin]

Can you first give a definition without using Lean? Just write down an informal definition here.

[Hoang Le Truong]

An Euler walk in an undirected graph is a walk that uses each edge exactly once.

[Hoang Le Truong]

this is a general definition. I formed it in Lean. Now I want to apply it to exactly example to check the definition Euler walk is correct or wrong in lean.

[Johan Commelin]

How did you put that statement into Lean?

[Hoang Le Truong]

yes

[Johan Commelin]

Please show it to us.

[Johan Commelin]

We can not help you with defining your Koenigsberg example if we don't know how you put "undirected graph" in Lean.

[Hoang Le Truong]

```definition undirected_graph ( graph:α × α → ℕ ): Prop :=
∀ u v:α, graph(u,v)=graph(v,u)

[Hoang Le Truong]

definition undirected_graph ( graph:α × α → ℕ  ): Prop :=
       ∀ u v:α, graph(u,v)=graph(v,u)

[Johan Commelin]

Right, so for your example, you need the following ingredients: a type alpha, a function alpha \times alpha \to nat and a proof that your graph is undirected.

[Johan Commelin]

There is no reason at all to take a subset of nat for alpha.

[Johan Commelin]

You could define an inductive type for the four vertices.

[Johan Commelin]

And it will allow you to define your function encoding the graph with matching.

[Johan Commelin]

Like Mario wrote above: inductive vertices | north_shore | west_island | ...

[Hoang Le Truong]

Thank you for that. I understood

[Johan Commelin]

So, that is the same thing as your first method, except Mario's suggestion is more readable

[Johan Commelin]

(For people who have walked through Koenigsberg...; or those who looked at the map on Wikipedia...)

[Johan Commelin]

Ok, so, afterwards you have to prove that the thing is undirected, and then you have to show us the formalisation of "Euler walk"