simp not using a simp lemma

Stream: mathlib4

[Winston Yin]

In the following example, why isn't simp using map_one?

import Mathlib.Data.FunLike.Basic

variable {M N P F : Type _} [MulOneClass M] [MulOneClass N]

structure OneHom (M : Type _) (N : Type _) [One M] [One N] where
  toFun : M → N
  map_one' : toFun 1 = 1

class OneHomClass (F : Type _) (M N : outParam <| Type _)
  [outParam <| One M] [outParam <| One N] extends FunLike F M fun _ => N where
  map_one : ∀ f : F, f 1 = 1

instance OneHom.oneHomClass : OneHomClass (OneHom M N) M N where
  coe := OneHom.toFun
  coe_injective' f g h := by cases f; cases g; congr
  map_one := OneHom.map_one'

@[simp]
theorem map_one [OneHomClass F M N] (f : F) : f 1 = 1 :=
  OneHomClass.map_one f

structure MulHom (M : Type _) (N : Type _) [Mul M] [Mul N] where
  toFun : M → N
  map_mul' : ∀ x y, toFun (x * y) = toFun x * toFun y

infixr:25 " →ₙ* " => MulHom

class MulHomClass (F : Type _) (M N : outParam <| Type _)
  [outParam <| Mul M] [outParam <| Mul N] extends FunLike F M fun _ => N where
  map_mul : ∀ (f : F) (x y : M), f (x * y) = f x * f y

@[simp]
theorem map_mul [MulHomClass F M N] (f : F) (x y : M) : f (x * y) = f x * f y :=
  MulHomClass.map_mul f x y

structure MonoidHom (M : Type _) (N : Type _) [MulOneClass M] [MulOneClass N] extends
  OneHom M N, M →ₙ* N

class MonoidHomClass (F : Type _) (M N : outParam <| Type _)
  [outParam <| MulOneClass M] [outParam <| MulOneClass N] extends
  MulHomClass F M N, OneHomClass F M N

infixr:25 " →* " => MonoidHom

instance MonoidHom.monoidHomClass : MonoidHomClass (M →* N) M N where
  coe f := f.toFun
  coe_injective' f g h := by
    cases f
    cases g
    congr
    apply OneHom.oneHomClass.coe_injective'
    exact h
  map_mul := MonoidHom.map_mul'
  map_one f := f.toOneHom.map_one'

def MonoidHom.comp [MulOneClass M] [MulOneClass N] [MulOneClass P] (hnp : N →* P) (hmn : M →* N) : M →* P where
  toFun := hnp ∘ hmn
  map_one' := by simp [-FunLike.coe_eq_coe_fn]; rw [map_one, map_one] -- map_one can be applied manually
-- fails to complete goal: by simp [-FunLike.coe_eq_coe_fn]
  map_mul' := by simp [-FunLike.coe_eq_coe_fn]

[Eric Rodriguez]

I wonder if this is the same issue as I'm having with EmbeddingLike, see https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/EmbeddingLike

[Eric Rodriguez]

I think this is likely a serious problem

[Andrew Yang]

Is this related to the head symbol simp optimization thingy?

[Mario Carneiro]

I can't replicate misread the issue

[Scott Morrison]

I wonder if this is the same as https://github.com/leanprover/lean4/issues/1869.

[Winston Yin]

Hmm that issue seems to be about simp attribute applied to Prop fields of structures. In my case, map_one is defined as a standalone simp theorem.

[Reid Barton]

Is this the same issue?

import Mathlib.Order.Hom.Basic

theorem ex {α : Type} [PartialOrder α] {x : α} : (OrderHom.id.comp OrderHom.id) x = x := by
  dsimp only [OrderHom.comp_coe] -- no change
  simp only [OrderHom.comp_coe]  -- no change
  rw [OrderHom.comp_coe]         -- better!
  rfl

[Reid Barton]

MWE

structure THom (a b : Type) : Type where
  toFun : a → b

def THom.comp {a b c : Type} : THom a b → THom b c → THom a c :=
fun f g => ⟨g.1 ∘ f.1⟩

@[simp] theorem THom.comp_toFun {a b c : Type} (f : THom a b) (g : THom b c)
  : (f.comp g).toFun = g.toFun ∘ f.toFun :=
rfl

def THom.id {a : Type} : THom a a := ⟨@_root_.id a⟩

theorem ex2 {a : Type} (x : a) : (THom.id.comp THom.id).toFun x = x :=
by
  simp only [THom.comp_toFun]   -- does nothing
  rw [THom.comp_toFun]          -- works
  rfl

[Reid Barton]

Maybe simp somehow can't simplify function applications properly?

Meta.Tactic.simp.unify] @THom.comp_toFun:1000, failed to unify
      (THom.comp ?f ?g).toFun
    with
      THom.toFun (THom.comp THom.id THom.id) x

[Reid Barton]

Of course they don't unify, because of the x

[Reid Barton]

Looks like this is https://github.com/leanprover/lean4/issues/1937

[Kevin Buzzard]

Reid Barton said:

Of course they don't unify, because of the x

I don't understand this. Why don't they unify? This works in Lean 3:

-- lean 3

structure THom (a b : Type) : Type :=
(toFun : a → b)

