can't find instance

Stream: new members

[Rémi Bottinelli]

Hi, I'm trying to refactor the quiver code a bit and got into some instance troubles.
here, lean doesn't find the necessary quiver instance on V, even though I have an instance as a variable.
I'm pretty sure it's related to universe incompatibilities, but can't really figure out where they come from.
I can't really get a MWE out of that: what kind of approach should I take to debug this?

[Yaël Dillies]

Try set_option pp.universes true

[Rémi Bottinelli]

OK, I get

failed to synthesize type class instance for
V : Type u,
_inst_1 : quiver.{u_1 u} V,
H : wide_subquiver.{u ?l_1} (symmetrify.{u} V)
⊢ quiver.{?l_2+1 u} V

which I guess is related to the transition to psum, maybe?

[Yaël Dillies]

Yeah, very possible...

[Rémi Bottinelli]

Alright… I'm a bit clueless as to how to fix that so I might leave that aside for a while. Thanks!

[Eric Wieser]

This feels like a Type vs Sort issue

[Rémi Bottinelli]

Indeed, but no idea what's the cause

[Eric Wieser]

Do things become more obvious if you use [quiver.{v} V] for a new universe v?

[Eric Wieser]

I would guess that quiver.{v+1} V solves the issue

[Rémi Bottinelli]

let me see

[Rémi Bottinelli]

lol, it does…

[Rémi Bottinelli]

But am I risking a kind of domino effect here where the +1 has to be appended everytime?

[Eric Wieser]

I expect the real solution is to change a Type to a Sort somewhere

[Rémi Bottinelli]

One of the thing I did was change symmetrify from being defined as sum (x --> y) (y --> X) to psum …, so that I can symmetrify a Propositional quiver. This could mean that this is simply incompatible with doing things cleanly?

[Eric Wieser]

Does V : Sort* work?

[Rémi Bottinelli]

quivers take V : Type*, so doing that would imply redefining quivers themselves, no?

[Rémi Bottinelli]

I'm trying, but it's not entirely mechanical afaict

[Rémi Bottinelli]

(and redefining quivers would redefine categories I guess… which looks quite dangerous to me)

[Eric Wieser]

Do they? docs#quiver

[Yaël Dillies]

Yes, there's a difference between the index type and the return type of the homs.

[Eric Wieser]

Yes. Then my Sort suggestion is a bad idea!

[Rémi Bottinelli]

(haha I'm relieved I don't have to go there :) )

[Eric Wieser]

Maybe docs#wide_subquiver is the issue?

[Rémi Bottinelli]

Mmh, that would make sense, and then I'd only have to "up" the level there, but I actually get other errors somewhere else also related to bad universes.

To be more precise: now it's category_theory/groupoid/free_groupoid.lean that complains: the abbreviations at the beginning fail already.

[Rémi Bottinelli]

Doesn't set support Prop types?

[Rémi Bottinelli]

Bargh, got to go, thanks for the help debugging this!

[Kevin Buzzard]

Scott Morrison once tried to generalise the category theory library so that it allowed morphisms to take values in Sort u rather than Type u and after some struggling he gave up on the idea and reverted. This feels like the same sort of thing

[Yaël Dillies]

... which is really a shame, because that would allow us to unify orders and categories.

[Rémi Bottinelli]

mmh, that's sad indeed

[Rémi Bottinelli]

The symmetrify code has been ported to mathlib4, and it seems the universe problem disappears, so that one should be able to take symmetrify V as a PSum rather than a Sum. Is making such a change incompatible with the port having to be kind of 1-1 ?

/-
Copyright (c) 2021 David Wärn. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: David Wärn
Ported by: Joël Riou
-/
import Mathlib.Combinatorics.Quiver.Subquiver
import Mathlib.Combinatorics.Quiver.Path
import Mathlib.Data.Sum.Basic

/-!
## Weakly connected components

