Zulip Chat Archive

Stream: new members

Topic: Dependency problem


view this post on Zulip Heather Macbeth (May 15 2020 at 19:26):

I made a new branch, modifying normed_space.basic (see discussions 1 2), which broke normed_space.operator_norm. I can't figure out why, and wondered if someone would mind diagnosing it for me.

view this post on Zulip Heather Macbeth (May 15 2020 at 19:26):

The first error is, "term f has type š•œ ā†’ā‚—[š•œ] E : Type (max u_1 u_2) but is expected to have type ?m_2 ā†’ā‚—[?m_1] ?m_3 : Type (max ? ?)".

view this post on Zulip Johan Commelin (May 15 2020 at 19:29):

That looks ugly )-; [The error, I mean]

view this post on Zulip Kevin Buzzard (May 15 2020 at 19:31):

  type mismatch at application
    @linear_map.mk_continuous.{?l_1 ?l_2 ?l_3} ?m_4 ?m_5 ?m_6 ?m_7 ?m_8 ?m_9 ?m_10 ?m_11 f
  term
    f
  has type
    @linear_map.{u_1 u_1 u_2} š•œ š•œ E
      (@normed_ring.to_ring.{u_1} š•œ (@normed_field.to_normed_ring.{u_1} š•œ _inst_4))
      (@normed_group.to_add_comm_group.{u_1} š•œ
         (@normed_ring.to_normed_group.{u_1} š•œ (@normed_field.to_normed_ring.{u_1} š•œ _inst_4)))
      (@normed_group.to_add_comm_group.{u_2} E _inst_1)
      (@field.to_vector_space.{u_1} š•œ (@normed_field.to_field.{u_1} š•œ _inst_4))
      (@normed_space.to_module.{u_1 u_2} š•œ E _inst_4 _inst_1 _inst_5) : Type (max u_1 u_2)
  but is expected to have type
    @linear_map.{?l_1 ?l_2 ?l_3} ?m_4 ?m_5 ?m_6
      (@normed_ring.to_ring.{?l_1} ?m_4 (@normed_field.to_normed_ring.{?l_1} ?m_4 ?m_7))
      (@normed_group.to_add_comm_group.{?l_2} ?m_5 ?m_8)
      (@normed_group.to_add_comm_group.{?l_3} ?m_6 ?m_9)
      (@normed_space.to_module.{?l_1 ?l_2} ?m_4 ?m_5 ?m_7 ?m_8 ?m_10)
      (@normed_space.to_module.{?l_1 ?l_3} ?m_4 ?m_6 ?m_7 ?m_9 ?m_11) : Type (max ?l_1 ?l_2)

Is it a diamond?

view this post on Zulip Johan Commelin (May 15 2020 at 19:31):

@Heather Macbeth (Btw, I think these questions could go in "general")
https://github.com/leanprover-community/mathlib/commit/0f96de153ffb79f9c3cb147f6c206e67cc09aa49#diff-fc5c89c1d4551a23597885d48b6ed4e5R705
this looks like an instance loop

view this post on Zulip Johan Commelin (May 15 2020 at 19:31):

It should probably be a def instead of an instance

view this post on Zulip Heather Macbeth (May 15 2020 at 19:33):

I'll try that! Of of_normed_module or to_normed_module, which should be the instance and which the def?

view this post on Zulip Johan Commelin (May 15 2020 at 19:34):

The one that makes your life easier when defining a new normed_space

view this post on Zulip Johan Commelin (May 15 2020 at 19:34):

So of_

view this post on Zulip Mario Carneiro (May 15 2020 at 19:35):

I think of_ should be the def

view this post on Zulip Mario Carneiro (May 15 2020 at 19:35):

I'm confused, are these two classes the same?

view this post on Zulip Johan Commelin (May 15 2020 at 19:36):

If at some point someone encounters a normed_module over a field, they will have to work a little bit to make it a normed_space. But the rest of the time, we want lemmas about normed_modules to automatically apply to normed_spaces.

view this post on Zulip Heather Macbeth (May 15 2020 at 19:36):

There is a typo in my documentation.

view this post on Zulip Mario Carneiro (May 15 2020 at 19:36):

or does this equivalence only hold under certain conditions

view this post on Zulip Heather Macbeth (May 15 2020 at 19:36):

It should read, "Over a normed field, āˆ„c ā€¢ xāˆ„ ā‰¤ āˆ„cāˆ„ āˆ„xāˆ„ automatically implies āˆ„c ā€¢ xāˆ„ = āˆ„cāˆ„ āˆ„xāˆ„"

view this post on Zulip Heather Macbeth (May 15 2020 at 19:36):

The equivalence holds when the ring is a field

view this post on Zulip Mario Carneiro (May 15 2020 at 19:37):

In general, if A -> B and C -> B -> A then B should be the parent and A -> B an instance

view this post on Zulip Johan Commelin (May 15 2020 at 19:37):

@Heather Macbeth We could also decide to do away with normed_module and just define normed_space over general rings, right?

view this post on Zulip Heather Macbeth (May 15 2020 at 19:37):

