Zulip Chat Archive

While porting CategoryTheory.Sites.Canonical !4#3936 I found that simp is no longer able to do rewrites inside the parameters of some functions, see https://github.com/leanprover-community/mathlib4/pull/3936/files#diff-05251fffaaa48e9800b7258562e693d46eb691664bd89a0ae32add964dad435fR89-R110
In the first of the similar simp problems which appear we have a goal bind U B (m ≫ l ≫ h ≫ f), we prove first this : bind U B ((m ≫ l ≫ h) ≫ f), and then simpa only [assoc] using this should close it, but it does not. I had to use convert or conv instead to make these proofs work. Does someone understand why simp does not work here?

Mauricio Collares (May 12 2023 at 13:09):

Kevin had the same problem in CategoryTheory.Sites.CoverLifting, so this is probably worth reporting upstream.

Yury G. Kudryashov (Jun 04 2023 at 04:37):

It seems that sometimes simp can't apply a lemma about FunLike.coe. See the first two failures of !4#4642. In both cases, Lean fails to apply lemmas like docs4#ContinuousLinearMap.coe_comp'

Yury G. Kudryashov (Jun 04 2023 at 04:37):

How do I debug this?

Yury G. Kudryashov (Jun 04 2023 at 04:39):

P.S.: I know how I can work around this.

Heather Macbeth (Jun 04 2023 at 04:43):

Is this the same issue as in ContDiff recently, where a simp featuring that lemma was replaced by a long list of rw?
https://github.com/leanprover-community/mathlib4/pull/4532/commits/b74605bca7b0498b800ecda2f5aa625d88d7cd37

Kevin Buzzard (Jun 04 2023 at 08:38):

There's a "simp [X] fails, rw [X] works" thread in #lean4 which contained I think three distinct reasons for simp failing to apply a lemma, none of which were fixed IIRC

Yury G. Kudryashov (Jun 05 2023 at 00:23):

One of these regressions is going to be really annoying in geometry/manifold

Yury G. Kudryashov (Jun 05 2023 at 00:24):

We have docs#model_prod and docs#model_pi

Yury G. Kudryashov (Jun 05 2023 at 00:24):

And simp no longer can apply lemmas about, e.g., docs#local_equiv.prod to model_prod

Yury G. Kudryashov (Jun 05 2023 at 00:25):

What should we do? Duplicate parts of the API for this type?

Yury G. Kudryashov (Jun 05 2023 at 00:26):

BTW, the example in https://leanprover-community.github.io/mathlib_docs/notes.html#Manifold%20type%20tags no longer applies in Lean 4.

Yury G. Kudryashov (Jun 05 2023 at 00:27):

However, univ ×ˢ univ = univ is still not a defeq.

Yury G. Kudryashov (Jun 05 2023 at 00:27):

So, we can't drop these type tags in Lean 4.

Yury G. Kudryashov (Jun 05 2023 at 00:30):

Can we have a command that goes over all lemmas about LocalEquiv.prod marked with mfld_simps and adds ModelProd versions?

Yury G. Kudryashov (Jun 05 2023 at 00:30):

Or should we drop mfld_simps tags from these lemmas and list them as arguments to this future command instead?

Yury G. Kudryashov (Jun 09 2023 at 19:06):

One more simp regression:

import Mathlib.GroupTheory.GroupAction.Defs

variable {M N α} [SMul M α] [SMul N α] [SMulCommClass M N α]

example (m : M) (n : N) (x : α) : m • n • x = n • m • x := by
  simp only [smul_comm m]