!4#2797 / !4#2769

Stream: mathlib4

[Jeremy Tan]

@Chris Hughes what are you waiting on me for? No question is asked there and no changes have been requested

[Kevin Buzzard]

You have a red x, not a green tick, so the PR can't be merged.

[Jeremy Tan]

@Chris Hughes It's still failing for the same reason as !4#2769

[Jeremy Tan]

And nobody knows why simpNF is being overly aggressive here

[Mauricio Collares]

Rather than simpNF being overly aggressive, probably the search was just below the timeout and newly added instances broke the camel's back. Profiling would be required to see what's causing the HasZeroObject failures.

[Jeremy Tan]

how does profiling work?

[Matthew Ballard]

!4#2797 adds no new instances.

[Adam Topaz]

What’s the error the linter gives for !4#2797 ?

[Jeremy Tan]

Adam Topaz said:

What’s the error the linter gives for !4#2797 ?

/- The `simpNF` linter reports:
SOME SIMP LEMMAS ARE NOT IN SIMP-NORMAL FORM.
see note [simp-normal form] for tips how to debug this.
https://leanprover-community.github.io/mathlib_docs/notes.html#simp-normal%20form -/
-- Mathlib.CategoryTheory.Linear.LinearFunctor
#check CategoryTheory.Functor.map_smul.{u_5, u_4, u_3, u_2, u_1} /- LINTER FAILED:
simplify fails on left-hand side:
failed to synthesize
  CategoryTheory.Limits.HasZeroObject D
(deterministic) timeout at 'typeclass', maximum number of heartbeats (20000) has been reached (use 'set_option synthInstance.maxHeartbeats <num>' to set the limit) -/
#check CategoryTheory.Functor.mapLinearMap_apply.{u_1, u_2, u_3, u_4, u_5} /- LINTER FAILED:
simplify fails on left-hand side:
failed to synthesize
  CategoryTheory.Limits.HasZeroObject D
(deterministic) timeout at 'typeclass', maximum number of heartbeats (20000) has been reached (use 'set_option synthInstance.maxHeartbeats <num>' to set the limit) -/

-- Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
#check CategoryTheory.Functor.map_add.{u_4, u_3, u_2, u_1} /- LINTER FAILED:
simplify fails on left-hand side:
failed to synthesize
  CategoryTheory.Limits.HasZeroObject D
(deterministic) timeout at 'typeclass', maximum number of heartbeats (20000) has been reached (use 'set_option synthInstance.maxHeartbeats <num>' to set the limit) -/
#check CategoryTheory.Functor.mapAddHom_apply.{u_1, u_2, u_3, u_4} /- LINTER FAILED:
simplify fails on left-hand side:
failed to synthesize
  CategoryTheory.Limits.HasZeroObject D
(deterministic) timeout at 'typeclass', maximum number of heartbeats (20000) has been reached (use 'set_option synthInstance.maxHeartbeats <num>' to set the limit) -/
#check CategoryTheory.Functor.map_neg.{u_4, u_3, u_2, u_1} /- LINTER FAILED:
simplify fails on left-hand side:
failed to synthesize
  CategoryTheory.Limits.HasZeroObject D
(deterministic) timeout at 'typeclass', maximum number of heartbeats (20000) has been reached (use 'set_option synthInstance.maxHeartbeats <num>' to set the limit) -/
#check CategoryTheory.Functor.map_sub.{u_4, u_3, u_2, u_1} /- LINTER FAILED:
simplify fails on left-hand side:
failed to synthesize
  CategoryTheory.Limits.HasZeroObject D
(deterministic) timeout at 'typeclass', maximum number of heartbeats (20000) has been reached (use 'set_option synthInstance.maxHeartbeats <num>' to set the limit) -/
#check CategoryTheory.Functor.map_sum.{u_5, u_4, u_3, u_2, u_1} /- LINTER FAILED:
simplify fails on left-hand side:
failed to synthesize
  CategoryTheory.Limits.HasZeroObject D
(deterministic) timeout at 'typeclass', maximum number of heartbeats (20000) has been reached (use 'set_option synthInstance.maxHeartbeats <num>' to set the limit) -/
#check CategoryTheory.AdditiveFunctor.forget_map.{u_4, u_3, u_2, u_1} /- LINTER FAILED:
simplify fails on left-hand side:
failed to synthesize
  CategoryTheory.Limits.HasZeroObject (C ⥤ D)
(deterministic) timeout at 'typeclass', maximum number of heartbeats (20000) has been reached (use 'set_option synthInstance.maxHeartbeats <num>' to set the limit) -/
#check CategoryTheory.AdditiveFunctor.ofLeftExact_map.{v₁, v₂, u₁, u₂} /- LINTER FAILED:
simplify fails on left-hand side:
failed to synthesize
  CategoryTheory.Limits.HasZeroObject (C ⥤+ D)
(deterministic) timeout at 'typeclass', maximum number of heartbeats (20000) has been reached (use 'set_option synthInstance.maxHeartbeats <num>' to set the limit) -/
#check CategoryTheory.AdditiveFunctor.ofRightExact_map.{v₁, v₂, u₁, u₂} /- LINTER FAILED:
simplify fails on left-hand side:
failed to synthesize
  CategoryTheory.Limits.HasZeroObject (C ⥤+ D)
(deterministic) timeout at 'typeclass', maximum number of heartbeats (20000) has been reached (use 'set_option synthInstance.maxHeartbeats <num>' to set the limit) -/
#check CategoryTheory.AdditiveFunctor.ofExact_map.{v₁, v₂, u₁, u₂} /- LINTER FAILED:
simplify fails on left-hand side:
failed to synthesize
  CategoryTheory.Limits.HasZeroObject (C ⥤+ D)
(deterministic) timeout at 'typeclass', maximum number of heartbeats (20000) has been reached (use 'set_option synthInstance.maxHeartbeats <num>' to set the limit) -/
make: *** [GNUmakefile:16: lint] Error 1
Error: Process completed with exit code 2.

[Matthew Ballard]

They are all searching for HasZeroObject instances. Originally it was in Preadditive.AdditiveFunctor but !4#2797 add Linear.LinearFunctor Load up master and see if you can find a HasZeroObject D instance here

