# Zulip Chat Archive

## Stream: general

### Topic: Dealing with different paths in type class inference

#### Tomas Skrivan (Oct 28 2020 at 16:51):

How do I deal with the problem when there are two ways to infer an instance of a type class, but I know that the instances are propositionally equal. I'm getting type mismatch error when applying a function that expects one way of inferring such a type class, but I provide the other way.

An example: normed spaces have products and have topology induced by the norm. To get topology on the product I can either infer topology from the product of normed spaces or take a product of topologies induced by individual norms.

#### Mario Carneiro (Oct 28 2020 at 16:53):

The standard solution in mathlib is to have `normed_space`

extend `topological_space`

, meaning that a normed space has the apparently redundant information of a norm and a topology, together with a (propositional) proof that they cohere

#### Reid Barton (Oct 28 2020 at 16:53):

I'm a bit surprised this is a problem for normed spaces because for *metric* spaces, we take specific measures to avoid exactly this problem

#### Mario Carneiro (Oct 28 2020 at 16:54):

Do you have a #mwe? A cursory look at `normed_space`

seems to indicate that it is set up in the recommended way

#### Reid Barton (Oct 28 2020 at 16:55):

But, when you find yourself in this situation, often `convert e`

instead of `refine e`

will be able to make progress, or `congr`

if you already have an equality where the sides differ only in a choice of instance

#### Tomas Skrivan (Oct 28 2020 at 16:55):

This was just an example and I'm running into a problem somewhere else.

#### Reid Barton (Oct 28 2020 at 16:55):

but of course this will only succeed in the end if you actually have a lemma that says the topologies (or whatever) are propositionally equal

#### Mario Carneiro (Oct 28 2020 at 16:58):

So when you make an instance of `normed_space`

for the product, you give the product topological space as the topology and the product norm for the norm, and then the coherence proof contains the content of the statement that the product of induced topologies is the topology induced by the product norm

#### Mario Carneiro (Oct 28 2020 at 17:01):

There are also constructors like docs#normed_group.of_core that can be used to skip the coherence proof by actually defining the topology as the one induced by the norm. This constructor should *not* be used if there is any other way of getting the topology because it will cause diamond problems

#### Tomas Skrivan (Oct 28 2020 at 17:01):

Actually, I'm defining `locally_convex_space`

just extends `vector_spaces`

and having a trouble coping with `normed_space`

. In particular, the locally convex structure on the product of normed spaces is the same as the product of locally convex spaces induced by normed spaces.

Probably the way to resolve this, would be to make `normed_space`

to extend `locally_convex_space`

, but I'm afraid touching mathlib.

#### Mario Carneiro (Oct 28 2020 at 17:04):

yes, you have to change the definition, or else introduce `normed_space'`

that extends `normed_space`

and `locally_convex_space`

#### Mario Carneiro (Oct 28 2020 at 17:06):

or live with the diamond and use `convert`

as reid suggested

#### Tomas Skrivan (Oct 28 2020 at 17:14):

I'm a bit confused how to make `normed_space`

extend `locally_convex_space`

without introducing another diamond. The `normed_space`

assumes that you already provide `normed_group`

on the base type. Therefore there would be two ways of getting topology, through the extension from `locally_convex_space`

and from the `normed_group`

.

#### Mario Carneiro (Oct 28 2020 at 17:17):

You make `normed_space`

extend `locally_convex_space`

and `normed_group`

, and the common fields are merged

#### Mario Carneiro (Oct 28 2020 at 17:17):

You have to use `old_structure_cmd`

to make it work

#### Tomas Skrivan (Oct 28 2020 at 17:20):

So i'm thinking that the definition of `locally_convex_space`

should be:

```
class locally_convex_space {a : Type} {b : Type} [normed_field a] [toplogical_group b] extends semimodule a b := ... zero has neighbourhood basis made of convex sets...
```

and then change the definition of `normed_space`

to

```
class normed_space (a : Type*) (b : Type*) [normed_field a] [normed_group b] extends locally_convex_space a b := ...
```

