Topological structures on numfields #205

mkerjean · 2020-05-15T23:12:44Z

This PR aims to get rid of the notation ^ o, by endowing any numFieldType with a canonical normedModType structure.

theories/normedtype.v

CohenCyril · 2020-05-26T17:59:43Z

I am not sure it is the problem, but I see one possible explanation: you are missing the closure under the join, e.g. solution to GRing.Ring.sort ?1 = GRing.LModule.sort ?2, must go through GRing.LAlgebra and GRing.Field.sort ?1 = GRing.LModule.sort ?2 must go through FieldExtension. So it seems to me that providing canonical structures only up to lmodType may cause unification failures and the fix is to state and make canonical that F is a (trivial) field extension over itself...

mkerjean · 2020-05-29T15:37:49Z

I am not sure it is the problem, but I see one possible explanation: you are missing the closure under the join, e.g. solution to GRing.Ring.sort ?1 = GRing.LModule.sort ?2, must go through GRing.LAlgebra and GRing.Field.sort ?1 = GRing.LModule.sort ?2 must go through FieldExtension. So it seems to me that providing canonical structures only up to lmodType may cause unification failures and the fix is to state and make canonical that F is a (trivial) field extension over itself...

Would that be a way to resolve the rift between NormedModule.lmodType and numfield_lmodType ? I'm puzzled about wether a new structure mimicking numFieldType but with a forgetful functor to lmodType is necessary.
Also where can I find FieldExtenstion ?

CohenCyril · 2020-05-29T21:34:54Z

I am not sure it is the problem, but I see one possible explanation: you are missing the closure under the join, e.g. solution to GRing.Ring.sort ?1 = GRing.LModule.sort ?2, must go through GRing.LAlgebra and GRing.Field.sort ?1 = GRing.LModule.sort ?2 must go through FieldExtension. So it seems to me that providing canonical structures only up to lmodType may cause unification failures and the fix is to state and make canonical that F is a (trivial) field extension over itself...

Would that be a way to resolve the rift between NormedModule.lmodType and numfield_lmodType ? I'm puzzled about wether a new structure mimicking numFieldType but with a forgetful functor to lmodType is necessary.

I do not think a new structure is necessary. But I could be wrong... but it's difficult to say until we check whether all the joins can be defined...

Also where can I find FieldExtenstion ?

https://github.com/math-comp/math-comp/blob/master/mathcomp/field/fieldext.v#L10

theories/normedtype.v

pi8027 · 2020-09-23T09:27:58Z

PR math-comp/math-comp#591 reimplements the solution to the issue of ambiguous paths (math-comp/math-comp#546) using primitive class records. I suggest using the new one to work on this PR. If there is a problem, please let me know.

pi8027 · 2020-12-09T21:35:26Z

@mkerjean Do you need any help? I would like to take a look at this PR after merging #275.

mkerjean · 2020-12-09T21:43:34Z

@mkerjean Do you need any help? I would like to take a look at this PR after merging #275.

Yes ! I think this PR begins to look better. I moved your previous definitions at the end of topology.v , as they are now needed by ereal.v.

I would be especially happy to have your opinion on these new definitions : should normedModType structures on rcfType, realType and others be defined this way ? Shoud we define them without a clone of the structure using _^o ?

mkerjean · 2020-12-09T21:48:03Z

@affeldt-aist The way I did it, taking ^o out of ereal.v as the unfortunate consequence that ereal_hausdorff needs to be explicitely used sometimes (here for example). Do you see why ?

affeldt-aist · 2020-12-10T02:10:08Z

@affeldt-aist The way I did it, taking ^o out of ereal.v as the unfortunate consequence that ereal_hausdorff needs to be explicitely used sometimes (here for example). Do you see why ?

It seems to be fixable by changing the Hint (I committed).

mkerjean · 2020-12-18T15:06:49Z

That woudl be great! I'm afraid that these definitions should be done directly one the hierarchy of topological structures.

I'm not sure if I understood what you say, but is it the same as the following one?:

I would be especially happy to have your opinion on these new definitions : should normedModType structures on rcfType, realType and others be defined this way ? Shoud we define them without a clone of the structure using _^o ?

OK, I actually did not answer this. I think we should define a regular instance for each topological structure (pointed, filtered, topological, normed modules, etc.), but not for each numeric field structure (rcfType, realType, etc.), and then define instances for non-forgetful inheritance based on them. These regular instances solve unification problems of the form Pointed.sort ?1 = regular ?2, Filtered.sort ?1 = regular ?2, and so on, and then force ?2 to be canonically a numFieldType. Since other numeric field structures are canonically numFieldType, we do not need regular instances for them. Also, if we define such regular instances, they will be redundant with ones for numFieldType.

