Universe issues with dependent walks

Stream: lean4

[Peter Nelson]

I am trying to tinker with walks in multigraphs and how they relate to simple graphs, and I'm running into a universe issue which is related to the one mentioned in docs#PSigma .

The structure I am trying to define is a walk $x_0, e_1, x_1, \dotsc, e_n, x_n$ in a multigraph, where the $x_i$ are vertices and the $e_i$ are edges. If the $x_i$ and $e_i$ have fixed types, then this is a nice notion of multigraph walk.

However, if we allow $e_{i+1}$ to have a type (sort) that depends on $x_i$ and $x_{i+1}$, then this also generalizes walks in simple graphs, since $e_i$ can be a proof of adjacency. So I really want Sort in the code below.

But the basic definitions give universe problems, like so :

import Mathlib.Data.List.Basic

variable {α β γ : Type*} {ε : α → α → Sort*} {a b c x y z : α}

universe u v

/-- A `DWalk a b` (dependent walk from `a` to `b`) is a list of the form
`a = a₀, e₁, a₁, e₂, ..., eₙ, aₙ = b`, where each `aᵢ` has type `α`,
and each `e_(i+1)` has type `ε a_i a_{i+1}`.

If `ε := fun _ _ ↦ β`, then the `eᵢ` are simply terms (edges) in `β`.
If `G : SimpleGraph α`, then `DWalk G.Adj a b` is equivalent to `SimpleGraph.Walk a b`.

 -/
inductive DWalk {α : Type u} (ε : α → α → Sort v) : α → α → Type (max u v) where
  /-- The `DWalk` with no edges at a vertex `a`. -/
  | nil (x : α) : DWalk ε x x
  /-- Add an edge `(x, e, y)` to the beginning of `w : DWalk y z`. -/
  | cons (x : α) {y z : α} (e : ε x y) (W : DWalk ε y z) : DWalk ε x z

namespace DWalk

/-- a triple `⟨a,b,e⟩` with `e : ε a b` -/
structure Dart {α : Type u} (ε : α → α → Sort v) where
  fst : α
  snd : α
  edge : ε fst snd

/-- The list of darts of a `DWalk`-/
def darts {α : Type u} {ε : α → α → Sort v} {x y : α}  : DWalk ε x y → List (Dart ε)
  | nil x => []
  | cons x (y := y) e W => (Dart.mk x y e) :: W.darts

/-
stuck at solving universe constraint
  ?u.2098+1 =?= max (u+1) v
while trying to unify
  Type ?u.2098 : Type (?u.2098 + 1)
with
  Sort (max (u + 1) v) : Type (max (u + 1) v)

(Same error occurs with `#check List (Dart ε)`)
-/

Is there any way around this?

[Jihoon Hyun]

Separating the definition for Prop and Type works:

import Mathlib.Data.List.Basic

variable {α β γ : Type*} {ε : α → α → Sort*} {a b c x y z : α}

universe u v

/-- A `DWalk a b` (dependent walk from `a` to `b`) is a list of the form
`a = a₀, e₁, a₁, e₂, ..., eₙ, aₙ = b`, where each `aᵢ` has type `α`,
and each `e_(i+1)` has type `ε a_i a_{i+1}`.

If `ε := fun _ _ ↦ β`, then the `eᵢ` are simply terms (edges) in `β`.
If `G : SimpleGraph α`, then `DWalk G.Adj a b` is equivalent to `SimpleGraph.Walk a b`.

 -/
inductive DWalk {α : Type u} (ε : α → α → Sort v) : α → α → Sort (max (u + 1) v) where
  /-- The `DWalk` with no edges at a vertex `a`. -/
  | nil (x : α) : DWalk ε x x
  /-- Add an edge `(x, e, y)` to the beginning of `w : DWalk y z`. -/
  | cons (x : α) {y z : α} (e : ε x y) (W : DWalk ε y z) : DWalk ε x z

namespace DWalk

/-- a triple `⟨a,b,e⟩` with `e : ε a b` -/
structure Dart {α : Type u} (ε : α → α → Sort v) where
  fst : α
  snd : α
  edge : ε fst snd

/-- The list of darts of a `DWalk`-/
def pdarts {α : Type u} {ε : α → α → Prop} {x y : α}  : DWalk.{u} ε x y → List (Dart ε)
  | nil x => []
  | cons x (y := y) e W => (Dart.mk x y e) :: W.pdarts

/-- The list of darts of a `DWalk`, accepting higher types. -/
def darts {α : Type u} {ε : α → α → Type v} {x y : α} : DWalk ε x y → List (Dart ε)
  | nil x => []
  | cons x (y := y) e W => (Dart.mk x y e) :: W.darts

/-
stuck at solving universe constraint
  ?u.2098+1 =?= max (u+1) v
while trying to unify
  Type ?u.2098 : Type (?u.2098 + 1)
with
  Sort (max (u + 1) v) : Type (max (u + 1) v)

(Same error occurs with `#check List (Dart ε)`)
-/

It seems like lean cannot deduce that max (u + 1) v is positive.

[Edward van de Meent]

the issue is that Dart.{u,v} ε : Sort (max (u + 1) v), while List.{w} : Sort (w + 1) -> Sort (w + 1), meaning that in order to make the application List (Dart ε), lean needs to find a solution to max (u + 1) v = w + 1, which i don't think exists in the language of lean's universes

[Edward van de Meent]

to even give an expression for w, you'd (on paper) write down w = (max u (v.pred)), but there is no pred operator for universe levels in lean

[Kyle Miller]

I might suggest changing it to ε : α → α → Type v and then use PLift in the Prop case.

[Edward van de Meent]

i guess this would be fixed by having List accept all Sort instead of just Types

[Edward van de Meent]

but then again, that's a change in core, so...

[Peter Nelson]

I ended up putting PLift in the definition of Dart, like this:

/-- a triple `⟨a,b,e⟩` with `e : ε a b`.
We need `PLift` to prevent universe issues when `e` is a `Prop`. -/
structure Dart {α : Type u} (ε : α → α → Sort v) where
  fst : α
  snd : α
  edge' : PLift (ε fst snd)

def Dart.ofEdge (a b : α) (e : ε a b) : Dart ε :=
  Dart.mk a b ⟨e⟩

/-- The list of darts of a `DWalk`-/
def darts {α : Type u} {ε : α → α → Sort v} {a b : α}  : DWalk ε a b → List (Dart ε)
  | nil => []
  | cons (a' := a') e W => (Dart.ofEdge a a' e) :: W.darts

[Eric Wieser]

Probably that comment belongs on edge' not the type itself

[Eric Wieser]

This works for me:

/-- a triple `⟨a,b,e⟩` with `e : ε a b` -/
structure Dart {α : Type u} (ε : α → α → Sort v) : Type (max u v) where
  fst : α
  snd : α
  edge : ε fst snd

/-- The list of darts of a `DWalk`-/
def pdarts {α : Type u} {ε : α → α → Sort*} {x y : α}  : DWalk.{u} ε x y → List (Dart ε)
  | nil x => []
  | cons x (y := y) e W => (Dart.mk x y e) :: W.pdarts