simp for ModelProd

Stream: mathlib4

[Mario Carneiro]

For Yuri's Q about ModelProd, perhaps no_index might help?

[Jireh Loreaux]

What is no_index?

[Eric Wieser]

It's an instruction to tell the discrimination tree used for lookup to not "index" the lookup on the term that noindex refers to

[Yury G. Kudryashov]

How do I use it? Can't find it in Mathlib 4

[Mario Carneiro]

def foo (x : A) : Nat := 0

@[simp] theorem foo_eq (x : A × B) : foo x = 0 := rfl

def ModelProd (A B : Type) := A × B

example : foo (x : ModelProd A B) = 0 := by simp -- fails

@[simp] theorem foo_eq' (x : no_index (A × B)) : foo x = 0 := rfl

example : foo (x : ModelProd A B) = 0 := by simp -- ok

[Yury G. Kudryashov]

The problem with this solution is that we have to go over all lemmas that we may want to apply with a type synonym.

[Yury G. Kudryashov]

E.g., vector bundles define a type synonym for docs#ContinuousLinearMap and lemmas like docs#ContinuousLinearMap.add_apply don't work on Bundle.ContinuousLinearMaps.

[Yury G. Kudryashov]

There are many basic lemmas that we may want to use for Bundle.ContinuousLinearMap, some of them are generated by @[simps] and adding no_index to all of them doesn't look like a good solution.