Feasibility of graph or simplicial complex statement

Stream: new members

[Tony]

I've very new, but I have one very specific question and one general question. (1) Say I had some proposition that came up about graphs (it's currently phrased in the language of Serre and his book on Trees) about paths/geodesics and how they "overlap", would lean be a reasonable place to try to prove it formally? (2) Is there a good source that maps the different proof languages to underlying type systems and compares them - in a way that a math person could read and then decide which is best?

[Mario Carneiro]

The underlying foundation is almost completely irrelevant when it comes to deciding which prover is most suitable for mathematician use

[Patrick Massot]

I don't understand question 2, but the answer to question 1 is yes.

[Patrick Massot]

Mario, you are assuming dependent types here, right?

[Mario Carneiro]

No

[Mario Carneiro]

Although possibly you are hitting on the "almost" in my statement wrt Isabelle limitations

[Patrick Massot]

Then I disagree. Simple types are not good enough for mathematicians

[Mario Carneiro]

It's a problem they could fix if they cared to

[Patrick Massot]

Who is "they" in this message?

[Mario Carneiro]

isabelle community

[Mario Carneiro]

The problem with simple types is not the axiomatic framework itself, but rather the tooling to support "dependent" uses

[Patrick Massot]

You mean they could create Isabelle/DTT?

[Mario Carneiro]

They have ZFC already

[Mario Carneiro]

but as a matter of course, everyone uses Isabelle/HOL and its tactics and they get an impression of the weakness of simple type theory from that

[Tony]

re:Question 2, I'm a non-expert but I would be interested to know if say, system A did dependent types (or your-favorite-thing) and system B didn't. I'd be interested to just have an accurate mapping of which concepts go where even if I didn't understand them - but also interested in which things have practical considerations and which are totally theoretical.

[Mario Carneiro]

Every prover does all math, to a zeroth order approximation

[Mario Carneiro]

the real things to worry about are whether the prover gives you enough sugar to work with it effectively

[Tony]

nCatLab is occasionally abstruse but it's still very useful just because it names concepts and organizes them. Is there a similar thing in this area?
I care about which things formally can do what but I'm also asking about the maturity of the libraries and the real human effectiveness

[Tony]

Thanks for the answers so far :)

[Mario Carneiro]

That said, if you just want to know what axiomatic system the various provers are using: Coq, Lean - CIC (dependent type theory); HOL, HOL4, HOL Light, Isabelle/HOL - HOL (simple type theory); Mizar, Metamath, Isabelle/ZF - ZFC (set theory); Agda, RedPRL, Cubicaltt, UniMath, NuPRL - specialized logics or HoTT variants

[Mario Carneiro]

The most "mature" libraries are Coq, Isabelle, and Mizar; Lean is a newcomer but it has also learned from its predecessors in a lot of ways and is I think pretty nice to use

[Tony]

I suppose there is also Idris?
This list helps!
I'm sort of hoping for me a 1-dimensional simplicial complex with boundary maps etc. will suffice for the graph (maybe this is even already done in lean) and I'll probably have to do my own work to define what I mean by path and some other data

I'd be interested if there were formal reasons to prefer dependent vs simple types but practically speaking it sounds like dependent+Lean is the way to go.

[Patrick Massot]

My honest opinion is the community is at least as important as the technology. The community here is very mathematician friendly.

[Kevin Buzzard]

As Patrick says, there is nothing in theory to stop one from formalising all of Serre's book on trees in Lean. It would take some time though! I read all the earlier chapters once but I don't recall anything about geodesics.

[Bryan Gin-ge Chen]

I vaguely recall from one of the Lean Together 2020 discussion session streams that someone was going to try to add graph theory to mathlib - is this still work in progress?

[Kevin Buzzard]

With high probability they will use a different definition of "graph". IIRC the Lean Together 2020 talk was about finite graphs, and in Serre's book there are infinite trees all over the place.

[Tony]

In my case I wouldn't need infinite things but I think an infinite path for Serre is implemented as a direct limit.

[Yury G. Kudryashov]

I hope that we'll have a general definition of a graph, then some theorems can assume fintype

[Kevin Buzzard]

