Zulip Chat Archive

Stream: new members

Topic: universes in lean


view this post on Zulip Harsha Nyapathi (Dec 24 2019 at 05:55):

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.

view this post on Zulip Johan Commelin (Dec 24 2019 at 06:00):

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

view this post on Zulip Johan Commelin (Dec 24 2019 at 06:01):

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

view this post on Zulip Johan Commelin (Dec 24 2019 at 06:01):

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}

view this post on Zulip Yury G. Kudryashov (Dec 24 2019 at 06:28):

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.

view this post on Zulip Jesse Michael Han (Dec 24 2019 at 06:41):

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)

view this post on Zulip Kevin Buzzard (Dec 24 2019 at 09:57):

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

view this post on Zulip Harsha Nyapathi (Dec 26 2019 at 11:12):

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

view this post on Zulip Yury G. Kudryashov (Dec 27 2019 at 07:15):

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


Last updated: May 09 2021 at 19:11 UTC