Zulip Chat Archive

Stream: new members

Topic: Feasibility of graph or simplicial complex statement


view this post on Zulip Tony (Feb 10 2020 at 16:08):

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?

view this post on Zulip Mario Carneiro (Feb 10 2020 at 16:10):

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

view this post on Zulip Patrick Massot (Feb 10 2020 at 16:10):

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

view this post on Zulip Patrick Massot (Feb 10 2020 at 16:10):

Mario, you are assuming dependent types here, right?

view this post on Zulip Mario Carneiro (Feb 10 2020 at 16:10):

No

view this post on Zulip Mario Carneiro (Feb 10 2020 at 16:11):

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

view this post on Zulip Patrick Massot (Feb 10 2020 at 16:11):

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

view this post on Zulip Mario Carneiro (Feb 10 2020 at 16:11):

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

view this post on Zulip Patrick Massot (Feb 10 2020 at 16:12):

Who is "they" in this message?

view this post on Zulip Mario Carneiro (Feb 10 2020 at 16:12):

isabelle community

view this post on Zulip Mario Carneiro (Feb 10 2020 at 16:12):

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

view this post on Zulip Patrick Massot (Feb 10 2020 at 16:12):

You mean they could create Isabelle/DTT?

view this post on Zulip Mario Carneiro (Feb 10 2020 at 16:12):

They have ZFC already

view this post on Zulip Mario Carneiro (Feb 10 2020 at 16:13):

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

view this post on Zulip Tony (Feb 10 2020 at 16:14):

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.

view this post on Zulip Mario Carneiro (Feb 10 2020 at 16:15):

Every prover does all math, to a zeroth order approximation

view this post on Zulip Mario Carneiro (Feb 10 2020 at 16:16):

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

view this post on Zulip Tony (Feb 10 2020 at 16:17):

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

view this post on Zulip Tony (Feb 10 2020 at 16:18):

Thanks for the answers so far :)

view this post on Zulip Mario Carneiro (Feb 10 2020 at 16:20):

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

view this post on Zulip Mario Carneiro (Feb 10 2020 at 16:22):

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

view this post on Zulip Tony (Feb 10 2020 at 16:29):

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.

view this post on Zulip Patrick Massot (Feb 10 2020 at 16:30):

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

view this post on Zulip Kevin Buzzard (Feb 10 2020 at 17:30):

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.

view this post on Zulip Bryan Gin-ge Chen (Feb 10 2020 at 17:36):

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?

view this post on Zulip Kevin Buzzard (Feb 10 2020 at 17:57):

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.

view this post on Zulip Tony (Feb 10 2020 at 18:03):

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

view this post on Zulip Yury G. Kudryashov (Feb 10 2020 at 18:06):

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

view this post on Zulip Kevin Buzzard (Feb 10 2020 at 18:07):

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 :-(

view this post on Zulip Yury G. Kudryashov (Feb 10 2020 at 18:08):

BTW, who's working on graphs?

view this post on Zulip Kevin Buzzard (Feb 10 2020 at 18:16):

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

view this post on Zulip Vincent Beffara (Feb 10 2020 at 18:26):

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"?

view this post on Zulip Johan Commelin (Feb 10 2020 at 18:33):

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

view this post on Zulip Tony (Feb 10 2020 at 18:33):

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

view this post on Zulip Vaibhav Karve (Feb 10 2020 at 18:33):

@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.

view this post on Zulip Johan Commelin (Feb 10 2020 at 18:33):

Especially if it works with recent mathlib

view this post on Zulip Johan Commelin (Feb 10 2020 at 18:33):

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

view this post on Zulip Kevin Buzzard (Feb 10 2020 at 18:37):

Thanks Vaibhav for reminding me :-)

view this post on Zulip Yury G. Kudryashov (Feb 10 2020 at 18:49):

@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.

view this post on Zulip Yury G. Kudryashov (Feb 10 2020 at 18:50):

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

view this post on Zulip Yury G. Kudryashov (Feb 10 2020 at 18:53):

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

view this post on Zulip Yury G. Kudryashov (Feb 10 2020 at 18:53):

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

view this post on Zulip Kevin Buzzard (Feb 10 2020 at 18:53):

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 :-)

view this post on Zulip Tony (Feb 10 2020 at 18:55):

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.

view this post on Zulip Yury G. Kudryashov (Feb 10 2020 at 18:56):

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

view this post on Zulip Vaibhav Karve (Feb 10 2020 at 18:58):

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.

view this post on Zulip Yury G. Kudryashov (Feb 10 2020 at 18:59):

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.

view this post on Zulip Tony (Feb 10 2020 at 18:59):

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*)

view this post on Zulip Tony (Feb 10 2020 at 19:01):

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

view this post on Zulip Vaibhav Karve (Feb 10 2020 at 19:01):

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

view this post on Zulip Yury G. Kudryashov (Feb 10 2020 at 19:06):

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).

