Dangerous instance vs elaboration problems

Stream: maths

[Heather Macbeth]

I think you could have asked this in #maths! :) @Yury G. Kudryashov @Sebastien Gouezel ?

[Frédéric Dupuis]

I guess it feels like a rookie mistake! :-)

[Floris van Doorn]

The problem is that when we search for normed_group α we then also have to search for has_inner ?? α. Normally this is a big problem, since if you don't know what you are searching for, type-class inference is likely to loop. But in the special case of has_inner this might be fine, if there will never be instances that can be applied indefinitely if 𝕜 is not known.

I'm not surprised that if you make [normed_group α] an argument you would then have to provide 𝕜 when rewriting a norm into a inner product: Lean doesn't know the inner product over which 𝕜 you need. Type-class inference will only fire once it knows the 𝕜. However, you can change the type of 𝕜 as (𝕜 : out_param Type*) in the definition of inner_product_space. Then you tell Lean to fire type-class inference for inner_product_space even if 𝕜 is not yet known. Can you test whether that solves your rewrite issues?

I recommend to make 𝕜 out_param and move [normed_group α] to an argument.
A second reason to move normed_group α as an argument is that α might have more structure, that implies that α is a normed group. (Maybe α can be a normed ring?) That will work more smoothly if [normed_group α] is an argument.

[Frédéric Dupuis]

Thanks! I'll give the out_param thing a shot and we'll see how it goes.

[Frédéric Dupuis]

It doesn't seem to do much... It turns out that telling it 𝕜 explicitly is often not enough, it even needs to be told α explicitly, I have no idea why. I even get really bizarre cases like:

lemma inner_self_eq_norm_square (x : α) : re ⟪x, x⟫ = ∥x∥ * ∥x∥ :=
by rw[norm_eq_sqrt_inner, ←sqrt_mul inner_self_nonneg (re ⟪x, x⟫),
  sqrt_mul_self inner_self_nonneg]

fails, whereas

lemma inner_self_eq_norm_square (x : α) : re ⟪x, x⟫ = ∥x∥ * ∥x∥ :=
by rw[@norm_eq_sqrt_inner _ _ _ _ _ _ _, ←sqrt_mul inner_self_nonneg (re ⟪x, x⟫),
  sqrt_mul_self inner_self_nonneg]

works. I thought these were equivalent!

[Yury G. Kudryashov]

complex is a normed space with two reasonable inner_product structures, real and complex. So, it shouldn't be an out_param

[Yury G. Kudryashov]

@Sebastien Gouezel you rewrote inner_product to its current state. How do you prefer to solve this problem? Take [normed_group] as an argument? Something else?

[Sebastien Gouezel]

I still don't know how the real_or_complex typeclass is supposed to make things: is it just a device to prove theorems in both situations, but then one would also state separately the real and the complex version (to get rid of the awkawadness that might show up in a statement trying to apply in both situations), or are we going to use just one class covering both situations uniformly?

In any case, for the definition of inner product spaces using is_real_or_complex, taking [normed_group alpha] as a parameter looks like the only reasonable option. There is also the question of has_inner, which currently is has_inner alpha, but could become has_inner k alpha if you want to have something uniform over reals or complexes, or has_real_inner alpha and has_complex_inner alpha if one wants to keep the final statements separate.

[Frédéric Dupuis]

So far it looks like just having one class covering both situations works well whenever the final statement doesn't explicitly involve re, im, conj, or I. When it does then it makes sense to also have a separate statement for the real case. Regarding has_inner, in that PR I've redefined it to be has_inner 𝕜 α.

[Sebastien Gouezel]

For instance, if you want to say that the (real) scalar product is linear with respect to the second variable, then you don't want to see re or im in the statement. The right design is not obvious to me in terms of typeclasses.

(A possibility would be to have two classes has_real_inner and has_complex_inner, and an analogue of to_additive that would create the real and the complex versions of a theorem given the general version with is_real_or_complex, but I am afraid this would be more work than just duplicating the theory over the reals and complexes).

I'd say: let's go for it, try to come up with something that is satisfactory, but if in the end it creates more difficulties than it solves we can keep in mind the option to come back to the stupid duplication with reals and complexes.

[Frédéric Dupuis]

I don't think having separate statements in the real case when it's needed is a major issue: so far in the proofs I've done, the real case (without the re and im) can be proven from the general is_R_or_C statement with a quick call to simp to clean it up. Right now it works very well except for the dangerous instance issue (i.e. if I leave in the dangerous instance it all works).

[Frédéric Dupuis]

If we could somehow have the same elaboration behavior but with [normed_group α] as an argument it would be perfect.

[Sebastien Gouezel]

This instance is indeed dangerous, as Lean can in general not guess what the field k is here. If the only fields that satisfy is_R_or_C k are reals and complexes, though, this would mean that the search would stop right away unless k is reals or complexes, so maybe it is not that dangerous. We would need advice of typeclass inference experts here to see if we can safely ignore the dangerous instance or not.

The situation is the following: Frédéric would like to define a class inner_product_space k alpha, having as (last) instance parameter is_R_or_C k and extending normed_group alpha. This is normally a bad instance because k is unknown, but we can promise that the only instances of is_R_or_C k are k = R and k = C, so hopefully the search should not get crazy: searching for normed_group alpha, Lean would only search for inner_product_space R alpha and inner_product_space C alpha, no blow-up. Is that what is going to happen, or are things more complicated?

[Scott Morrison]

I'm pretty sure this is safe.

If we really wanted to be careful we could add a new linter. For example we could create a @[sealed_class] attribute, mark is_R_or_C with that, and then require putting @[nolint sealed_class] on any instances that get creates. This would be a (perhaps unnecessarily cumbersome!) mechanism to prevent anyone adding further instances heedlessly.

[Frédéric Dupuis]

In this particular case the new linter is probably overkill -- just the name of the class should be enough to raise eyebrows if one puts in another instance!

[Sebastien Gouezel]

I agree there is no linter needed for this case. The conclusion of the discussion is that you don't need to change the definition of your class in #4507! You will need a nolint attribute on your class definition though (together with a docstring explaining why this is reasonable).

[Frédéric Dupuis]

Sounds good!