universes in lean

Stream: new members

[Harsha Nyapathi]

I have tried to represent graphs and paths using inductive data type in lean.
https://github.com/enharsha/Graphs-in-Lean/blob/master/graph.lean
However, while compiling definition of path, it shows the following error - "universe level of type_of(arg #3) of 'path.addedge' is too big for the corresponding inductive datatype". Could anyone help me out? I have referred to inductive types section in Theorem Proving in Lean, where vectors have been defined in a similar fashion.

[Johan Commelin]

Well, your edges live in some universe v, and paths must live (by your definition) in universe u. That doesn't fit...

[Johan Commelin]

So, either you just use one universe, or paths should live in Type (max u v)

[Johan Commelin]

Also, when you write g : graph, I feat that Lean can't figure out the universes by itself. So maybe you need to write g : graph.{u v}

[Yury G. Kudryashov]

Another approach is to define

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

This is similar to the approach taken by category_theory.category. Not sure which approach is better.

[Jesse Michael Han]

this compiles for me:

inductive path (g : graph.{u v}) (start : g.vertex) : (g.vertex) → Type (max u v)
| fix : path start
| addedge (add : g.edge) (last : g.vertex) (p : path last) (pr : last = g.φ1 add) : path (g.φ2 add)

[Kevin Buzzard]

I know it's sacreligious to suggest this here but you could just put vertices in edges in the same universe (something mathematicians have been doing for 100 years) and then you can just forget all about them

[Harsha Nyapathi]

Yes, mismatch of the universes seems to be the issue. It compiles now. Thanks a lot!

[Yury G. Kudryashov]

@Harsha Nyapathi It seems to me that

universes v u
structure graph (α : Type u) := (edge : α → α → Type v)

requires fewer equality assumptions in various lemmas. E.g., paths can be defined as

inductive path {α : Type u} (g : graph.{v} α) (start : α) : α → Type (max v u)
| fix : path start
| addedge {last : α} (p : path last) {last' : α} (e : g.edge last last') : path last'

Of course, a downside of this approach is that you need to write {v₁ v₂ : α} (e : g.edge v₁ v₂) instead of e : g.edge.
Another bonus of this definition is that it makes easier to define, e.g., the graph corresponding to a category (no need to bundle homs with domain/codomain).