#### Mario Carneiro (Oct 28 2020 at 17:21):

oh, in that case I don't see a problem

#### Tomas Skrivan (Oct 28 2020 at 17:21):

Mario Carneiro said:

You make

`normed_space`

extend`locally_convex_space`

and`normed_group`

, and the common fields are merged

In mathlib `normed_space`

does not extends `normed_group`

it extends only `semimodule`

. Should I keep it that way?

#### Mario Carneiro (Oct 28 2020 at 17:22):

yes, I was thinking about unary type classes

#### Mario Carneiro (Oct 28 2020 at 17:22):

with the parameters as you have them I don't see where the diamond arises

#### Tomas Skrivan (Oct 28 2020 at 17:23):

Is the whole mathlib going to break if I introduce this changes?

#### Mario Carneiro (Oct 28 2020 at 17:23):

probably not

#### Mario Carneiro (Oct 28 2020 at 17:24):

it mostly comes up when introducing new instances, since these now have to prove that they have a locally convex structure

#### Mario Carneiro (Oct 28 2020 at 17:25):

I count 5 instances of `normed_space`

in mathlib, so not horrible

#### Tomas Skrivan (Oct 28 2020 at 17:26):

Ok, I will try it out.

#### Yury G. Kudryashov (Oct 28 2020 at 18:46):

Note that `metric_space`

and `normed_space`

don't use `old_structure_cmd`

#### Yury G. Kudryashov (Oct 28 2020 at 18:48):

And you won't have a diamond problem if `locally_convex_space`

will be a `Prop`

mixin taking `semimodule`

as an argument

#### Yury G. Kudryashov (Oct 28 2020 at 18:49):

But @Mario Carneiro doesn't like mixins

#### Mario Carneiro (Oct 28 2020 at 18:49):

I assumed from "local convex structure" that there is some non-propositional data

#### Yury G. Kudryashov (Oct 28 2020 at 18:54):

It seems that the only non-propositional data comes from `semimodule`

. At least based on the textual description.

#### Yury G. Kudryashov (Oct 28 2020 at 18:55):

I guess, something like `∀ U ∈ nhds (0:E), ∃ s ∈ nhds (0:E), convex s ∧ s ⊆ U`

.

#### Tomas Skrivan (Oct 28 2020 at 19:08):

Yury G. Kudryashov said:

I guess, something like

`∀ U ∈ nhds (0:E), ∃ s ∈ nhds (0:E), convex s ∧ s ⊆ U`

.

I will probably go this way. The problem is that convexity makes sense only for real or complex vector spaces, this prevents me from making `normed_space`

to extend `locally_convex_space`

.

#### Kevin Buzzard (Oct 28 2020 at 19:09):

https://www.springer.com/gp/book/9783540425335 :P

#### Kevin Buzzard (Oct 28 2020 at 19:10):

"The fourth more advanced chapter was added to give the reader a rather complete tour through all the important aspects of the theory of locally convex vector spaces over nonarchimedean fields. "

#### Yury G. Kudryashov (Oct 28 2020 at 19:15):

You don't need `normed_space`

to extend `locally_convex_space`

if `locally_convex_space`

is a `Prop`

-valued mixin.

#### Tomas Skrivan (Oct 28 2020 at 19:17):

Yury G. Kudryashov said:

You don't need

`normed_space`

to extend`locally_convex_space`

if`locally_convex_space`

is a`Prop`

-valued mixin.

Yes, I understand that now, which is great! But I have already started modifying matlib to do such an extension, but I will abandon that approach now.

#### Tomas Skrivan (Oct 28 2020 at 19:18):

Kevin Buzzard said:

"The fourth more advanced chapter was added to give the reader a rather complete tour through all the important aspects of the theory of locally convex vector spaces over nonarchimedean fields. "

Ohhh ok. I need to have a look at their definition of locally convex space then. The definition via seminorms probably still works, but I do not see how to define a convex set.

