unbearable unhappiness of `simp` not working

Stream: general

[Scott Morrison]

If someone could help me diagnose the following issue, of simp failing to work, I would be very happy.

import algebra.category.CommRing.basic

example {R S : CommRing} (i : R ⟶ S) : i 0 = 0 :=
by simp -- succeeds, using `ring_hom.map_zero`

example {R S : Type} [comm_ring R] [comm_ring S] (i : R →+* S) (r : R) (h : r = 0) : i r = 0 :=
by simp [h] -- succeeds

-- I really want this to work!
example {R S : CommRing} (i : R ⟶ S) (r : R) (h : r = 0) : i r = 0 :=
by simp [h] -- fails, only uses `h`, leaves unsolved goal `⇑i 0 = 0`

example {R S : CommRing} (i : R ⟶ S) (r : R) (h : r = 0) : i r = 0 :=
begin
  simp [h],
  exact ring_hom.map_zero i, -- works, so this is a syntax level problem
end

example {R S : CommRing} (i : R ⟶ S) (r : R) (h : r = 0) : i r = 0 :=
begin
  simp [h],
  rw ring_hom.map_zero i, -- fails, couldn't find `⇑i 0` in the goal `⇑i 0 = 0`...
end

set_option pp.all true
example {R S : CommRing.{0}} (i : R ⟶ S) (r : R) (h : r = 0) : i r = 0 :=
begin
  simp [h],
  rw ring_hom.map_zero i, -- fails, error at https://gist.github.com/semorrison/61d25641003cdba43dda1f07246661bb
end

example {R S : CommRing.{0}} (i : R ⟶ S) (r : R) (h : r = 0) : i r = 0 :=
begin
  simp [h],
  erw ring_hom.map_zero i, -- succeeds, but is unbearably sad
end

[Gabriel Ebner]

So the issue is once again with having the wrong type class instances types. This doesn't work either:

example {R S : CommRing} (i : R ⟶ S) (r : R) (h : r = 0) : i r = 0 :=
begin
  simp only [h],
  simp only [ring_hom.map_zero],
end

[Gabriel Ebner]

This doesn't work either:

example {R S : CommRing.{0}} (i : R ⟶ S) : i (0 : R) = 0 :=
by simp

[Gabriel Ebner]

But this works:

example {R S : CommRing.{0}} (i : R ⟶ S) : i (0 : R.α) = 0 :=
by simp only [ring_hom.map_zero]

[Gabriel Ebner]

So the difference is between (0 : R) and (0 : R.α), for the simp lemma to apply they should be reducibly definitionally equal.

example {R : CommRing} : (0 : R.α) = (0 : R) :=
by tactic.reflexivity tactic.transparency.reducible -- we just need to make this work

[Gabriel Ebner]

Not sure if this is the right solution, but this makes all the simps work:

attribute [reducible]
  SemiRing.has_coe_to_sort
  Ring.has_coe_to_sort
  CommRing.has_coe_to_sort
  category_theory.induced_category.has_coe_to_sort
  category_theory.bundled.has_coe_to_sort

[Kevin Buzzard]

@Gabriel Ebner how do you do such efficient simp debugging? simp is one of those areas of Lean where for years I just figured it was magic and left it at that. But there have been some really interesting simp threads recently, and the linter and your paper with Floris and Rob have both given me a much better idea about what simp actually does (I had no idea what a confluent rewriting system was about a week ago). But these posts of yours above are still quite amazing. What tools are you using?

[Gabriel Ebner]

The posts in this thread are roughly the steps I took:

1. Original failing example was example {R S : CommRing} (i : R ⟶ S) (r : R) (h : r = 0) : i r = 0 := by simp [h]
2. If I manually replace r by 0 then it works. What happens if I let simp replace it for me ... := begin simp only [h], simp end.
3. Oh wow, now the goal is ⊢ i 0 = 0 but simp can't solve it!?! But simp could solve i 0 = 0 previously. Obviously there must be some difference between these two goals.
4. Let's do set_option pp.all true and use good old vimdiff. So the zeros are different???
5. Hypothesis validated! simp can solve i (0 : R.α) = 0 but not i (0 : R) = 0.
6. Let's check if (0 : R.α) = (0 : R) are reducibly equivalent (i.e., what simp requires for matching). example : (0 : R.α) = (0 : R) := by reflexivity transparency.reducible
7. Great, they're not! Let's do set_option trace.type_context.is_def_eq true and set_option trace.type_context.is_def_eq_detail true and see what it doesn't unfold. I searched for the last occurrence of "failed", and then marked the offending definitions as reducible.

