# Zulip Chat Archive

## Stream: new members

### Topic: Feasibility of graph or simplicial complex statement

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

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

#### Patrick Massot (Feb 10 2020 at 16:10):

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

#### Patrick Massot (Feb 10 2020 at 16:10):

Mario, you are assuming dependent types here, right?

#### Mario Carneiro (Feb 10 2020 at 16:10):

No

#### Mario Carneiro (Feb 10 2020 at 16:11):

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

#### Patrick Massot (Feb 10 2020 at 16:11):

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

#### Mario Carneiro (Feb 10 2020 at 16:11):

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

#### Patrick Massot (Feb 10 2020 at 16:12):

Who is "they" in this message?

#### Mario Carneiro (Feb 10 2020 at 16:12):

isabelle community

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

#### Patrick Massot (Feb 10 2020 at 16:12):

You mean they could create Isabelle/DTT?

#### Mario Carneiro (Feb 10 2020 at 16:12):

They have ZFC already

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

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

#### Mario Carneiro (Feb 10 2020 at 16:15):

Every prover does all math, to a zeroth order approximation

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

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

#### Tony (Feb 10 2020 at 16:18):

Thanks for the answers so far :)

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

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

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

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

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

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

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

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

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

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

#### Yury G. Kudryashov (Feb 10 2020 at 18:08):

BTW, who's working on graphs?

#### Kevin Buzzard (Feb 10 2020 at 18:16):

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

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

#### Johan Commelin (Feb 10 2020 at 18:33):

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

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

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

#### Johan Commelin (Feb 10 2020 at 18:33):

Especially if it works with recent mathlib

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

#### Kevin Buzzard (Feb 10 2020 at 18:37):

Thanks Vaibhav for reminding me :-)

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

#### Yury G. Kudryashov (Feb 10 2020 at 18:50):

Am I right that `llist α`

is the set of nonempty lists?

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

#### Yury G. Kudryashov (Feb 10 2020 at 18:53):

You don't have to open `section`

inside a `namespace`

.

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

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

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

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

aftereach of them gets to some advanced stage.

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

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

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

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

#### Vaibhav Karve (Feb 10 2020 at 19:01):

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

#### 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)`

.

#### 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'`

.

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

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

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

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

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

#### 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 `parameter`

s outside a `section`

. Does that mean that it is a bad idea to use `parameter`

?

#### Yury G. Kudryashov (Feb 10 2020 at 23:13):

I'm doing that because lean told me I couldn't have

`parameter`

s outside a`section`

. Does that mean that it is a bad idea to use`parameter`

?

AFAIK `parameter`

s will not work in Lean 4. Try `variable`

s.

#### 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!

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

#### Yury G. Kudryashov (Feb 12 2020 at 14:29):

I'd go with `structure`

, though maybe `structure Graph V := ...`

.

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

#### Yury G. Kudryashov (Feb 12 2020 at 14:50):

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

.

#### Yury G. Kudryashov (Feb 12 2020 at 14:50):

(probably with a better name)

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

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

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

#### Sebastien Gouezel (Feb 12 2020 at 15:06):

OK. We probably need both :)

#### Yury G. Kudryashov (Feb 12 2020 at 15:07):

Something like `structure Graph V := ...`

+ `class CanonicalGraph V := (G : Graph V)`

?

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

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

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

#### 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`

.

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

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

#### Yury G. Kudryashov (Feb 12 2020 at 18:27):

(deleted)

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

#### 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}`

?

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

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

#### Johan Commelin (Feb 12 2020 at 20:48):

Aside: wouldn't it be more natural to use `vertices`

instead of `carrier`

(in this context)?

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

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

#### Vincent Beffara (Feb 12 2020 at 20:56):

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

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

#### Vincent Beffara (Feb 12 2020 at 22:07):

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

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

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

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

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

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

#### Reid Barton (Feb 13 2020 at 21:44):

Try adding `{}`

after `sym`

like so: `(sym {} : symmetric adj)`

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

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

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

#### 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 ;-) )

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

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

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

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

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

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