You will be able to do it in Lean and Coq and Mizar, you may or may not be able to do it in Isabelle/HOL depending on whether you need dependent types or not (e.g. topological spaces don't need dependent types, sheaves on topological spaces do), and who knows whether you'll be able to do it in HoTT because the moment you ask someone about it they'll start talking about infinity-topoi :-(

[Yury G. Kudryashov]

BTW, who's working on graphs?

[Kevin Buzzard]

Someone gave a talk about it but I can't remember their name :-(

[Vincent Beffara]

I tried to implement a few things in graph theory, here https://github.com/vbeffara/lean and went as far as proving that Cayley graphs of the same group are bilipschitz equivalent, and tried to define graph minors but what I did was very awkward all over. I would love to see what someone who knows what they are doing would write :-)

BTW, is there a canonical way to say "I wrote something that does not quite fit in a chat like here, is definitely PR material, and I would like to get some feedback"?

[Johan Commelin]

@Vincent Beffara A pointer to a repository is probably the best thing (-;

[Tony]

That's cool! That's very much in my wheelhouse. Also it looks like you're already using the Serre defn

[Vaibhav Karve]

@Bryan Gin-ge Chen @Kevin Buzzard I was the one who talked about wanting to add graph theory to lean. I am still working on the basic definitions right now (with the help of an undergraduate here at Univ. of Illinois Urbana-Champaign). I hope to have some code ready to show here in a few weeks. We are only getting started.

[Johan Commelin]

Especially if it works with recent mathlib

[Johan Commelin]

@Vincent Beffara You could always take a look at graph libraries in coq. (Disclaimer: I have never actually studied a coq library myself.)

[Kevin Buzzard]

Thanks Vaibhav for reminding me :-)

[Yury G. Kudryashov]

@Vaibhav Karve @Vincent Beffara Probably it makes sense for you to collaborate on this. I assume that we don't want to have to choose between two approaches after each of them gets to some advanced stage.

[Yury G. Kudryashov]

Am I right that llist α is the set of nonempty lists?

[Yury G. Kudryashov]

BTW, I wouldn't include symmetric in the basic definition. It makes sense to consider oriented graphs in many cases.

[Yury G. Kudryashov]

You don't have to open section inside a namespace.

[Kevin Buzzard]

BTW, I wouldn't include symmetric in the basic definition. It makes sense to consider oriented graphs in many cases.

aah it's started already :-) There are 10 different definitions :-)

[Tony]

Depending on who you talk to, there's a few defn of "graph" out there: (1) subset of V x V (2) Serre (3) specialization of cell-complex (simplicial, delta, CW?) to 1-dim.

[Yury G. Kudryashov]

I don't know Serre's definition. I speak based on my math/programming experience with using graphs in other theories.

[Vaibhav Karve]

Vaibhav Karve Vincent Beffara Probably it makes sense for you to collaborate on this. I assume that we don't want to have to choose between two approaches after each of them gets to some advanced stage.

Thanks for the suggestion. I have PM'ed him.

[Yury G. Kudryashov]

I don't know if it makes sense to allow multiple edges between a given pair of vertices. On the one hand, sometimes it makes sense (e.g., interpreting a category as a graph). On the other hand, it probably makes the definition/code harder to read.

[Tony]

It is nice to be able to have them as a specialization of a cell-complex so you can cone off or add things but it depends on what you're doing. (I don't currently need it but having general cell-complex stuff implemented would be really neat)

For Serre a graph is a set of edges and vertices where you think of the edges as being directed. Formally there's a map called * from E to E such that (e)=e and e* != e and a initial and terminal boundary map from E to V that satisfies b_initial(e)=b_terminal(e*)

[Tony]

( To get from a Serre graph to a combinatorial graph you can take combinatorial edges to be pairs of directed edges {e, e*} )

[Vaibhav Karve]

The results I am interested in in graph theory very much require multi-edges, for example.

[Yury G. Kudryashov]

Then we should have something like

structure Graph := (V : Type u) (E : Type u) (start end : E → V)

or

universes v u
structure Graph := (V : Type u) (edges : V → V → Sort v)

or

universes v u
structure graph (V : Type u) := (edges : V → V → Sort v)

