Zulip Chat Archive

Stream: general

Topic: unbearable unhappiness of `simp` not working


view this post on Zulip Scott Morrison (Mar 30 2020 at 08:43):

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

view this post on Zulip Gabriel Ebner (Mar 30 2020 at 08:58):

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

view this post on Zulip Gabriel Ebner (Mar 30 2020 at 09:06):

This doesn't work either:

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

view this post on Zulip Gabriel Ebner (Mar 30 2020 at 09:21):

But this works:

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

view this post on Zulip Gabriel Ebner (Mar 30 2020 at 09:22):

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

view this post on Zulip Gabriel Ebner (Mar 30 2020 at 09:24):

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

view this post on Zulip Kevin Buzzard (Mar 30 2020 at 09:33):

@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?

view this post on Zulip Gabriel Ebner (Mar 30 2020 at 09:42):

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.

view this post on Zulip Scott Morrison (Mar 30 2020 at 09:53):

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

view this post on Zulip Scott Morrison (Mar 30 2020 at 09:54):

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.

view this post on Zulip Scott Morrison (Mar 30 2020 at 09:55):

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

view this post on Zulip Scott Morrison (Mar 30 2020 at 09:55):

:fingers_crossed:

view this post on Zulip Kevin Buzzard (Mar 30 2020 at 10:02):

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

view this post on Zulip Reid Barton (Mar 31 2020 at 17:59):

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.

view this post on Zulip Reid Barton (Mar 31 2020 at 18:01):

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

view this post on Zulip Gabriel Ebner (Mar 31 2020 at 18:01):

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

view this post on Zulip Reid Barton (Mar 31 2020 at 18:03):

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

view this post on Zulip Reid Barton (Mar 31 2020 at 18:03):

Or perhaps that is what you are referring to.

view this post on Zulip Yury G. Kudryashov (Mar 31 2020 at 18:04):

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

view this post on Zulip Reid Barton (Mar 31 2020 at 18:06):

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.

view this post on Zulip Gabriel Ebner (Mar 31 2020 at 18:13):

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

view this post on Zulip Gabriel Ebner (Mar 31 2020 at 18:14):

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.

view this post on Zulip Gabriel Ebner (Mar 31 2020 at 18:18):

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?

view this post on Zulip Gabriel Ebner (Mar 31 2020 at 18:19):

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

view this post on Zulip Reid Barton (Mar 31 2020 at 18:20):

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?

view this post on Zulip Reid Barton (Mar 31 2020 at 18:20):

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

view this post on Zulip Reid Barton (Mar 31 2020 at 18:21):

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

view this post on Zulip Reid Barton (Mar 31 2020 at 18:22):

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

view this post on Zulip Gabriel Ebner (Mar 31 2020 at 18:23):

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.

view this post on Zulip Reid Barton (Mar 31 2020 at 18:24):

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?

view this post on Zulip Reid Barton (Mar 31 2020 at 18:24):

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

view this post on Zulip Gabriel Ebner (Mar 31 2020 at 18:26):

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

view this post on Zulip Reid Barton (Mar 31 2020 at 18:26):

Oh, I see, okay.

view this post on Zulip Reid Barton (Mar 31 2020 at 18:33):

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.

view this post on Zulip Reid Barton (Mar 31 2020 at 18:35):

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.

view this post on Zulip Reid Barton (Mar 31 2020 at 18:41):

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!

view this post on Zulip Gabriel Ebner (Mar 31 2020 at 18:43):

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.)

view this post on Zulip Reid Barton (Mar 31 2020 at 18:47):

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

view this post on Zulip Reid Barton (Mar 31 2020 at 18:51):

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

view this post on Zulip Scott Morrison (Apr 01 2020 at 09:33):

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

view this post on Zulip Kevin Buzzard (Apr 01 2020 at 09:36):

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)

view this post on Zulip Kevin Buzzard (Apr 01 2020 at 09:36):

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

view this post on Zulip Scott Morrison (Apr 01 2020 at 09:39):

I suspect this is the same issue.

view this post on Zulip Gabriel Ebner (Apr 01 2020 at 09:44):

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

{ change _, simp, sorry },

view this post on Zulip Scott Morrison (Apr 01 2020 at 09:45):

what does that even mean? :-)

view this post on Zulip Gabriel Ebner (Apr 01 2020 at 09:45):

Try set_option trace.simplify true and behold the output:

view this post on Zulip Gabriel Ebner (Apr 01 2020 at 09:45):

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

view this post on Zulip Gabriel Ebner (Apr 01 2020 at 09:46):

I think simp is missing an instantiate_mvars here.

view this post on Zulip Gabriel Ebner (Apr 01 2020 at 09:46):

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

view this post on Zulip Scott Morrison (Apr 01 2020 at 09:49):

oh!

view this post on Zulip Scott Morrison (Apr 01 2020 at 09:51):

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

view this post on Zulip Gabriel Ebner (Apr 01 2020 at 09:54):

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.

view this post on Zulip Scott Morrison (Apr 01 2020 at 09:54):

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...)

view this post on Zulip Gabriel Ebner (Apr 01 2020 at 09:55):

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

view this post on Zulip Gabriel Ebner (Apr 01 2020 at 09:56):

This is how you make parameters implicit:

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

view this post on Zulip Scott Morrison (Apr 01 2020 at 10:00):

okay!

view this post on Zulip Scott Morrison (Apr 01 2020 at 10:00):

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

view this post on Zulip Scott Morrison (Apr 01 2020 at 10:06):

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

view this post on Zulip Scott Morrison (Apr 01 2020 at 10:06):

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

view this post on Zulip Gabriel Ebner (Apr 01 2020 at 10:10):

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.

view this post on Zulip Scott Morrison (Apr 01 2020 at 11:16):

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.

view this post on Zulip Scott Morrison (Apr 01 2020 at 12:04):

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

view this post on Zulip Gabriel Ebner (Apr 01 2020 at 12:08):

Yes, please PR it.


Last updated: May 14 2021 at 06:16 UTC