Zulip Chat Archive

Stream: new members

Topic: can't find instance

Rémi Bottinelli (Oct 15 2022 at 13:29):

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 (Oct 15 2022 at 13:37):

Try set_option pp.universes true

Rémi Bottinelli (Oct 15 2022 at 13:39):

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 (Oct 15 2022 at 13:39):

Yeah, very possible...

Rémi Bottinelli (Oct 15 2022 at 13:45):

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

Eric Wieser (Oct 15 2022 at 13:49):

This feels like a Type vs Sort issue

Rémi Bottinelli (Oct 15 2022 at 13:59):

Indeed, but no idea what's the cause

Eric Wieser (Oct 15 2022 at 14:02):

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

Eric Wieser (Oct 15 2022 at 14:05):

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

Rémi Bottinelli (Oct 15 2022 at 14:05):

let me see

Rémi Bottinelli (Oct 15 2022 at 14:05):

lol, it does…

Rémi Bottinelli (Oct 15 2022 at 14:06):

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

Eric Wieser (Oct 15 2022 at 14:10):

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

Rémi Bottinelli (Oct 15 2022 at 14:14):

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 (Oct 15 2022 at 14:19):

Does V : Sort* work?

Rémi Bottinelli (Oct 15 2022 at 14:22):

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

Rémi Bottinelli (Oct 15 2022 at 14:22):

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

Rémi Bottinelli (Oct 15 2022 at 14:23):

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

Eric Wieser (Oct 15 2022 at 14:23):

Do they? docs#quiver

Yaël Dillies (Oct 15 2022 at 14:24):

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

Eric Wieser (Oct 15 2022 at 14:24):

Yes. Then my Sort suggestion is a bad idea!

Rémi Bottinelli (Oct 15 2022 at 14:24):

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

Eric Wieser (Oct 15 2022 at 14:26):

Maybe docs#wide_subquiver is the issue?

Rémi Bottinelli (Oct 15 2022 at 14:32):

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 (Oct 15 2022 at 14:34):

Doesn't set support Prop types?

Rémi Bottinelli (Oct 15 2022 at 14:39):

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

Kevin Buzzard (Oct 15 2022 at 14:49):

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 (Oct 15 2022 at 14:51):

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

Rémi Bottinelli (Oct 15 2022 at 15:54):

mmh, that's sad indeed

Rémi Bottinelli (Dec 12 2022 at 07:45):

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

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

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

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 :
      (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. -/
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

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

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]

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]

/-- 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
  · rintro X Y f

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
  · simp only
    rw [h.inv']

/-- `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
  fapply Prefunctor.ext
  · rintro X
  · 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) :=

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

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 (Dec 12 2022 at 08:06):

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

Last updated: Dec 20 2023 at 11:08 UTC