view this post on Zulip Yury G. Kudryashov (Feb 10 2020 at 19:16):

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'.

view this post on Zulip Vincent Beffara (Feb 10 2020 at 19:29):

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

view this post on Zulip Vincent Beffara (Feb 10 2020 at 19:31):

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 ...)

view this post on Zulip Vincent Beffara (Feb 10 2020 at 19:34):

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?

view this post on Zulip Vincent Beffara (Feb 10 2020 at 19:36):

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

view this post on Zulip Vincent Beffara (Feb 10 2020 at 19:39):

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.

view this post on Zulip Vincent Beffara (Feb 10 2020 at 21:59):

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?

view this post on Zulip Yury G. Kudryashov (Feb 10 2020 at 23:13):

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.

view this post on Zulip Sebastien Gouezel (Feb 12 2020 at 14:09):

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!

view this post on Zulip Yury G. Kudryashov (Feb 12 2020 at 14:28):

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.

view this post on Zulip Yury G. Kudryashov (Feb 12 2020 at 14:29):

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

view this post on Zulip Sebastien Gouezel (Feb 12 2020 at 14:48):

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.

view this post on Zulip Yury G. Kudryashov (Feb 12 2020 at 14:50):

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

view this post on Zulip Yury G. Kudryashov (Feb 12 2020 at 14:50):

(probably with a better name)

view this post on Zulip Sebastien Gouezel (Feb 12 2020 at 15:00):

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.

view this post on Zulip Yury G. Kudryashov (Feb 12 2020 at 15:04):

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

view this post on Zulip Yury G. Kudryashov (Feb 12 2020 at 15:05):

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

view this post on Zulip Sebastien Gouezel (Feb 12 2020 at 15:06):

OK. We probably need both :)

view this post on Zulip Yury G. Kudryashov (Feb 12 2020 at 15:07):

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

view this post on Zulip Sebastien Gouezel (Feb 12 2020 at 15:15):

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.

view this post on Zulip Vincent Beffara (Feb 12 2020 at 16:27):

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?

view this post on Zulip Vincent Beffara (Feb 12 2020 at 16:30):

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

view this post on Zulip Sebastien Gouezel (Feb 12 2020 at 16:54):

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.

view this post on Zulip Tony (Feb 12 2020 at 17:45):

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

view this post on Zulip Johan Commelin (Feb 12 2020 at 17:57):

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

view this post on Zulip Yury G. Kudryashov (Feb 12 2020 at 18:27):

(deleted)

view this post on Zulip Vincent Beffara (Feb 12 2020 at 19:14):

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.

view this post on Zulip Vincent Beffara (Feb 12 2020 at 19:16):

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} ?

view this post on Zulip Sebastien Gouezel (Feb 12 2020 at 19:31):

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.

view this post on Zulip Vincent Beffara (Feb 12 2020 at 20:46):

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

view this post on Zulip Johan Commelin (Feb 12 2020 at 20:48):

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

view this post on Zulip Vincent Beffara (Feb 12 2020 at 20:51):

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

It would :-)

view this post on Zulip Vincent Beffara (Feb 12 2020 at 20:56):

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?

view this post on Zulip Vincent Beffara (Feb 12 2020 at 20:56):

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

view this post on Zulip Sebastien Gouezel (Feb 12 2020 at 21:47):

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.

view this post on Zulip Vincent Beffara (Feb 12 2020 at 22:07):

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

view this post on Zulip Kevin Buzzard (Feb 12 2020 at 22:09):

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.

view this post on Zulip Reid Barton (Feb 12 2020 at 22:10):

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.

view this post on Zulip Yury G. Kudryashov (Feb 13 2020 at 01:24):

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.

view this post on Zulip Vincent Beffara (Feb 13 2020 at 21:35):

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 ...

view this post on Zulip Vincent Beffara (Feb 13 2020 at 21:43):

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?

view this post on Zulip Reid Barton (Feb 13 2020 at 21:44):

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

view this post on Zulip Reid Barton (Feb 13 2020 at 21:44):

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

view this post on Zulip Reid Barton (Feb 13 2020 at 21:46):

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.

view this post on Zulip Reid Barton (Feb 13 2020 at 21:47):

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.

view this post on Zulip Vincent Beffara (Feb 13 2020 at 21:48):

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

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

view this post on Zulip Yury G. Kudryashov (Feb 13 2020 at 21:54):

@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.

view this post on Zulip Yury G. Kudryashov (Feb 13 2020 at 21:58):

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) :=
...

view this post on Zulip Sebastien Gouezel (Feb 13 2020 at 22:37):

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.

view this post on Zulip Vincent Beffara (Feb 13 2020 at 22:49):

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

view this post on Zulip Yury G. Kudryashov (Feb 13 2020 at 23:30):

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

view this post on Zulip Yury G. Kudryashov (Feb 13 2020 at 23:32):

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.


Last updated: May 15 2021 at 23:13 UTC