Commit 2023-03-24 21:41 46b633fd

refactor(analysis/inner_product_space/basic): do not extend normed_add_comm_group (#18583) This replaces [inner_product_space K V] with [normed_add_comm_group V] [inner_product_space K V]. Before this PR, we had inner_product_space K V extends normed_add_comm_group V. At first glance this is a rather strange arrangement; we certainly don't have module R V extends add_comm_group V. The argument usually goes that Derived A B extends Base B is unsafe, because the Derived.toBase instance has no way of knowing which A to look for. For inner_product_space K V we argued that this problem doesn't apply, as is_R_or_C K means that in practice there are only two possible values of K. This is indeed enough to stop typeclass search grinding to a halt. The motivation for the old design is described by @dupuisf on Zulip:

However, when I do (the contents of this PR), I run into some very annoying elaboration issues where I have to constantly spoonfeed it 𝕜 and/or α in lemmas that rewrite norms in terms of inner products, even though the relevant instance is directly present in the context. While it may ease elaboration issues, there are a number of new problems that inner_product_space K V extends normed_add_comm_group V causes:

1. It is confusing when compared to all other typeclasses. After being told to write

   variables [add_comm_group U] [module R U]
   variables [normed_add_comm_group V] [normed_space R V]
   

   it is natural to assume that the inner product space version would be

   variables [normed_add_comm_group W] [inner_product_space K W]
   

   But writing this leads to W having two unrelated addition operations!
2. It doesn't allow a space W to be an inner product space over both R and C. For a (normed) module, you can write

   variables [add_comm_group U] [module R U] [module C U]
   variables [normed_add_comm_group V] [normed_space R V] [normed_space C V]
   

   but writing [inner_product_space R W] [inner_product_space C W] again puts two unrelated + operators on V
3. It doesn't compose with other normed typeclasses. We can talk about a (normed) module with multiplication as

   variables [ring U] [module R U]
   variables [normed_ring V] [normed_space K V]
   

   but once again, typing [normed_ring W] [inner_product_space K W] gives us two unrelated + operators. This prevents us generalizing over real, complex, and quaternion. We could work around this by defining variants of inner_product_space for normed_ring A, normed_comm_ring A, normed_division_ring A, normed_field A, but this doesn't scale well. If we do things "the module way" then we only need one new typeclass instead of four,

   class inner_product_algebra (K A) [is_R_or_C K] [normed_ring A]
     extends normed_algebra K A, inner_product_space K A
   

4. The "is_R_or_C makes it OK" argument stops working if we generalize to quaternionic inner product spaces The majority of this PR is adding [normed_add_comm_group _] to every variables line about inner_product_space. The rest is specifying the scalar manually where previously unification would find it for us. This Zulip thread has some initial discussion about this change.