Bug in `simps`

Stream: mathlib4

[Jakob von Raumer]

We've found this bug which seems to appear if a structure has a structure-typed field the name of which is a prefix of another field.

import Mathlib

structure MyStruct where
  foo : Bool
  bar_b : Bool
  bar : Fin 5

@[simps]  -- Error Failed to find constructor b in structure Fin.
def set_foo (s : MyStruct) (val : Bool) : MyStruct :=
  { s with foo := val }

Has anyone seen this before?

cc @Yury G. Kudryashov

[Edward van de Meent]

that's a very weird bug, i haven't seen that before... let me add to it that if you move the field bar_b after bar, the error seems to disappear? (on live lean at least)

[Jakob von Raumer]

It also disappears if I name it bar_2 instead, it seems super cursed

[Edward van de Meent]

(btw, your error is inconsistent with the name of your field)

[Edward van de Meent]

(i.e. it should be bar_baz or Failed to find constructor b in structure Fin.. It seems you (accidentally?) edited it)

[Edward van de Meent]

a first guess as to why this happens: @[simps] generates lemmas and names them [def_name]_[projection_name]_[projection_name], and this specific naming causes there to be a clash

[Jakob von Raumer]

Edward van de Meent said:

(i.e. it should be bar_baz or Failed to find constructor b in structure Fin.. It seems you (accidentally?) edited it)

Ah, yes sorry, minimized it some more afterwards

[Edward van de Meent]

and then this clash :sparkles:somehow:sparkles: causes this weird error rather than failing gracefully

[Edward van de Meent]

Jakob von Raumer said:

Edward van de Meent said:

(i.e. it should be bar_baz or Failed to find constructor b in structure Fin.. It seems you (accidentally?) edited it)

Ah, yes sorry, minimized it some more afterwards

tbh i think bar_baz illustrates the correspondence between the error and the code more clearly...

[Jovan Gerbscheid]

I guess that simps is doing some really cursed name handling

[Yury G. Kudryashov]

Also, if we use a non-structure instead of Fin 5, then it panics.

[Floris van Doorn]

This is indeed a bug in simps.

I think the main problems here are that:
(1) the naming scheme is ambiguous in edge cases, e.g.

import Mathlib

structure Foo where
  b : Bool

structure MyStruct where
  foo : Bool
  bar_b : Bool
  bar : Foo

@[simps bar_b] -- which projection do you want here?
def set_foo (s : MyStruct) (val : Bool) : MyStruct :=
  [...]

(2) The internal representation simps used for what projection you want is just a string, and it assumes that this is unambiguous.
(3) There is not enough logic to catch all errors, causing it to fail ungracefully.

The weird behavior with numbers was a workaround added in #15095 when people ran into a similar issue.

(2) + (3) can be fixed, and I can add some logic that simps tries to use the longest matching projection. E.g. when you want projection bar_b_baz, and both bar and bar_b are projections of your current structure, then it will only consider bar_b, not bar. I could even add a rule to the parser that bar__b_baz will consider projection bar only.

[Jovan Gerbscheid]

Surely it would be much easier if we used the syntax @[simps bar.b] (where bar.b is parsed as an ident)?

[Jakob von Raumer]

In our a case, another workaround would also be a simps simps argument which restricts the "depth" to 1