normed_module is brand new, I just made it.

view this post on Zulip Heather Macbeth (May 15 2020 at 19:38):

(Was going to open a discussion topic later.)

view this post on Zulip Johan Commelin (May 15 2020 at 19:38):

And then this:
Heather Macbeth said:

It should read, "Over a normed field, āˆ„c ā€¢ xāˆ„ ā‰¤ āˆ„cāˆ„ āˆ„xāˆ„ automatically implies āˆ„c ā€¢ xāˆ„ = āˆ„cāˆ„ āˆ„xāˆ„"

just becomes a lemma about normed spaces, if the base ring happens to be a field.

view this post on Zulip Johan Commelin (May 15 2020 at 19:38):

Heather Macbeth said:

normed_module is brand new, I just made it.

Sure, so I should have said: change the def or normed_space to work for general rings.

view this post on Zulip Heather Macbeth (May 15 2020 at 19:38):

I think normed_space means normed_vector_space

view this post on Zulip Johan Commelin (May 15 2020 at 19:39):

We decided to have both module and vector_space in mathlib, but it creates extra technical nuissance. The only reason we keep it is psychological/pedagogical.

view this post on Zulip Johan Commelin (May 15 2020 at 19:40):

You don't want a library without vector_space, but renaming module to vector_space also seems dishonest.

view this post on Zulip Heather Macbeth (May 15 2020 at 19:40):

I think consistency is good -- what is done in the general category should also be done in the normed category, etc.

view this post on Zulip Johan Commelin (May 15 2020 at 19:40):

But in the normed category, you won't have beginning users that don't know that modules and vector spaces are just the same thing.

view this post on Zulip Johan Commelin (May 15 2020 at 19:43):

Unifying the two concepts would allow you to get rid of this instance loops altogether. But keeping it for the sake of consistency isn't a big problem either. Upgrading a normed_module over a field to a normed_space is just a one-liner in a proof.

view this post on Zulip Heather Macbeth (May 15 2020 at 19:43):

I'm not sure it would be wise to go down the path of Banach modules, Hilbert modules, ...

view this post on Zulip Heather Macbeth (May 15 2020 at 19:43):

Sobolev modules

view this post on Zulip Heather Macbeth (May 15 2020 at 19:43):

The module of measures of bounded variation

view this post on Zulip Sebastien Gouezel (May 15 2020 at 19:59):

I think vector_space is just an abbreviation for module. We could have normed_module, and then normed_space as an abbreviation of normed_module.

view this post on Zulip Johan Commelin (May 15 2020 at 20:00):

But "just an abbreviation" is not good enough for type class inference.

view this post on Zulip Johan Commelin (May 15 2020 at 20:00):

I wish the pretty printer could do type class inference :oops: :head_bandage:

view this post on Zulip Heather Macbeth (May 15 2020 at 20:01):

Let me add that I made up these "normed modules" this morning because I had some instances in mind

view this post on Zulip Johan Commelin (May 15 2020 at 20:01):

Then everything would be a module, but print as vector_space if the pretty printer can infer that the base ring is a field.

view this post on Zulip Heather Macbeth (May 15 2020 at 20:01):

(I was going to start a thread discussing it, but here will do.)

view this post on Zulip Heather Macbeth (May 15 2020 at 20:02):

Notably: if E is a normed k-space then C(a, E) is a C(a, k)-module

view this post on Zulip Heather Macbeth (May 15 2020 at 20:04):

In that case, one has norm_smul_le rather than norm_smul, i.e., āˆ„c ā€¢ xāˆ„ ā‰¤ āˆ„cāˆ„ āˆ„xāˆ„ without equality

view this post on Zulip Heather Macbeth (May 15 2020 at 20:05):

So if normed_module becomes the basic object, it should still be with the norm_smul_le axiom rather than the norm_smul axiom, which is only equivalent over fields.

view this post on Zulip Johan Commelin (May 15 2020 at 20:07):

Sure. And norm_smul would be a lemma with the assumption [normed_field k]

view this post on Zulip Heather Macbeth (May 15 2020 at 20:32):

Hmm. Won't this break all the existing instances of normed spaces in the library? They are all constructed by checking the axiom norm_smul.

view this post on Zulip Johan Commelin (May 16 2020 at 04:15):

Yup, that's right. So all their constructions should be prepended with normed_space.mk' or some other name that provided a second constructor.
@Heather Macbeth You might be shocked if you read the defn of metric_space in mathlib. It hardcodes a metric + a topology + proof that they are compatible.
But of course nobody creates metric spaces like that, so there is a 2nd constructor that only asks for a metric.

view this post on Zulip Johan Commelin (May 16 2020 at 04:17):

The reason for this design is: in the case of the product metric/topology, you don't use the 2nd constructor, but fill in all fields by hand. And now the product metric induces a topology that is definitionally the product topology! :tada:

view this post on Zulip Yury G. Kudryashov (May 16 2020 at 08:44):

so there is a 2nd constructor that only asks for a metric.

AFAIR, metric_space is done by using := and . types, not by a second constructor.


Last updated: May 08 2021 at 05:14 UTC