[Adam Topaz]

Is the issue that it’s looking for an additive instance via preadditive plus zero objects plus binary biproducts?

[Matthew Ballard]

My guess. But it knows not to do this when building

[Matthew Ballard]

And last I checked, Lean cannot synthesize an instance of HasZeroObject in that file at the appropriate locations

[Adam Topaz]

Which file?

[Matthew Ballard]

It seems the search done when building the file is a different from the simpNF search

[Matthew Ballard]

https://github.com/leanprover-community/mathlib4/blob/baf8d765412d7f8ad43200bc7ca83edacdf14da0/Mathlib/CategoryTheory/Preadditive/AdditiveFunctor.lean#L56

[Adam Topaz]

I think the difference is that the linter works globally somehow, not locally in an individual file

[Matthew Ballard]

I confess to never having looked at the linter files

[Matthew Ballard]

Rebuilt master from scratch with no problem and

variable {C D : Type _} [Category C] [Category D] [Preadditive C] [Preadditive D] (F : C ⥤ D)
  [Functor.Additive F]

#synth Limits.HasZeroObject D  -- failed

For reference one of the simpNF errors is for timing out in a search for HasZeroObject D in the next declaration.

[Kevin Buzzard]

And does etaExperiment help?

[Matthew Ballard]

Can you remind of the syntax to turn it on?

[Adam Topaz]

Has zero object is a prop right? It probably won’t make a difference

[Matthew Ballard]

The linter is a black box to me. Just curious to poke it with this stick

[Kevin Buzzard]

set_option synthInstance.etaExperiment true in
#synth ...

[Matthew Ballard]

I set it true globally. Lean is not finding a HasZeroObject D instance because there is none

[Matthew Ballard]

Running the linter with it in there for fun

[Matthew Ballard]

-- Linting passed.

:rofl:

[Matthew Ballard]

Let me check if other changes to master didn't induce this

[Matthew Ballard]

Failed!!

[Matthew Ballard]

Solution

set_option synthInstance.etaExperiment true in simpNF

is clearly the fix :lol:

[Matthew Ballard]

Well, now it fails again even with EE turned on

[Adam Topaz]

A MWE to help debugging (using the branch from !4#2797):

import Mathlib

open CategoryTheory
variable {C D : Type _} [Category C] [Category D] [Preadditive C] [Preadditive D]

set_option trace.Meta.synthInstance true
example (F : C ⥤ D) [Functor.Additive F] {X Y : C} {f g : X ⟶ Y} :
  F.map (f + g) = F.map f + F.map g := by simp

[Matthew Ballard]

New theory: the fresh build of master on my machine did it

[Adam Topaz]

My guess is that lean is trying to use a lemma which requires Additive D, and it looks for an additive instance from preadditive+zeroobj+binarybiprods which it can deduce from preadditive+finitebiprods which it can deduce from preadditive+zeroobj+binarybiprods, etc.

[Adam Topaz]

But the trace itself is crashing my vscode, so it's hard to tell what's actually going on

[Matthew Ballard]

The oddness for me is the divergence between Lean and simpNF

[Adam Topaz]

Is there a way to emit the synthInstance trace in the command line instead of vscode?

[Gabriel Ebner]

If you call lean from the command-line, yes.

[Adam Topaz]

bah of course :)

[Gabriel Ebner]

What I often do is add set_option synthInstance.maxHeartbeats N with N ranging from 0 to 20000 (the default) to reduce the output.

[Adam Topaz]

Gabriel Ebner said:

If you call lean from the command-line, yes.

okay, lean4 doesn't let me do lean --make foobar.lean. What's the right flag?

[Adam Topaz]

Gabriel Ebner said:

What I often do is add set_option synthInstance.maxHeartbeats N with N ranging from 0 to 20000 (the default) to reduce the output.

I'll try this as well.

[Matthew Ballard]

lake env lean

[Adam Topaz]

?

[Adam Topaz]

anyway, lean is indeed stuck trying to find an additive instance.

[Adam Topaz]

[Meta.synthInstance] 💥 CategoryTheory.Limits.HasZeroObject D ▼
  [] new goal CategoryTheory.Limits.HasZeroObject D ▶
  [] ✅ apply @CategoryTheory.NonPreadditiveAbelian.has_zero_object to CategoryTheory.Limits.HasZeroObject D ▶
  [] ✅ apply CategoryTheory.Limits.hasZeroObject_of_hasFiniteBiproducts to CategoryTheory.Limits.HasZeroObject D ▶
  [] ✅ apply @CategoryTheory.NonPreadditiveAbelian.toHasZeroMorphisms to CategoryTheory.Limits.HasZeroMorphisms D ▶
  [] ✅ apply @CategoryTheory.Preadditive.preadditiveHasZeroMorphisms to CategoryTheory.Limits.HasZeroMorphisms D ▶
  [] ✅ apply inst✝¹ to CategoryTheory.Preadditive D ▶
  [resume] propagating CategoryTheory.Preadditive
        D to subgoal CategoryTheory.Preadditive D of CategoryTheory.Limits.HasZeroMorphisms D ▶
  [resume] propagating CategoryTheory.Limits.HasZeroMorphisms
        D to subgoal CategoryTheory.Limits.HasZeroMorphisms D of CategoryTheory.Limits.HasZeroObject D ▶
  [] 💥 apply @CategoryTheory.AdditiveCategory.toHasFiniteBiproducts to CategoryTheory.Limits.HasFiniteBiproducts D ▼
    [tryResolve] 💥 CategoryTheory.Limits.HasFiniteBiproducts D ≟ CategoryTheory.Limits.HasFiniteBiproducts ?m.2287 ▼
      [] ❌ CategoryTheory.AdditiveCategory D ▼
        [] no instances for CategoryTheory.AdditiveCategory D ▼
          [instances] #[]
      [] ❌ CategoryTheory.AdditiveCategory D ▼
        [] no instances for CategoryTheory.AdditiveCategory D ▼
          [instances] #[]
      [] ❌ CategoryTheory.AdditiveCategory D ▶
      [] ❌ CategoryTheory.AdditiveCategory D ▶
      [] ❌ CategoryTheory.AdditiveCategory D ▶
      [] ❌ CategoryTheory.AdditiveCategory D ▶
      [] ❌ CategoryTheory.AdditiveCategory D ▶
      [] ❌ CategoryTheory.AdditiveCategory D ▶
      [] ❌ CategoryTheory.AdditiveCategory D ▶
      [] ❌ CategoryTheory.AdditiveCategory D ▶
      [] ❌ CategoryTheory.AdditiveCategory D ▶
      [] ❌ CategoryTheory.AdditiveCategory D ▶
      [] ❌ CategoryTheory.AdditiveCategory D ▶
      [] ❌ CategoryTheory.AdditiveCategory D ▶

