Zulip Chat Archive

Stream: mathlib4

Topic: New exotic simp failure

Patrick Massot (Sep 12 2023 at 14:27):

I have a new puzzle for simp debugging lovers. I tried to minimize but it's a very shy bug which very quickly disappear.

import Mathlib.Analysis.InnerProductSpace.Projection

lemma Prod.snd_mk {α β : Type*} (a : α) (b : β) : (a, b).2 = b := rfl

example {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (v : E) (t : ℝ) :
    orthogonalProjection (Submodule.span ℝ {(t, v).snd}) = 0 := by
  simp only [Prod.snd_mk] -- fails to make progress and to report it didn't make progress
  -- dsimp only [Prod.snd_mk] -- works
  sorry

Patrick Massot (Sep 12 2023 at 14:28):

The goal here is to get simp to transform (t, v).snd into v.

Eric Wieser (Sep 12 2023 at 16:54):

If you do it twice it doesn't make progress the second time

Eric Wieser (Sep 12 2023 at 16:56):

I think we're missing a congruence lemma for docs#orthogonalProjection, as it takes a dependently-typed argument

Eric Wieser (Sep 12 2023 at 16:56):

Or the auto-generated ones are broken

Damiano Testa (Sep 12 2023 at 19:45):

In 4 places of the expression, the following

|   |   |   |   |-'Prod.snd' -- app
|   |   |   |   |   |-'Real' '[]' -- const
|   |   |   |   |   |-'_uniq.2901' -- fvar
|   |   |   |   |   |-'Prod.mk' -- app
|   |   |   |   |   |   |-'Real' '[]' -- const
|   |   |   |   |   |   |-'_uniq.2901' -- fvar
|   |   |   |   |   |   |-'_uniq.2905' -- fvar
|   |   |   |   |   |   |-'_uniq.2904' -- fvar

was replaced by

|   |   |   |   |-'_uniq.2904' -- fvar

Damiano Testa (Sep 12 2023 at 19:47):

This is how the expression begins, until the first position where they differ

Damiano Testa (Sep 12 2023 at 19:47):

and this did not fit in the previous message

Patrick Massot (Sep 12 2023 at 20:06):

Interesting. So indeed simp does something, but no what we expected.

Kyle Miller (Sep 12 2023 at 20:06):

Here's a hint, the congruence lemma for orthogonalProjection needs to be a HEq

def orthogonalProjection.congr {𝕜 E : Type*} [IsROrC 𝕜] [NormedAddCommGroup E]
    [InnerProductSpace 𝕜 E] (K K' : Submodule 𝕜 E) (h : K = K') [HasOrthogonalProjection K] :
    haveI : HasOrthogonalProjection K' := by cases h; assumption
    HEq (orthogonalProjection K) (orthogonalProjection K') := by
  congr!

Kyle Miller (Sep 12 2023 at 20:07):

Rewriting K in orthogonalProjection K changes the type

Kyle Miller (Sep 12 2023 at 20:07):

dsimp can make progress because it's allowed to change K to something that's defeq

Damiano Testa (Sep 12 2023 at 20:07):

Upon better inspection, it seems that simp simplified the product inside the type of the left-hand side of the equality, but failed to enter the lhs and perform the substitution there.

Of the probably 22 places where the expression could change, simp seems to only "see" 4, all inside the type and none in the actual terms.

Damiano Testa (Sep 12 2023 at 20:11):

Here you can see the locations where the relevant mvar appears, the end of the implicit argument to Eq. and the beginning of the LHS.

image.png

Patrick Massot (Sep 12 2023 at 20:12):

Again this does not explain why the Lean 3 simplifier was happy to do its job and the Lean 4 simplifier isn't.

Damiano Testa (Sep 12 2023 at 20:12):

The diff highlights how the expression became, only the first 4 occurrences were rewritten.

Damiano Testa (Sep 12 2023 at 20:12):

No, this is just a text based description!

Damiano Testa (Sep 12 2023 at 20:12):

Sorry, it is bed-time! Have fun with this puzzle!

Kyle Miller (Sep 12 2023 at 20:13):

@Damiano Testa When simp comes across "fixed" variables it will usually dsimp them, but I'm not sure it will always do so.

Kyle Miller (Sep 12 2023 at 20:14):

(@Patrick Massot It doesn't help simp make progress, but I noticed that Prod.snd_mk is specialized to Type instead of Type*!)

Patrick Massot (Sep 12 2023 at 20:14):

Oops, that's a copy-paste mistake.

Patrick Massot (Sep 12 2023 at 20:15):

I'll fix it in my post above to avoid confusion.

Last updated: Dec 20 2023 at 11:08 UTC