simp [X] fails, rw [X] works

Stream: lean4

[Kevin Buzzard]

Porting RingTheory.TensorProduct I noticed that there were a few times when simp only [A,B,C] in mathlib3 had to be changed to simp only [A], rw [B], simp only [C]. This is kind of annoying because debugging a failing simp call is slow and you never know what isn't firing if you don't understand the mathematics properly.

So here's an example on the RingTheory.TensorProduct branch !4#4004, which I know isn't ideal, but it at least indicates how far I've got with debugging. The simp call which fails and needs to be turned into a rw is here, and here's what's going on:

import Mathlib.RingTheory.TensorProduct

variable {R : Type} [CommSemiring R]

variable {A : Type} [Semiring A] [Algebra R A]

variable {B : Type} [Semiring B] [Algebra R B]

open TensorProduct -- for notation

example (x y z : A ⊗[R] B) : x * (y + z) = x * y + x * z := by
  simp only [mul_add] -- works fine
  done

example (x y z : A ⊗[R] B) : x *
    -- `(y + z)` but with a different `+`
    (@HAdd.hAdd.{0, 0, 0}
      (@TensorProduct.{0, 0, 0} R _ A B
        (@NonUnitalNonAssocSemiring.toAddCommMonoid.{0} A
          (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{0} A (@Semiring.toNonAssocSemiring.{0} A _)))
        (@NonUnitalNonAssocSemiring.toAddCommMonoid.{0} B
          (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{0} B (@Semiring.toNonAssocSemiring.{0} B _)))
        (@Algebra.toModule.{0, 0} R A _ _ _) (@Algebra.toModule.{0, 0} R B _ _ _))
      (@TensorProduct.{0, 0, 0} R _ A B
        (@NonUnitalNonAssocSemiring.toAddCommMonoid.{0} A
          (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{0} A (@Semiring.toNonAssocSemiring.{0} A _)))
        (@NonUnitalNonAssocSemiring.toAddCommMonoid.{0} B
          (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{0} B (@Semiring.toNonAssocSemiring.{0} B _)))
        (@Algebra.toModule.{0, 0} R A _ _ _) (@Algebra.toModule.{0, 0} R B _ _ _))
      (@TensorProduct.{0, 0, 0} R _ A B
        (@NonUnitalNonAssocSemiring.toAddCommMonoid.{0} A
          (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{0} A (@Semiring.toNonAssocSemiring.{0} A _)))
        (@NonUnitalNonAssocSemiring.toAddCommMonoid.{0} B
          (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{0} B (@Semiring.toNonAssocSemiring.{0} B _)))
        (@Algebra.toModule.{0, 0} R A _ _ _) (@Algebra.toModule.{0, 0} R B _ _ _))
      (@instHAdd.{0}
        (@TensorProduct.{0, 0, 0} R _ A B
          (@NonUnitalNonAssocSemiring.toAddCommMonoid.{0} A
            (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{0} A (@Semiring.toNonAssocSemiring.{0} A _)))
          (@NonUnitalNonAssocSemiring.toAddCommMonoid.{0} B
            (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{0} B (@Semiring.toNonAssocSemiring.{0} B _)))
          (@Algebra.toModule.{0, 0} R A _ _ _) (@Algebra.toModule.{0, 0} R B _ _ _))
        (@AddZeroClass.toAdd.{0}
          (@TensorProduct.{0, 0, 0} R _ A B
            (@NonUnitalNonAssocSemiring.toAddCommMonoid.{0} A
              (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{0} A (@Semiring.toNonAssocSemiring.{0} A _)))
            (@NonUnitalNonAssocSemiring.toAddCommMonoid.{0} B
              (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{0} B (@Semiring.toNonAssocSemiring.{0} B _)))
            (@Algebra.toModule.{0, 0} R A _ _ _) (@Algebra.toModule.{0, 0} R B _ _ _))
          (@TensorProduct.addZeroClass.{0, 0, 0} R _ A B
            (@NonUnitalNonAssocSemiring.toAddCommMonoid.{0} A
              (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{0} A (@Semiring.toNonAssocSemiring.{0} A _)))
            (@NonUnitalNonAssocSemiring.toAddCommMonoid.{0} B
              (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{0} B (@Semiring.toNonAssocSemiring.{0} B _)))
            (@Algebra.toModule.{0, 0} R A _ _ _) (@Algebra.toModule.{0, 0} R B _ _ _))))
        y z) = x * y + x * z := by
  -- Goal is `x * (y + z) = x * y + x * z`
  simp only [mul_add] -- does nothing
  rw [mul_add] -- works
  -- Alternative finish:
  -- change x * (y + z) = x * y + x * z -- changes `+` syntactically but not definitionally
  -- simp only [mul_add] -- now works
  done

In the PR, somehow addition has managed to become a noncanonical addition, which is what seems to stop simp from working, but doesn't stop rw. Hopefully someone will come up with a better example but maybe is this already enough of a clue for people to explain what's going on.

[Eric Wieser]

Uh oh; does this mean simp is keying on the instance arguments in the DiscrTree?

[Eric Wieser]

RingTheory.TensorProduct not LinearAlgebra.TensorProduct, right?

[Kevin Buzzard]

Thanks -- fixed

[Eric Wieser]

simp only [(mul_add)] works here

[Eric Wieser]

simp [(X)] is a standard trick to fix simp [X] not working

[Kevin Buzzard]

simp only [mul_add x] also works, but I saw an example of the form forall x y z, x * (y + z) = ... where you didn't have access to the variables.

[Kevin Buzzard]

Eric Wieser said:

simp only [(mul_add)] works here

Whatever is going on?

[Eric Wieser]

mul_add by itself is treated like @mul_add I think. (mul_add) is the same as @mul_add _ _ _

[Eric Wieser]

simp treats it as a lemma name not an expression

[Eric Wieser]

Like #check mul_add vs #check (mul_add)

[Eric Wieser]

So I think the cause of the failure is the same as whatever causes simp [@mul_add] to fail

[Eric Wieser]

Not that I know what that is

[Kevin Buzzard]

I can't get the bracket trick to work on lines 1191-1193 of RingTheory.TensorProduct. The Lean 3 proof simp only [module_aux_apply, mul_smul, smul_comm a₁ b₂, algebra.tensor_product.tmul_mul_tmul, linear_map.mul_apply] becomes

      simp only [(· • ·), Algebra.TensorProduct.tmul_mul_tmul]
      simp only [moduleAux_apply, mul_smul]
      rw [smul_comm a₁ b₂]

in Lean 4 -- but regardless of what the Lean 3 proof is, is it surprising that this can't be compressed (by me) to one line in Lean 4? Note also that "you have to randomly put brackets around some of the proofs" is not particularly user-friendly.

[Eric Wieser]

Note also that "you have to randomly put brackets around some of the proofs" is not particularly user-friendly.

Especially since this makes @[simp] useless, as the rule is also "anything tagged simp that has this problem has to be added manually in ()s"

[Eric Wieser]

Does replacing smul_comm a₁ b₂ with smul_comm a₁ b₂ _ work?

[Eric Wieser]

And if not, then smul_comm a₁ b₂ (_ : TheRightType) will almost certainly work

[Kyle Miller]

If this is the "simp wants the canonical instance" problem, another thing is @mul_comm _ (_), where (_) is at the instance argument, and the parentheses cause it to be treated like an implicit argument instead.

[Kevin Buzzard]

The goal is ⊢ a₂ • a₁ • b₂ • b₁ • m = a₂ • b₂ • a₁ • b₁ • m on line 1193, and rw [smul_comm a₁ b₂] works, but simp only [smul_comm a₁ b₂] fails, simp only [smul_comm a₁ b₂ (b₁ • m)] works, simp only [(smul_comm a₁ b₂)] fails.

[Eric Wieser]

The paren trick only makes a difference for unapplied lemmas

[Eric Wieser]

Did simp only [smul_comm a₁ b₂ _] fail? What type is m?

[Kyle Miller]

This works on line 497 simp [@mul_add _ (_) (_) (_), @add_mul _ (_) (_) (_), h, h'] (though of course it's uglier than before)

[Eric Wieser]