For a quiver `V`, we build a quiver `Symmetrify V` by adding a reversal of every edge.
Informally, a path in `Symmetrify V` corresponds to a 'zigzag' in `V`. This lets us
define the type `WeaklyConnectedComponent V` as the quotient of `V` by the relation which
identifies `a` with `b` if there is a path from `a` to `b` in `Symmetrify V`. (These
zigzags can be seen as a proof-relevant analogue of `EqvGen`.)

Strongly connected components have not yet been defined.
-/

universe v u

namespace Quiver

/-- A type synonym for the symmetrized quiver (with an arrow both ways for each original arrow).
    NB: this does not work for `Prop`-valued quivers. It requires `[Quiver.{v+1} V]`. -/
-- Porting note: no hasNonemptyInstnace linter yet
def Symmetrify (V : Type u) :=
  V

instance symmetrifyQuiver (V : Type u) [Quiver V] : Quiver (Symmetrify V) :=
  ⟨fun a b : V ↦ PSum (a ⟶ b) (b ⟶ a)⟩

variable (V : Type u) [Quiver V]

/-- A quiver `HasReverse` if we can reverse an arrow `p` from `a` to `b` to get an arrow
    `p.reverse` from `b` to `a`.-/
class HasReverse where
  /-- the map which sends an arrow to its reverse -/
  reverse' : ∀ {a b : V}, (a ⟶ b) → (b ⟶ a)

/-- Reverse the direction of an arrow. -/
def reverse {V} [Quiver V] [HasReverse V] {a b : V} : (a ⟶ b) → (b ⟶ a) :=
  HasReverse.reverse'

/-- A quiver `HasInvolutiveReverse` if reversing twice is the identity.`-/
class HasInvolutiveReverse extends HasReverse V where
  /-- `reverse` is involutive -/
  inv' : ∀ {a b : V} (f : a ⟶ b), reverse (reverse f) = f

@[simp]
theorem reverse_reverse {V} [Quiver V] [h : HasInvolutiveReverse V] {a b : V} (f : a ⟶ b) :
    reverse (reverse f) = f := by apply h.inv'

variable {V}

instance : HasReverse (Symmetrify V) :=
  ⟨fun e ↦ match e with
            | (PSum.inl f) => PSum.inr f
            | (PSum.inr f) => PSum.inl f⟩

instance :
    HasInvolutiveReverse
      (Symmetrify V) where
  toHasReverse := ⟨fun e ↦
    match e with
    | (PSum.inl f) => PSum.inr f
    | (PSum.inr f) => PSum.inl f⟩
  inv' e :=
    match e with
    | (PSum.inl _) => rfl
    | (PSum.inr _) => rfl

/-- Reverse the direction of a path. -/
@[simp]
def Path.reverse [HasReverse V] {a : V} : ∀ {b}, Path a b → Path b a
  | _, Path.nil => Path.nil
  | _, Path.cons p e => (Quiver.reverse e).toPath.comp p.reverse

@[simp]
theorem Path.reverse_toPath [HasReverse V] {a b : V} (f : a ⟶ b) :
    f.toPath.reverse = (Quiver.reverse f).toPath :=
  rfl
#align quiver.path.reverse_to_path Quiver.Path.reverse_toPath

@[simp]
theorem Path.reverse_comp [HasReverse V] {a b c : V} (p : Path a b) (q : Path b c) :
    (p.comp q).reverse = q.reverse.comp p.reverse := by
  induction' q with _ _ _ _ h
  · simp
  · simp [h]

@[simp]
theorem Path.reverse_reverse [h : HasInvolutiveReverse V] {a b : V} (p : Path a b) :
    p.reverse.reverse = p := by
  induction' p with _ _ _ _ h
  · simp
  · rw [Path.reverse, Path.reverse_comp, h, Path.reverse_toPath, Quiver.reverse_reverse]
    rfl

/-- The inclusion of a quiver in its symmetrification -/
def Symmetrify.of : Prefunctor V (Symmetrify V) where
  obj := id
  map := PSum.inl

/-- Given a quiver `V'` with reversible arrows, a prefunctor to `V'` can be lifted to one from
    `Symmetrify V` to `V'` -/
