CategoryTheory.PathCategory

Stream: mathlib4

[Rémi Bottinelli]

https://github.com/leanprover-community/mathlib4/pull/2580 I got it to compile but:

• I made a def noncomputable since it was using Quiver.Path.Rec
• In composePath_id, I had to force a type cast through an alias using id, what should one do in cases like this?

[Rémi Bottinelli]

@Eric Wieser (discussing here to stay on-topic): I have a preference for the simple solution of noncomputable plus a porting note, versus implementing a new function, but if the latter is considered better, I can do that.

[Eric Wieser]

The latter is definitely better in general for when things are noncomputable that should obviously be computable (as was the case for Nat and List). I don't know how reasonable it is to consider docs4#Quiver.Path a computable object.

Note though that it ought to be straighforward to implement the computable rec anyway in the style of docs4#Nat.recC and docs4#Nat.rec_eq_recC; you just write out the obvious equations.

[Eric Wieser]

It looks like morallly Quiver.Path is just a cleverly typed list, so probably it deserves the same treatment as List; but on the other hand, there's no reason it needs to block porting the file

[Rémi Bottinelli]

I guess I shouldn't squeeze such an addition (Quiver.Path.recC) in the present PR?

[Eric Wieser]

Right; it probably makes sense as prework or as a follow-up

[Rémi Bottinelli]

def Path.recC {V : Type u} [Quiver.{v} V] {a : V} {motive : (b : V) → Path a b → Sort _}
    (nil : motive a Path.nil)
    (cons : ({b c : V} → (p : Path a b) → (e : b ⟶ c) → motive b p → motive c (p.cons e))) :
    {b : V} → (p : Path a b) → motive b p
  | _, (Path.nil) => nil
  | _, (Path.cons p e) => cons p e (Quiver.Path.recC nil cons p)

@[csimp] lemma Path.rec_eq_recC : @Path.rec = @Path.recC := by
  ext V _ a motive nil cons b p
  induction p with
  | nil => rfl
  | cons p e ih =>
    rw [Path.recC, ←ih]

lean tells me:

invalid 'csimp' theorem, only constant replacement theorems (e.g., `@f = @g`) are currently supported.

[Eric Wieser]

You have to have the arguments in exactly the same order for recC

[Eric Wieser]

I think the universe arguments have to be in the same order too

[Rémi Bottinelli]

Ah, I dropped them, let me try

[Eric Wieser]

They might even have to have the same names

[Rémi Bottinelli]

not the same name, it works with:

def Path.recC.{w, z, t} {V : Type t} [Quiver.{z} V] {a : V} {motive : (b : V) → Path a b → Sort w}
    (nil : motive a Path.nil)
    (cons : ({b c : V} → (p : Path a b) → (e : b ⟶ c) → motive b p → motive c (p.cons e))) :
    {b : V} → (p : Path a b) → motive b p
  | _, (Path.nil) => nil
  | _, (Path.cons p e) => cons p e (Quiver.Path.recC nil cons p)

[Rémi Bottinelli]

but I had to use new letters because u,v were already universe variables.

[Eric Wieser]

I would guess that

def Path.recC.{w} {V : Type w} [Quiver.{v} V] {a : V} {motive : (b : V) → Path a b → Sort u}

works with the ambient universe variables

[Rémi Bottinelli]

But trying to replace the use of rec by recC gives me an error:

invalid use of field notation with `@` modifier

[Rémi Bottinelli]

Eric Wieser said:

I would guess that

def Path.recC.{w} {V : Type w} [Quiver.{v} V] {a : V} {motive : (b : V) → Path a b → Sort u}

works with the ambient universe variables

not in my case it seems

[Eric Wieser]

Where/why are you trying to replace the use of rec with recC?

[Eric Wieser]

The purpose of csimp is that it does that for you behind the scenes

[Rémi Bottinelli]

In the PathCategory PR

[Rémi Bottinelli]

and it knows that I can drop the noncomputable thing?

[Eric Wieser]

Yes, it should do

[Rémi Bottinelli]

Doesn't seem to work for me, but the error might be something I'm doing wrong.

[Rémi Bottinelli]

I'm tempted to push it to the PR so you can have a look, but that would probably not be ideal.

[Eric Wieser]

You could push to a different branch

[Rémi Bottinelli]

D: that's the limit of my git-fu https://github.com/leanprover-community/mathlib4/compare/master...bottine:mathlib4:investigating_things?expand=1

[Eric Wieser]

Just to check; you restarted lean after editing the other file?

[Rémi Bottinelli]

nope

[Rémi Bottinelli]

ah, it's a compiler thing, so I should restart?

[Eric Wieser]