Maybe this should be called MultiGraph, then graph can extend it adding the axiom ∀ x y, subsingleton (edges x y).

[Yury G. Kudryashov]

With the (V, E) approach you'll have a lot of equality assumptions here and there, and you'll have to rewrite on them. With the edges : V → V → Sort v approach you'll have troubles whenever you have (x y y' z : V) (e : edges x y) (e' : edges y' z) (h : y = y') (f : Π x y z, edges x y → edges y z → α) and want to write f _ _ _ e e'.

[Vincent Beffara]

Am I right that llist α is the set of nonempty lists?

Yes, precisely. I tried with V \times list V, lean had trouble with recursion, so then I tried to define everything in terms of something like fold but in the end a type with explicit constructors was easier to work with

[Vincent Beffara]

BTW, I wouldn't include symmetric in the basic definition. It makes sense to consider oriented graphs in many cases.

Sure, and whether v should be adjacent to itself (it makes some definitions easier, and graph minors awful with all the loops ...)

[Vincent Beffara]

I don't know if it makes sense to allow multiple edges between a given pair of vertices. On the one hand, sometimes it makes sense (e.g., interpreting a category as a graph). On the other hand, it probably makes the definition/code harder to read.

It makes sense in many contexts to have adj : V -> V -> W for some labelling type W that would be Prop (or bool ? I seem to remember that in Coq it makes a huge difference for some reason, probably due to decidability/proof irrelevance/something) for usual graphs, but W = \nat gives multiplicity, probabilists like W = nnreal, computer scientists like to put a monoid there.

Is it easy to add that after the fact, or would it be better to start in more generality?

[Vincent Beffara]

It is nice to be able to have them as a specialization of a cell-complex so you can cone off or add things but it depends on what you're doing. (I don't currently need it but having general cell-complex stuff implemented would be really neat)

For Serre a graph is a set of edges and vertices where you think of the edges as being directed. Formally there's a map called * from E to E such that (e)=e and e* != e and a initial and terminal boundary map from E to V that satisfies b_initial(e)=b_terminal(e*)

That seems to be what they do in Coq libraries, they have types for both vertices and edges rather than an adjacency relation IIRC

[Vincent Beffara]

With the (V, E) approach you'll have a lot of equality assumptions here and there, and you'll have to rewrite on them. With the edges : V → V → Sort v approach you'll have troubles whenever you have (x y y' z : V) (e : edges x y) (e' : edges y' z) (h : y = y') (f : Π x y z, edges x y → edges y z → α) and want to write f _ _ _ e e'.

Path concatenation caused me some trouble with the V -> V -> Prop option (with a Path x y type), indeed. Still felt more manageable to me than the (V,E) version.

[Vincent Beffara]

You don't have to open section inside a namespace.

I'm doing that because lean told me I couldn't have parameters outside a section. Does that mean that it is a bad idea to use parameter?

[Yury G. Kudryashov]

I'm doing that because lean told me I couldn't have parameters outside a section. Does that mean that it is a bad idea to use parameter?

AFAIK parameters will not work in Lean 4. Try variables.

[Sebastien Gouezel]

BTW, is there a canonical way to say "I wrote something that does not quite fit in a chat like here, is definitely PR material, and I would like to get some feedback"?

@Vincent Beffara , here is some feedback :)

Let me just look at the first line of your file, i.e.,

structure Graph := (V : Type) (adj : V -> V -> Prop) (sym : symmetric adj)

because there is a lot to say on this, and it determines everything that follows. What you are doing here is called a fully bundled approach, i.e., a Graph object contains a carrier type, and additional data on this type. This is the way things are typically done in coq. The usual approach in Lean is just a little bit more unbundled: we would start from a type, say V, and then we would tell Lean that this type has a graph structure by registering a graph typeclass. An advantage of this approach is that you work with a single underlying type, and you can put several structures on it (a graph structure, a group structure, and so on), and you can discuss how they relate "from the inside". It would read something like

class Graph (V : Type*) :=
(adj : V -> V -> Prop)
(sym : symmetric adj)

Let me show what the next lines could look like, to show how one uses such typeclasses:

namespace Graph

variables {V : Type*} {V' : Type*} [Graph V]  [Graph V']