output truncated by many more of the same line

[Matthew Ballard]

Are you trying to synthesize a HasZeroObject D instance in the original file?

[Adam Topaz]

no I'm just using the following to investigate precisely the failure of map_add:

import Mathlib

open CategoryTheory
variable {C D : Type _} [Category C] [Category D] [Preadditive C] [Preadditive D]

set_option maxHeartbeats 2000

example (F : C ⥤ D) [Functor.Additive F] {X Y : C} {f g : X ⟶ Y} :
  F.map (f + g) = F.map f + F.map g :=
set_option trace.Meta.synthInstance true in by simp

[Matthew Ballard]

Wait. That fails to build?

[Adam Topaz]

yup

[Adam Topaz]

error @ simp

[Matthew Ballard]

Huh. I didn't check that branch. On port/CategoryTheory.Abelian.Basic everything always built

[Matthew Ballard]

Does it fail on master?

[Matthew Ballard]

It doesn't crash nvim :)

[Adam Topaz]

I haven't checked but my guess is that it would. The issue is in Additive.Basic:

import Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
import Mathlib.CategoryTheory.Additive.Basic -- uncomment this line to get rid of error.

open CategoryTheory
variable {C D : Type _} [Category C] [Category D] [Preadditive C] [Preadditive D]

set_option maxHeartbeats 2000

example (F : C ⥤ D) [Functor.Additive F] {X Y : C} {f g : X ⟶ Y} :
  F.map (f + g) = F.map f + F.map g :=
set_option trace.Meta.synthInstance true in by simp

[Adam Topaz]

Matthew Ballard said:

It doesn't crash nvim :)

did you use the heartbeats setting in my code block? ;)

[Matthew Ballard]

I don't think so. (I would make a terrible lab scientist...)

[Matthew Ballard]

Fails on master and yes no limit on the heartbeats

[Adam Topaz]

Matthew Ballard said:

Fails on master and yes no limit on the heartbeats

okay, that's not good

[Matthew Ballard]

Well, I also just dropped that into the CategoryTheory/Preadditive/Additive.lean directly and I get a different trace

[Adam Topaz]

This is working for me on master:

import Mathlib

open CategoryTheory
variable {C D : Type _} [Category C] [Category D] [Preadditive C] [Preadditive D]

set_option maxHeartbeats 2000

example (F : C ⥤ D) [Functor.Additive F] {X Y : C} {f g : X ⟶ Y} :
  F.map (f + g) = F.map f + F.map g :=
set_option trace.Meta.synthInstance true in by simp

[Matthew Ballard]

As I said, terrible lab scientist.

[Matthew Ballard]

If you change the proof of map_add in CategoryTheory/Preadditive/AdditiveFunctor.lean to set_option trace.Meta.synthInstance true in by simp does it succeed?

[Adam Topaz]

that file builds fine. I don't think that would change anything. I think the issue is in the Additive class itself.

[Adam Topaz]

I'll try to extract a MWE

[Matthew Ballard]

The current proof is not simp

[Matthew Ballard]

Ah ok. simpNF is testing for proofs by by simp and this is happening

[Adam Topaz]

yeah exactly

[Matthew Ballard]

Shouldn't it just say "there is no proof by simp, we are ok"

[Adam Topaz]

import Mathlib.CategoryTheory.Preadditive.AdditiveFunctor

open CategoryTheory
variable {C D : Type _} [Category C] [Category D] [Preadditive C] [Preadditive D]

set_option maxHeartbeats 2000

/-
Uncomment the first one and comment out the second to get an error.
-/

--class thing (C : Type _) [Category C] extends Preadditive C, Limits.HasFiniteBiproducts C
class thing (C : Type _) [Category C] [Preadditive C] extends Limits.HasFiniteBiproducts C

example (F : C ⥤ D) [Functor.Additive F] {X Y : C} {f g : X ⟶ Y} :
  F.map (f + g) = F.map f + F.map g :=
set_option trace.Meta.synthInstance true in by simp

[Matthew Ballard]

Well, Additive and Abelian fit that

[Adam Topaz]

that foo lemma wasn't actually needed

[Matthew Ballard]

You aren't suggesting unbundling Preadditive in Additive and Abelianright?

[Adam Topaz]

I'm not suggesting anything. I'm just trying to isolate the issue

[Matthew Ballard]

Just asked for clarity

[Adam Topaz]

Abelian should be a prop anyway ;)

[Adam Topaz]

re :thinking: : There is only ever at most one abelian category instance on any given category

[Adam Topaz]

But that's not an actual suggestion. We sometimes want to exploit the definitional properties of addition of morphisms (like in the category of modules), so making it a prop is not a good thing to do.

[Adam Topaz]

well, I couldn't track down the issue. I hope a typeclass expert can help us out here? The current MWE is this:

import Mathlib.CategoryTheory.Preadditive.AdditiveFunctor

open CategoryTheory
variable {C D : Type _} [Category C] [Category D] [Preadditive C] [Preadditive D]

set_option maxHeartbeats 2000

/-
Comment out the first one and uncomment out the second to get rid of the error.
-/

class thing (C : Type _) [Category C] extends Preadditive C, Limits.HasFiniteBiproducts C
--class thing (C : Type _) [Category C] [Preadditive C] extends Limits.HasFiniteBiproducts C

example (F : C ⥤ D) [Functor.Additive F] {X Y : C} {f g : X ⟶ Y} :
  F.map (f + g) = F.map f + F.map g :=
set_option trace.Meta.synthInstance true in by simp

And it's valid on current mathlib4 master