By default, lean4 does not rebuild downstream files after changes in upstream ones

[Eric Wieser]

I think there's a "refresh dependencies" command too

[Rémi Bottinelli]

Works now :)

[Rémi Bottinelli]

Should I open a PR just for the rec thing ?

[Eric Wieser]

Fixes work much better when you actually run the code that contains them ;)

[Rémi Bottinelli]

Haha, yeah, I've just been drilled on "is there some orange or red anywhere"

[Rémi Bottinelli]

Merged, and I updated the present PR. I've got #lint complaining about a lemma not being in simp normal form and provable by other simp lemmas, so I just removed it.

[Eric Wieser]

The simpNF problem is https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/simp.20on.20defs.20.28lean4.232042.29/near/339141703

[Rémi Bottinelli]

Thanks, I removed the simp attribute, added lemmas and made a note.

[Rémi Bottinelli]

To what extent is it allowed to shorten proofs when porting?

[Johan Commelin]

If it is due to technical problems, please record this in a porting note. Otherwise, a bit of golfing is fine. But I encourage you to keep it proof-local, otherwise it becomes a refactor that needs to be backported.

[Rémi Bottinelli]

https://github.com/leanprover-community/mathlib4/pull/2580 In the case I'm looking at now, it's stuff where more can be easily moved to term mode, or extraneous dsimp.

[Johan Commelin]

Which proof specifically are you looking at?

[Johan Commelin]

I think the golf should be uncontroversial. If there's $\varepsilon$ chance that someone might complain during review, then I wouldn't do it during the port. You can leave a Porting note: TODO golf instead.

[Rémi Bottinelli]

From:

def quotientPathsEquiv : Quotient (pathsHomRel C) ≌ C where
functor := quotientPathsTo C
  inverse := toQuotientPaths C
  unitIso :=
    NatIso.ofComponents
      (fun X => by
        cases X
        rfl)
      (by
        intros X Y
        cases X
        cases Y
        apply Quot.ind
        intro f
        simp only [Category.comp_id, Category.id_comp]
        apply Quot.sound
        apply Quotient.CompClosure.of
        simp [pathsHomRel])
  counitIso := NatIso.ofComponents (fun X => Iso.refl _) (fun f => by simp [Quot.liftOn_mk])
  functor_unitIso_comp := by
    intros X
    cases X
    dsimp
    simp
    rfl
#align category_theory.quotient_paths_equiv CategoryTheory.quotientPathsEquiv

to:

def quotientPathsEquiv : Quotient (pathsHomRel C) ≌ C where
  functor := quotientPathsTo C
  inverse := toQuotientPaths C
  unitIso :=
    NatIso.ofComponents
      (fun X => by cases X; rfl)
      (fun {X} {Y} => Quot.ind $ fun f => by
        apply Quot.sound
        apply Quotient.CompClosure.of
        simp [Category.comp_id, Category.id_comp, pathsHomRel])
  counitIso := NatIso.ofComponents (fun X => Iso.refl _) (fun f => by simp [Quot.liftOn_mk])
  functor_unitIso_comp X := by
    cases X
    simp only [pathsHomRel, pathComposition_obj, pathComposition_map, Functor.id_obj,
               quotientPathsTo_obj, Functor.comp_obj, toQuotientPaths_obj_as,
               NatIso.ofComponents_hom_app, Iso.refl_hom, quotientPathsTo_map, Category.comp_id]
    rfl
#align category_theory.quotient_paths_equiv CategoryTheory.quotientPathsEquiv

Granted, it's nothing especially impressive, but long winded intro; case; case; dsimp; simp; … sequences kind of hurt my eyes.

[Johan Commelin]

Yeah, this golf looks good.

[Rémi Bottinelli]

Great, thanks!

[Johan Commelin]

You don't seem to use {X} {Y} in the 2nd branch of NatIso.ofComponents. So you can even leave them out, I guess.

[Rémi Bottinelli]

Mmh, yep, thanks but now I'm confused.

[Rémi Bottinelli]

Is that a lean4 thing where lambdas can have hidden arguments?

[Johan Commelin]

yep

[Rémi Bottinelli]

But in this case, there is actually no lambda. The expected type is ({X} {Y} (f) -> …) and I'm feeding it a (f -> …) and I guess it auto-inserts X and Y. That's close to the limits of magic for me!

[Mario Carneiro]

that's implicit lambda

[Mario Carneiro]

when the goal is \forall {x}, A x and you write e lean autocompletes that to fun {x} => e

[Mario Carneiro]

if you want to suppress the automatic lambda and add it yourself either use @(e) or fun {x} => e

[Rémi Bottinelli]

Ah, thanks, that makes sense.