def linked (x y : V) := relation.refl_trans_gen adj x y

class connected_graph (V : Type*) extends Graph V :=
(connected : ∀ (x : V) y, linked x y)

@[ext] structure edge (V : Type*) [Graph V] :=
{x y : V}
(h : adj x y)

First, I enter a namespace, to make sure that I keep my names separated from other areas where one could use the words edge, for instance, and also to make adj available. Then, I declare some variables and some typeclasses that will be available from this point on, to avoid restating them all the time. The interesting point is when I define linked: there is no explicit reference to the graph structure, but since I am mentioning points on V Lean will try to find the graph structure on V (which is given by the typeclass declared two lines above) and understand by itself that adj refers to this graph structure.

Then in your file you have two definitions of connected, that I have merged in one single definition because I don't see why we would need two. And I have declared it as a type class extending Graph, which means that you will only need to declare [connected_graph V] if you want to assume that there is a connected graph structure on V, without writing [Graph V] first.

If you have some questions about what I have just written, or if you would be interested in the same kind of "standardification" on some other parts of your files, don't hesitate to ask!

[Yury G. Kudryashov]

I'm not sure that I like graphs as typeclasses. I assume that typeclasses are for canonical structures, and I can't think of any canonical graph structure on a type.

[Yury G. Kudryashov]

I'd go with structure, though maybe structure Graph V := ....

[Sebastien Gouezel]

For instance, if G is a group and S is a generating set, then its Cayley graph Cay S (which, as a type, is just a copy of G, but it really should be distinguished from G) has a canonical graph structure. I think it is important to do it this way because then you want to deduce a distance on Cay S and do some analysis/geometry, for which you need the metric space typeclass. You can not get the metric space typeclass if you don't have first a graph typeclass to start with.

[Yury G. Kudryashov]

You can have a generic type tag graph_dist V G := V.

[Yury G. Kudryashov]

(probably with a better name)

[Sebastien Gouezel]

Sure, but I don't see the advantage compared to a graph typeclass. If you want to do some finite graph theory, or some automaton theory, you will start with a type with a graph structure, and you will work with this structure, just like you would do with a group structure or with a metric space structure, so typeclasses look like a good choice. Of course, if you start putting several graph structures on the same type, you would need to play the @ dance, just like for metric spaces say.

[Yury G. Kudryashov]

In my experience dealing with several graphs on the same type is more common than dealing with several distances.

[Yury G. Kudryashov]

E.g., I'd prefer to do common operations like adding/removing an edge without introducing new type tags.

[Sebastien Gouezel]

OK. We probably need both :)

[Yury G. Kudryashov]

Something like structure Graph V := ... + class CanonicalGraph V := (G : Graph V)?

[Sebastien Gouezel]

Or just structure Graph V := ... and attribute [class] Graph, but many theorems would be stated with the structure as an explicit argument. It is a little bit like the problem for measure spaces, where one would like to have an implicit measure when building the theory or when doing probability, but an explicit measure when doing analysis.

[Vincent Beffara]

I'm trying to understand this whole typeclass thing ... I get the unbundling of the carrier type, but certainly

@[ext] structure edge {V : Type*} (G : Graph V) :=
{x y : V}
(h : adj G x y)

feels more natural to me than

@[ext] structure edge (V : Type*) [Graph V] :=
{x y : V}
(h : adj x y)

I don't see how having the graph structure being implicit would help comparing two graphs on the same carrier?

[Vincent Beffara]

(At the beginning I did have Graph V, I tried bundling to also try coercions at the same time)

[Sebastien Gouezel]

I don't see how having the graph structure being implicit would help comparing two graphs on the same carrier?

The graph structure being implicit is useful when you have one single graph on some type, and you want to talk about it without ever modifying it. If you want to modify a graph, or have several graph structures, then you should go for the structure approach (but still with Graph V instead of having V as a data inside the graph structure, as this is the way everything is done in Lean, so once you want to interface with other parts of the library it will be much easier this way).