[Matthew Ballard]

I just cloned a fresh copy of mathlib and built it from scratch (for some reason cache was not unpacking the files from get!). If I replace the proof of map_add in CategoryTheory/Preadditive/AdditiveFunctor.lean with

set_option trace.Meta.synthInstance true in by simp

then it is already looking for HasZeroObject D

[Matthew Ballard]

Output

[Meta.synthInstance] :check: CategoryTheory.Category C :play:

[Meta.synthInstance] :check: CategoryTheory.Category D :play:

[Meta.synthInstance] :cross_mark: CategoryTheory.Limits.HasZeroObject D ▼
[] new goal CategoryTheory.Limits.HasZeroObject D ▶
[] ✅ apply CategoryTheory.Limits.hasZeroObject_of_hasFiniteBiproducts to CategoryTheory.Limits.HasZeroObject D ▶
[] ✅ apply @CategoryTheory.Preadditive.preadditiveHasZeroMorphisms to CategoryTheory.Limits.HasZeroMorphisms D ▶
[] ✅ apply inst✝¹ to CategoryTheory.Preadditive D ▶
[resume] propagating CategoryTheory.Preadditive
D to subgoal CategoryTheory.Preadditive D of CategoryTheory.Limits.HasZeroMorphisms D ▶
[resume] propagating CategoryTheory.Limits.HasZeroMorphisms
D to subgoal CategoryTheory.Limits.HasZeroMorphisms D of CategoryTheory.Limits.HasZeroObject D ▶
[] ❌ apply inst✝² to CategoryTheory.Preadditive D ▶

[Meta.synthInstance] :check: CategoryTheory.Category C :play:

[Meta.synthInstance] :check: CategoryTheory.Category D :play:

[Meta.synthInstance] :cross_mark: CategoryTheory.Limits.HasZeroObject D ▼
[] result <not-available> (cached)

[Meta.synthInstance] :check: CategoryTheory.Category C :play:

[Meta.synthInstance] :check: CategoryTheory.Category D :play:

[Meta.synthInstance] :cross_mark: CategoryTheory.Limits.HasZeroObject D ▼
[] result <not-available> (cached)

[Meta.synthInstance] :cross_mark: Subsingleton (F.obj X ⟶ F.obj Y) ▼
[] new goal Subsingleton (F.obj X ⟶ F.obj Y) ▶
[] ❌ apply instSubsingleton to Subsingleton (F.obj X ⟶ F.obj Y) ▶
[] ✅ apply @Unique.instSubsingleton to Subsingleton (F.obj X ⟶ F.obj Y) ▶
[] ✅ apply @IsEmpty.instSubsingleton to Subsingleton (F.obj X ⟶ F.obj Y) ▶

[Kevin Buzzard]

Re the MWE: for me you don't need to uncomment the second thing to get rid of the error -- just removing the first one does the job.

[Adam Topaz]

yeah true

[Adam Topaz]

but uncommenting out the second doesn't introduce an error, which might be useful information as well

[Matthew Ballard]

Why is Lean searching for HasZeroObject D in map_add? (This may be orthogonal to the looping with the new class)

[Adam Topaz]

you can trace the simp as well:

set_option trace.Meta.synthInstance true in
set_option trace.Meta.Tactic.simp true in by simp

[Adam Topaz]

It seems that this HasZeroObject search is due to CategoryTheory.Limits.IsZero.map.

[Matthew Ballard]

Output

[Meta.synthInstance] :check: CategoryTheory.Category C :play:

[Meta.synthInstance] :check: CategoryTheory.Category D :play:

[Meta.synthInstance] :boom: CategoryTheory.Limits.HasZeroObject D ▼
[] new goal CategoryTheory.Limits.HasZeroObject D ▼
[instances] #[CategoryTheory.Limits.hasZeroObject_of_hasFiniteBiproducts]
[] ✅ apply CategoryTheory.Limits.hasZeroObject_of_hasFiniteBiproducts to CategoryTheory.Limits.HasZeroObject D ▼
[tryResolve] ✅ CategoryTheory.Limits.HasZeroObject D ≟ CategoryTheory.Limits.HasZeroObject D
[] new goal CategoryTheory.Limits.HasZeroMorphisms D ▼
[instances] #[@CategoryTheory.Preadditive.preadditiveHasZeroMorphisms]
[] ✅ apply @CategoryTheory.Preadditive.preadditiveHasZeroMorphisms to CategoryTheory.Limits.HasZeroMorphisms D ▼
[tryResolve] ✅ CategoryTheory.Limits.HasZeroMorphisms D ≟ CategoryTheory.Limits.HasZeroMorphisms D
[] new goal CategoryTheory.Preadditive D ▶
[] ✅ apply inst✝¹ to CategoryTheory.Preadditive D ▶
[resume] propagating CategoryTheory.Preadditive
D to subgoal CategoryTheory.Preadditive D of CategoryTheory.Limits.HasZeroMorphisms D ▼
[] size: 1
[resume] propagating CategoryTheory.Limits.HasZeroMorphisms
D to subgoal CategoryTheory.Limits.HasZeroMorphisms D of CategoryTheory.Limits.HasZeroObject D ▼
[] size: 2
[synthInstance] new goal CategoryTheory.Limits.HasFiniteBiproducts D ▼
[instances] #[@thing.toHasFiniteBiproducts]
[] 💥 apply @thing.toHasFiniteBiproducts to CategoryTheory.Limits.HasFiniteBiproducts D ▼
[tryResolve] 💥 CategoryTheory.Limits.HasFiniteBiproducts D ≟ CategoryTheory.Limits.HasFiniteBiproducts ?m.2238 ▶

My output from @Adam Topaz MWE (in its borked mode) (edit: expanded)

[Matthew Ballard]

Nuking hasZeroObject_of_hasFiniteBiproducts fixes things

[Adam Topaz]

But I think we want that instance. And I still can't figure out where the loop is coming from.

[Matthew Ballard]

It has lower priority in the original file for some reason

[Adam Topaz]

This also works:

import Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
import Mathlib.Tactic.LibrarySearch

open CategoryTheory Limits
variable {C D : Type _} [Category C] [Category D] [Preadditive C] [Preadditive D]