[Scott Morrison]

Fantastic, thank you. I made it halfway through step 4. :-)

[Scott Morrison]

I observed that the zeroes were different, but also that the ring_hom arguments of coe_fn were different, and despaired of knowing which one to pursue. I suspect that actually the difference there is actually the same difference as the one in the zeroes that you identified.

[Scott Morrison]

I will investigate if that [reducible] attribute breaks things elsewhere.

[Scott Morrison]

:fingers_crossed:

[Kevin Buzzard]

This is great Gabriel -- many thanks for this extra info.

[Reid Barton]

Is it possible to argue that simp ought to behave as though instances are reducible by default? Instance search itself already does this as far as I can tell.

[Reid Barton]

I was quite confused by #2290 until I realized that the original issue was not with typeclass search but with simp.

[Gabriel Ebner]

I think there's some special hack in type_context for this. Let me look.

[Reid Barton]

If you could confirm my theory about instance search seeing instances as reducible (https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/instance.20matching/near/176678244) that would also be great

[Reid Barton]

Or perhaps that is what you are referring to.

[Yury G. Kudryashov]

Another example of simp not working: here rw succeeds while simp fails (it's in the algebra-bundled branch).

[Reid Barton]

Yes, I've seen cases of this as well but this one is probably simpler. Maybe it's worth trying to track down these issues now that it could potentially result in fixing them.

[Gabriel Ebner]

I think there are two things going on:

1. type-class resolution indeed has a special feature, unification is done using "instance" transparency. Instance transparency unfolds instances even if they're not reducible.
2. During unification of implicit and instance-implicit arguments, transparency is temporarily upgraded to semireducible: https://github.com/leanprover-community/lean/blob/9c57e4cd150cf036e6a8a8303a94f854f738994e/src/library/type_context.cpp#L2544-L2557

[Gabriel Ebner]

I'm not sure what this means for our example here. The R and R.α terms should only occur in implicit arguments, so they should actually unify even in simp.

[Gabriel Ebner]

Gabriel Ebner said:

The R and R.α terms should only occur in implicit arguments.

No they don't. Did you know that has_zero.zero has an explicit argument?

[Gabriel Ebner]

I'm not sure if this means we should change has_zero.zero and has_one.one.

[Reid Barton]

is the idea then that the "wrong" (syntactically) form of the type gets chosen when we encounter the type for the first type as an implicit argument (where we could have chosen to reduce the type, but we had no reason to yet) and then later we see the type as an explicit argument to something else and there we're not allowed to match it semireducibly?

[Reid Barton]

This might explain also why simp so often fails to apply things like category.comp_id

[Reid Barton]

because the object in question (which might be written in several definitionally equivalent ways, for example as an application of the identity functor) appears as an explicit argument of category.id but not as an explicit argument of anything else

[Reid Barton]

Of course this is especially insidious here where the notation 0 hides the explicit argument

[Gabriel Ebner]

This is the issue in this thread. When we first see 0, Lean assigns it the "wrong" type and later the simp lemmas don't apply because 0 has the type as an explicit argument.

[Reid Barton]

and in this case we got lucky because the type that appeared as an explicit argument was something that could be reduced after expanding the definition of an instance?

[Reid Barton]

whereas if the roles had been swapped, even marking the instance as reducible would not help, right?

[Gabriel Ebner]

The order of reduction shouldn't matter. Lean reduces both sides of the unification problem.

[Reid Barton]

Oh, I see, okay.

[Reid Barton]

But anyways simp's behavior vis-à-vis 2. above still seems "inconsistent". If it tried to solve the unification problems in a different order, it would succeed.

[Reid Barton]

This issue is a big pain in category theory and it's the reason why we have proofs like simp, dsimp, simp and arguably the reason why we have so many rfl-lemmas and maybe why simps even exists. It's nice to at least know why it happens now.

[Reid Barton]

It's particularly frustrating that simp won't notice that two types are definitionally equal in examples like this where if they weren't definitionally equal then the original expression wouldn't even type check!

[Gabriel Ebner]

I'm not sure if we were talking about the same thing. If you unify two function applications, then Lean first unifies the explicit arguments with reducible transparency, and then the implicit ones with semireducible transparency. (It could of course still be that this makes the "wrong" assigment to a metavariable which appears explicitly in another subterm.)

[Reid Barton]

Right, I'm talking about the situation where a metavariable will also appear later in an explicit argument of a subterm.

[Reid Barton]

If we could somehow defer the semireducible-transparency unification in the outer term until after the inner term, then both unifications would succeed

[Scott Morrison]

I think I just encountered another example of this.

import data.mv_polynomial

noncomputable theory

open finsupp mv_polynomial

variables {R : Type} [comm_ring R]
variable {S : Type}

/-- `pderivative v p` is the partial derivative of `p` with respect to `v` -/
def pderivative (v : S) (p : mv_polynomial S R) : mv_polynomial S R :=
p.sum (λ A B, monomial (A - single v 1) (B * (A v)))

lemma pderivative_monomial_single {a : R} {v : S} {n : ℕ} :
  pderivative v (monomial (single v n) a) = monomial (single v (n-1)) (a * n) :=
begin
  simp [pderivative],
  convert sum_single_index _,
  sorry, -- don't worry about this for now; this is an actual missing simp lemma.
  simp,
  { simp, /- failed to apply `zero_mul`! -/ rw [zero_mul], sorry },
end

[Kevin Buzzard]

When looking at this PR I noticed that some zeros were finsupp zeros and some were mv_polynomial zeros. This stopped zero_add from working at all at some point. Or are you convinced that this is unrelated? It might be (I need to work on my OWLS talk for the next few hours so don't want to investigate right now)

[Kevin Buzzard]

https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/strange.20rw.20behaviour.20with.20mv_polynomial/near/192269030

[Scott Morrison]

I suspect this is the same issue.

[Gabriel Ebner]

@Scott Morrison I think you've hit a completely different issue here. This works and applies zero_mul:

{ change _, simp, sorry },

[Scott Morrison]

what does that even mean? :-)

[Gabriel Ebner]

Try set_option trace.simplify true and behold the output:

[Gabriel Ebner]

[simplify] eq: ?m_2 ?m_3 0 = 0
[simplify] eq: ?m_1 ?m_2 0
...

[Gabriel Ebner]

I think simp is missing an instantiate_mvars here.

[Gabriel Ebner]

The change _ tactic is the quickest hack I could think of to instantiate the metavariables in the goal.

[Scott Morrison]

oh!

[Scott Morrison]

What do you mean when you say "I think simp is missing an instantiate_mvars here"?

[Gabriel Ebner]

We've had this problem with other tactics as well, but I can't remember the issue number. At some point simp does tgt ← target when it should actually do tgt ← target >>= instantiate_mvars.

[Scott Morrison]

Gabriel Ebner said:

I'm not sure if this means we should change has_zero.zero and has_one.one.

Did anyone (@Gabriel Ebner or @Reid Barton) investigate this? I have just been trying a little, but without much success. To make the type argument in has_zero and has_one implicit I used:

structure has_zero     (α : Type u) := (zero : α)
structure has_one      (α : Type u) := (one : α)
attribute [class] has_zero has_one

but it quickly led to woe. In various places in library/init/algebra/ring.lean, rw mul_zero fails to work at all. (You can still erw mul_zero, refl...)

[Gabriel Ebner]

With your definition, the typeclass argument is explicit, which is also not good.

[Gabriel Ebner]

This is how you make parameters implicit:

class has_zero (α : Type u) := mk {} :: (zero : α)

[Scott Morrison]

okay!

[Scott Morrison]

I will try that at some point too. For now I'm recompiling with t ← target >>= instantiate_mvars in simp_target.

[Scott Morrison]

Actually, @Gabriel Ebner, was the problem here that convert ought to have called instantiate_mvarsitself, before returning all the goals?

[Scott Morrison]

Maybe it's not simp's job to worry about this.

[Gabriel Ebner]

This is the latest PR I could find related to this issue: #1520 I think the general idea is that we want to fix both tactics.

[Scott Morrison]

Summary: for the issue with mul_zero in mv_polynomial.lean, changing simp to instantiate_mvars in target first worked great, but changing convert did not.

[Scott Morrison]

Do you think it's reasonable to PR t ← target >>= instantiate_mvars to core?

[Gabriel Ebner]

Yes, please PR it.