Dealing with different paths in type class inference

Stream: general

[Tomas Skrivan]

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]

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]

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]

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]

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]

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

[Reid Barton]

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]

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]

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]

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]

yes, you have to change the definition, or else introduce normed_space' that extends normed_space and locally_convex_space

[Mario Carneiro]

or live with the diamond and use convert as reid suggested

[Tomas Skrivan]

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]

You make normed_space extend locally_convex_space and normed_group, and the common fields are merged

[Mario Carneiro]

You have to use old_structure_cmd to make it work

[Tomas Skrivan]

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]

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

[Tomas Skrivan]

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]

yes, I was thinking about unary type classes

[Mario Carneiro]

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

[Tomas Skrivan]

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

[Mario Carneiro]

probably not

[Mario Carneiro]

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

[Mario Carneiro]

I count 5 instances of normed_space in mathlib, so not horrible

[Tomas Skrivan]

Ok, I will try it out.

[Yury G. Kudryashov]

Note that metric_space and normed_space don't use old_structure_cmd

[Yury G. Kudryashov]

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]

But @Mario Carneiro doesn't like mixins

[Mario Carneiro]

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

[Yury G. Kudryashov]

It seems that the only non-propositional data comes from semimodule. At least based on the textual description.

[Yury G. Kudryashov]

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

[Tomas Skrivan]

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]

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

[Kevin Buzzard]

"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]

You don't need normed_space to extend locally_convex_space if locally_convex_space is a Prop-valued mixin.

[Tomas Skrivan]

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]

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]

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

[Kevin Buzzard]

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]

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]

@Tomas Skrivan I think if you fill in the sorry, then the problem might go away.

[Johan Commelin]

Because then Lean can check that the two paths give the same add_comm_group (definitionally)

[Tomas Skrivan]

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]

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]

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]

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]

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]

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.