Zulip Chat Archive

Stream: Is there code for X?

Topic: Inner product space is metric space


view this post on Zulip Heather Macbeth (Dec 12 2020 at 20:22):

Is there a way for typeclass inference to find the metric space structure on an inner product space? It doesn't seem to be the case at the moment:

import analysis.normed_space.inner_product

variables (𝕜 : Type*) [is_R_or_C 𝕜]
variables (E : Type*) [inner_product_space 𝕜 E]

-- works
example : normed_space 𝕜 E := by apply_instance

-- fails
example : metric_space E := by apply_instance

-- works
example : metric_space E := (inner_product_space.to_normed_group 𝕜).to_metric_space

The situation is as follows: docs#inner_product_space has a to_normed_group field, docs#normed_group has a to_metric_space field.

view this post on Zulip Heather Macbeth (Dec 12 2020 at 20:31):

Actually,

example : normed_group E := by apply_instance

fails as well. I can't see why the normed_group structure can't be found but the normed_space structure can be.

view this post on Zulip Sebastien Gouezel (Dec 12 2020 at 20:45):

What happens if you include 𝕜? Otherwise, your inner product space instance is probably not included in your examples.

view this post on Zulip Heather Macbeth (Dec 12 2020 at 20:46):

Sebastien Gouezel said:

What happens if you include 𝕜?

This works, thank you!

view this post on Zulip Heather Macbeth (Dec 12 2020 at 20:46):

Sebastien Gouezel said:

Otherwise, your inner product space instance is probably not included in your examples.

Could you explain this a little more?

view this post on Zulip Sebastien Gouezel (Dec 12 2020 at 20:48):

When you have variables and instances in scope, Lean does not include all of them in lemmas. For instance, if you have two variables a and b, and the statement of a lemma only involves a, then Lean will not make the lemma have the b variable. For instances, it only includes all the instances for which all the variables are present in the statement.

view this post on Zulip Heather Macbeth (Dec 12 2020 at 20:50):

Sebastien Gouezel said:

For instances, it only includes all the instances for which all the variables are present in the statement.

I didn't know this, but it makes perfect sense. Thank you!


Last updated: May 16 2021 at 05:21 UTC