Indeed, it was the same question. Thanks for your explanations. So we are ok for now, and wait for PR#275 to be merged to rebase.

Do you want to merge already the cleanup you did in your fork of the PR ?

No (I mean, not now). I'd like to wait for #275.

pi8027 · 2020-12-21T07:12:57Z

I'm working on a fix for this PR. I suggest not to touch this branch until further notice so that we do not duplicate our efforts.

pi8027 · 2020-12-22T13:27:47Z

I still have to fix canonical declarations, but I do not see any serious unfixable issues. Here is the inheritance diagram excluding countalg and finalg structures:

pi8027 · 2020-12-25T22:13:31Z

I made some progress. See: https://github.com/pi8027/analysis/tree/numfield_topology.

Here is the list of remaining issues I discovered:

Currently, the smallest ssralg/ssrnum structure that inherits from pointedType is numFieldType as in the above diagram, and the following R_pointedType (which improperly make numDomainType inheriting from pointedType) has been removed.

analysis/theories/topology.v

Line 3902 in 823ad8d

Canonical R_pointedType := PointedType R 0.

As a consequence of the removal, I had to put ^o back in the following two places:

analysis/theories/normedtype.v

Line 301 in e954498

pose D := [set d : R^o | d > 0 /\ ball x d `<=` ~` P].

analysis/theories/normedtype.v

Line 322 in e954498

pose D := [set d : R^o | d > 0 /\ forall y, ball x d y -> P y].

I'd like to hear @CohenCyril's opinion on whether we should make numDomainType inheriting from pointedType properly to fix this or not. I think that downsides to doing so are that,
1. normedZmodType has also to inherit from pointedType to avoid ambiguous join (if we simply add an edge from pointedType to numDomainType, pointedType and zmodType have two joins: numDomainType and pseudoMetricNormedZmodType),
2. then pseudoMetricNormedZmodType has also to inherit from pointedType by non-forgetful inheritance to avoid ambiguous coercion paths (I mean, in the definition of the pseudoMetricNormedZmodType, the pointedType mixin has to be removed from the class record and derived from the zmodType mixin instead), and
3. we have to be really careful not to introduce conversion issues of pointedType instances.
I had to patch the proof of cvg_norm but do not understand why. e954498#diff-ec3855f35a085739515162cb2620b5daea6488b737c11df25d618370adc5e240R2595-R2596
There is only one remaining explicit application of harmonic. I think this is unfixable.

analysis/theories/sequences.v

Line 693 in e954498

apply: (@squeeze _ _ (cst 0) _ (t^-1 *: (@harmonic R)) oo_filter); last 2 first.

mkerjean · 2021-01-04T09:53:57Z

I made some progress. See: https://github.com/pi8027/analysis/tree/numfield_topology.

Could you describe the changes you made to normedtype.v in this branch, in particular concerning the module nonforgetful_inheritance ? Is it mainly a reordering of the deleted canonical definitions, or are they new structures at stakes ?

pi8027 · 2021-01-04T11:01:49Z

I made some progress. See: https://github.com/pi8027/analysis/tree/numfield_topology.

Could you describe the changes you made to normedtype.v in this branch, in particular concerning the module nonforgetful_inheritance ? Is it mainly a reordering of the deleted canonical definitions, or are they new structures at stakes ?

@mkerjean Since Coq gives precedence to the oldest coercion path between two coercion classes, the coercion from realType (and other structures that inherit from numFieldType) to normedModType (and pseudoMetricNormedZmodType) has to be declared before one from numFieldType to normedModType. So I reordered them upside down (from realType to numFieldType ordering). A bunch of missing (non-trivial) joins have also been added, e.g., the join of numDomainType and normedModType should be numFieldType.

pi8027 · 2021-01-13T18:51:04Z

I will unlikely be able to make more progress until Feb 2. Also, I need feedback from Cyril to make more progress anyway. (No pressure intended.)

mkerjean · 2021-01-13T18:58:22Z

I will unlikely be able to make more progress until Feb 2. Also, I need feedback from Cyril to make more progress anyway. (No pressure intended.)

The status of this PR could be discussed in the next Analysis meeting. I am waiting for it to be merged to rebase the PRs related to Hahn Banach, Banach Steinhauss and holomorpy on it.

CohenCyril · 2021-01-14T00:02:02Z

Ah sorry, I've been kind of busy...
The problem is that forgetful inheritance from mathcomp analysis to mathcomp (core) is not possible in the current state of affairs, and altering mathcomp with anything that might lead to to blowup in Galois is risky, so I'm afraid we cannot do a proper inheritance between numDomainType and pointedType and we'll have to go to the non forgetful one, unless I missed something...

mkerjean · 2021-02-17T15:40:48Z

Did you had a chance to merge your fork of the PR @pi8027 ? Should this branch be merged with master afterwards @CohenCyril ? See the todos from the last meeting.

affeldt-aist · 2021-03-11T15:23:57Z

small questions about this PR:

should default.nix be changed? (l.49 mentions numfield_topology which is this very branch) @CohenCyril
in ereal.v, lee_fin, lte_fin, lee_tofin, lte_tofin should use %O or %R? @pi8027

affeldt-aist · 2021-03-11T15:40:51Z

I tried to reflect the changes in the changelog but I am not sure it is good enough. You may want to take a look at it.

affeldt-aist · 2021-03-12T04:22:02Z

@pi8027 maybe we should put a date to the diagram to avoid any confusion, or do you have a more recent one?

pi8027 · 2021-03-12T05:13:42Z

in ereal.v, lee_fin, lte_fin, lee_tofin, lte_tofin should use %O or %R? @pi8027

The LHS and RHS of lee_fin are inequations of extended reals and a numeric domain, and should use ereal_scope and ring_scope, respectively. However, the latter one should be order_scope if we generalize it to porderType.

@pi8027 maybe we should put a date to the diagram to avoid any confusion, or do you have a more recent one?

#205 (comment) is up to date.

pi8027 · 2021-03-12T05:23:16Z

In the case you need the dot file, here it is: hierarchy.dot.

affeldt-aist · 2021-03-18T08:20:23Z

The LHS and RHS of lee_fin are inequations of extended reals and a numeric domain, and should use ereal_scope and ring_scope, respectively. However, the latter one should be order_scope if we generalize it to porderType.

I propose to create an issue for that and to merge this PR now. What do you think? @CohenCyril @pi8027 @mkerjean

pi8027 · 2021-03-18T19:16:02Z

@affeldt-aist The module nonforgetful_inheritance has to be renamed to numFieldTopology according to the last meeting.

pi8027

Fine with me.

- Issue with harmonic Co-authored-by: Kazuhiko Sakaguchi <pi8027@gmail.com> Co-authored-by: Reynald Affeldt <reynald.affeldt@aist.go.jp>

- add inheritance diagram to readme

mkerjean marked this pull request as draft May 15, 2020 23:13

mkerjean force-pushed the numfield_topology branch from 3159f85 to 90cc8e8 Compare May 25, 2020 20:42

CohenCyril reviewed May 25, 2020

View reviewed changes

theories/normedtype.v Outdated Show resolved Hide resolved

mkerjean force-pushed the numfield_topology branch from 2c5886e to a5f6075 Compare July 7, 2020 21:28

pi8027 reviewed Jul 8, 2020

View reviewed changes

theories/normedtype.v Outdated Show resolved Hide resolved

theories/normedtype.v Outdated Show resolved Hide resolved

pi8027 reviewed Jul 8, 2020

View reviewed changes

theories/normedtype.v Outdated Show resolved Hide resolved

pi8027 mentioned this pull request Jul 8, 2020

Make [fieldExtType F of L] work for abstract instances math-comp/math-comp#545

Merged

pi8027 reviewed Jul 10, 2020

View reviewed changes

theories/normedtype.v Outdated Show resolved Hide resolved

pi8027 mentioned this pull request Jul 10, 2020

[DO NOT MERGE] Fix a coherence (ambiguous paths) issue of fieldExtType and a conversion issue of "regular" instances math-comp/math-comp#546

Closed

2 tasks

affeldt-aist mentioned this pull request Jul 20, 2020

Topological structures on numFields #188

Closed

affeldt-aist mentioned this pull request Sep 13, 2020

move contents out of normedtype.v #261

Closed

mkerjean force-pushed the numfield_topology branch from db2628f to 607dc6d Compare October 12, 2020 13:37

pi8027 mentioned this pull request Nov 10, 2020

Compatible with MathComp 1.12 #275

Merged

mkerjean force-pushed the numfield_topology branch 2 times, most recently from 02447a1 to 7679f31 Compare November 21, 2020 18:42

mkerjean force-pushed the numfield_topology branch 6 times, most recently from b603ca9 to b3a6737 Compare December 9, 2020 21:33

mkerjean marked this pull request as ready for review December 10, 2020 22:04

affeldt-aist mentioned this pull request Jan 15, 2021

wrongly located documentation #323

Closed

affeldt-aist force-pushed the numfield_topology branch from 9a74605 to 3d0f1bf Compare January 26, 2021 15:25

affeldt-aist mentioned this pull request Jan 27, 2021

Endow R^o, C^o (which are copies of R, C) with structures #156

Open

affeldt-aist force-pushed the numfield_topology branch from 3d0f1bf to c9cd6ac Compare March 11, 2021 15:20

affeldt-aist force-pushed the numfield_topology branch from 117615d to 36d9d18 Compare March 12, 2021 04:20

pi8027 approved these changes Mar 19, 2021

View reviewed changes

mkerjean and others added 4 commits March 19, 2021 09:46

normedType on numFieldType

0f83012

- Issue with harmonic Co-authored-by: Kazuhiko Sakaguchi <pi8027@gmail.com> Co-authored-by: Reynald Affeldt <reynald.affeldt@aist.go.jp>

module for canonical topological structure on regular

52cd42e

Fix non-forgetful inheritance

6a7cc18

changelog, meta

b60e93d

- add inheritance diagram to readme

affeldt-aist force-pushed the numfield_topology branch from 49b699a to b60e93d Compare March 19, 2021 00:47

affeldt-aist merged commit 23583e7 into master Mar 19, 2021

affeldt-aist deleted the numfield_topology branch March 23, 2021 03:15

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Topological structures on numfields #205

Topological structures on numfields #205

mkerjean commented May 15, 2020

CohenCyril commented May 26, 2020

mkerjean commented May 29, 2020 •

edited

Loading

CohenCyril commented May 29, 2020

pi8027 commented Sep 23, 2020

pi8027 commented Dec 9, 2020

mkerjean commented Dec 9, 2020

mkerjean commented Dec 9, 2020

affeldt-aist commented Dec 10, 2020 •

edited

Loading

mkerjean commented Dec 18, 2020 •

edited

Loading

pi8027 commented Dec 21, 2020

pi8027 commented Dec 22, 2020 •

edited

Loading

pi8027 commented Dec 25, 2020 •

edited

Loading

mkerjean commented Jan 4, 2021

pi8027 commented Jan 4, 2021

pi8027 commented Jan 13, 2021

mkerjean commented Jan 13, 2021

CohenCyril commented Jan 14, 2021

mkerjean commented Feb 17, 2021

affeldt-aist commented Mar 11, 2021

affeldt-aist commented Mar 11, 2021

affeldt-aist commented Mar 12, 2021

pi8027 commented Mar 12, 2021

pi8027 commented Mar 12, 2021

affeldt-aist commented Mar 18, 2021

pi8027 commented Mar 18, 2021

pi8027 left a comment

Topological structures on numfields #205

Topological structures on numfields #205

Conversation

mkerjean commented May 15, 2020

CohenCyril commented May 26, 2020

mkerjean commented May 29, 2020 • edited Loading

CohenCyril commented May 29, 2020

pi8027 commented Sep 23, 2020

pi8027 commented Dec 9, 2020

mkerjean commented Dec 9, 2020

mkerjean commented Dec 9, 2020

affeldt-aist commented Dec 10, 2020 • edited Loading

mkerjean commented Dec 18, 2020 • edited Loading

pi8027 commented Dec 21, 2020

pi8027 commented Dec 22, 2020 • edited Loading

pi8027 commented Dec 25, 2020 • edited Loading

mkerjean commented Jan 4, 2021

pi8027 commented Jan 4, 2021

pi8027 commented Jan 13, 2021

mkerjean commented Jan 13, 2021

CohenCyril commented Jan 14, 2021

mkerjean commented Feb 17, 2021

affeldt-aist commented Mar 11, 2021

affeldt-aist commented Mar 11, 2021

affeldt-aist commented Mar 12, 2021

pi8027 commented Mar 12, 2021

pi8027 commented Mar 12, 2021

affeldt-aist commented Mar 18, 2021

pi8027 commented Mar 18, 2021

pi8027 left a comment

Choose a reason for hiding this comment

mkerjean commented May 29, 2020 •

edited

Loading

affeldt-aist commented Dec 10, 2020 •

edited

Loading

mkerjean commented Dec 18, 2020 •

edited

Loading

pi8027 commented Dec 22, 2020 •

edited

Loading

pi8027 commented Dec 25, 2020 •

edited

Loading