def Symmetrify.lift {V' : Type _} [Quiver V'] [HasReverse V'] (φ : Prefunctor V V') :
    Prefunctor (Symmetrify V) V' where
  obj := φ.obj
  map f := match f with
  | PSum.inl g => φ.map g
  | PSum.inr g => reverse (φ.map g)

theorem Symmetrify.lift_spec (V' : Type _) [Quiver V'] [HasReverse V'] (φ : Prefunctor V V') :
    Symmetrify.of.comp (Symmetrify.lift φ) = φ := by
  fapply Prefunctor.ext
  · rintro X
    rfl
  · rintro X Y f
    rfl

theorem Symmetrify.lift_reverse (V' : Type _) [Quiver V'] [h : HasInvolutiveReverse V']
    (φ : Prefunctor V V') {X Y : Symmetrify V} (f : X ⟶ Y) :
    (Symmetrify.lift φ).map (Quiver.reverse f) = Quiver.reverse ((Symmetrify.lift φ).map f) := by
  dsimp [Symmetrify.lift]; cases f
  · simp only
    rfl
  · simp only
    rw [h.inv']
    rfl

/-- `lift φ` is the only prefunctor extending `φ` and preserving reverses. -/
theorem Symmetrify.lift_unique (V' : Type _) [Quiver V'] [HasReverse V'] (φ : Prefunctor V V')
    (Φ : Prefunctor (Symmetrify V) V') (hΦ : Symmetrify.of.comp Φ = φ)
    (hΦinv : ∀ {X Y : Symmetrify V} (f : X ⟶ Y),
      Φ.map (Quiver.reverse f) = Quiver.reverse (Φ.map f)) :
    Φ = Symmetrify.lift φ := by
  subst_vars
  fapply Prefunctor.ext
  · rintro X
    rfl
  · rintro X Y f
    cases f
    · rfl
    · exact hΦinv (PSum.inl _)
#align quiver.symmetrify.lift_unique Quiver.Symmetrify.lift_unique

variable (V)

/-- Two vertices are related in the zigzag setoid if there is a
    zigzag of arrows from one to the other. -/
def zigzagSetoid : Setoid V :=
  ⟨fun a b ↦ Nonempty (@Path (Symmetrify V) _ a b), fun _ ↦ ⟨Path.nil⟩, fun ⟨p⟩ ↦
    ⟨p.reverse⟩, fun ⟨p⟩ ⟨q⟩ ↦ ⟨p.comp q⟩⟩

/-- The type of weakly connected components of a directed graph. Two vertices are
    in the same weakly connected component if there is a zigzag of arrows from one
    to the other. -/
def WeaklyConnectedComponent : Type u :=
  Quotient (zigzagSetoid V)

namespace WeaklyConnectedComponent

variable {V}

/-- The weakly connected component corresponding to a vertex. -/
protected def mk : V → WeaklyConnectedComponent V :=
  @Quotient.mk' _ (zigzagSetoid V)

instance : CoeTC V (WeaklyConnectedComponent V) :=
  ⟨WeaklyConnectedComponent.mk⟩

instance [Inhabited V] : Inhabited (WeaklyConnectedComponent V) :=
  ⟨show V from default⟩

protected theorem eq (a b : V) :
    (a : WeaklyConnectedComponent V) = b ↔ Nonempty (@Path (Symmetrify V) _ a b) :=
  Quotient.eq'

end WeaklyConnectedComponent

variable {V}

-- Without the explicit universe level in `Quiver.{v+1}` Lean comes up with
-- `Quiver.{max u_2 u_3 + 1}`. This causes problems elsewhere, so we write `Quiver.{v+1}`.
/-- A wide subquiver `H` of `Symmetrify V` determines a wide subquiver of `V`, containing an
    an arrow `e` if either `e` or its reversal is in `H`. -/
def wideSubquiverSymmetrify (H : WideSubquiver (Symmetrify V)) : WideSubquiver V :=
  fun _ _ ↦ { e | H _ _ (PSum.inl e) ∨ H _ _ (PSum.inr e) }

end Quiver

[Kevin Buzzard]

My instinct is that the port should be 1-1 and any refractors should be done after it's complete.