def THom.comp {a b c : Type} : THom a b → THom b c → THom a c :=
fun f g, ⟨g.1 ∘ f.1⟩

@[simp] theorem THom.comp_toFun {a b c : Type} (f : THom a b) (g : THom b c)
  : (f.comp g).toFun = g.toFun ∘ f.toFun :=
rfl

def THom.id {a : Type} : THom a a := ⟨@_root_.id a⟩

theorem ex2 {a : Type} (x : a) : (THom.id.comp THom.id).toFun x = x :=
begin
  simp only [THom.comp_toFun],   -- does something
  refl,
end

[Kevin Buzzard]

-- lean 4
example (f g : α → β) (h : f = g) (a : α) (b : β) : f a = b := by
  simp only [h] -- does something
  sorry

That unifies fine.

[Reid Barton]

Right, simp should work. But for some reason it tries to unify the LHS of comp_toFun with the entire LHS of the goal--maybe because it counted some arguments wrong or something.

[Reid Barton]

Yeah, it is something more specific than "simp a function application, with a lemma about the function".

[Reid Barton]

On the lean4 issue linked above, @Anne Baanen says it happens when there is a structure field projection involved

[Kevin Buzzard]

Aah I see, I had not properly grokked the trace output.

[Kevin Buzzard]

Is this issue

import Mathlib.CategoryTheory.StructuredArrow

open CategoryTheory Limits

variable (C: Type _) [Category C] (D : Type _) [Category D]
(J : Type _) [SmallCategory J]
(F: C ⥤ D)
(K: J ⥤ C)
(c: Cone K)
(s: Cone (K ⋙ F))
(j₁ j₂: J) (φ: j₁ ⟶ j₂)
(f₁ f₂: s.pt ⟶ F.obj c.pt)
(foo : (StructuredArrow.mk (f₁ ≫ F.map (c.π.app j₂)) : StructuredArrow s.pt (K ⋙ F)) =
          StructuredArrow.mk (s.π.app j₂))
(bar : (StructuredArrow.mk (f₁ ≫ F.map (c.π.app j₁)) : StructuredArrow s.pt (K ⋙ F)) =
          StructuredArrow.mk (s.π.app j₁))

example: φ ≫ (eqToHom foo).right = (eqToHom bar).right ≫ φ := by
  simp -- does nothing
  rw [Comma.eqToHom_right] -- a `simp` lemma
  simp -- small progress
  rw [Comma.eqToHom_right] -- a `simp` lemma
  simp
  done

related to the discussion above or is this an unrelated problem?

[Eric Wieser]

This is about !4#3703, right?

[Kevin Buzzard]

I've left a porting note. It's here and again a few lines later.

[Eric Wieser]

Making StructuredArrow reducible solves everything here

[Eric Wieser]

The problem is that eqToHom_right is about Comma (Functor.fromPUnit S) T, but our goal contains StructuredArrow S T.

For whatever reason, simp isn't happy to unfold things, but rw is.

I suspect this is like #mathlib4 > LinearAlgebra.Dual, where making things reducible is the right call.

[Sebastian Ullrich]

A note on simp debugging: you should always start with trace.Meta.Tactic.simp. If, like here, it doesn't even say that it tried to apply the lemma and failed, then it's not a problem with TC synth or unification, but with simp lemma indexing (the discrimination tree)

[Sebastian Ullrich]

Eric Wieser said:

For whatever reason, simp isn't happy to unfold things, but rw is.

Since StructuredArrow is an implicit parameter to eqToHom, it might be the case that rw succeeds because the unifier always unfolds non-irreducible defs when visiting implicit parameters, while the discrimination tree does not have such a special case. In the end it is expected that simp lemma indexing trades some accuracy for performance.

[Eric Wieser]

In this particular case I don't think we're getting any advantage by not making the definition reducible

[Eric Wieser]

I will try it out in Mathlib3 to find out... (edit: #18973)

[Sebastian Ullrich]

That sounds like the right call, but just to further illustrate the issue: using

    (eqToHom (C := no_index _) H).right = ...

in eqToHom_right also fixes the proof

[Kevin Buzzard]

So should this change be made to mathlib?

[Eric Wieser]

Which change? Mine (#18973) or Sebastian's?

[Kevin Buzzard]

I was asking about Sebastian's but anything is fine. I just wanted to make progress with !4#3703

[Eric Wieser]

My preference would be to try these reducibility changes and see if that allows us to remove most of the workarounds from the file, rather than just merge things with the workaround and clean up later; but I've no feel for how important doing this file quickly is. The argument for sorting out the workarounds first is that it may make downstream files easier too.

[Eric Wieser]

I don't think @Sebastian Ullrich's solution scales very well here; we don't really want to tell lean that every lemma about Comma should be no-indexed to allow it to work for semireducible aliases

[Kevin Buzzard]

I've just checked that Sebastian's suggested change lets me remove three workarounds in !4#3703; I'll now check that yours does too.

[Eric Wieser]

(To be clear sebastian's comment is very helpful here, especially for debugging; I just don't think it's something mathlib can exploit much)

[Kevin Buzzard]

Yeah your change also lets me remove the workarounds, although it breaks mathlib a bit more than Sebastian's suggestion (I also had to edit CategoryTheory.Elements (I had to add two rfls after simps) and CategoryTheory.Comma (a new goal appeared which simp closed))