One subtely though: metric space structures are implicit type classes in all mathlib, because most of the time you use just one such structure on the space, and you don't want to specify it all the time. This means that if you want to put a metric space structure on a type using the graph distance, then different graphs will give you different distances, and things will become messy. A trick in situations like that (which is in fact more than a trick) is to have copies of the same type, but with different names. For instance, if you have a group G and a generating set S, then you could define Cay S to be a copy of G, and endow it with the graph distance coming from the Cayley graph structure for the generating S. In this way, you get different metric spaces structures on the different Cay S, which to Lean kernel are the same, but to typeclass resolution are different. If the graph structure was a typeclass, then this would also work well here, as you would put different graph structures on different Cay S.

[Tony]

I'm not sure if this kind of double induction is more or less amenable to how things are done in Lean but it's yet another way: Capture.PNG

[Johan Commelin]

I think that something like that is certainly possible, but that exact definition will be really awkward to work with.

[Yury G. Kudryashov]

(deleted)

[Vincent Beffara]

One subtely though: metric space structures are implicit type classes in all mathlib, because most of the time you use just one such structure on the space, and you don't want to specify it all the time. This means that if you want to put a metric space structure on a type using the graph distance, then different graphs will give you different distances, and things will become messy. A trick in situations like that (which is in fact more than a trick) is to have copies of the same type, but with different names. For instance, if you have a group G and a generating set S, then you could define Cay S to be a copy of G, and endow it with the graph distance coming from the Cayley graph structure for the generating S. In this way, you get different metric spaces structures on the different Cay S, which to Lean kernel are the same, but to typeclass resolution are different. If the graph structure was a typeclass, then this would also work well here, as you would put different graph structures on different Cay S.

This seems to have something to do with the fact that a graph structure given a type is not canonical, while a metric structure given a graph is canonical (are there cases where a graph is endowed with a metric that is not the graph distance ?) At least lurking in this chatroom, and reading some of your comments, makes me afraid to use typeclasses here.

[Vincent Beffara]

Isn't the case where you have one graph structure that you want to talk about covered by parameter (G : Graph V) or perhaps variable {G : Graph V} ?

[Sebastien Gouezel]

I never used parameters. variable is just a shorthand: it means that instead of writing my_beautiful_theorem {V : Type*} {G : Graph V} ... you can just write my_beautiful_theorem .... The theorems with one syntax or the other are exactly the same.

The summary is: if you will just use one graph structure on your type, go for typeclasses. Otherwise, use a structure, and pass it as one of the arguments of all your theorems, eiter as {G : Graph V} if it can be inferred by some other data in the statement of the theorem, or as (G : Graph V) otherwise. This can be done explicitly in all your statements if needed, or using a variable at the beginning of the section to avoid repetitions.

[Vincent Beffara]

So like this ?

def carrier {V : Type} (G : Graph V) := V

noncomputable instance {V : Type} (G : Graph V) [Graph.connected_graph G] : has_dist (carrier G)
    := ⟨λ x y, G.dist x y⟩

def id_S : carrier (Cay S1) -> carrier (Cay S2) := id

theorem bilipschitz : ∃ K, lipschitz_with K (id_S S1 S2) := sorry

[Johan Commelin]

Aside: wouldn't it be more natural to use vertices instead of carrier (in this context)?

[Vincent Beffara]

Aside: wouldn't it be more natural to use vertices instead of carrier (in this context)?

It would :-)

[Vincent Beffara]

Shouldn't I be afraid that lean will see through what I am trying to do, unfold (Cay S1).vertices and (Cay S2).vertices, see that they are the underlying group, forget about the graphs, and then fail to select the right instance of has_dist?

[Vincent Beffara]

(Well probably not, since it seems to work...)

[Sebastien Gouezel]

Typeclass search will never unfold anything, unless it is marked reducible. So, the following would work if you had defined graphs as typeclasses (I understand that you don't want to do it, but still I would like to show how it would work :)

class Graph (V : Type*) :=
(adj : V → V → Prop)

instance Graph.to_metric_space {V : Type*} [Graph V] : metric_space V := sorry

def Cay {G : Type*} [group G] (S : set G) : Type* := G

instance {G : Type*} [group G] (S : set G) : Graph (Cay S) := sorry

instance {G : Type*} [group G] (S : set G) : metric_space (Cay S) := by apply_instance

In the first sorry, you would explain to Lean how a graph structure gives a metric space structure. In the second sorry, you would construct the Cayley graph structure on Cay S, which is just G in disguise. And then Lean knows that Cay S is a graph, and therefore a metric space thanks to the first instance. The last line is only there to check that Lean does indeed know this, but it can be safely removed.

[Vincent Beffara]

OK, thanks, it is beginning to slowly sink in :-)

