simp requires a universe annotation?

Stream: mathlib4

[Kim Morrison]

Has anyone seen this phenomenon before:

    fail_if_success
      simp only [foo] -- Doesn't work as a simp lemma until we specify the universe levels explicitly!
    simp only [foo.{v₁ + 1}] -- Succeeds

[Kim Morrison]

(If anyone wants to play with it, it is on branch#Bimon, in Mathlib/CategoryTheory/Monoidal/Bimon_.lean, in to_Mon_Comon_obj.)

[Kim Morrison]

I'm mystified

[Daniel Weber]

Not sure what's going on there, but just apply Mon_.mul_one seems to work

[Kim Morrison]

Thanks. I would like to get to the bottom of this, as this goal should work by simp and this issue badly breaks automation.

[Eric Wieser]

Does it work as (foo)?

[Daniel Weber]

Eric Wieser said:

Does it work as (foo)?

Seems like it, yeah

[Daniel Weber]

Comparing the traces, the relevant difference seems to be that for the one without a specific universe it fails to find anything for this term:

[Debug.Meta.Tactic.simp] no theorems found for post-rewriting { unop := { hom := M.X.one.op, one_hom := ⋯, mul_hom := ⋯ } }.unop

[Debug.Meta.Tactic.simp] no post-simprocs found for { unop := { hom := M.X.one.op, one_hom := ⋯, mul_hom := ⋯ } }.unop

whereas foo.{v₁ + 1} has

[Meta.Tactic.simp.rewrite] foo.{v₁ +
          1}:1000, {
        unop :=
          { hom := M.X.one.op, one_hom := ⋯, mul_hom := ⋯ } }.unop ==> { hom := M.X.one.op, one_hom := ⋯, mul_hom := ⋯ }

Using (foo) has almost the same output there, just (foo):1000 instead of foo.{v₁ + 1}:1000.

[Eric Wieser]

Are those first logs for (foo) or foo?

[Eric Wieser]

I think the issue here is that simp [foo] is shorthand for simp [@foo], and so you need to insert some other syntax to prevent the special case for identifiers taking over; either () or a universe annotation is enough to do that

[Daniel Weber]

Eric Wieser said:

Are those first logs for (foo) or foo?

The first logs are for foo. (foo) gives

[Meta.Tactic.simp.rewrite] (foo):1000, {
        unop :=
          { hom := M.X.one.op, one_hom := ⋯, mul_hom := ⋯ } }.unop ==> { hom := M.X.one.op, one_hom := ⋯, mul_hom := ⋯ }

[Daniel Weber]

Shouldn't it also work for dsimp? For dsimp even foo.{v₁ + 1} fails

[Matthew Ballard]

This works

@[simp] theorem foo {V} [Quiver V] {X Y x} :
    @Quiver.Hom.unop V _ X Y no_index (Opposite.op (unop := x)) = x := rfl

[Matthew Ballard]

I am sure someone has a handy way to dump the keys for the two the cases. (I've got to go to Costco.)

[Matthew Ballard]

But my guess from this is that the keys are getting crunched down too much to match

[Matthew Ballard]

Another fix: make docs#Quiver.Hom.unop and docs#Quiver.Hom.op abbrev.

Not sure of the impact of this.

[Matthew Ballard]

Bonus: you don't even need foo anymore

[Matthew Ballard]

Performance impact: http://speed.lean-fro.org/mathlib4/run-detail/72df5316-31cc-4c76-b571-906f13c0dcce

#12936

[Johan Commelin]

Some proofs became longer to write. But performance also improved.
So... @Kim Morrison are you happy with this solution?

[Kim Morrison]

:writing:

[Kim Morrison]

Not concerned by the changes to proofs, just by nolint simpVarHead, which I think is bad news.

[Matthew Ballard]

I responded to the comments there with agreement but I think broader discussion would be useful.

Now that docs#Quiver.Hom.unop_op and docs#Quiver.Hom.op_unop are covered by built in reduction rules, I thought we would be fine removing them from the simp tree.

[Matthew Ballard]

But! Automation starts breaking immediately. Why? Well the following works fine for docs#CategoryTheory.Category.opposite

instance Category.opposite : Category.{v₁} Cᵒᵖ where
  comp := fun ⟨f⟩ ⟨g⟩ => ⟨g ≫ f⟩
  id := fun ⟨X⟩ => ⟨𝟙 X⟩

Whereas the current statement

instance Category.opposite : Category.{v₁} Cᵒᵖ where
  comp f g := (g.unop ≫ f.unop).op
  id X := (𝟙 (unop X)).op

is broken

[Matthew Ballard]

Eg #lean4 > optimal instance design for structure wrappers

[Matthew Ballard]

Also, I've never seen a simpVarHead warning that isn't secretly provable with by simp

[Matthew Ballard]

Here is an example.

universe v u

class Quiver (V : Type u) where
  Hom : V → V → Sort v

infixr:10 " ⟶ " => Quiver.Hom

namespace CategoryTheory

class CategoryStruct (obj : Type u) extends Quiver.{v + 1} obj : Type max u (v + 1) where
  id : ∀ X : obj, Hom X X
  comp : ∀ {X Y Z : obj}, (X ⟶ Y) → (Y ⟶ Z) → (X ⟶ Z)

notation "𝟙" => CategoryStruct.id

infixr:80 " ≫ " => CategoryStruct.comp

class Category (obj : Type u) extends CategoryStruct.{v} obj : Type max u (v + 1) where
  comp_id : ∀ {X Y : obj} (f : X ⟶ Y), f ≫ 𝟙 Y = f

open Category in
attribute [simp] comp_id

end CategoryTheory

structure Opposite (α : Sort u) :=
  op :: unop : α

notation:max α "ᵒᵖ" => Opposite α

open Opposite

namespace Quiver

instance opposite {V} [Quiver V] : Quiver Vᵒᵖ :=
  ⟨fun a b => (unop b ⟶  unop a)ᵒᵖ⟩

abbrev Hom.op {V} [Quiver V] {X Y : V} (f : X ⟶ Y) : op Y ⟶ op X := Opposite.op f

abbrev Hom.unop {V} [Quiver V] {X Y : Vᵒᵖ} (f : X ⟶ Y) : unop Y ⟶ unop X := Opposite.unop f

variable [Quiver.{v} C]

@[simp] -- we should remove this since it's proof is `simp` right? but doing so breaks the example
theorem Quiver.Hom.unop_op {X Y : C} (f : X ⟶ Y) : f.op.unop = f := by simp only -- red flag!

@[simp]
theorem Quiver.Hom.op_unop {X Y : Cᵒᵖ} (f : X ⟶ Y) : f.unop.op = f :=
  rfl

end Quiver

open CategoryTheory Quiver Category

variable (C : Type u) [Category.{v} C]

example (X Y : Cᵒᵖ) (f : X ⟶  Y) : (f.unop ≫ (𝟙 (unop X)).op.unop).op = f  := by simp?

[Matthew Ballard]

This takes the existing definitions in the library and makes docs#Quiver.Hom.op and docs#Quiver.Hom.unop abbrev's.

[Matthew Ballard]

Now docs#Quiver.Hom.unop_op becomes a simp only so we should remove @[simp].

[Matthew Ballard]

But that breaks the example

[Matthew Ballard]

If we change the Quiver instance on the opposite to

instance opposite {V} [Quiver V] : Quiver Vᵒᵖ :=
  ⟨fun ⟨a⟩ ⟨b⟩ => (b ⟶  a)ᵒᵖ⟩

then

theorem Hom.op_unop' {X Y : Cᵒᵖ} (f : X ⟶ Y) : op (unop f) = f := by simp

works fine as does

example (X Y : Cᵒᵖ) (f : X ⟶  Y) : op (unop f ≫ (unop (op (𝟙 (unop X))))) = f := by simp

[Matthew Ballard]

Neither of these work with the original syntax

[Matthew Ballard]

[simp] theorems with bad keys ▼
  comp_id, key: @CategoryStruct.comp _ _ _ _ _ _ (@CategoryStruct.id _ _ _)

Hmm, that seems bad

[Matthew Ballard]

If we go back to the original definition of opposite, then

[simp] theorems with bad keys ▼
  Hom.op_unop, key: @op (@Hom _ _ (@op _ _.1).1 (@op _ _.1).1) _.1

for

set_option diagnostics true in
example {X Y : Cᵒᵖ} (f : X ⟶  Y) : op (unop f) = f := by simp (config := { index := false })

[Matthew Ballard]

What the heck! Should what namespace things live in affect the behavior of simp?

universe v u

class Quiver (V : Type u) where
  Hom : V → V → Sort v

infixr:10 " ⟶ " => Quiver.Hom

structure Opposite (α : Sort u) :=
  op :: unop : α

notation:max α "ᵒᵖ" => Opposite α

open Opposite

namespace Quiver

instance opposite {V} [Quiver V] : Quiver Vᵒᵖ :=
  ⟨fun a b => (unop b ⟶  unop a)ᵒᵖ⟩

abbrev Hom.op {V} [Quiver V] {X Y : V} (f : X ⟶ Y) : op Y ⟶ op X := Opposite.op f

abbrev Hom.unop {V} [Quiver V] {X Y : Vᵒᵖ} (f : X ⟶ Y) : unop Y ⟶ unop X := Opposite.unop f

variable (C : Type u) [Quiver.{v} C]

@[simp]
theorem Hom.op_unop {X Y : Cᵒᵖ} (f : X ⟶ Y) : f.unop.op = f := rfl

theorem Hom.bar {X Y : Cᵒᵖ} (f : X ⟶  Y) : op (unop f) = f := by simp -- works
theorem bar {X Y : Cᵒᵖ} (f : X ⟶ Y) : op (unop f) = f := by simp -- fails

[Matthew Ballard]

I can't move messages to another thread so I just copied the last one.

[Mario Carneiro]

Isn't the different namespace changing the name resolution of op and unop here?

[Yaël Dillies]

Yes, Matthew figured that out

[Matthew Ballard]

Yes. But hover was tricking me

[Mario Carneiro]

maybe you want to make Hom.op and Hom.unop protected

[Matthew Ballard]

My main issue is trying to figure out why the example at the start of the thread (EDIT: today!) didn’t work

[Matthew Ballard]

If X is closed by simp, should I need to add X to the simp set?

[Matthew Ballard]

We have a linter for this so I thought the answer was no

[Matthew Ballard]

The example at the start runs counter to the expectation.

[Yaël Dillies]

Matthew Ballard said:

If X is closed by simp, should I need to add X to the simp set?

Depends

[Yaël Dillies]

Possibly simp is simplifying the equality itself, in which case simp-nf shouldn't complain

[Yaël Dillies]

The true test is whether the LHS gets simplified to the RHS (without simp seeing the equality)

[Matthew Ballard]

Hmm. Can you point me to an example?

[Matthew Ballard]

The issue goes away here with the index := false config option on lean4 master

[Yaël Dillies]

Can't think of an actual example off the top of my head, but imagine we were making docs#Set.eq_empty_iff_forall_not_mem a simp lemma and we had a simp lemma foo (x): x ∉ fancySet. Then fancySet = ∅ can be proved by simp, but simp can't simplify fancySet to ∅.

[Matthew Ballard]

I see

[Yaël Dillies]

Note that I'm not inventing anything. The simpNF linter already follows this logic.

[Matthew Ballard]

This is the same behavior as in Lean 3?

[Yaël Dillies]

Basically. The only difference is that sometimes simp applies extensionality on the fly using congruence lemmas, meaning that it might actually be able to simplify fancySet to ∅ in my toy example above. I don't really understand under which conditions this happens, though.

[Matthew Ballard]

It looks like you should assign a * to any implicit argument taking [self : Class]

[Matthew Ballard]

And that structure eta has to be a bit more aggressive