Kyle, I thought we already found that simp[(mul_add), (add_mul), h, h'] works fine there too?

[Eric Wieser]

I think the two are equivalent

[Kevin Buzzard]

Eric Wieser said:

Did simp only [smul_comm a₁ b₂ _] fail? What type is m?

simp only [smul_comm a₁ b₂ _] fails. The relevant types are

R: Type ?u.2364979
A: Type ?u.2364982
B: Type ?u.2364985
M: Type ?u.2364988
inst✝¹¹: CommSemiring R
inst✝¹⁰: AddCommMonoid M
inst✝⁹: Module R M
inst✝⁸: Semiring A
inst✝⁷: Semiring B
inst✝⁶: Module A M
inst✝⁵: Module B M
inst✝⁴: Algebra R A
inst✝³: Algebra R B
inst✝²: IsScalarTower R A M
inst✝¹: IsScalarTower R B M
inst✝: SMulCommClass A B M
m: M
a₁: A
b₁: B
a₂: A
b₂: B

[Eric Wieser]

Then I predict simp only [smul_comm a₁ b₂ (_ : M)] will work

[Kevin Buzzard]

Indeed it does work. But the bottom line is that this is very confusing for users. My mental model of simp is "try rw [X] for every X which looks like it might work" and this is clearly not what's happening here, in the sense that rw works but simp needs some hints. Why is this happening? Is it worth opening an issue? Do you have any idea how to minimise? This is confusing for users.

[Eric Wieser]

My guess it that simp gives up on the typeclass argument to smul_comm rather than finding it by unification

[Matthew Ballard]

Is there a simp -vvvv mode?

[Eric Wieser]

Which is a general pattern in Lean 4; there are many places where typeclass search is no longer allowed to fall back to unification. I think this was a deliberate choice to avoid confusion, but I can't help but feel this consistently makes things more confusing.

[Kevin Buzzard]

Matthew Ballard said:

Is there a simp -vvvv mode?

Do you just mean set_option trace.Meta.Tactic.simp true or something else?

[Kevin Buzzard]

simp only [smul_comm a₁ b₂] ->

...
inst✝: SMulCommClass A B M
x y: A ⊗[R] B
m: M
a₁: A
b₁: B
a₂: A
b₂: B
⊢ a₂ • a₁ • b₂ • b₁ • m = a₂ • b₂ • a₁ • b₁ • m
Messages (1)
TensorProduct.lean:1195:6
[Meta.Tactic.simp.discharge] >> discharge?: SMulCommClass A B M

[Meta.Tactic.simp.discharge] smul_comm a₁ b₂, failed to discharge hypotheses
      SMulCommClass A B M

[Matthew Ballard]

I confess to not knowing about that. Is it helpful?

[Eric Wieser]

Oh, I was expecting that to be SMulCommClass A B ?_. I'm even more confused about why it's stuck there. Maybe it forgot to instantiate the metavariable before doing TC search?

[Matthew Ballard]

Thanks! That should be helpful to me though maybe not verbose enough in general

[Kevin Buzzard]

You can also switch on isDefEq for more fun (I forget its full name, but set_option is one of the few places where autocomplete currently works well in Lean 4, unlike imports and theorem names...)

[Matthew Ballard]

Yeah and tracing synthInstance too

[Matthew Ballard]

I don’t know how many times I’ve had to break out a giant failingsimp (that worked ML3) into line by line rw because I can’t see inside

[Sebastian Ullrich]

Kevin Buzzard said:

(I forget its full name, but set_option is one of the few places where autocomplete currently works well in Lean 4, unlike imports and theorem names...)

What's this about theorem names?

[Kevin Buzzard]

Autocomplete: I'll start a new thread. I had assumed this was well-known. Maybe I'm doing something wrong

[Kevin Buzzard]

I tried to minimise this more. Is this behaviour expected?

import Mathlib.Algebra.Ring.Defs

variable {R : Type} [Semiring R]

def bar : AddZeroClass R := inferInstance -- note AddZeroClass -> Add -> HAdd

example (a b c : R) : a * (@HAdd.hAdd R R R (@instHAdd R (@AddZeroClass.toAdd R bar)) b c) = a * b + a * c := by
  -- ⊢ a * (b + c) = a * b + a * c
  simp only [mul_add] -- does nothing
  rw [mul_add] -- works
  done

I don't know whether randomly making defs and throwing them into the typeclass system is asking for trouble. Note that in LinearAlgebra.TensorProduct we have

-- porting note: This is added as a local instance for `SMul.aux`.
-- For some reason type-class inference in Lean 3 unfolded this definition.
def addMonoid : AddMonoid (M ⊗[R] N) :=
  { (addConGen (TensorProduct.Eqv R M N)).addMonoid with }

[Eric Wieser]

Probably that should have been reducible

[Kevin Buzzard]

That fixes the simple example

[Kevin Buzzard]

Rather annoyingly it doesn't fix the RingTheory.TensorProduct example (although mathlib compiles up to this point with the definition made reducible)

[Kevin Buzzard]

OK so maybe the reducible def is a red herring. This demonstrates the issue on master:

import Mathlib.RingTheory.TensorProduct

variable {R : Type} [CommSemiring R]

variable {A : Type} [Semiring A] [Algebra R A]

variable {B : Type} [Semiring B] [Algebra R B]

open TensorProduct -- for notation

example (x y z : A ⊗[R] B) : x * (y + z) = x * y + x * z := by
  simp only [mul_add] -- works fine
  done

-- stuff which comes up in the below trace
example : (AddZeroClass.toAdd : Add (A ⊗[R] B)) = (Distrib.toAdd : Add (A ⊗[R] B)) := rfl -- works fine

example : A ⊗[R] B = AddCon.Quotient (addConGen (TensorProduct.Eqv R A B)) := rfl -- works fine

example : (@HAdd.hAdd _ _ _ (@instHAdd _ (@AddZeroClass.toAdd _ (inferInstance))) : A → A → A)
  = ((· + ·) : A → A → A) := rfl -- works fine

example (x y z : A ⊗[R] B) : x *
    -- `(y + z)` but with `+` coming from `AddZeroClass` instead of via `Distrib`
    (@HAdd.hAdd _ _ _ (@instHAdd _ (@AddZeroClass.toAdd _ (inferInstance))) y z)
    = x * y + x * z := by
  -- Goal is `x * (y + z) = x * y + x * z`
  set_option trace.Meta.Tactic.simp true in
  set_option trace.Meta.isDefEq true in
  simp only [mul_add] -- does nothing
  change x *
    -- `(y + z)` but with `+` coming from `Distrib` (the default `+`)
    (@HAdd.hAdd _ _ _ (@instHAdd _ (@Distrib.toAdd _ (inferInstance))) y z)
    = x * y + x * z
  simp only [mul_add] -- now works
  done

The relevant trace is

...
[Meta.isDefEq] ❌ AddZeroClass.toAdd =?= Distrib.toAdd ▼
  [] ❌ AddZeroClass.toAdd =?= Distrib.toAdd ▼
    [] ❌ inferInstance.2 =?= NonUnitalNonAssocSemiring.toDistrib.2 ▼
      [] ❌ AddSemigroup.toAdd =?= AddSemigroup.toAdd ▼
        [] ❌ AddMonoid.toAddSemigroup.1 =?= AddMonoid.toAddSemigroup.1 ▼
          [] ❌ AddSemigroup.toAdd =?= { add := fun x x_1 ↦ x + x_1 } ▼
            [] ❌ (Function.Surjective.addSemigroup Quotient.mk'' (_ : Function.Surjective Quotient.mk'')
                    (_ :
                      ∀ (x x_1 : FreeAddMonoid (A × B)),
                        Quotient.mk'' (x + x_1) = Quotient.mk'' (x + x_1))).1 =?= { add := fun x x_1 ↦ x + x_1 } ▼
              [] ❌ { add := Add.add } =?= { add := fun x x_1 ↦ x + x_1 } ▼
                [] ❌ Add.add =?= fun x x_1 ↦ x + x_1 ▼
                  [] ❌ fun x x_1 ↦ x + x_1 =?= fun a ↦ Add.add a ▼
                    [] ❌ A ⊗[R] B =?= AddCon.Quotient (addConGen (TensorProduct.Eqv R A B)) ▼
                      [] ❌ TensorProduct =?= @AddCon.Quotient
                      [onFailure] ❌ A ⊗[R] B =?= AddCon.Quotient (addConGen (TensorProduct.Eqv R A B))
                      [onFailure] ❌ A ⊗[R] B =?= AddCon.Quotient (addConGen (TensorProduct.Eqv R A B))
                [onFailure] ❌ { add := Add.add } =?= { add := fun x x_1 ↦ x + x_1 }
                [onFailure] ❌ { add := Add.add } =?= { add := fun x x_1 ↦ x + x_1 }

[Meta.Tactic.simp.discharge] @mul_add, failed to assign instance
      Add (A ⊗[R] B)
    sythesized value
      Distrib.toAdd
    is not definitionally equal to
      AddZeroClass.toAdd

[Kevin Buzzard]

It looks to me like Meta.isDefEq is telling lies with [onFailure] ❌ A ⊗[R] B =?= AddCon.Quotient (addConGen (TensorProduct.Eqv R A B)). Any idea why?

def TensorProduct : Type _ :=
  (addConGen (TensorProduct.Eqv R M N)).Quotient

[Eric Wieser]

Is it irreducible somehow?

[Eric Wieser]

And can you get to a #mwe that fails to prove the equality of those types by rfl?

[Kevin Buzzard]

They're definitionally equal. The three examples near the top of the code are all rfl. I wouldn't know where to start answering your question (or, in some sense, what it means)

[Kevin Buzzard]

Does [onFailure] ❌ A ⊗[R] B =?= AddCon.Quotient (addConGen (TensorProduct.Eqv R A B)) indicate that Lean can get into a state where this is not proved by rfl?

[Eric Wieser]

I'm concerned there might be some unpleasant eta-and-quotients problem going on here

[Eric Wieser]

But maybe it just means "not proved by refl with reducible transparency"

[Eric Wieser]

Which is still a problem, because somehow we've ended up unfolded on the RHS but not the LHS and now lean says "oh, these aren't reducibly equal any more"

[Eric Wieser]

I think this is the failure:

import Mathlib.RingTheory.TensorProduct

variable {R : Type} [iR : CommSemiring R]
variable {A : Type} [iA : Semiring A] [iRA : Algebra R A]
variable {B : Type} [iB : Semiring B] [iRB : Algebra R B]

open TensorProduct -- for notation

example :
      @Distrib.toAdd
        (@TensorProduct R iR A B
          (@NonUnitalNonAssocSemiring.toAddCommMonoid A
            (@NonAssocSemiring.toNonUnitalNonAssocSemiring A (@Semiring.toNonAssocSemiring A iA)))
          (@NonUnitalNonAssocSemiring.toAddCommMonoid B
            (@NonAssocSemiring.toNonUnitalNonAssocSemiring B (@Semiring.toNonAssocSemiring B iB)))
          (@Algebra.toModule R A iR iA iRA) (@Algebra.toModule R B iR iB iRB))
        (@NonUnitalNonAssocSemiring.toDistrib
          (@TensorProduct R iR A B
            (@NonUnitalNonAssocSemiring.toAddCommMonoid A
              (@NonAssocSemiring.toNonUnitalNonAssocSemiring A (@Semiring.toNonAssocSemiring A iA)))
            (@NonUnitalNonAssocSemiring.toAddCommMonoid B
              (@NonAssocSemiring.toNonUnitalNonAssocSemiring B (@Semiring.toNonAssocSemiring B iB)))
            (@Algebra.toModule R A iR iA iRA) (@Algebra.toModule R B iR iB iRB))
          (@NonAssocSemiring.toNonUnitalNonAssocSemiring
            (@TensorProduct R iR A B
              (@NonUnitalNonAssocSemiring.toAddCommMonoid A
                (@NonAssocSemiring.toNonUnitalNonAssocSemiring A (@Semiring.toNonAssocSemiring A iA)))
              (@NonUnitalNonAssocSemiring.toAddCommMonoid B
                (@NonAssocSemiring.toNonUnitalNonAssocSemiring B (@Semiring.toNonAssocSemiring B iB)))
              (@Algebra.toModule R A iR iA iRA) (@Algebra.toModule R B iR iB iRB))
            (@Semiring.toNonAssocSemiring
              (@TensorProduct R iR A B
                (@NonUnitalNonAssocSemiring.toAddCommMonoid A
                  (@NonAssocSemiring.toNonUnitalNonAssocSemiring A (@Semiring.toNonAssocSemiring A iA)))
                (@NonUnitalNonAssocSemiring.toAddCommMonoid B
                  (@NonAssocSemiring.toNonUnitalNonAssocSemiring B (@Semiring.toNonAssocSemiring B iB)))
                (@Algebra.toModule R A iR iA iRA) (@Algebra.toModule R B iR iB iRB))
              (@Algebra.TensorProduct.instSemiringTensorProductToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiringToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiringToModuleToModule
                R iR A iA iRA B iB iRB))))
    =
      @AddZeroClass.toAdd
        (@TensorProduct R iR A B
          (@NonUnitalNonAssocSemiring.toAddCommMonoid A
            (@NonAssocSemiring.toNonUnitalNonAssocSemiring A (@Semiring.toNonAssocSemiring A iA)))
          (@NonUnitalNonAssocSemiring.toAddCommMonoid B
            (@NonAssocSemiring.toNonUnitalNonAssocSemiring B (@Semiring.toNonAssocSemiring B iB)))
          (@Algebra.toModule R A iR iA iRA) (@Algebra.toModule R B iR iB iRB))
        (@inferInstance
          (AddZeroClass
            (@TensorProduct R iR A B
              (@NonUnitalNonAssocSemiring.toAddCommMonoid A
                (@NonAssocSemiring.toNonUnitalNonAssocSemiring A (@Semiring.toNonAssocSemiring A iA)))
              (@NonUnitalNonAssocSemiring.toAddCommMonoid B
                (@NonAssocSemiring.toNonUnitalNonAssocSemiring B (@Semiring.toNonAssocSemiring B iB)))
              (@Algebra.toModule R A iR iA iRA) (@Algebra.toModule R B iR iB iRB)))
          (@TensorProduct.addZeroClass R iR A B
            (@NonUnitalNonAssocSemiring.toAddCommMonoid A
              (@NonAssocSemiring.toNonUnitalNonAssocSemiring A (@Semiring.toNonAssocSemiring A iA)))
            (@NonUnitalNonAssocSemiring.toAddCommMonoid B
              (@NonAssocSemiring.toNonUnitalNonAssocSemiring B (@Semiring.toNonAssocSemiring B iB)))
            (@Algebra.toModule R A iR iA iRA) (@Algebra.toModule R B iR iB iRB))) :=
          by
            with_reducible_and_instances
              rfl

[Eric Wieser]

replacing docs4#inferInstance with id fixes it!?

[Eric Wieser]

Also the name of docs4#Algebra.TensorProduct.instSemiringTensorProductToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiringToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiringToModuleToModule is outrageous

[Kevin Buzzard]

Maybe this is less painful to look at:

import Mathlib.RingTheory.TensorProduct

variable {R : Type} [CommSemiring R]

variable {A : Type} [Semiring A] [Algebra R A]

variable {B : Type} [Semiring B] [Algebra R B]

open TensorProduct -- for notation

example : (AddZeroClass.toAdd : Add (A ⊗[R] B)) = (Distrib.toAdd : Add (A ⊗[R] B)) := rfl

example : (AddZeroClass.toAdd : Add (A ⊗[R] B)) = (Distrib.toAdd : Add (A ⊗[R] B)) := by
            with_reducible_and_instances
              rfl -- fails

[Kevin Buzzard]

I hope you're laughing because this helps, as opposed to my having completely misunderstood something :-) I've never seen with_reducible_and_instances before (as you can probably guess from my earlier posts). Is this example a problem? Is it a "diamond" if different instances aren't definitionally equal at this level of reducibility?

[Eric Wieser]

I'm laughing because mine was outrageously long

[Eric Wieser]

Yours doesn't look like quite the same state as mine (mine is exactly what simp tried), but probably it makes sense to debug yours first

[Kevin Buzzard]

I'm surprised that mine isn't the same as yours, I've been looking at these terms for hours today and I thought that the Add point was was precisely where they were diverging and it was all typeclass inference after that.

[Kevin Buzzard]

Note that this is yet another example from the port where simp is failing but rwing the appropriate lemma saves the day.

[Kevin Buzzard]

(a) Are you expecting my example (or more generally our examples) to not fail and (b) could it be fixed by some simp! tactic which tries harder?

[Eric Wieser]

Maybe https://github.com/leanprover-community/mathlib4/compare/remove-weird-TensorProduct-instance will help?

[Eric Wieser]

I think the problem is not simp, but the rules for typeclass unification in the face of type wrappers

[Eric Wieser]

Maybe making TensorProduct reducible would solve the problem!

[Eric Wieser]

(after all, it is "just" the quotient of a FreeAddMonoid; it's not like we put any incompatible instances on it)

[Kevin Buzzard]

I tried making TensorProduct reducible and a simp call in the same file broke

[Eric Wieser]

That might be because of hacks that were added during porting

[Kevin Buzzard]

So you think that this is not a lean issue but a mathlib issue? In which case we could move to #mathlib4

[Kevin Buzzard]

Maybe typeclass unification in the face of type wrappers is still sufficiently leany

[Gabriel Ebner]

There's also the related (new?) gotcha that { add := fun (a b : A) => .. } and { add := fun (a b : id A) => .. } are no longer defeq instances.

[Kevin Buzzard]

So we should make id reducible? ;-)

[Gabriel Ebner]

I actually wanted to write ᵒᵖ, but that's been changed to a structure recently. But I think we have plenty of other def MyType := ...

[Eric Wieser]

Lex might be a reasonable example

[Eric Wieser]

Gabriel Ebner said:

There's also the related (new?) gotcha that { add := fun (a b : A) => .. } and { add := fun (a b : id A) => .. } are no longer defeq instances.

I think this is pretty much the same gotcha

[Kevin Buzzard]

Eric Wieser said:

That might be because of hacks that were added during porting

How do I see the diff between what mathlib3port thought and what Floris thought in !4#2539 ? After the squash merge has the relevant commit (the one generated by the script) vanished?

[Eric Wieser]

I'm sad we don't have a good answer to that

[Kevin Buzzard]

RingTheory.TensorProduct compiles on branch remove-weird-TensorProduct-instance BTW

[Eric Wieser]

Your best options are:

• open up the porting PR and look at the original commits there
• download the latest version from mathport, and pretend the hundreds of lines of warnings aren't there

[Eric Wieser]

The first option doesn't capture any additional hacks that were added in further porting PRs

[Kevin Buzzard]

example : (AddZeroClass.toAdd : Add (A ⊗[R] B)) = (Distrib.toAdd : Add (A ⊗[R] B)) := by
            with_reducible_and_instances
              rfl -- fails

still fails on remove-weird-TensorProduct-instance

[Eric Wieser]

Thanks for checking, I didn't bother doing a build locally, and of course was punished by having to wait for the entire build to get oleans

[Eric Wieser]

I'm not really surprised, but it was worth a try

[Eric Wieser]

I think diagnosing the failure that made us need that instance in the first place might help work out what's going on here

[Kevin Buzzard]

I tried making TensorProduct reducible but it's horrible:

synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
  AddCon.addMonoid (addConGen (Eqv R M N))
inferred
  AddCommMonoid.toAddMonoid

etc (200 errors)

[Kevin Buzzard]

(on your branch,

    nsmul_succ := by
      simp [Nat.succ_eq_one_add, TensorProduct.one_smul, TensorProduct.add_smul, add_comm]

fixes the first one, and then all hell breaks loose)

[Kevin Buzzard]

(Re the diff, I just downloaded the raw files after each relevant commit from GH and then compared locally)

[Kevin Buzzard]

So I'm now out of ideas and out of my depth with this one. Note that this works:

example : (AddZeroClass.toAdd : Add (R)) = (Distrib.toAdd : Add (R)) := by
            with_reducible_and_instances
              rfl -- works

I have no idea what this with_reducible_and_instances thing is about, or how to debug further.

[Kevin Buzzard]

OK, next example (found by Jeremy Tan in porting PR !4#4120):

import Mathlib.Topology.MetricSpace.Isometry

variable {PF : Type _} {PE : Type _} [MetricSpace PF] [MetricSpace PE]

example {f : PF → PE} (hi : Isometry f) (p : PF)  : dist (f p) (f p) = 37 := by
  simp only [hi.dist_eq] -- no change
  rw [hi.dist_eq] -- dist (f p) (f p) -> dist p p
  change dist p p = 37
  sorry

[Kevin Buzzard]

simp only [hi.dist_eq p p] doesn't work, simp only [(hi.dist_eq)] doesn't work

[Kevin Buzzard]

Solved: this one is fixed by changing {PF : Type _} to {PF : Type u}. OK so what the heck is going on there?

[Kevin Buzzard]

This is the second time today that a problem has been solved by changing Type _ to Type u. Is Type _ considered harmful?

[Kevin Buzzard]

(first time)

[Kevin Buzzard]

OK next one:

import Mathlib.CategoryTheory.Filtered

universe v

open CategoryTheory CategoryTheory.Category

namespace CategoryTheory.Limits

variable {J K : Type v} [SmallCategory J] [SmallCategory K]

variable (F : J × K ⥤ Type v)

variable [IsFiltered K]

variable [FinCategory J]

example (j : J) (k: J → K) (k' k'' : K) (g: (j : J) → k j ⟶ k') (kf: {j j' : J} → (j ⟶ j') → K)
    (gf: {j j' : J} → (f : j ⟶ j') → k' ⟶ kf f) (i: {j j' : J} → (f : j ⟶ j') → kf f ⟶ k'')
    (y: (j : J) → F.obj (j, k j)) :
    F.map ((𝟙 j, 𝟙 k'') : (j, k'') ⟶ (j, k''))
      (F.map ((𝟙 j, g j ≫ gf (𝟙 j) ≫ i (𝟙 j)) : (j, k j) ⟶ (j, _)) (y j)) =
    F.map ((𝟙 j, g j ≫ gf (𝟙 j) ≫ i (𝟙 j)) : (j, k j) ⟶ (j, _)) (y j) := by
  simp only [Bifunctor.map_id_comp] -- does nothing
  rw [Bifunctor.map_id_comp] -- does something
  rw [Bifunctor.map_id_comp] -- does something
  sorry

No Type _ in sight, the bracket trick doesn't fix it, it's unfortunately now my bedtime. This came from !4#3605 (now merged).

[Kevin Buzzard]

One might hope that this one is minimisable to something mathlib-free without too much trouble.

[Eric Wieser]

Kevin Buzzard said:

Is Type _ considered harmful?

I'd say yes. It's certainly far more harmful than it was in lean 3.

The lean 4

variable {A : Type _}

def something : that_uses A := sorry

is the same as the Lean 3

def something {A : Type _} : that_uses A := sorry

But not the same as using variable {A : Type _} in Lean 3

[Yaël Dillies]

Should we repurpose Type* to mean variable {A : Type*}?

[Eric Wieser]

I would like it to mean universe uA {A : Type uA}

[Yaël Dillies]

Yeah sorry that's I meant

[Ruben Van de Velde]

If Type _ is a footgun, wouldn't it be better to suggest changing it?

[Yaël Dillies]

You mean, in core Lean?

[Eric Wieser]

It's not so much that Type _ is a new footgun, but that variable is much better at aiming things towards your feet than it used to be

[Kevin Buzzard]

Oh docs4#CategoryTheory.Bifunctor.map_id_comp just doesn't work at all with simp; here's a much simpler example (just copying the definition of the declaration):

import Mathlib.CategoryTheory.Products.Basic

open CategoryTheory

universe v₁ v₂ v₃ u₁ u₂ u₃

variable {C : Type u₁} {D : Type u₂} {E : Type u₃}

variable [Category.{v₁} C] [Category.{v₂} D] [Category.{v₃} E]

@[simp]
theorem map_id_comp (F : C × D ⥤ E) (W : C) {X Y Z : D} (f : X ⟶ Y) (g : Y ⟶ Z) :
    F.map ((𝟙 W, f ≫ g) : (W, X) ⟶ (W, Z)) =
      F.map ((𝟙 W, f) : (W, X) ⟶ (W, Y)) ≫ F.map ((𝟙 W, g) : (W, Y) ⟶ (W, Z)) := by
  rw [← Functor.map_comp, prod_comp, Category.comp_id]

example (F : C × D ⥤ E) (W : C) {X Y Z : D} (f : X ⟶ Y) (g : Y ⟶ Z) :
    F.map ((𝟙 W, f ≫ g) : (W, X) ⟶ (W, Z)) =
      F.map ((𝟙 W, f) : (W, X) ⟶ (W, Y)) ≫ F.map ((𝟙 W, g) : (W, Y) ⟶ (W, Z)) := by
  simp -- does nothing
  simp only [map_id_comp] -- does nothing
  rw [map_id_comp] -- closes goal
  done

[Kevin Buzzard]

Now mathlib-free:

universe v₁ v₂ v u₁ u₂ u

class Category (V : Type u) where
  Hom : V → V → Type v
  id : ∀ X : V, Hom X X
  comp : ∀ {X Y Z : V}, (Hom X Y) → (Hom Y Z) → (Hom X Z)

infixr:10 " ⟶ " => Category.Hom -- \hom
notation "𝟙" => Category.id  -- \b1
infixr:80 " ≫ " => Category.comp -- \gg

variable {C : Type u₁} {D : Type u₂} [Category.{v₁} C] [Category.{v₂} D]

instance prod : Category.{max v₁ v₂} (C × D) where
  Hom X Y := (X.1 ⟶ Y.1) × (X.2 ⟶ Y.2)
  id X := ⟨𝟙 X.1, 𝟙 X.2⟩
  comp f g := (f.1 ≫ g.1, f.2 ≫ g.2)

variable [Category.{v₁} C] [Category.{v₂} D] [Category.{v₃} E]

structure Functor' (V : Type u₁) [Category.{v₁} V] (W : Type u₂) [Category.{v₂} W] where
  obj : V → W
  map : ∀ {X Y : V}, (X ⟶ Y) → (obj X ⟶ obj Y)

infixr:26 " ⥤ " => Functor' -- \func

@[simp]
theorem map_id_comp (F : C × D ⥤ E) (W : C) {X Y Z : D} (f : X ⟶ Y) (g : Y ⟶ Z) :
    F.map ((𝟙 W, f ≫ g) : (W, X) ⟶ (W, Z)) =
      F.map ((𝟙 W, f) : (W, X) ⟶ (W, Y)) ≫ F.map ((𝟙 W, g) : (W, Y) ⟶ (W, Z)) := by
  sorry

example (F : C × D ⥤ E) (W : C) {X Y Z : D} (f : X ⟶ Y) (g : Y ⟶ Z) :
    F.map ((𝟙 W, f ≫ g) : (W, X) ⟶ (W, Z)) =
      F.map ((𝟙 W, f) : (W, X) ⟶ (W, Y)) ≫ F.map ((𝟙 W, g) : (W, Y) ⟶ (W, Z)) := by
  simp -- does nothing
  simp only [map_id_comp] -- does nothing
  simp only [(map_id_comp)] -- does nothing
  simp only [map_id_comp F W f g] -- does nothing
  rw [map_id_comp] -- closes goal
  done

What's going on here?

[Kevin Buzzard]

So in summary, I'm baffled by: (1) the above example (mathlib-free), (2) this example (using mathlib) where changing Type _ to Type u makes simp magically work, and (3) the discussion about tensor products above, where I am unclear about whether that is something which needs to be fixed in mathlib and, if so, how to fix it. They're all examples from the port where simp [X] failed but rw [X] worked.

[Kevin Buzzard]

@Mario Carneiro any ideas? I've tried to summarise this thread in the above post.

[Mario Carneiro]

The MWE example fails because map_id_comp F W f g has the type

Functor'.map F (@Prod.mk ((W, X).fst ⟶ (W, Z).fst) ((W, X).snd ⟶ (W, Z).snd) (𝟙 W) (f ≫ g)) = ...

and the goal has type

Functor'.map F (@Prod.mk (W ⟶ W) (X ⟶ Z) (𝟙 W) (f ≫ g)) = ...

This works:

example (F : C × D ⥤ E) (W : C) {X Y Z : D} (f : X ⟶ Y) (g : Y ⟶ Z) :
    F.map ((𝟙 W, f ≫ g) : (W, X) ⟶ (W, Z)) =
      F.map ((𝟙 W, f) : (W, X) ⟶ (W, Y)) ≫ F.map ((𝟙 W, g) : (W, Y) ⟶ (W, Z)) := by
  have : F.map (X := (W, X)) (Y := (W, Z)) (@Prod.mk (W ⟶ W) (X ⟶ Z) (𝟙 W) (f ≫ g)) = _ :=
    map_id_comp F W f g
  simp only [this]

[Kevin Buzzard]

It worked in Lean 3. Do you understand why?

[Mario Carneiro]

My guess is that the (W, X).fst subterm is entered into the discrimination tree without being reduced, which means that it will not match W

[Mario Carneiro]

In this case you can fix the issue at the simp lemma

[Mario Carneiro]

this also works

@[simp]
theorem map_id_comp (F : C × D ⥤ E) (W : C) {X Y Z : D} (f : X ⟶ Y) (g : Y ⟶ Z) :
    F.map (X := (W, X)) (Y := (W, Z)) (@Prod.mk (W ⟶ W) (X ⟶ Z) (𝟙 W) (f ≫ g)) =
      F.map ((𝟙 W, f) : (W, X) ⟶ (W, Y)) ≫ F.map ((𝟙 W, g) : (W, Y) ⟶ (W, Z)) := by
  sorry

example (F : C × D ⥤ E) (W : C) {X Y Z : D} (f : X ⟶ Y) (g : Y ⟶ Z) :
    F.map ((𝟙 W, f ≫ g) : (W, X) ⟶ (W, Z)) =
      F.map ((𝟙 W, f) : (W, X) ⟶ (W, Y)) ≫ F.map ((𝟙 W, g) : (W, Y) ⟶ (W, Z)) := by
  simp only [map_id_comp]

[Mario Carneiro]

this is a bug, I think

[Kevin Buzzard]

Is there some way that an end user like me can see this forest of discrimination trees somehow?

[Mario Carneiro]

I'm using this for testing right now

open Lean Meta Elab Term
elab "discriminate" t:term : tactic => do
  let e ← elabTerm t none
  logInfo <| repr (← @DiscrTree.mkPath true e)

@[simp]
theorem map_id_comp (F : C × D ⥤ E) (W : C) {X Y Z : D} (f : X ⟶ Y) (g : Y ⟶ Z) :
    F.map ((𝟙 W, f ≫ g) : (W, X) ⟶ (W, Z)) =
      F.map ((𝟙 W, f) : (W, X) ⟶ (W, Y)) ≫ F.map ((𝟙 W, g) : (W, Y) ⟶ (W, Z)) := by
  discriminate Functor'.map F ((𝟙 W, f ≫ g) : (W, X) ⟶ (W, Z))
  discriminate F.map (X := (W, X)) (Y := (W, Z)) (@Prod.mk (W ⟶ W) (X ⟶ Z) (𝟙 W) (f ≫ g))

[Mario Carneiro]

Here's an even simpler version:

  discriminate (W, X).fst
  discriminate W

#[Lean.Meta.DiscrTree.Key.proj `Prod 0 0, Lean.Meta.DiscrTree.Key.const `Prod.mk 4,
  Lean.Meta.DiscrTree.Key.fvar (Lean.Name.mkNum `_uniq 32614) 0,
  Lean.Meta.DiscrTree.Key.fvar (Lean.Name.mkNum `_uniq 32616) 0,
  Lean.Meta.DiscrTree.Key.fvar (Lean.Name.mkNum `_uniq 32983) 0,
  Lean.Meta.DiscrTree.Key.fvar (Lean.Name.mkNum `_uniq 32984) 0]
#[Lean.Meta.DiscrTree.Key.fvar (Lean.Name.mkNum `_uniq 32983) 0]

[Mario Carneiro]

As I understand it this should be reduced

[Mario Carneiro]

so that they are the same

[Mario Carneiro]

It appears this is deliberate, this is the action of the simpleReduce := true flag in DiscrTree, which was added in response to a previous mathlib bug report

[Mario Carneiro]

basically without it you can't have simp lemmas like (W, X).fst = W because they look like W = W to simp

[Adam Topaz]

So do we just have to add a ton of little simp lemmas like (W,X).fst = W?

[Mario Carneiro]

I think this requires some more design work, because we can't just undo the previous bugfix, there is a tension here

[Mario Carneiro]

like, do you want that to be a simp lemma or not?

[Mario Carneiro]

should simp see through it or not?

[Mario Carneiro]

the example that is used in the DiscrTree docstring is

@[simp] theorem liftOn_mk (a : α) (f : α → γ) (h : ∀ a₁ a₂, r a₁ a₂ → f a₁ = f a₂) :
    Quot.liftOn (Quot.mk r a) f h = f a := rfl

(which is a real simp lemma in mathlib)

[Adam Topaz]

If we had a separate tactic that does all such reductions, the we wouldn’t need any additional silly simp lemmas, and for the category theory library we could just add that tactic to aesop_cat’s rules

[Adam Topaz]

In lean3 it was quite common to use dsimp only for such a purpose

[Mario Carneiro]

I think it might make sense to let simp apply lemmas up to reducible defeq as normal (meaning that liftOn_mk et al would loop and are not marked simp), and then when it is done to postprocess any remaining result by doing reducible defeq reductions (i.e. dsimp only)

[Mario Carneiro]

without that follow up step something like Quot.liftOn (Quot.mk r a) f h = sorry would be left unreduced because simp would look at it and see f a and hence have nothing to do

[Adam Topaz]

BTW I recently ran into an example where rw doesn’t work (without explicitly filling in some parameters) but simp only … does. It didn’t involve any binders, and rw really should have worked. It came up in !4#4113 . I didn’t think it was a big deal, but if it is, I could try to minimize the example.

[Adam Topaz]

Specifically it was the simp only [<- types_comp_apply] steps in that PR

[Mario Carneiro]

Hard to say, it doesn't sound familiar

[Adam Topaz]

I thought it might be related, because I suspected some differences in reduction strategies were to blame here as well.

[Adam Topaz]

But I didn’t really spend too much time investigating.

[Oliver Nash]

I'm quite surprised by a failure illustrated in Example 2 below. It has the characteristics that:

1. simp only [Pi.smul_apply] fails but both simp only [Pi.smul_apply _] and rw [Pi.smul_apply] work,
2. the failure is triggered by adding let statement to the context which does not change the goal.

Here are the examples:

import Mathlib.Data.Pi.Algebra
import Mathlib.Algebra.Algebra.Basic

-- Example 1: succeeds
example {α R : Type*} [CommRing R] (f : α → R) (r : R) (a : α) :
    (r • f) a = r • (f a) := by
  simp only [Pi.smul_apply] -- succeeds

-- Example 2: fails!
example {α R : Type*} [CommRing R] (f : α → R) (r : R) (a : α) :
    (r • f) a = r • (f a) := by
  let bar : SMul R R := SMulZeroClass.toSMul
  simp only [Pi.smul_apply] -- Fails!

[Oliver Nash]

Further experimentation reveals other things like:

-- Example 3: succeeds
example {α R : Type*} [CommRing R] (f : α → R) (r : R) (a : α) :
    (r • f) a = r • (f a) := by
  let foo : SMul R R := Algebra.toSMul
  simp only [Pi.smul_apply] -- succeeds

-- Example 4: succeeds
example {α R : Type*} [CommRing R] (f : α → R) (r : R) (a : α) :
    (r • f) a = r • (f a) := by
  let bar : SMul R R := SMulZeroClass.toSMul
  let foo : SMul R R := Algebra.toSMul
  simp only [Pi.smul_apply] -- succeeds

-- Example 5: succeeds
example {α R : Type*} [CommRing R] (f : α → R) (r : R) (a : α) :
    (r • f) a = r • (f a) := by
  let foo : SMul R R := Algebra.toSMul
  let bar : SMul R R := SMulZeroClass.toSMul
  have foobar : foo = bar := rfl
  simp only [foobar, Pi.smul_apply] -- succeeds

[Oliver Nash]

(This came up in the course of trying to understand why I had to write Pi.smul_apply _ instead of just Pi.smul_apply in #6666 )

[Matthew Ballard]

If you bump maxHeartbeats.synthInstance does Example 2 succeed?

[Oliver Nash]

Nope. I just tried adding: set_option synthInstance.maxHeartbeats 10000000 and the failure persists (everything is instant btw.)

[Matthew Ballard]

What does trace.Meta.synthInstance look like between the Example 1 and 2? (Sorry, I would look but am not at a computer.)

[Oliver Nash]

If I place set_option trace.Meta.synthInstance true at the top of the file and then place the cursor over the simp only lines, then for both Example 1 and Example 2 I see the same result, namely:

[Meta.synthInstance] ✅ α → SMul R R ▶

[Matthew Ballard]

I should asked for isDefEq! Here is the failure

[Meta.isDefEq] [0.000443s] ❌ fun i ↦ Algebra.toSMul =?= fun i ↦ bar ▼
  [] [0.000000s] ✅ α =?= α
  [] [0.000439s] ❌ Algebra.toSMul =?= bar ▼
    [] [0.000431s] ❌ Algebra.toSMul =?= SMulZeroClass.toSMul ▼
      [] [0.000366s] ❌ (Algebra.id R).1 =?= SMulWithZero.toSMulZeroClass.1 ▼
        [] [0.000293s] ❌ (Algebra.id R).1 =?= { smul := fun x x_1 ↦ x * x_1 } ▼
          [] [0.000000s] ✅ SMul R R =?= SMul R R
          [] [0.000258s] ❌ SMul.smul =?= fun x x_1 ↦ x * x_1 ▼
            [] [0.000252s] ❌ fun x x_1 ↦ x * x_1 =?= fun a ↦ SMul.smul a ▼
              [] [0.000000s] ✅ R =?= R
              [] [0.000249s] ❌ fun x ↦ x✝ * x =?= SMul.smul x✝ ▼
                [] [0.000234s] ❌ fun x ↦ x✝ * x =?= fun a ↦ SMul.smul x✝ a ▼
                  [] [0.000000s] ✅ R =?= R
                  [] [0.000230s] ❌ x✝¹ * x✝ =?= SMul.smul x✝¹ x✝ ▼
                    [] [0.000023s] ❌ @HMul.hMul =?= @SMul.smul
                    [onFailure] [0.000004s] ❌ x✝¹ * x✝ =?= SMul.smul x✝¹ x✝
                    [] [0.000110s] ❌ Mul.mul x✝¹ x✝ =?= SMul.smul x✝¹ x✝ ▼
                      [] [0.000012s] ❌ @Mul.mul =?= @SMul.smul
                      [onFailure] [0.000003s] ❌ Mul.mul x✝¹ x✝ =?= SMul.smul x✝¹ x✝
                      [onFailure] [0.000003s] ❌ Mul.mul x✝¹ x✝ =?= SMul.smul x✝¹ x✝
          [onFailure] [0.000006s] ❌ (Algebra.id R).1 =?= { smul := fun x x_1 ↦ x * x_1 }

vs

[Meta.isDefEq] [0.000002s] ✅ fun i ↦ Algebra.toSMul =?= fun i ↦ Algebra.toSMul

[Matthew Ballard]

Note that changing CommRing to Ring makes things succeed.

[Matthew Ballard]

Going through Algebra does seem to happen quite often with CommRing. Is this intended?

[Oliver Nash]

I don't know (and thanks for digging into this btw!).

[Oliver Nash]

I don't understand why adding something to the context using let can have such an (or indeed any) effect and I wonder should this be the case.

In fact my understanding here is all very shallow, what I really want to know is: can we make simp work in cases like this?

[Matthew Ballard]

This is odd. Replacing simp only with rw in Example 2 gives unification success

[Meta.isDefEq] [0.001067s] ✅ fun i ↦ Algebra.toSMul =?= fun i ↦ bar ▼
  [] [0.000000s] ✅ α =?= α
  [] [0.001064s] ✅ Algebra.toSMul =?= bar ▼
    [] [0.001052s] ✅ Algebra.toSMul =?= SMulZeroClass.toSMul ▼
      [] [0.000927s] ✅ (Algebra.id R).1 =?= SMulWithZero.toSMulZeroClass.1 ▼
        [] [0.000843s] ✅ { smul := fun c x ↦ ↑(RingHom.id R) c * x } =?= { smul := fun x x_1 ↦ x * x_1 } ▼
          [] [0.000824s] ✅ fun c x ↦ ↑(RingHom.id R) c * x =?= fun x x_1 ↦ x * x_1 ▶
          [] [0.000000s] ✅ R =?= R
          [] [0.000000s] ✅ R =?= R

[Oliver Nash]

That's right, I even highlighted this in my first post!

[Oliver Nash]

Even weirder (I think) is that simp only [Pi.smul_apply _] works whereas simp only [Pi.smul_apply] fails!

[Damiano Testa]

Oliver Nash said:

I don't understand why adding something to the context using let can have such an (or indeed any) effect and I wonder should this be the case.

In fact my understanding here is all very shallow, what I really want to know is: can we make simp work in cases like this?

I've seen this already and in the past it was that the let introduces some mdata in the target expression. I do not exactly know why, but I suspect that this is some of the issue.

[Damiano Testa]

Here is how you can see it:

open Lean Meta Elab Tactic in
-- Example 2: fails!
example {α R : Type*} [CommRing R] (f : α → R) (r : R) (a : α) :
    (r • f) a = r • (f a) := by
  run_tac do  -- app
    logInfo (← getMainTarget).ctorName
  let bar : SMul R R := SMulZeroClass.toSMul
  run_tac do  -- mdata
    logInfo (← getMainTarget).ctorName
  simp only [Pi.smul_apply] -- Fails!

[Damiano Testa]

So, the let binding changes the expression underlying your goal. .mdata is DefEq to the original thing, but there might be a missing consumeMData somewhere.

[Damiano Testa]

This is how the two expressions begin:

-- pre let: inspect '(r • f) a = r • f a'
'Eq' -- app
|-'_uniq.1612' -- fvar
|-'HSMul.hSMul' -- app
|   |-'_uniq.1612' -- fvar
|   |-('a._@.Mathlib.Tactic.LeanUtils.to_left_right._hyg.47') -- forallE

-- post let: inspect '(r • f) a = r • f a'
'[noImplicitLambda := true] (r • f) a = r • f a' -- mdata
|-'Eq' -- app
|   |-'_uniq.1612' -- fvar
|   |-'HSMul.hSMul' -- app
|   |   |-'_uniq.1612' -- fvar
|   |   |-('a._@.Mathlib.Tactic.LeanUtils.to_left_right._hyg.47') -- forallE

[Damiano Testa]

The extra mdata field is [noImplicitLambda := true], while (r • f) a = r • f a is the "initial" expression.

[Damiano Testa]

Matthew, maybe this is entirely unrelated, but I have seen you fight very successfully a great battle with the lets in instances. I wonder now if the mdata could be responsible for some of the issues...

[Damiano Testa]

As far as I know, mdata is a new feature of Lean 4 Expr: Lean 3 expr did not have an mdata field.

[Jon Eugster]

I haven't read most of the details in this topic, but this bug was also observed in the last nightly bump #6019 (see comment and the comment below that) where sometimes simp_rw wouldn't work without these extra _. (simp_rw is implemented as simp only-calls)

[Oliver Nash]

Interesting. I think having to add these extra underscores is very bad because it means the user cannot trust simp to find the relevant lemmas and now needs to learn API by hand.

[Oliver Nash]

Interesting. I think having to add these extra underscores is very bad because it means the user cannot trust simp to find the relevant lemmas and now needs to learn API by hand.

[Matthew Ballard]

Damiano Testa said:

Matthew, maybe this is entirely unrelated, but I have seen you fight very successfully a great battle with the lets in instances. I wonder now if the mdata could be responsible for some of the issues...

Good idea. Though most of the problems I’ve seen, that we thought were due to expanded let’s, were our old friend structure eta, there are still some slowdowns in AG I cannot place. I’ll keep an eye peeled

[Damiano Testa]

Anyway, there is something else at play, since even manually replacing the target expression with the cleared mdata, leaves simp unable to continue:

open Lean Meta Elab Tactic in
-- Example 2: fails!
example {α R : Type*} [CommRing R] (f : α → R) (r : R) (a : α) :
    (r • f) a = r • (f a) := by
  run_tac do  -- app
    logInfo (← getMainTarget).ctorName
  let bar : SMul R R := SMulZeroClass.toSMul
  run_tac do  -- before: mdata
              -- after: app
    let tgt := ← getMainTarget
    let mtgt := tgt.consumeMData
    logInfo m!"before: {tgt.ctorName}\nafter: {mtgt.ctorName}"
    let new := ← (← getMainGoal).replaceTargetDefEq mtgt
    setGoals [new]
  simp only [Pi.smul_apply] -- Fails!

[Matthew Ballard]

Also Ring would suffer similar to CommRing I imagine

[Damiano Testa]

By the way, any underscore seems to work:

example {α R : Type*} [CommRing R] (f : α → R) (r : R) (a : α) :
    (r • f) a = r • (f a) := by
  let bar : SMul R R := SMulZeroClass.toSMul
  simp only [Pi.smul_apply (I := _)] -- Success!

[Matthew Ballard]

Here is where things go off track: we are trying

(Algebra.id R).1 =?= SMulWithZero.toSMulZeroClass.1

which unfolds to

(Algebra.id R).1 =?= { smul := fun x x_1 ↦ x * x_1 }

and then to

SMul.smul =?= fun x x_1 ↦ x * x_1

when it fails and

{ smul := fun c x ↦ ↑(RingHom.id R) c * x } =?= { smul := fun x x_1 ↦ x * x_1 }

when it succeeds with rw

[Matthew Ballard]

That SMul.smul is @SMul.smul R R (Algebra.id R).1

[Matthew Ballard]

This works

example {α R : Type*} [CommRing R] (f : α → R) (r : R) (a : α) :
    (r • f) a = r • (f a) := by
  let foo := (Algebra.id R).toSMul
  let bar : SMul R R := SMulZeroClass.toSMul
  have : foo = bar := rfl
  simp only [Pi.smul_apply, this]

and this doesn't

example {α R : Type*} [CommRing R] (f : α → R) (r : R) (a : α) :
    (r • f) a = r • (f a) := by
  let foo := (Algebra.id R).toSMul
  let bar : SMul R R := SMulZeroClass.toSMul
  have : foo = bar := rfl
  simp only [Pi.smul_apply]

[Matthew Ballard]

In the rfl proof, we again unfold to

{ smul := fun c x ↦ ↑(RingHom.id R) c * x } =?= { smul := fun x x_1 ↦ x * x_1 }

[Matthew Ballard]

It will just never unfold @SMul.smul R R (Algebra.id R).1 inside the simp

[Oliver Nash]

I wish I had something that I could add; all I can say is that I'm very grateful that this is still receiving attention.

[Matthew Ballard]

With

simp only [Pi.smul_apply (I := _)]

it creates a metavariable for the pi instance of SMul instead of using bar and assigns it during unification

[Meta.isDefEq] (?b • ?x) ?i =?= (r • f) a

[Damiano Testa]

I am not really talking about anything that I know, but does this look like lean should be waiting a little longer for something to unify?

[Matthew Ballard]

Hmm. Actually it does the same thing (creates a metavariable and assigns it) when it fails but then looks again for a pi instance.

[Matthew Ballard]

It looks for the pi SMul instance when it succeeds but it fails to find it after a few attempts.

[Matthew Ballard]

And just carries on to completion

[Matthew Ballard]

These traces are not linear right?

[Kevin Buzzard]

What do you mean? The indentation is telling you the tree I guess.

[Matthew Ballard]

I get a bunch of separate nodes in the infoview window before expanding. Is this the order that Lean is doing things during its program flow?

[Kevin Buzzard]

I guess I was assuming that but I guess I can't be sure.

[Kevin Buzzard]

darn it, I minimised to make it mathlib free (this was easy thanks to https://github.com/kbuzzard/MweSkeletons) but then the problem goes away :-/

[Kevin Buzzard]

Oh I got it working on the tube home, will post in a bit

[Kevin Buzzard]

So here is a 500-line repro of the issue with no imports. I'm sure it can be cut down much further: I made it by cutting and pasting from other MWEs I've made over the last year or so.

[Eric Wieser]

I don't see it mentioned above, but simp only [(Pi.smul_apply)] works instead of simp only [Pi.smul_apply _]

[Eric Wieser]

This came up repeatedly during the port

[Eric Wieser]

The problem is that simp only [foo] actually means simp only [@foo], and if you actually want to use the expression foo as is, it needs to be (foo) to stop simp trying to be clever.

[Kevin Buzzard]

But does this explain the regression when you randomly add a term to the context?

[Eric Wieser]

No, it just explains why adding a seemingly obvious underscore makes a difference, because actually the change is that you added ~5 underscores, some of them as typeclass arguments

[Kevin Buzzard]

I'm working on minimising the repro BTW

[Kevin Buzzard]

universe u v w

section algebra_hierarchy_classes_to_comm_ring

class Zero (α : Type u) where
  zero : α

class One (α : Type u) where
  one : α

class Semiring (α : Type u) extends Add α, Mul α, Zero α, One α

class CommSemiring (R : Type u) extends Semiring R

class Ring (R : Type u) extends Semiring R

class CommRing (α : Type u) extends Ring α

end algebra_hierarchy_classes_to_comm_ring

section algebra_hierarchy_morphisms

class FunLike (F : Sort _) (α : outParam (Sort _)) (β : outParam <| α → Sort _) where
  coe : F → ∀ a : α, β a

instance (priority := 100) FunLike.insthasCoeToFun {F α : Sort _} {β : α → Sort _} [FunLike F α β] : CoeFun F fun _ ↦ ∀ a : α, β a where coe := FunLike.coe

structure ZeroHom (M : Type _) (N : Type _) [Zero M] [Zero N] where
  toFun : M → N

class ZeroHomClass (F : Type _) (M N : outParam (Type _)) [Zero M] [Zero N]
  extends FunLike F M fun _ => N where

structure OneHom (M : Type _) (N : Type _) [One M] [One N] where
  toFun : M → N

class OneHomClass (F : Type _) (M N : outParam (Type _)) [One M] [One N]
  extends FunLike F M fun _ => N where

structure AddHom (M : Type _) (N : Type _) [Add M] [Add N] where
  toFun : M → N

class AddHomClass (F : Type _) (M N : outParam (Type _)) [Add M] [Add N]
  extends FunLike F M fun _ => N where

structure MulHom (M : Type _) (N : Type _) [Mul M] [Mul N] where
  toFun : M → N

infixr:25 " →ₙ* " => MulHom

class MulHomClass (F : Type _) (M N : outParam (Type _)) [Mul M] [Mul N]
  extends FunLike F M fun _ => N where

structure AddMonoidHom (M : Type _) (N : Type _) [Add M] [Zero M] [Add N] [Zero N] extends
  ZeroHom M N, AddHom M N

infixr:25 " →+ " => AddMonoidHom

class AddMonoidHomClass (F : Type _) (M N : outParam (Type _)) [Add M] [Zero M] [Add N] [Zero N]
  extends AddHomClass F M N, ZeroHomClass F M N

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

infixr:25 " →* " => MonoidHom

class MonoidHomClass (F : Type _) (M N : outParam (Type _)) [Mul M] [One M] [Mul N] [One N]
  extends MulHomClass F M N, OneHomClass F M N

structure MonoidWithZeroHom (M : Type _) (N : Type _)
  [Mul M] [Zero M] [One M] [Mul N] [Zero N] [One N] extends ZeroHom M N, MonoidHom M N

infixr:25 " →*₀ " => MonoidWithZeroHom

structure NonUnitalRingHom (α β : Type _) [Add α] [Zero α] [Mul α]
  [Add β] [Zero β] [Mul β] extends α →ₙ* β, α →+ β

class MonoidWithZeroHomClass (F : Type _) (M N : outParam (Type _)) [Mul M] [Zero M] [One M]
  [Mul N] [Zero N] [One N] extends MonoidHomClass F M N, ZeroHomClass F M N

infixr:25 " →ₙ+* " => NonUnitalRingHom

structure RingHom (α : Type _) (β : Type _) [Semiring α] [Semiring β] extends
  α →* β, α →+ β, α →ₙ+* β, α →*₀ β

infixr:25 " →+* " => RingHom

class RingHomClass (F : Type _) (α β : outParam (Type _)) [Semiring α]
  [Semiring β] extends MonoidHomClass F α β, AddMonoidHomClass F α β,
  MonoidWithZeroHomClass F α β

instance instRingHomClass {R S : Type _} {_ : Semiring R} {_ : Semiring S} :
    RingHomClass (R →+* S) R S where
  coe f := f.toFun

-- this is needed to create the troublesome instance `Algebra.instid`
def RingHom.id (α : Type _) [Semiring α] : α →+* α := by
  refine' { toFun := _root_.id.. }

end algebra_hierarchy_morphisms

section HSMul_stuff

class HSMul (α : Type u) (β : Type v) (γ : outParam (Type w)) where
  hSMul : α → β → γ

class SMul (M : Type _) (α : Type _) where
  smul : M → α → α

infixr:73 " • " => HSMul.hSMul

instance instHSMul {α β : Type _} [SMul α β] : HSMul α β β where
  hSMul := SMul.smul

-- note that the function `SMulZeroClass.toSMul` is what disrupts `simp` later
class SMulZeroClass (M A : Type _) extends SMul M A where

class SMulWithZero (R M : Type _) extends SMulZeroClass R M where

instance MulZeroClass.toSMulWithZero (R : Type _) [Mul R] [Zero R] : SMulWithZero R R where
  smul := (· * ·)

end HSMul_stuff

section Algebra_stuff

class Algebra (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] extends SMul R A,
  R →+* A where

-- needed for troublesome `Algebra.instid`
def RingHom.toAlgebra' {R S} [CommSemiring R] [Semiring S] (i : R →+* S)
    : Algebra R S where
  smul c x := i c * x
  toRingHom := i

-- needed for troublesome `Algebra.instid`
def RingHom.toAlgebra {R S} [CommSemiring R] [CommSemiring S] (i : R →+* S) : Algebra R S :=
  i.toAlgebra'

-- comment this out and the failing `simp` works
instance Algebra.instid (R : Type _) [CommSemiring R] : Algebra R R :=
  (RingHom.id R).toAlgebra

end Algebra_stuff

namespace Pi_stuff

instance instSMul {I : Type v} {f : I → Type w} {M : Type u} [∀ i, SMul M <| f i] : SMul M (∀ i : I, f i) :=
  ⟨fun s x => fun i => s • x i⟩

end Pi_stuff

section oliver_example

theorem Pi.smul_apply {I : Type} {f : I → Type} {β : Type} [∀ i, SMul β (f i)] (x : ∀ i, f i) (b : β) (i : I) : (b • x) i = b • (x i) :=
  rfl

instance (R : Type) [CommRing R] : CommSemiring R where

example {R : Type} [CommRing R] : True :=
  let foo := (Algebra.instid R).toSMul
  let bar : SMul R R := SMulZeroClass.toSMul
  have : foo = bar := rfl -- they are defeq
  trivial

-- this proof works fine
example {α R : Type} [CommRing R] (f : α → R) (r : R) (a : α) :
    (r • f) a = r • (f a) := by
  simp only [Pi.smul_apply]

-- as does this one
example {α R : Type} [CommRing R] (f : α → R) (r : R) (a : α) :
    (r • f) a = r • (f a) := by
  simp only [Pi.smul_apply _]

-- the presence of `bar` messes up the first proof
-- set_option trace.Meta.isDefEq true in
example {α R : Type} [CommRing R] (f : α → R) (r : R) (a : α) :
    (r • f) a = r • (f a) := by
  let bar : SMul R R := SMulZeroClass.toSMul
--  have qux : Algebra.toSMul = bar := rfl
  fail_if_success simp only [Pi.smul_apply]
  sorry

-- but not the second
example {α R : Type} [CommRing R] (f : α → R) (r : R) (a : α) :
    (r • f) a = r • (f a) := by
  let bar : SMul R R := SMulZeroClass.toSMul
  simp only [Pi.smul_apply _]

-- The first proof is fixed again if we use `Ring` instead of `CommRing`.
example {α R : Type} [Ring R] (f : α → R) (r : R) (a : α) :
    (r • f) a = r • (f a) := by
  let bar : SMul R R := SMulZeroClass.toSMul
  simp only [Pi.smul_apply]

end oliver_example

(edit: removed all the monoids)

[Kevin Buzzard]

That's all I have time for today but hopefully it is enough to help someone who wants to get to the bottom of this random apparently incorrect defeq failure.

[Kevin Buzzard]

The trace of the failing defeq (obtained with set_option trace.Meta.isDefEq true) is here. If I've not made a mistake Algebra.toSMul and bar are defeq but the second cross in the list below is a failure.

[Meta.isDefEq] ❌ fun i ↦ Algebra.toSMul =?= fun i ↦ bar ▼
  [] ✅ α =?= α
  [] ❌ Algebra.toSMul =?= bar ▼
    [] ❌ Algebra.toSMul =?= SMulZeroClass.toSMul ▼
      [] ❌ (Algebra.instid R).1 =?= SMulWithZero.toSMulZeroClass.1 ▼
        [] ❌ (Algebra.instid R).1 =?= { smul := fun x x_1 ↦ x * x_1 } ▼
          [] ✅ SMul R R =?= SMul R R
          [] ❌ SMul.smul =?= fun x x_1 ↦ x * x_1 ▼
            [] ❌ fun x x_1 ↦ x * x_1 =?= fun a ↦ SMul.smul a ▼
              [] ✅ R =?= R
              [] ❌ fun x ↦ x✝ * x =?= SMul.smul x✝ ▼
                [] ❌ fun x ↦ x✝ * x =?= fun a ↦ SMul.smul x✝ a ▼
                  [] ✅ R =?= R
                  [] ❌ x✝¹ * x✝ =?= SMul.smul x✝¹ x✝ ▼
                    [] ❌ @HMul.hMul =?= @SMul.smul
                    [onFailure] ❌ x✝¹ * x✝ =?= SMul.smul x✝¹ x✝
                    [] ❌ Mul.mul x✝¹ x✝ =?= SMul.smul x✝¹ x✝ ▼
                      [] ❌ @Mul.mul =?= @SMul.smul
                      [onFailure] ❌ Mul.mul x✝¹ x✝ =?= SMul.smul x✝¹ x✝
                      [onFailure] ❌ Mul.mul x✝¹ x✝ =?= SMul.smul x✝¹ x✝
          [onFailure] ❌ (Algebra.instid R).1 =?= { smul := fun x x_1 ↦ x * x_1 }

[Matthew Ballard]

They are but it cannot figure that out because it refuses to unfold (Algebra.instid R).1 for some reason.

[Kevin Buzzard]

My understanding of the trace is that (Algebra.instid R).1 is being unfolded, and what is failing is x✝¹ * x✝ =?= SMul.smul x✝¹ x✝ for some reason. Lean seems to want to deduce this from @HMul.hMul =?= @SMul.smul which I don't think is true in the generality it asks?

[Kevin Buzzard]

This failure here

[] ❌ x✝¹ * x✝ =?= SMul.smul x✝¹ x✝

with pp.all on is @HMul.hMul R R R instHMul x✝¹ x✝ =?= @SMul.smul R R (Algebra.instid R).1 x✝¹ x✝ ... aah, maybe I see what you're getting at...

[Matthew Ballard]

The fact it flipped it to the other side is also part of the indication it doesn't want to unfold it

[Kevin Buzzard]

lean4#2461

[Patrick Massot]

Is the following a new example or more of the same?

example {α β : Type} {f : α × β → β → β} (h : ∀ p : α × β, f p p.2 = p.2)
  (a : α) (b : β) : f (a, b) b = b := by
  -- simp [h] -- fails
  rw [h] -- works

It seems especially simple. Fun fact: you can copy-paste this example into either Lean 3 or Lean 4 with no difference (except of course that simp will fail in Lean 4 and succeed in Lean 3).

[Matthew Ballard]

Can one change the transparency level unfolded for simp in some way? I didn't see it docs#Lean.Meta.Simp.Config

[Matthew Ballard]

Tracing is not giving a lot to work with

[Kevin Buzzard]

At least I don't have to spend 5 hours making it mathlib-free though :D This is a great example and I wonder how much other stuff it explains.

[Kevin Buzzard]

Note that the standard hacks simp [(h)] and simp [h _] don't fix the problem.

[Kevin Buzzard]

Even simp [h (a, b)] fails.

[Matthew Ballard]

Related

example {α β : Type} {f : α × β → β → β}
  (a : α) (b : β) (h : f (a,b) (a,b).2 = (a,b).2) : f (a, b) b = b := by
  -- simp [h] -- fails
  rw [h] -- works

[Matthew Ballard]

Also

example {α β : Type} {f : α × β → β → β}
  (a : α) (b : β) (h : f (a,b) (a,b).2 = b) : f (a, b) b = b := by
  -- simp [h] -- fails
  rw [h] -- works

[Matthew Ballard]

example {α β : Type} {f : α × β → β → β}
  (a : α) (b : β) (h : f (a,b) b = (a,b).2) : f (a, b) b = b := by
  simp [h] -- works!

[Damiano Testa]

Using Lean 3 and looking at the proof terms constructed with rw and simp, I guess that simp is using some auto-generated congr-lemmas, maybe? (Those lovely ᾰs make me suspect this.)

lemma As {α β : Type} {f : α × β → β → β} (h : ∀ p : α × β, f p p.2 = p.2)
  (a : α) (b : β) : f (a, b) b = b := by
  simp [h]

lemma Ar {α β : Type} {f : α × β → β → β} (h : ∀ p : α × β, f p p.2 = p.2)
  (a : α) (b : β) : f (a, b) b = b := by
  rw [h]

#print As
  /-
  theorem As : ∀ {α β : Type} {f : α × β → β → β},
    (∀ (p : α × β), f p p.snd = p.snd) → ∀ (a : α) (b : β), f (a, b) b = b :=
  λ {α β : Type} {f : α × β → β → β} (h : ∀ (p : α × β), f p p.snd = p.snd) (a : α) (b : β),
    (id_tag tactic.id_tag.simp
       (((λ (a a_1 : β) (e_1 : a = a_1) (ᾰ ᾰ_1 : β) (e_2 : ᾰ = ᾰ_1), congr (congr_arg eq e_1) e_2) (f (a, b) b)
           b
           (h (a, b))
           b
           b
           (eq.refl b)).trans
          (propext (eq_self_iff_true b)))).mpr
      trivial
  -/

#print Ar
/-
theorem Ar : ∀ {α β : Type} {f : α × β → β → β},
  (∀ (p : α × β), f p p.snd = p.snd) → ∀ (a : α) (b : β), f (a, b) b = b :=
λ {α β : Type} {f : α × β → β → β} (h : ∀ (p : α × β), f p p.snd = p.snd) (a : α) (b : β),
  (id_tag tactic.id_tag.rw (eq.rec (eq.refl (f (a, b) b = b)) (h (a, b)))).mpr (eq.refl (a, b).snd)
-/

[Matthew Ballard]

Speaking of terms

example {α β : Type} {f : α × β → β → β}
  (a : α) (b : β) (h : f (a,b) (a,b).2 = b) : f (a, b) b = b := h -- works

[Kyle Miller]

@Damiano Testa congr lemmas are how simp navigates expressions. The h (a, b) in the term is what it's doing to the LHS of the eq and the eq.refl b is what it's doing to the RHS. You can also read off that h (a, b) is for turning f (a, b) b into b.

[Damiano Testa]

Matthew Ballard said:

Speaking of terms

example {α β : Type} {f : α × β → β → β}
  (a : α) (b : β) (h : f (a,b) (a,b).2 = b) : f (a, b) b = b := h -- works

Automation is good, but the human touch is still out of reach...

[Matthew Ballard]

example {α β : Type} {f : β → β}
  (a : α) (b : β) (h : f (a,b).2 = b) : f b = b := by
  simp [h] -- fails

[Damiano Testa]

Matt, do you have an import for the working example in the last batch? I get a no progress error.

[Matthew Ballard]

No imports. Only the first should work but typos might very easily creep in

[Matthew Ballard]

I guess I did something else because I get the error copying it back in...

[Damiano Testa]

Ok, in your last batch, none of them work for me, not the first, nor the last, because of unit.

[Matthew Ballard]

Trimmed

[Matthew Ballard]

example {α β : Type} {f : β → β}
  (a : α) (b : β) (h : f (a,b).2 = b) : f (a,b).2 = b := by
  simp [h] -- goal is now f b = b and is not closed

[Damiano Testa]

You can also dispense with the two types:

example {α : Type} {f : α → α}
  (a b : α) (h : f (a,b).2 = b) : f b = b := by
  simp [h] -- fails

[Matthew Ballard]

How does simp reduce the extra simp args?

[Damiano Testa]

No progress above and here:

example {f : Prop → Prop}
  (a b : Prop) (h : f (a,b).2 = b) : f b = b := by
  simp [h] -- simp made no progress

[Matthew Ballard]

Unit?

[Damiano Testa]

example {f : Unit → Unit}
  (a b : Unit) (h : f (a,b).2 = b) : f b = b := by
  simp [h] -- works!

[Damiano Testa]

The proof term is back at eq_self:

theorem A : ∀ {f : Unit → Unit} (a b : Unit), f (a, b).snd = b → f b = b :=
fun {f} a b h ↦ of_eq_true (eq_self (f b))

[Matthew Ballard]

set_option trace.Debug.Meta.Tactic.simp is little more chatty. It says no theorems found for rewriting f (a,b) b

[Damiano Testa]

Turns out that also b is a red herring:

theorem A {f : Prop → Prop}
  (a : Prop) (h : f (a,a).2 = a) : f a = a := by
  simp [h] -- no progress

[Matthew Ballard]

Bool fails if you want a "small" type

[Eric Wieser]

Patrick Massot said:

Is the following a new example or more of the same?

I'm not sure I'd expect either simp or rw to work here; there's no syntactic match.

[Damiano Testa]

If you use simp_all this is what you get:

theorem B {f : Prop → Prop}
  (a : Prop) (h : f (a,a).1 = a) : f a = a := by
  simp_all [h] -- works
#print B
/-
theorem B : ∀ {f : Prop → Prop} (a : Prop), f (a, a).fst = a → f a = a :=
fun {f} a h ↦ of_eq_true (Eq.trans (congrFun (congrArg Eq (id (id h))) a) (eq_self a))
-/

[Matthew Ballard]

It doesn't seem to work on Patrick's original example. What does simp_all do?

[Damiano Testa]

Here is also an example, after Eric's comment:

example {f : Prop → Prop}
  (a : Prop) (h : f (id a) = a) : f a = a := by
  simp [h] -- no progress

In this case, also rw fails, though (and of course exact h does work).

[Damiano Testa]

I only know what simp_all says when you hover over it:

`simp_all` is a stronger version of `simp [*] at *`
where the hypotheses and target are simplified multiple times
until no simplication is applicable.
Only non-dependent propositional hypotheses are considered.

[Matthew Ballard]

Damiano Testa said:

Here is also an example, after Eric's comment:

example {f : Prop → Prop}
  (a : Prop) (h : f (id a) = a) : f a = a := by
  simp [h] -- no progress

In this case, also rw fails, though (and of course exact h does work).

This is a transparency issue. Using

@[reducible]
def myid {A : Type} (a : A) : A := a

works for all tactics

[Eric Wieser]

I'd argue this is a transparency feature, not an issue

[Eric Wieser]

If tactics randomly treat things as transparent then transparency controls become useless (which was pretty much the case in Lean 3)

[Matthew Ballard]

Ok. I meant "the failure is due to transparency settings". :wink:

[Patrick Massot]

I prefer a useful simp with useless transparency controls rather than a useless simp with "useful" transparency controls.

[Matthew Ballard]

But this gets back to my continuing confusion here and in lean4#2461. I thought that simp and rw shared the same default transparency setting (note do not read as transparency setting is .default). It is easy to see that in the rw config but I don't know where to look for simp. If they do share the same default, then I would expect some of these to succeed.

[Matthew Ballard]

I think transparency controls are good and this is something else. But I am just talking out my :peach: atm

[Oliver Nash]

I think we should make an effort to highlight just how much we care about the issue of simp not firing when we would like, to the Lean developers. I spoke with @Sebastian Ullrich in person at LFTCM last week and I mentioned https://github.com/leanprover/lean4/issues/2461 (I was very impressed that he knew exactly which issue I meant from the vague description I gave!) The impression I got was that we have not conveyed how big a deal simp not firing is for us.

I also note that we haven't really addressed Sebastian's question here and we probably should.

I'd like to say more but I have to run and cook dinner now!

[Patrick Massot]

I think the answer to this question is: no there is no such policy.

[Patrick Massot]

And I agree that this simp issue is really crucial. I'm porting the sphere eversion project and this issue is using 90% of my time.

[Matthew Ballard]

Assuming I didn't make a silly mistake

inductive MyProd (α β : Type) where
  | intro (a : α) (b : β) : MyProd α β

@[reducible]
def MyProd.snd {α β : Type} (p : MyProd α β) : β :=
  match p with
  | intro _ b => b

example {α β : Type} {f : β → β}
(a : α) (b : β) (h : f (MyProd.intro a b).snd = b) : f b = b := by
  simp [h] -- fails
  -- rw [h] -- works

[Patrick Massot]

What would be really really nice would be to have a tactic simp! that would work as the Lean 3 simp and a variant simp!? that would flag lemmas that required extra work, hopefully with advice about how to rewrite a better version.

[Mario Carneiro]

you know simp! already exists, right?

[Patrick Massot]

No, I don't.

[Patrick Massot]

But it doesn't help with my example, so it's something different.

[Patrick Massot]

And I can't learn what it does since it displays the docstring of simp and jump to definition jumps to simp.

[Mario Carneiro]

simp‼

[Mario Carneiro]

the docstring of simp should mention the ! option

[Mario Carneiro]

I think it did in lean 3

[Mario Carneiro]

I guess not

[Patrick Massot]

I want simp☢️ that tries really hard.

[Mario Carneiro]

there is a short note in the lean 3 changelog:

• Add iota_eqn : bool field to simp_config. simp {iota_eqn := tt} uses
  all non trivial equation lemmas generated by equation/pattern-matching compiler.
  A lemma is considered non trivial if it is not of the form forall x_1 ... x_n, f x_1 ... x_n = t and
  a proof by reflexivity. simp! is a shorthand for simp {iota_eqn := tt}.
  For example, given the goal ... |- [1,2].map nat.succ = t, simp! reduces the left-hand-side
  of the equation to [nat.succ 1, nat.succ 2]. In this example, simp! is equivalent to
  simp [list.map].

[James Gallicchio]

Patrick Massot said:

I want simp☢️ that tries really hard.

but which isn't aesop? :joy:

[Kevin Buzzard]

Does Aesop know and use all simp lemmas?

[James Gallicchio]

only thing is I'm not sure how good it is as a non-finishing tactic. I think Jannis is working on that?

[Eric Wieser]

Patrick Massot said:

I think the answer to this question is: no there is no such policy.

This is in answer to

Is there a mathlib policy about whether two instances should be defeq without unfolding standard defs?

right?

[Eric Wieser]

I think the answer is "yes, we almost have such a policy, there's a library note about putting @[reducible] on non-instance defs"

[Matthew Ballard]

Sounds like we should see if a reducible RingHom.toAlgebra will make our lives better. Nothing breaks quickly

[Eric Wieser]

I think we might still run into trouble because RingHom.id is not (and should not be) reducible

[Matthew Ballard]

I think it might reap some nice performance benefits even if it doesn't address the problems in this thread

[Eric Wieser]

I can confirm that making toAlgebra reducible doesn't help with the mwe