Also to keep `locally_convex_space`

as a `Prop`

I will only state an existence of a family of seminorms that generates the given topology.

#### Kevin Buzzard (Oct 28 2020 at 19:19):

Honestly I wouldn't worry about the nonarchimedean case right now :-)

#### Kevin Buzzard (Oct 28 2020 at 19:20):

but FWIW this is the definition in the nonarchimedean case too -- the p-adic numbers are a complete normed field and there is a theory of Banach spaces, locally convex spaces etc over this field (which is important in the p-adic Langlands program)

#### Tomas Skrivan (Nov 02 2020 at 19:04):

I'm running into these problems again, this time with `inner_product_space`

.

First, I need a product of `inner_product_spaces`

and there does not seems to be one defined, so I have defined it. (currently just with a `sorry`

, so that might be a problem)

Example of a problem with this is when deducing `add_comm_group`

of a product. I get two different paths:

1. product of two `inner_product_space`

-> `inner_product_space`

to `normed group`

-> `normed_group`

to `add_comm_group`

2. `inner_product_space`

to `normed group`

-> `normed_group`

to `add_comm_group`

-> product of two `add_comm_group`

The problem is all over the place, when deducing `topological_space`

`semimodule`

etc.

This leads to the question why is `inner_product_space`

not a `Prop`

? It is just a `normed_space`

that satisfy parallelogram law.

Going down the rabbit hole. Cannot we define `normed_group`

also as a `Prop`

? Maybe there is some sufficient and necessary condition on the metric to be induced by a norm.

#### Johan Commelin (Nov 02 2020 at 19:06):

@Tomas Skrivan I think if you fill in the `sorry`

, then the problem might go away.

#### Johan Commelin (Nov 02 2020 at 19:07):

Because then Lean can check that the two paths give the same `add_comm_group`

(definitionally)

#### Tomas Skrivan (Nov 03 2020 at 08:49):

Ok, I will try that, but I'm expecting there will be a problem with topology because if I have checked correctly, the product of normed space is given with sup norm but product of inner product spaces gives product with l2 norm. The resulting norm/metric is different but the topology is the same, but that is non-trivial theorem. Let's see if I get into trouble.

#### Johan Commelin (Nov 03 2020 at 09:16):

yup, that sounds like you might get some trouble at some point... but I don't know that part of the library well enough to know how much trouble

#### Sebastien Gouezel (Nov 03 2020 at 09:24):

You should be using a type synonym.

In the same way, the product of finitely many spaces is endowed with the sup norm, so to define the product of finitely many inner spaces, with the canonical inner product structure, we use `pi_Lp 2 one_le_two`

, which as a type is just the same as the product type, but as a normed space is registered with a different norm. That's why the instance `pi_Lp.inner_product_space`

in `inner_product.lean`

does not create a problem.

Note that the product of two spaces is *not* a special case of the product of finitely many spaces (an element of the first one has two components `x.fst`

and `x.snd`

, while an element of the second one is a function on a finite space)...

#### Eric Wieser (Mar 20 2023 at 13:50):

This leads to the question why is inner_product_space not a Prop? It is just a normed_space that satisfy parallelogram law.

There are a handful of lemmas in mathlib that say "this thing is true for `inner_product_space K V`

" which don't mention `K`

at all in the statement. In these places, a `is_inner_product_norm V`

typeclass would probably make sense (in addition to the current typeclass). This would be a nice follow-up to #18583, which now makes these "unused" `K`

arguments more obvious.

#### Jireh Loreaux (Mar 20 2023 at 14:30):

There's a characterization of inner product norms purely in terms of the norm: when it satisfies the parallelogram identity. So, I would call this class `parallelogram_norm`

. Then we can have the construction that creates an `inner_product_space`

from a normed space with this property.

#### Jireh Loreaux (Mar 20 2023 at 14:38):

In general, of course, you wouldn't want to use this construction because it goes through the polarization identity, so the definition would be gross.

Last updated: Aug 03 2023 at 10:10 UTC