Zulip Chat Archive

Stream: new members

Topic: Dangerous instance vs elaboration problems


view this post on Zulip FrΓ©dΓ©ric Dupuis (Sep 19 2020 at 03:28):

In #4057 (which defines inner products based on is_R_or_C), the main outstanding issue is that the linter reports a dangerous instance in the definition:

class inner_product_space (π•œ : Type*) (Ξ± : Type*)
  [nondiscrete_normed_field π•œ] [normed_algebra ℝ π•œ] [is_R_or_C π•œ]
  extends normed_group Ξ±, normed_space π•œ Ξ±, has_inner π•œ Ξ± := sorry

which presumably comes from the fact that normed_group Ξ± doesn't have π•œ as a parameter. I gather that the usual way to fix this is to move normed_group Ξ± into the assumptions, as in

class inner_product_space (π•œ : Type*) (Ξ± : Type*)
  [nondiscrete_normed_field π•œ] [normed_algebra ℝ π•œ] [is_R_or_C π•œ]  [normed_group Ξ±]
  extends normed_space π•œ Ξ±, has_inner π•œ Ξ± := sorry

However, when I do that, 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.

So: just how dangerous is an instance like this? Would it still send the search algorithm into a wild goose chase, even though the only possibilities for π•œ should always remain only β„‚ and ℝ?

view this post on Zulip Heather Macbeth (Sep 19 2020 at 15:58):

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


Last updated: May 13 2021 at 06:15 UTC