[Kevin Buzzard]

Do we have any reason to believe that fully bundled structures a la category theory will be easier to work with in Lean 4? One nice thing about partially bundled structures is that morphisms are actually functions -- although when you start dealing with e.g. algebra maps then they become types again.

[Reid Barton]

At least coercions to functions should work better in Lean 4, so applying a morphism as a function should work more reliably. But it mostly works fine already in Lean 3, if the morphism is a variable for instance.

[Yury G. Kudryashov]

One of the downsides of using structure Graph instead of structure Graph V is that with structure Graph it's much harder to consider two graphs on the same type because you can't rely on G.V = G'.V being a rfl anymore.

[Vincent Beffara]

So I tried the type class route, but I'm confused about something:

@[ext] class Graph (V : Type) := (adj : V -> V -> Prop) (sym : symmetric adj)
#check Graph.adj -- Graph.adj : ?M_1 → ?M_1 → Prop
#check Graph.sym -- Graph.sym : ∀ (V : Type) [c : Graph V], symmetric Graph.adj

Why is the V parameter implicit (or meta-variable-ish) in adj and not in sym? Is there a way to set things up so that one can use the symmetry assumption as Graph.sym rather than Graph.sym G? In all cases I met, Graph.sym _ works just fine ...

[Vincent Beffara]

Second question, still following the type class option, how do you say "there is a graph structure on type G that satisfies this and that property"? Is it just ∃ C : Graph G and then use all the definitions and theorems with @ all over to specify the instance every time?

[Reid Barton]

Try adding {} after sym like so: (sym {} : symmetric adj)

[Reid Barton]

For the second question, usually you should also be able to write ∃ C : Graph G, by exactI ...

[Reid Barton]

by exactI ... is a variant of by exact ... (which in turn is more or less the same as just the ...) that makes all variables in the context available for instance search.

[Reid Barton]

Normally, the rule is that only variables to the left of the : in the def/lemma statement are available. Variables introduced by a pi/exists/etc. are not.

[Vincent Beffara]

Try adding {} after sym like so: (sym {} : symmetric adj)

Ah, thanks, that works! (but the notation is not easy to guess ;-) )

[Yury G. Kudryashov]

@Vincent Beffara I'd go with @[class] structure Graph V := (adj : V → V → Prop), then you'll have a normal structure for non-canonical graphs while being able to write instance ... : Graph V for canonical graphs.

[Yury G. Kudryashov]

As of now, I see one use case of a canonical graph (auto coercion to a metric space), and I'd do it with

def graph_space {V} (G : Graph V) := V
instance graph_space.emetric_space {V} {G : Graph V} : emetric_space (graph_space G) :=
{ edist := λ x y, G.edist x y, .. }
instance graph_space.metric_space {V} {G : Graph V} [connected_graph G] : metric_space (graph_space G) :=
...

[Sebastien Gouezel]

I agree with Yury that this is probably the best approach. For instance, if you want to do percolation at some point, you will have a bunch of different random graphs on Z^d, so registering them as a type class would be a really bad idea. But having a copy of the space associated to the graph makes it possible to use a metric space structure as he explains.

[Vincent Beffara]

OK thanks, that feels reasonable. Will it be easy to apply a theorem using [Graph G] to a specific graph (G : Graph V)? Just use lots of @ and _ and plug G where it expects an instance of [Graph G]? Or would it have to be something weird like

instance {V} (G : Graph V) : Graph (graph_space G) := G

[Yury G. Kudryashov]

I'd formulate most theorems with (G : Graph V) or {G : Graph V}, then it will be easy to apply them in both scenarios.

[Yury G. Kudryashov]

And you can have

def the_graph (V) [G : Graph V] := G

for those cases when you want to specify explicitly that you're dealing with the canonical graph.