set_option maxHeartbeats 2000

class thing (C : Type _) [Category C] extends Preadditive C, HasFiniteBiproducts C

attribute [-simp] IsZero.map

example (F : C ⥤ D) [Functor.Additive F] {X Y : C} {f g : X ⟶ Y} :
  F.map (f + g) = F.map f + F.map g :=
set_option trace.Meta.Tactic.simp true in
set_option trace.Meta.synthInstance true in by simp

[Matthew Ballard]

FWIW, removing from the simp set IsZero.map globally doesn't break anything (yet)

[Matthew Ballard]

It is a strange result

[Matthew Ballard]

I don't think checking if F = 0 is a good place to start looking for a proof that F.map is a homomorphism

[Matthew Ballard]

Matthew Ballard said:

FWIW, removing from the simp set IsZero.map globally doesn't break anything (yet)

Removing @[simp] doesn't seem to cause any problems in mathlib(3)

[Kevin Buzzard]

If you change

class thing (C : Type _) [Category C] extends Preadditive C, Limits.HasFiniteBiproducts C

to

class thing (C : Type _) [Category C] extends HasZeroMorphisms C, Limits.HasFiniteBiproducts C, Preadditive C

then the problem goes away. Are these the same?

[Matthew Ballard]

More output

[] :boom: apply @thing.toHasFiniteBiproducts to CategoryTheory.Limits.HasFiniteBiproducts D ▼
[tryResolve] 💥 CategoryTheory.Limits.HasFiniteBiproducts D ≟ CategoryTheory.Limits.HasFiniteBiproducts ?m.2238 ▼
[synthInstance] ❌ thing D ▼
[] no instances for thing D ▶
[synthInstance] ❌ thing D ▼
[] no instances for thing D ▶
[synthInstance] ❌ thing D ▼
[] no instances for thing D ▶
[synthInstance] ❌ thing D ▼
[] no instances for thing D ▶
[synthInstance] ❌ thing D ▼
[] no instances for thing D ▶
[synthInstance] ❌ thing D ▼
[] no instances for thing D ▶
[synthInstance] ❌ thing D ▼
[] no instances for thing D ▶
[synthInstance] ❌ thing D ▼
[] no instances for thing D ▶
[synthInstance] ❌ thing D ▼
[] no instances for thing D ▼
[instances] #[]
[synthInstance] ❌ thing D ▼
[] no instances for thing D ▼
[instances] #[]
[synthInstance] ❌ thing D ▶
....

[Adam Topaz]

Kevin Buzzard said:

If you change

class thing (C : Type _) [Category C] extends Preadditive C, Limits.HasFiniteBiproducts C

to

class thing (C : Type _) [Category C] extends HasZeroMorphisms C, Limits.HasFiniteBiproducts C, Preadditive C

then the problem goes away. Are these the same?

Preadditive implies HasZeroMorphisms, and both are data, so this is probably problematic

[Matthew Ballard]

Does it?

[Kevin Buzzard]

Matthew Ballard said:

More output

[] :boom: apply @thing.toHasFiniteBiproducts to CategoryTheory.Limits.HasFiniteBiproducts D ▼
[tryResolve] 💥 CategoryTheory.Limits.HasFiniteBiproducts D ≟ CategoryTheory.Limits.HasFiniteBiproducts ?m.2238 ▼
[synthInstance] ❌ thing D ▼
[] no instances for thing D ▶
[synthInstance] ❌ thing D ▼
[] no instances for thing D ▶
[synthInstance] ❌ thing D ▼
[] no instances for thing D ▶
[synthInstance] ❌ thing D ▼
[] no instances for thing D ▶
[synthInstance] ❌ thing D ▼
[] no instances for thing D ▶
[synthInstance] ❌ thing D ▼
[] no instances for thing D ▶
[synthInstance] ❌ thing D ▼
[] no instances for thing D ▶
[synthInstance] ❌ thing D ▼
[] no instances for thing D ▶
[synthInstance] ❌ thing D ▼
[] no instances for thing D ▼
[instances] #[]
[synthInstance] ❌ thing D ▼
[] no instances for thing D ▼
[instances] #[]
[synthInstance] ❌ thing D ▶
....

That's probably lean4#2055

[Adam Topaz]

https://github.com/leanprover-community/mathlib4/blob/6f2b42f1aafa2e47304d7515c10523f85655bec8/Mathlib/CategoryTheory/Preadditive/Basic.lean#L203

[Adam Topaz]

Kevin Buzzard said:

That's probably lean4#2055

I think we're on to something here...

[Matthew Ballard]

Only about 20000 repeated failures here

[Adam Topaz]

@Kevin Buzzard do you know if the diamond in the BadClass example from lean4#2055 is really necessary?

[Kevin Buzzard]

There's a diamond?

[Adam Topaz]

not in BadClass, but in CommRing

[Matthew Ballard]

With trace.Meta.isDefEq true

[Meta.isDefEq] :cross_mark: ?F.map ?f =?= F.map (f + g) :play:

[Meta.Tactic.simp.unify] @CategoryTheory.Discrete.functor_map_id:1000, failed to unify
?F.map ?f
with
F.map (f + g)

[Meta.isDefEq] :check: ?F.map ?f =?= F.map (f + g) :play:

[Meta.isDefEq] :cross_mark: CategoryTheory.Category C =?= CategoryTheory.Category D :play:

[Meta.isDefEq] :check: CategoryTheory.Category C =?= CategoryTheory.Category C

[Meta.isDefEq] :check: ?m.2200 =?= inst:cross:⁴ :play:

[Meta.isDefEq] :check: CategoryTheory.Category C =?= CategoryTheory.Category C

[Meta.isDefEq] :check: inst:cross:⁴ =?= inst:cross:⁴

[Meta.isDefEq] :check: CategoryTheory.Category D =?= CategoryTheory.Category D

[Meta.isDefEq] :check: ?m.2207 =?= inst:cross:³ :play:

[Meta.isDefEq] :check: CategoryTheory.Category D =?= CategoryTheory.Category D

[Meta.isDefEq] :check: inst:cross:³ =?= inst:cross:³

