Structure for simple graphs

Stream: new members

[Vaibhav Karve]

I am trying to create the following structure.

structure SimpleGraph (α : Type) :=
(vertexset : set α)
(adjacent : set (vertexset × vertexset))

But then, i am unable to create this graph object.

def triangle_graph : SimpleGraph ℕ :=
  {SimpleGraph . vertexset := {1, 2, 3},
                 adjacent  := {(1, 2), (2, 3), (3, 1)}}

Lean gives me the following error, but I don't know what it means.

failed to synthesize type class instance for
⊢ has_insert (ℕ × ℕ) (set (↥(set.insert 3 (set.insert 2 {1})) × ↥(set.insert 3 (set.insert 2 {1}))))

[Kevin Buzzard]

Your adjacent seems to me to have type set ℕ × ℕ rather than what you want. set alpha is actually just alpha -> Prop, so vertexset is a function. You treat it as a type, which Lean deals with internally by coercing it to a subtype of alpha, but now a term of type vertexset × vertexset must be of the form (a,b) with a and b having type not alpha but the subtype.

[Vaibhav Karve]

@Kevin Buzzard Does import data.set have any effect on this?

[Kevin Buzzard]

No. [edit: yes]

[Vaibhav Karve]

Thank you. How then can I translate the idea that "A vertexset is a set of elements of type alpha"?

[Patrick Massot]

It may have.

[Patrick Massot]

I think the coercion from set to type is in mathlib

[Kevin Buzzard]

Oh!

[Patrick Massot]

With no import at all, Lean probably won't like the definition.

[Kevin Buzzard]

I would knock up some code but I switched computers yesterday so currently have no Lean. Hang on...

[Vaibhav Karve]

With no import at all, Lean probably won't like the definition.

You are right about that. I had included the import already. Just forgot to mention it in my original question.

[Kevin Buzzard]

3 is not a great thing to be using. When Lean sees 3 it immediately wants to know what the definition of addition and 1 are, and then defines 3 to basically be 1 + 1 + 1. That's fine for nat, but this is type theory, not set theory, and vertexset is a type. I guess I would not use sets at all.

structure SimpleGraph (V : Type) :=
(adjacent : set (V × V))

inductive V3
| a : V3
| b : V3
| c : V3

open V3

def triangle_graph : SimpleGraph V3 :=
  {adjacent  := {((a, b)), (b, c), (c, a)}}

[Bryan Gin-ge Chen]

There's also the approach of this gist of @Jeremy Avigad.

[Kevin Buzzard]

The reason we don't have graphs in mathlib is that everyone seems to have slightly different ideas about what a graph is, and people are reluctant to choose one way of setting it up with no applications in sight, in case the applications work much better with another choice. For example I could imagine a whole bunch of stuff could be made much easier if you're analysing a bunch of graphs all of whose vertex sets are subsets of alpha. But for other people this might just get in the way -- if I want a triangle graph I might not want to introduce some auxiliary type which contains my vertices and possibly other stuff, because then I will forever be having to supply proofs that a given vertex is in my set of vertices.

[Vaibhav Karve]

That makes sense. I do have a particular theorem in mind I wish to formalize. So it might still be worth the effort for me to try and have graphs in Lean.

[Vaibhav Karve]

@Bryan Gin-ge Chen Whoa! Thanks, this looks really useful.

[Kevin Buzzard]

It's definitely worth having graphs in Lean! There are complicated questions about which versions of the definition we should have in mathlib but the question you want to know the answer to is how best to formalise them in such a way that your life is easier

[Marc Huisinga]

(deleted)

[Vaibhav Karve]

I think the coercion from set to type is in mathlib

I looked around and found this line in mathlib. The comment says it is set coercion, but i don't see a function that i can simply borrow and use.

So now my new question is: is there a function that given a Type returns a Set of values that inhabit that type? Is there also a function that does the opposite?

[Simon Hudon]

set.univ will give you the set of objects that inhabits a type. Set coercion to type will do the opposite. There is an operator to do it but Lean inserts coercions automatically. The operator is ↥ and is typed as \u-|

[Kevin Buzzard]

If you are really sure that you want to use sets, then set.univ : set α is the set of values that inhabit α. This is just the function α -> Prop sending everything to True. But conversely given S : set α you already have alpha, it's mentioned in the type of S. But do be clear about what a set is -- there is no such thing as a random set in type theory, you should think of sets as being subsets of a given type, and you might find that subtypes work just as well.