[Meta.isDefEq] :check: CategoryTheory.Limits.HasZeroObject D =?= CategoryTheory.Limits.HasZeroObject ?m.2217 :play:

[Meta.isDefEq] :check: ?m.2214 =?= CategoryTheory.Limits.hasZeroObject_of_hasFiniteBiproducts D :play:

[Meta.isDefEq] :check: CategoryTheory.Limits.HasZeroMorphisms D =?= CategoryTheory.Limits.HasZeroMorphisms ?m.2226 :play:

[Meta.isDefEq] :check: ?m.2219 =?= CategoryTheory.Preadditive.preadditiveHasZeroMorphisms :play:

[Meta.isDefEq] :check: CategoryTheory.Preadditive D =?= CategoryTheory.Preadditive D :play:

[Meta.isDefEq] :check: ?m.2228 =?= inst:cross:¹ :play:

[Meta.isDefEq] :check: ?m.2228 =?= inst:cross:¹ :play:

[Meta.isDefEq] :check: ?m.2219 =?= CategoryTheory.Preadditive.preadditiveHasZeroMorphisms :play:

[Meta.isDefEq] :boom: CategoryTheory.Limits.HasFiniteBiproducts D =?= CategoryTheory.Limits.HasFiniteBiproducts ?m.2238 ▼
[] ✅ D =?= ?m.2238 ▶
[] ✅ inst✝³ =?= ?m.2239 ▶
[] 💥 CategoryTheory.Preadditive.preadditiveHasZeroMorphisms =?= CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ▼
[] ✅ D =?= D
[] ✅ inst✝³ =?= inst✝³
[] ❌ inst✝¹ =?= thing.toPreadditive ▶
[] 💥 CategoryTheory.Limits.HasZeroMorphisms.mk =?= CategoryTheory.Limits.HasZeroMorphisms.mk ▼
[] 💥 @CategoryTheory.Preadditive.preadditiveHasZeroMorphisms.proof_1 D inst✝³
inst✝¹ =?= @CategoryTheory.Preadditive.preadditiveHasZeroMorphisms.proof_1 D inst✝³ thing.toPreadditive ▼
[] 💥 ∀ {X Y : D} (f : X ⟶ Y) (R : D),
↑(CategoryTheory.Preadditive.leftComp R f) 0 =
0 =?= ∀ {X Y : D} (f : X ⟶ Y) (R : D), ↑(CategoryTheory.Preadditive.leftComp R f) 0 = 0 ▼
[] ✅ D =?= D
[] ✅ D =?= D
[] ✅ X✝ ⟶ Y✝ =?= X✝ ⟶ Y✝
[] ✅ D =?= D
[] 💥 ↑(CategoryTheory.Preadditive.leftComp R f) 0 = 0 =?= ↑(CategoryTheory.Preadditive.leftComp R f) 0 = 0 ▼
[] 💥 ↑(CategoryTheory.Preadditive.leftComp R f) 0 =?= ↑(CategoryTheory.Preadditive.leftComp R f) 0 ▼
[] found messy fun a => (fun x => X✝ ⟶ R) a =?= fun a => (fun x => X✝ ⟶ R) a
[] ❌ CategoryTheory.Preadditive.leftComp R f =?= CategoryTheory.Preadditive.leftComp R f ▼
[] ✅ R =?= R
[] ✅ f =?= f
[] ✅ D =?= D
[] ✅ inst✝³ =?= inst✝³
[] ❌ inst✝¹ =?= thing.toPreadditive ▶
[] ❌ AddMonoidHom.mk' (fun g => f ≫ g)
(_ :
∀ (g g' : Y✝ ⟶ R),
f ≫ (g + g') =
f ≫ g +
f ≫
g') =?= AddMonoidHom.mk' (fun g => f ≫ g)
(_ : ∀ (g g' : Y✝ ⟶ R), f ≫ (g + g') = f ≫ g + f ≫ g') ▶
[] 💥 AddHomClass.toFunLike.1 (CategoryTheory.Preadditive.leftComp R f)
0 =?= AddHomClass.toFunLike.1 (CategoryTheory.Preadditive.leftComp R f) 0 ▼
[] 💥 ZeroHom.toFun (↑(CategoryTheory.Preadditive.leftComp R f))
0 =?= ZeroHom.toFun (↑(CategoryTheory.Preadditive.leftComp R f)) 0 ▼
[] ❌ ↑(CategoryTheory.Preadditive.leftComp R f) =?= ↑(CategoryTheory.Preadditive.leftComp R f) ▶
[] 💥 (↑(CategoryTheory.Preadditive.leftComp R f)).1 0 =?= (↑(CategoryTheory.Preadditive.leftComp R f)).1 0 ▼
[] 💥 f ≫ 0 =?= f ≫ 0 ▼
[] ✅ f =?= f
[] ❌ 0 =?= 0 ▶
[] 💥 CategoryTheory.Category.toCategoryStruct.3 f 0 =?= CategoryTheory.Category.toCategoryStruct.3 f 0 ▼
[] ✅ CategoryTheory.Category.toCategoryStruct.3 =?= CategoryTheory.Category.toCategoryStruct.3
[] ✅ f =?= f
[] 💥 0 =?= 0 ▼
[] ✅ 0 =?= 0
[] ✅ Y✝ ⟶ R =?= Y✝ ⟶ R
[] 💥 Zero.toOfNat0 =?= Zero.toOfNat0 ▼
[] ✅ Y✝ ⟶ R =?= Y✝ ⟶ R
[] 💥 NegZeroClass.toZero =?= NegZeroClass.toZero ▼
[] ✅ Y✝ ⟶ R =?= Y✝ ⟶ R
[] 💥 SubNegZeroMonoid.toNegZeroClass =?= SubNegZeroMonoid.toNegZeroClass ▼
[] ✅ Y✝ ⟶ R =?= Y✝ ⟶ R
[] ❌ SubtractionMonoid.toSubNegZeroMonoid =?= SubtractionMonoid.toSubNegZeroMonoid ▶
[] 💥 NegZeroClass.mk (_ : -0 = 0) =?= NegZeroClass.mk (_ : -0 = 0) ▼
[] 💥 SubNegZeroMonoid.neg_zero =?= SubNegZeroMonoid.neg_zero ▼
[] 💥 -0 = 0 =?= -0 = 0 ▼
[] 💥 -0 =?= -0 ▼
[] ❌ 0 =?= 0 ▼
[] ✅ 0 =?= 0
[] ✅ Y✝ ⟶ R =?= Y✝ ⟶ R
[] ❌ Zero.toOfNat0 =?= Zero.toOfNat0 ▶
[] ❌ Zero.toOfNat0.1 =?= Zero.toOfNat0.1 ▶
[] 💥 SubNegMonoid.toNeg.1 0 =?= SubNegMonoid.toNeg.1 0 ▼
[] 💥 SubNegMonoid.toNeg.1 =?= SubNegMonoid.toNeg.1 ▼
[] 💥 SubNegMonoid.toNeg =?= SubNegMonoid.toNeg ▼
[] ✅ Y✝ ⟶ R =?= Y✝ ⟶ R
[] 💥 SubNegZeroMonoid.toSubNegMonoid =?= SubNegZeroMonoid.toSubNegMonoid ▼
[] ✅ Y✝ ⟶ R =?= Y✝ ⟶ R
[] 💥 SubtractionMonoid.toSubNegZeroMonoid =?= SubtractionMonoid.toSubNegZeroMonoid ▼
[] ✅ Y✝ ⟶ R =?= Y✝ ⟶ R
[] ❌ SubtractionCommMonoid.toSubtractionMonoid =?= SubtractionCommMonoid.toSubtractionMonoid ▶
[] 💥 let src := SubtractionMonoid.toSubNegMonoid;
SubNegZeroMonoid.mk
(_ : -0 = 0) =?= let src := SubtractionMonoid.toSubNegMonoid;
SubNegZeroMonoid.mk (_ : -0 = 0) ▼
[] 💥 SubNegZeroMonoid.mk (_ : -0 = 0) =?= SubNegZeroMonoid.mk (_ : -0 = 0) ▼
[] 💥 SubtractionMonoid.toSubNegZeroMonoid.proof_1 =?= SubtractionMonoid.toSubNegZeroMonoid.proof_1 ▼
[] 💥 -0 = 0 =?= -0 = 0 ▼
[] 💥 -0 =?= -0 ▶

[Matthew Ballard]

With pp all

[] :boom: @CategoryTheory.Limits.HasZeroMorphisms.mk.{?u.232, ?u.224} D inst:cross:³
(@inferInstance.{max (?u.224 + 1) (?u.232 + 1)}
((X Y : D) →
Zero.{?u.232}
(@Quiver.Hom.{?u.232 + 1, ?u.224} D
(@CategoryTheory.CategoryStruct.toQuiver.{?u.232, ?u.224} D
(@CategoryTheory.Category.toCategoryStruct.{?u.232, ?u.224} D inst:cross:³))
X Y))
fun (X Y : D) =>
@NegZeroClass.toZero.{?u.232}
(@Quiver.Hom.{?u.232 + 1, ?u.224} D
(@CategoryTheory.CategoryStruct.toQuiver.{?u.232, ?u.224} D
(@CategoryTheory.Category.toCategoryStruct.{?u.232, ?u.224} D inst:cross:³))
X Y)
(@SubNegZeroMonoid.toNegZeroClass.{?u.232}
(@Quiver.Hom.{?u.232 + 1, ?u.224} D
(@CategoryTheory.CategoryStruct.toQuiver.{?u.232, ?u.224} D
(@CategoryTheory.Category.toCategoryStruct.{?u.232, ?u.224} D inst:cross:³))
X Y)
(@SubtractionMonoid.toSubNegZeroMonoid.{?u.232}
(@Quiver.Hom.{?u.232 + 1, ?u.224} D
(@CategoryTheory.CategoryStruct.toQuiver.{?u.232, ?u.224} D
(@CategoryTheory.Category.toCategoryStruct.{?u.232, ?u.224} D inst:cross:³))
X Y)
(@SubtractionCommMonoid.toSubtractionMonoid.{?u.232}
(@Quiver.Hom.{?u.232 + 1, ?u.224} D
(@CategoryTheory.CategoryStruct.toQuiver.{?u.232, ?u.224} D
(@CategoryTheory.Category.toCategoryStruct.{?u.232, ?u.224} D inst:cross:³))
X Y)
(@AddCommGroup.toDivisionAddCommMonoid.{?u.232}
(@Quiver.Hom.{?u.232 + 1, ?u.224} D
(@CategoryTheory.CategoryStruct.toQuiver.{?u.232, ?u.224} D
(@CategoryTheory.Category.toCategoryStruct.{?u.232, ?u.224} D inst:cross:³))
X Y)
(@CategoryTheory.Preadditive.homGroup.{?u.232, ?u.224} D inst:cross:³ inst:cross:¹ X Y))))))
(@CategoryTheory.Preadditive.preadditiveHasZeroMorphisms.proof_1.{?u.232, ?u.224} D inst:cross:³ inst:cross:¹)
(@CategoryTheory.Preadditive.preadditiveHasZeroMorphisms.proof_2.{?u.232, ?u.224} D inst:cross:³
inst:cross:¹) =?= @CategoryTheory.Limits.HasZeroMorphisms.mk.{?u.232, ?u.224} D inst:cross:³
(@inferInstance.{max (?u.224 + 1) (?u.232 + 1)}
((X Y : D) →
Zero.{?u.232}
(@Quiver.Hom.{?u.232 + 1, ?u.224} D
(@CategoryTheory.CategoryStruct.toQuiver.{?u.232, ?u.224} D
(@CategoryTheory.Category.toCategoryStruct.{?u.232, ?u.224} D inst:cross:³))
X Y))
fun (X Y : D) =>
@NegZeroClass.toZero.{?u.232}
(@Quiver.Hom.{?u.232 + 1, ?u.224} D
(@CategoryTheory.CategoryStruct.toQuiver.{?u.232, ?u.224} D
(@CategoryTheory.Category.toCategoryStruct.{?u.232, ?u.224} D inst:cross:³))
X Y)
(@SubNegZeroMonoid.toNegZeroClass.{?u.232}
(@Quiver.Hom.{?u.232 + 1, ?u.224} D
(@CategoryTheory.CategoryStruct.toQuiver.{?u.232, ?u.224} D
(@CategoryTheory.Category.toCategoryStruct.{?u.232, ?u.224} D inst:cross:³))
X Y)
(@SubtractionMonoid.toSubNegZeroMonoid.{?u.232}
(@Quiver.Hom.{?u.232 + 1, ?u.224} D
(@CategoryTheory.CategoryStruct.toQuiver.{?u.232, ?u.224} D
(@CategoryTheory.Category.toCategoryStruct.{?u.232, ?u.224} D inst:cross:³))
X Y)
(@SubtractionCommMonoid.toSubtractionMonoid.{?u.232}
(@Quiver.Hom.{?u.232 + 1, ?u.224} D
(@CategoryTheory.CategoryStruct.toQuiver.{?u.232, ?u.224} D
(@CategoryTheory.Category.toCategoryStruct.{?u.232, ?u.224} D inst:cross:³))
X Y)
(@AddCommGroup.toDivisionAddCommMonoid.{?u.232}
(@Quiver.Hom.{?u.232 + 1, ?u.224} D
(@CategoryTheory.CategoryStruct.toQuiver.{?u.232, ?u.224} D
(@CategoryTheory.Category.toCategoryStruct.{?u.232, ?u.224} D inst:cross:³))
X Y)
(@CategoryTheory.Preadditive.homGroup.{?u.232, ?u.224} D inst:cross:³
(@thing.toPreadditive.{?u.224, ?u.232} D inst:cross:³ ?m.2240) X Y))))))
(@CategoryTheory.Preadditive.preadditiveHasZeroMorphisms.proof_1.{?u.232, ?u.224} D inst:cross:³
(@thing.toPreadditive.{?u.224, ?u.232} D inst:cross:³ ?m.2240))
(@CategoryTheory.Preadditive.preadditiveHasZeroMorphisms.proof_2.{?u.232, ?u.224} D inst:cross:³
(@thing.toPreadditive.{?u.224, ?u.232} D inst:cross:³ ?m.2240)) ▼
[] 💥 @CategoryTheory.Preadditive.preadditiveHasZeroMorphisms.proof_1.{?u.232, ?u.224} D inst✝³
inst✝¹ =?= @CategoryTheory.Preadditive.preadditiveHasZeroMorphisms.proof_1.{?u.232, ?u.224} D inst✝³
(@thing.toPreadditive.{?u.224, ?u.232} D inst✝³ ?m.2240) ▼
[] 💥 ∀ {X Y : D}
(f :
@Quiver.Hom.{?u.232 + 1, ?u.224} D
(@CategoryTheory.CategoryStruct.toQuiver.{?u.232, ?u.224} D
(@CategoryTheory.Category.toCategoryStruct.{?u.232, ?u.224} D inst✝³))
X Y)
(R : D),
@Eq.{?u.232 + 1}
((fun
(x :
@Quiver.Hom.{?u.232 + 1, ?u.224} D
(@CategoryTheory.CategoryStruct.toQuiver.{?u.232, ?u.224} D
(@CategoryTheory.Category.toCategoryStruct.{?u.232, ?u.224} D inst✝³))
Y R) =>
@Quiver.Hom.{?u.232 + 1, ?u.224} D
(@CategoryTheory.CategoryStruct.toQuiver.{?u.232, ?u.224} D
(@CategoryTheory.Category.toCategoryStruct.{?u.232, ?u.224} D inst✝³))
X R)
(@OfNat.ofNat.{?u.232}
(@Quiver.Hom.{?u.232 + 1, ?u.224} D
(@CategoryTheory.CategoryStruct.toQuiver.{?u.232, ?u.224} D
(@CategoryTheory.Category.toCategoryStruct.{?u.232, ?u.224} D inst✝³))
Y R)

[Matthew Ballard]

I don't think this gets fixed soon. What sounds like a good workaround until a fix is possible?

[Matthew Ballard]

/poll
nolint simpNF
remove hasZeroObject_of_hasFiniteBiproducts as an instance
remove IsZero.map from the simp set

[Kevin Buzzard]

Adam Topaz said:

Kevin Buzzard do you know if the diamond in the BadClass example from lean4#2055 is really necessary?

o_O it doesn't seem to be! Hang on

[Kevin Buzzard]

I updated the issue: you can get a smaller amount of chaos if you break the diamond (which you can upgrade to a much bigger amount of chaos by adding an instance of BadClass Nat.

[Adam Topaz]

The other option is to just get rid of Additive altogether and make it a mixin of the form Preadditive + HasFiniteBiproducts. That would probably require a refactor of mathlib3 before porting.

[Matthew Ballard]

Do you want Abelian categories for Denmark?

[Adam Topaz]

Not necessarily but it would be nice to have

[Adam Topaz]

FWIW I don’t think the refactor I suggested would be that bad

[Matthew Ballard]

Abelian too?

[Adam Topaz]

Does abelian extend additive? I thought it does not

[Matthew Ballard]

No but it extends Preadditive and HasFiniteBiproducts

[Adam Topaz]

Oh so that would cause similar issues

[Adam Topaz]

Yeah I guess we would refactor that as well

[Matthew Ballard]

It is the other PR in the title

[Matthew Ballard]

I would pause at refactoring and porting at the same time though within reason

[Matthew Ballard]

Other the Denmark school, I can't think of any hard constraints for these files (and their dependents)

[Adam Topaz]

Since lean4#2055 is causing issues for others (cf. this) I think the right solution is to wait for this issue to be resolved, unfortunately.

Let me also ping to see what @Scott Morrison thinks about this issue.

[Jeremy Tan]

Adam Topaz said:

Since lean4#2055 is causing issues for others (cf. this) I think the right solution is to wait for this issue to be resolved, unfortunately.

Let me also ping to see what Scott Morrison thinks about this issue.

Since you seem to be free from porting anything at the moment, why not work on lean4#2055?

[Jeremy Tan]

Our future depends on solving the above

[Johan Commelin]

@Jeremy Tan please calm down a bit! We appreciate your help with porting, but people have many obligations!
You only recently showed up on zulip. Please avoid sounding like you are bossing people around.