Hello!

こんにちは

does this mean "hello world"?

just "hello" :-)

Hi everyone, I just wanted to let you know that I am trying to formalize Hahn-Banach theorem. This uses infinite dimensional vector spaces, convexity and Zorn Lemma. I am not formalizing a more general theory of vectorial spaces as I am using lmodType over R.

The following thing however would be to formalize Hausdorff and locally convex topological vector spaces.

Hi, we have a few definitions and lemmas about convexity (see convex.v in https://github.com/affeldt-aist/infotheo) that we use to state and prove theorems about distributions and hulls, but that is work in progress.

Thanks ! For the moment I am just borrowing the definition I found in https://github.com/math-comp/analysis/altreals/distr.v - but I may need more. I will let you know !

BTW, at some point, we should discuss the merge of altreals/distr.v & your theory on finite distributions.

@Pierre-Yves Strub +1

agreed

Is analysis supposed to compile without changes using the latest commit of mathcomp and Coq 8.9?

@affeldt-aist sorry for the late answer

Hi everyone, I'm looking at topology.v and landau.v. I can't figure if the topology on the field K ( or on some real field R) is defined or used somewhere. I am missing something or do I need to define it ?

Ok, I see now that is is in Normedtype, which doesn't want to compile for me.

which version of Coq are you using?

sorry, which version of mathcomp

Do you have any idea of a good reason for opam not to find the last version of math-comp ?

I had a few of them, and it was none of them :laughing:

Hi, I've been desperately looking for the name of the lemmas giving me that 0 is neutral and + is commutative in ( V : normedtype). Could someone give me a hint on where I should find them ?

`add0r`

for neutrality (on the left) and `addrC`

for commutativity should work, don't they?

they are in `mathcomp.algebra.ssralg`

(they are generic theorems for Zmodules, and normedtypes are Zmodules)

Thanks, I was missing addrC, lesson learned.

:+1:

Hi, I am trying to use hahn banach theorem in the context of normedtypes. This supposes to see scalar maps (as used in the original version of hahn banach) as linear maps between normed spaces (which are bounded iff continuous). Is there a way to see linear maps : V -> R^0 as particular instance of {scalar V} ?

@mkerjean they should coincide

So if I proved properties for linear functions between normed spaces (in my case relating boundedness and continuity), and if I want to use if on functions of type {scalar V}, what should I do ?

Do I need to duplicate my lemmas for the case when the normed domain in R ?

Do I need to duplicate my lemmas for the case when the normed domain in R ?

Yes but you can reuse the proof

Ok, I wasn't able to find something unifying lemmas on normm and those on normr, so the proofs differ slightly.

@mkerjean can you show me?

For example the norm of scalar multiplication , it seemed to me that normmN and normrN apply in strictly different context ?

Otherwise there is an ugly and unfinished proof file hahn_banach_applications.v in the hb branch of the project

which line?

do you want to skype quickly?

(I in a conference, can't skype before tonight basically)

ok

Another example is the use of ball_absE and ball_normE, I was not able to use ball_normE to unfold a ball in R. Is there a way around ?

(line 144 vs line 82 in the file)

yes there are ways around, all this confusion is due to a bad design choice I made 8 years ago in mathcomp and is going to be fixed in the next release :cry: ...

meanwhile we have to make do with 3 notions that happen to coincide for `R`

for a domain `D`

, the ssrnum norm of type `F -> F`

, the absolute value of type `F -> R`

and the norm in a module `M`

on top of `F`

of type `M -> R`

:-/

When `F = M = R`

everything has the same type...

to use `normm`

lemmas on `R`

one has to annotate it like this `R^o`

(line 144 vs line 82 in the file)

I cannot compile line 82 :-/

```
Lemma continuous_bounded0 (V W : normedModType R) (f : {linear V -> W}) :
{for 0, continuous f} ->
exists2 r, r > 0 & forall x : V, `|[f x]| <= `|[x]| * r.
Proof.
Admitted.
Lemma continuousR_bounded0 (V : normedModType R) (f : {scalar V}) :
{for 0, continuous f} ->
(exists2 r, r > 0 & forall x : V, `|f x| <= `|[x]| * r).
Proof.
have f_linear : linear (f : V -> R^o) by exact: linearP.
exact: (@continuous_bounded0 _ _ (Linear f_linear)).
Qed.
```

I also wanted to use {scalar V} and not {linear V -> R^o}, as this was the notion used in the basic hahn banach theorem in hahn_banach.v

Ok now I see your code

This is experimental anyway, so I'll wait for the next release and correct the hahn_banach_applications at this point ?

This is experimental anyway, so I'll wait for the next release and correct the hahn_banach_applications at this point ?

Please do not refrain from experimenting, the next release of mathcomp could be in a few month...

Hi , it's me again. Is there a proven lemma allowing directly to deduce (x < z) from ( x <= y ) and ( y < z) or do I need to reason by case on x<=y ?

Moreover, I am giving a talk tomorrow at the BigProof Workshop, is it ok if I advertise this gitter forum ? I personnally would be happy to avoid other people the troubles I have encountered through this mean, but I don't remember if this gitter was intended for a larger group.

Maybe the lemma ler_lt_trans?

@mkerjean the gitter forum https://gitter.im/math-comp is indeed public, anyone can find it and join it, so if you want to, you may advertise it

Maybe the lemma ler_lt_trans?

That would have been my answer as well.

@affeldt-aist Thanks, no idea why I did not find it !

Hi, while finishing the applicaiton of Hahn-banach theorem to normed spaces I stumbled on the definition of restricted topologies, and in particular on the one subnormed spaces. Has this been done somewhere ? I can cheat by using the definition of restricted filter, but then it seems hard to reattached that definition with the existing lemmas.

```
Definition locally_restricted (G : set V) ( x : V) :=
fun A => (A= setT) \/ (exists B, locally x B /\ (B `&` G = A)).
```

Hi @mkerjean, I do not understand `locally_restricted`

, where does it come from? Did you try to use `within`

?

@Cyril Cohen I was trying to define the topology induced on a subset of a topological space. I did not understand that that was the point of `within`

.

@mkerjean you understand how to use it now?

@Cyril Cohen I think so, it seems to be working. Thank you very much !

Dear math-comp users and developpers. Tomorrow I will migrate all math-comp channels to zulip.

Hi, just to warn that this might happen, downloading Nix with eduroam did not work

Hi everyone, I've been using MathComp with Nix since this morning. How can I use the real-closed libraries in a file depending on the mathcomp-analysis library ? Adding a dependency in mathcom-real-closed in shell.nix is not working.

Hi everyone, I've been using MathComp with Nix since this morning. How can I use the real-closed libraries in a file depending on the mathcomp-analysis library ? Adding a dependency in mathcom-real-closed in shell.nix is not working.

https://github.com/math-comp/analysis/pull/147 is supposed to solve that.

thanks for signaling

@Cyril Cohen It's working, merci beaucoup !

@Cyril Cohen , is there a place which explains how to fix this kind of issues?

I mean, how to upgrade nixpkgs.

Cyril Cohen , is there a place which explains how to fix this kind of issues?

I realize I do not know where to find an explaination :-/ in a few words: nixpkgs is a repository (https://github.com/NixOS/nixpkgs) and each commit corresponds to a specific combination of versions of all packages. At the beginning of shell.nix I import a specific commit: actually I usually pick the latest one of https://github.com/NixOS/nixpkgs-channels/tree/nixpkgs-unstable which corresponds to the commits of https://github.com/NixOS/nixpkgs for which main binaries (including coq) have been cached. Changing the imported commit at the beginning of shell.nix may or may not trigger rebuilds (depending on what has been upgraded since the last commit that was imported)

Why changing this commit did solve Marie's issue?

Why changing this commit did solve Marie's issue?

because the previous commit dated from before I added real-closed to nixpkgs

How did you add real-closed to nixpgs?

How did you add real-closed to nixpgs?

Like this: https://github.com/NixOS/nixpkgs/pull/61959

I am trying to use the complex defined in real_closed as a topological space, and I am struggling with real closed field. Typically, when trying to define an AbsRingMixin or a ball on the zmodtype structure of R[i], I get :

```
(cannot unify "Num.NumDomain.sort (ComplexField.complex_numDomainType R)" and
"Rdefinitions.R").
```

Hi @mkerjean , sorry for the late reply. It looks like a few canonical instances are missing. Could you point us concrete code?

Anyone has seen my e-mail on the ssreflect mailing list ? I've trouble installing math-comp/analysis...

Hi @Florent Hivert ! Have you seen @affeldt-aist 's answer on the mailing list as well? He suggested an `opam update`

. Did you try? What went wrong?

I followed exactly the instruction of https://github.com/math-comp/analysis/blob/master/INSTALL.md

But got:

The following dependencies couldn't be met:

- coq-mathcomp-analysis -> coq-mathcomp-field < 1.9.0~

no matching version

At step 3.

you made a git clone ? I am afraid that the opam file in master has not been yet updated (this is a PR...)

I am pretty confident that "opam install coq-mathcomp-analysis.0.2.2" should do it

I'll try that as soon as my machine is done compiling coq...

[ERROR] Package coq-mathcomp-analysis has no version 0.2.2.

O_O

Now trying : opam install coq-mathcomp-ssreflect

- install coq-mathcomp-ssreflect dev

according to https://coq.inria.fr/opam/www/, coq-mathcomp-analysis 0.2.2 should be available...

(why does opam insist on installing a "dev" version?)

What does it mean ? There is a bug in my opam setting ? How to debug that ?

opam info package-name gives you a list of versions available

(but maybe you know all that)

opam install coq-mathcomp-ssreflect.1.9.0 should install the version 1.9.0

I'm completely new to opam ! Thanks for the tip.

I don't know what is the logic when no version is indicated but going for a "dev" version sounds wild :-)

I usually install coq/math-comp... by hand...

dev by default sounds also a bad design choice to me...

so opam install coq-mathcomp-analysis.0.2.2 should have triggered the installation of mathcomp version 1.9.0 and so on

Waiting some compilation to finish...

millsmess-~ $ opam info coq-mathcomp-analysis

<><> coq-mathcomp-analysis: information on all versions <><><><><><><><><><><><>

name coq-mathcomp-analysis

all-versions dev

<><> Version-specific details <><><><><><><><><><><><><><><><><><><><><><><><><>

[...]

Only the dev version is accessible...

(just to check: opam --version?)

opam doesn't find non dev version of the other mathcomp packages...

(I am wondering whether you use opam 2, the version has changed recently)

It seem to be related to

$ opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev

ah!

opam repo add coq-released https://coq.inria.fr/opam/released

maybe this would be better

Ok ! This is now installing things properly. https://github.com/math-comp/analysis/blob/master/INSTALL.md should be fixed

I guess that opam repo remove coq-extra-dev would be in order

I launched from an brand new opam repo and it seems fine.

Yes, sorry for the inconvenience (really), the installation information is outdated and will be fixed tomorrow

I just posted a small pull request on github fixing the install instruction.

Please ignore my PR if you have something better.

Anyway, thanks for the help !

Thanks for your patience!

Hi , I' m looking once again at normedmodule. Could someone remind me the reason for using R^o for the normed module type structure on R ? Is it fixable ? Should it be the same for making a normModType out of any absRingType ?

Hi , I' m looking once again at normedmodule. Could someone remind me the reason for using R^o for the normed module type structure on R ? Is it fixable ? Should it be the same for making a normModType out of any absRingType ?

`_^o`

is a wrapper around a type such that if this type `R`

is a ring then `R^o`

is a `LmodType`

, and normed module extends `LmodType`

. I think ideally all `absRingType`

should be normed module over themselves and hence `LmodType`

over themselves which can only be defined as a canonical instance on every instance of ring for now, which is not a good practice. The good practice is to embed a structure of normed mod type in the axiomatization of `absRingType`

which is not possible at the moment but will be possible after https://github.com/math-comp/math-comp/pull/270 is merged. I was going to way until this PR is merged, maybe we should do the quick fix anyway...

Thanks @Cyril Cohen ! Another question then : why does `NormedModule.mixin_of`

on a `lmodType`

asks for a `Uniform.mixin_of`

? Comparing Normed/uniform to Uniform/Topological, the construction of a uniform type only requires some `loc : T -> set ( set T)`

, allowing more flexibility and lemmas as `topologyOfBallMixin : forall (T : Type) (loc : T -> set (set T)), Uniform.mixin_of loc -> Topological.mixin_of loc`

. It seems then that the straightforward way to build a normed structure on a lmodule is too build first a uniform structure, instead of proving the necessary axioms for the norm and having a canonical way to infer the uniform structure from it. What am I missing ?

I guess my question was about the normedtype mixin, which is based on a uniform mixin instead on a `ball`

type. I was comparing with the uniform mixin, which asks for a `loc`

type but not for a topological mixin.

Hi @mkerjean I apparently missed the notifications from this channel, I'm so sorry to reply so late

I understand that we need to ensure the compatibility of the normed structure with the uniform structure, but it is not clear to me why `Normed.Mixin_of`

takes as argument the entire `Uniform.Mixin_of`

and not just a `ball`

.

The answer to your question is not so easy, and I am not sure I understood it.

What I will write is pervasive in mathcomp, so you will find this pattern everywhere: whenever you have two structures A and B, where B is a substructure of A (i.e. the inhabitants of B are inhabitants of A, e.g. A = group, B = ring, ... or A = uniform space, B = normed module), then we make sure all the operators of A are literally part of the operators of B, even if one could derive some operators of A from the ones of B. Since operators come in mixins together with the other (Prop) axioms, we generally include whole mixins instead of just operators (this is tied to our very specific representation/code structuration). That's why the whole `Uniform.mixin_of`

is included in `Normed.class_of`

.

Just in case it was also part of your question: the reason for this inclusion is the canonicity of these operators with regard to type constructors. For example the product of two uniform spaces is a a uniform space and the product of two normed modules is again a normed module, but the uniform space derived from the product of two normed modules is definitionally not the same as the product of two uniform spaces derived from (two) normed modules.

@mkerjean ok, thanks for you clarification, so only the last part of my first paragraph is useful to you now: it's just a technicity, and anyway before declaring a type as canonically a normed module one has to first declare it as a uniform type, so the job of tagging `ball`

as an generic operator for a given structure will be done that way anyway

we are currently working on more user-friendly ways to do this here: https://github.com/math-comp/hierarchy-builder

@Cyril Cohen But `uniform`

's `mixin_of`

departs from this rule of thumb right? It has a `locally`

parameter. (@Assia Mahboubi speaking)

yes indeed, it is an exception

because there is no way of writing the type of the structure that has a `loc`

on itself...

I will give more details

Right now `filteredType`

is very particuliar, it is sort of a mix between `predType`

and a traditional algebraic structure... Indeed `F : filterType T`

is a type `sort F`

for which every element `f`

has a `loc f : set (set T)`

i.e. a type that indexes "unlawful" filters on `T`

. Then a uniform space `U`

associate to every point a filter on `U`

, and since there is no way to write `U : filterType U`

, we reuse the operator `loc`

directly

(and it happens to be an "unboxed" mixin as well, since there is only one operator and no axioms (because it is unlawful))

(In https://github.com/math-comp/hierarchy-builder we are exploring the option when we inline all the mixins and depend only on other operators rather than whole mixins)

Great ! Thank you very much for all the explanations :-)

I have been working on holomorphic functions, and for this purpose working on the complex type`C`

(from real-closed/theories/complex.v ) as an absolute Ring and `C^o`

as a normedType. However, I can't define a canonical structure of normedType on C^o, as due to the notation `^o`

it identifies with the canonical normedType structure on `R^o`

. Is this problem going to be solved with math-comp/math-comp#270 ?

@mkerjean after https://github.com/math-comp/math-comp/pull/270, both R and C (without ^o) shall have normedType canonical structures over themselves.

@Cyril Cohen great, thanks

Just to let you know. I started today to write a library for formal power series using `boolp`

and `classical_sets`

. Is there a chance that it can be useful for analysis or do you have everything you need about series ?

@Florent Hivert it would be very useful, we barely started series

Ok ! I just created `https://github.com/hivert/FormalPowerSeries`

. I'm currently adapting what's makes sense in `poly.v`

. If you have any early suggestion...

Hi @Florent Hivert , this is great new! @mkerjean has started developing elementary complex analysis. We hope to deal with linear diff equations soon, and formal series might be useful by then.

A nix question again. I am trying to add mathcomp-real-closed to the packages made available in a nix-shell configured by the shell.nix of the repo. When I am adding `mathcomp-real-closed`

to this line and restart nix-shell, I get an error

```
error: undefined variable 'mathcomp-real-closed' at /home/assia/Sources/math-comp/analysis-main/shell.nix:26:50
(use '--show-trace' to show detailed location information)
```

This is blocking for us in the integral-draft branch when we need to import `complex`

. Any hint ?

Note that trying to have `mathcomp-multinomial`

or `mathcomp-coqeal`

fails as well.

I have to check which versions of what have been included in the nixpkgs repo and update to the right commit if it exists

@Cyril Cohen , did you check? can we help in any way? it is really blocking.

I will try now or tomorrow

I guess https://github.com/math-comp/analysis/pull/147 is what you were looking for? I'm looking into it

@Cyril Cohen , this is what we were looking for, but we had no idea it was the case. So we solved the issue independently with the help of @Théo Zimmermann @Vincent Laporte and @Gaëtan Gilbert. We spend a considerable amount of time (several hours) trying to fix this so I hope we will manage to introduce enough documentation files and good practice that will prevent this to happen again.

For instance, why was this a PR, and why this PR was not merged?

Also, I find it very annoying to have to mention literally a precise full commit name in the shell.nix file. Would it be possible to have tag names instead?

Finally, but this was less annoying in the end, the fact that the sha256 also has to be hard-coded, but the correct value is displayed if it is not, was also disturbing.

Also, I find it very annoying to have to mention literally a precise full commit name in the shell.nix file. Would it be possible to have tag names instead?

it's certainly possible, it's just a url after all

@Assia Mahboubi it was a PR because it needs to be tested and it was not merged because of the red cross, the fact that the issues you mentioned were not addressed (or resubmitted as an issue as I just did) and because this affect users so it must be tested before it is merged...

I do not know how to do name tags nor how to skip the sha256 elegantly, it requires a better nix expert than I am

This is all very experimental, I set up the mathcomp/extra.nix file this summer and I am not entirely satisfied...

I hope we will manage to introduce enough documentation files and good practice that will prevent this to happen again.

So do I

It's possible to omit the sha256 entirely I think (remove the line), but this means that your computer will redownload the archive every once in a while.

Whereas with the sha256, it knows that it has already downloaded it because it can find it within the store.

Some people in the Nix world are talking about having command-line tools that can update shell.nix and default.nix files automatically, but I don't think that this has been built yet.

(In the general case it would not be possible, but for some simple updates like this, it should be)

@Assia Mahboubi furthermore, I did not know it was blocking until your message here:

A nix question again. I am trying to add mathcomp-real-closed to the packages made available in a nix-shell configured by the shell.nix of the repo. When I am adding

`mathcomp-real-closed`

to this line and restart nix-shell, I get an error

I updated to the last nixpkgs-unstable commit (as I usually do) and merged

FYI, got this error this morning when installing on a new (Debian 10) machine (currently investigating):

```
analysis$ nix-shell
these derivations will be built:
/nix/store/8fjaqf0px3r6a1jzhhkbcdmjsv18rggb-source.drv
/nix/store/ybblj7zawv3q6bah8rx0sa66cdzah2v3-coq8.9-mathcomp-ssreflect-1.8.0.drv
[crunch]
building '/nix/store/8fjaqf0px3r6a1jzhhkbcdmjsv18rggb-source.drv'...
/nix/store/k7yalpjh53xra535xaip1pfq6q4jgsc0-stdenv-linux/setup: line 822: /build/env-vars: No such file or directory
trying https://github.com/math-comp/math-comp/archive/mathcomp-1.8.0.tar.gz
% Total % Received % Xferd Average Speed Time Time Time Current
Dload Upload Total Spent Left Speed
100 135 0 135 0 0 342 0 --:--:-- --:--:-- --:--:-- 342
Warning: Failed to create the file /build/file: No such file or directory
0 4262k 0 715 0 0 888 0 1:21:55 --:--:-- 1:21:55 888
curl: (23) Failed writing body (0 != 715)
error: cannot download source from any mirror
builder for '/nix/store/8fjaqf0px3r6a1jzhhkbcdmjsv18rggb-source.drv' failed with exit code 1
cannot build derivation '/nix/store/lhf61xy4bz8l1slds8579wn4926q87sq-coq8.9-mathcomp-algebra-1.8.0.drv': 1 dependencies couldn't be built
cannot build derivation '/nix/store/5b9i93hjkk902f2mkj9d795s21m3qyqw-coq8.9-mathcomp-all-1.8.0.drv': 1 dependencies couldn't be built
error: build of '/nix/store/4wwxcy57ckndgjjs2l1vy6hk2ilqc4bw-coq8.9-mathcomp1.8.0-real-closed-1.0.3.drv', [crunch] failed
```

@affeldt-aist I have no clue how to deal with this error so far...

thanks for taking a look anyway (hopefully there are alternatives)

Hi. I am back to hacking in mathcomp-analysis. What are the current deps for compiling the libraries ?

dev is not working, mathcomp is incompatible with finmap 1.2

Are we stuck with mathcomp 1.8 ?

Ah sorry, 1.2.1 seems to be the solution

compiles with mathcomp 1.9 (and Coq 8.10beta3)

The problem was finmap.dev

Why is this lemma named 'lim_cst' ? It is a very generic name for such a specialisation to normed modules and functions with same domain and codomain. And thus it is easier found than the more often useful one 'cst_continuous'. For the latter as well I am not sure about the naming policy.

This is not a direct answer but there is this issue about the naming policy of related lemmas: https://github.com/math-comp/analysis/issues/29

@Pierre-Yves Strub

The problem was finmap.dev

did I screw up with the dependencies?

BTW I would like to update everything to the last version of finmap... but I am missing a compatible mutlinomials release (even though the changes are minor...)

Why is the canonical realType structure on R (from Reals in Coq main library) named real_realType and not R_realType ( this line) ? The other canonical instances of structures on R are named R_ringType, R_rcfType ...

It would be great that we bump the versions. Currently, with the condition math-comp >= 1.8, we have to keep using, e.g., eq_big_perm. But this implies having a tetra-chié of warnings when compiling with math-comp 1.9.

I am going to look at multinomials VS finmap

Hi, why is Reals used in normedType.v ? In particular, any norm must have values in R from Reals, and not in R of realType, and I don't see immediately why.

Hi @mkerjean. I guess the authors @Cyril Cohen @Damien Rouhling @affeldt-aist would provide the best answer, but my feeling is that they wanted to avoid a noisy parameter. May be also did they find that some inferences are harder to implement in this setting. I would be interested to know if it is the case. Related question : why didn't they use the Eudoxus reals that are in the repo, and have only two admits (stay tuned) instead of the list of axioms in Reals.v :p

Why is the canonical realType structure on R (from Reals in Coq main library) named real_realType and not R_realType ( this line) ? The other canonical instances of structures on R are named R_ringType, R_rcfType ...

Probably because it is an old file, copied and pasted from one development to the other. Plus no one really sees the names of these constants, as they are only used in the inferred parts of the terms, which are hidden by notations.

We are in the process of removing `Require reals`

from `normedType.v`

.

Eudoxus reals came after `normedType.v`

was "completed".

What is the plan to remove « require Reals ». Does it mean that you are implemeting your own model?

No, it is to use numDomainType or types that inherit from it.

Ah, there is `Require Reals`

and `Require reals`

. :-)

Ok. We looked at the missing proofs in Eudoxus reals with Assia.

There is not that much to do.

I plan to be done with it within 2 weeks

@affeldt-aist so the plan is to remove ‘reals’ but not ‘Reals’ ?

@Assia Mahboubi thanks for the answers !

@mkerjean the topic of yesterday was indeed to remove 'reals' but I think that 'Reals' will naturally follow

hi, I'm beginning with the mathcomp-analysis lib

where can I find the lemma about function and set ? I'm not sure how is it called (hausdorf relationship ?) but it's like, inverse of f on an intersection is an intersection of the inverse of the function

Hi @vlj ! As explained in the readme, this library is still experimental so you will probably find that some lemmas are missing, and some definitions/statement may change.

In particular, after a quick check I can confirm that the lemma you are looking for is not in the library (it should be in the file `classical_sets.v`

but it is not).

Please, feel free to suggest any addition that corresponds to your need either by submitting a PR or by opening an issue listing what is missing.

:thumbsup:

Ok

There is another lemma, is it OK to add it ? It tells that any set s in a set of set D is included in the bigcup of éléments of D

It's almost immediat but I think it may save à few line there and there

I have a math question : is open_from generating a Topology ?

I learnt that Topology is defined by a set of set containing empty/full set, stable by union and finit intersection

And open_from seems to validate the empty/full axiom as well as the union one... But where does the intersection axiom fits there ?

There is another lemma, is it OK to add it ? It tells that any set s in a set of set D is included in the bigcup of éléments of D

If it saves lines, sure! I suggest you submit *any* lemma that you think should belong to the library and then people discuss them on github.

And open_from seems to validate the empty/full axiom as well as the union one... But where does the intersection axiom fits there ?

The intersection property only holds if your basis of open sets satisfies a few properties. In fact, if it is a *basis* of open sets… :-)

If you look below the definition of `open_from`

you will see the requirements `b_cover`

and `b_join`

and even further the proof of the intersection property as the first obligation in the definition of `topologyOfBaseMixin`

Right ! Sorry, I didnt notice that the proof of topologyOfBaseMixin was using them

I'm having some trouble writing the intersection of 2 sets as a bigcap

I'm trying ```
Lemma Intersect2 {I} (X: set I) (Y: set I):
\bigcap_ (i in [set X; Y]) (fun x => x) = X
```

&` Y.`

but it doesn't work (syntax error, '.' expected but I don't understand why

and if I add an auxiliary def, like ```
Definition I2 {I} (X: set I) (Y: set I):=(X
```

&` Y).`

and then

```
Lemma Intersect2 {I} (X: set I) (Y: set I):
\bigcap_ (i in [set X; Y]) (fun x => x) = (I2 X Y).
```

I have an error : The term "I2 X Y" has type "set I" while it is expected to have type

"set Prop" but I don't really know to deal with it

@vlj I dunno, this works for me:

```
Lemma Intersect2 (I : finType) (X: {set I}) (Y: {set I}): \bigcap_ (i in [set X; Y]) i = X :&: Y.
```

@vlj I think the problem is `(fun x => x)`

. The big notations automatically add the `fun i => `

. So that add @Emilio Jesús Gallego Arias did you want to write `\bigcap_ (i in [set X; Y]) i`

.

Indeed, the bigcap @vlj wrote intersects all sets of the form `fun x => x`

for any `i`

which is either `X`

or `Y`

.

Since `fun x => x`

must be a set, hence a function of type `?T -> Prop`

, the only possibility is to have `?T = Prop`

, which explains the message asking for an expression of type `set Prop`

.

Note that with the notations of mathcomp-analysis the solution of @Emilio Jesús Gallego Arias can be generalised to any type `I`

:

```
Lemma Intersect2 (I : Type) (X Y : set I) : \bigcap_(i in [set X; Y]) i = X `&` Y.
```

Hi mathcomp/analysis devs. A while ago, we promised to showcase the design choices of the library wrt exceptional points for real analysis (Rbar, infinity, Nan). Deadline Nov.15th. Has anyone started something?

Hi @Assia Mahboubi. Personally, I haven't written anything.

@Assia Mahboubi I did not start anything either...

I can write something with my experience on summability.

And positive stuffs.

Where should we put our stuffs?

In a subdirectory and/or a branch of math-comp/analysis?

Any solution will do. Decide, I obey :)

Then a subdirectory

@Emilio Jesús Gallego Arias thanks !

Is there à

Docker script to build analysis ?

I d like to check that a change I did is properly compiling with a clean setup

You can have a look at the travis script

E.g., it is using (among others): mathcomp/mathcomp:1.9.0-coq-8.10

Ok

@Damien Rouhling if we were to use bigop to define bigmax (instead of the fold in Rstruct.v), which branch could be used as a reference: bigmaxr, entourages_bigmax, entourages_bigmaxr_mem?

oh… we definitely should do some clean up

let me check

:-)

none of the above ! :-)

I would have said entourages_bigmaxr_mem :-/

the latest code is in uniform-entourages

thanks!

I opened a PR : https://github.com/math-comp/analysis/pull/162

I can write something with my experience on summability.

@Pierre-Yves Strub did you have time to do something?

I'm having an issue now, I have a proposition that tells that an element is in a singleton, but I don't know how to turn this into an equality

more precisely :

```
Lemma Intersect2 {I} (X: set I) (Y: set I):
\bigcap_ (i in ([set X] `|` [set Y])) i = (X `&` Y).
Proof. rewrite /bigsetI predeqE => //= ; split.
- move => H. split ; [apply: (H X) | apply: (H Y)]=> //= ; by [left|right].
- case. move => Xx Yy seti. case => //=.
```

The proof environnement at this step is :

```
I: Type
X, Y: set I
x: I
Xx: X x
Yy: Y x
seti: set I
________
[set X] seti -> seti x
```

the `[set X] seti`

means that X = seti and thus goal is solved

I tried with in_setE or things like that

`[set X]`

is a notation for `set1 X`

ie `[set a : _ | a = X].`

but I dont know how to "destruct" `set1 X seti`

Maybe you can prove `forall x, x \in [set X] -> x = X`

?

@vlj Maybe you want to do this

```
rewrite /set1.
move=> ->.
done.
```

(which can be of course shortened to `by move=> ->`

and furthermore streamlined into the previous line of script)

what does "->" do in a move => tactic ?

@affeldt-aist it works thanks ! but I don't understand why atm

the rewrite is not necessary actually

hi @vlj. When your goal is of the form `l = r -> G`

, `move=> ->`

or even `move->`

rewrites `l = r`

from left to right in `G`

(and you don't have access anymore to the assumption `l = r`

). From right to left it would be `move<-`

.

Thanks

Is there a way to know what coq "really sees" behind a notation ? I mean it was stuck to [set X] seti in the environnment even with a rewrite /set1

Completly unfolding the definition "on paper" and reducing shows that it is equivalent to X=seti but it the coq prompt didn't want to strip the notation for me

The command `Unset Printing Notations`

reveals what is behind notations.

Thanks

it works but it doesn't stay past the command that follows.

but actually it showed me that I need to rewrite `rewrite /classical_sets.set1`

and not just `rewrite /set1`

so that's useful.

I have another issue with type :s

```
From mathcomp Require Import topology.
Section Test.
Variable X: topologicalType.
Variable Y: pointedType.
Variable f: X -> Y.
Print topologyOfOpenMixin.
Definition minus := [ set A | open (f @^-1` A)].
Theorem minusT : minus setT.
```

The theorem fails to be properly typed, because of ```
The term "[set: fintype.Finite.sort ?T]" has type
"{set fintype.Finite.sort ?T}" while it is expected to have type
"set Y".
```

but I don't understand what's going on... As far as I understand, "minus" type is set (set Y) (at least that's what Print shows) and setT should be a set Y, so it should be correctly typed.

hmm apparently the issue is with setT, but I really don't understand why

err nvm it works with classical_sets.setT

actually I imported finset in my scope and it looks like it conflicts with things in classical_sets all over the place

maybe `Local Open Scope classical_set_scope.`

?

Yes

hi, I have (again) an issue with typing. The code :

```
From mathcomp Require Import classical_sets eqtype boolp seq.
Require Import ssreflect.
Open Scope classical_set_scope.
Lemma preimage_bigsetU {A B I} (P : set I) (g:A->B) F:
g @^-1` (\bigcup_ (i in P) F) = \bigcup_(i in P) (g @^-1` F).
Proof.
rewrite predeqE. split; rewrite /bigsetU /preimage ; by [].
Qed.
From mathcomp Require Import topology.
Section Ex.
Variable X: topologicalType.
Variable Y: pointedType.
Variable f: X -> Y.
Print topologyOfOpenMixin.
Definition minus := [ set A | open (f @^-1` A)].
Theorem minusT : minus setT.
Proof.
Print setT.
rewrite !/minus !/preimage => //=.
apply openT.
Qed.
Theorem intersect: forall (A:set Y) (B:set Y),
minus A -> minus B -> minus (A `&` B).
Proof.
rewrite !/minus.
move => A B.
Unset Printing Notations.
rewrite /setI /preimage.
apply: openI => //=.
Qed.
Theorem union (D : set (set Y)):
(forall i, D i -> minus i) -> minus (\bigcup_ (i in D) i).
Proof.
rewrite !/minus.
move => Siiopen.
(**Unset Printing Notations.*)
rewrite (preimage_bigsetU D f (fun i: set Y => i)).
```

I'd like to apply the preimage_bigsetU lemma (which tells that preimage union = union of preimage) but it fails to unify type.

Error message is : `Found type "set Y" where "Pointed.sort Y" was expected.`

the type of preimage_bigsetU according to check is ```
preimage_bigsetU
: forall (P : set ?I) (g : ?A -> ?B) (F : set ?B),
g @^-1 (\bigcup_(_ in P) F) = \bigcup_(_ in P) g @^-1 F
```

there's something I dont really grasp with the notation, it's that F should depend on i, but according to the type, it's not a function of i

actually simplifying the preimage_bigsetU (removing F, using i instead in a set (set B)) prop) works

Hi @vlj. The issue is in the definition of `preimage_bigsetU`

.

I think you mixed up the definition of the notation `\bigcup_(i in P) F`

, where we use a variable `F`

instead of the more precise `F i`

in order to match any expression used by the user, with the actual use of the notation, where you have to put `F i`

if you want Coq to infer that `F`

is a function whose argument is `i`

.

Here, since you used `\bigcup_(i in P) F`

instead, Coq inferred `F`

to be of type `set B`

which makes `preimage_bigsetU`

not very interesting: when `P`

is non-empty, `\bigcup_(i in P) F = F`

so this lemma almost just states that `g @^-1 F = g @^-1 F`

Ho yes you're right

I though F was a type in the notation indeed

Is there a definition of sqrt in mathcomp ? There is one in stdlib,and there is another one which may fit my needs (sqrt on int) but it uses module which are not recommended according to coq wiki (besides I don't know how to instantiate it ) https://coq.github.io/doc/master/stdlib/Coq.Numbers.NatInt.NZSqrt.html

Ssrnum has a sqrt but not for nat

there has been a minor update of mathcomp-analysis (0.2.3) so that it is compatible with mathcomp.1.10.0 (available on opam)

is there a lemma/theorem to "map" a comparaison from R to N ?

my use case is : I want to proof that ifloor (sqrt n) ^ 2 <= n

to do that I need at some point to rewrite n, which is a nat, as sqrt * sqrt, so I need to inject the inequality in a real closed field

but then I have no idea how to "go back" to N

hi @vlj, what do you need exactly? A definition for the largest `i : nat`

such that `n = i * i `

? If so, it might indeed be more convenient to use a dedicated definition, and not use the square root in real numbers.

S.t. `n >= i * i`

, no ?

Yes, sorry

@vlj, what about using `ex_maxn`

as provided in ssrnat?

```
Lemma leq_expr (e n : nat) : 0 < e -> n <= n ^ e.
Proof.
case: e => [| e] // _. case: n => [| n] //=.
by rewrite expnS; apply: leq_pmulr; rewrite expn_gt0.
Qed.
Lemma sqrtn_aux m : exists n, n ^ 2 <= m. Proof. by exists 0. Qed.
Lemma sqrtn_bound m n : n ^ 2 <= m -> n <= m.
Proof. apply: leq_trans; exact: leq_expr. Qed.
Definition sqrtn (n : nat) := ex_maxn (sqrtn_aux n) (@sqrtn_bound n).
Lemma sqrtn_ge0 n : 0 <= sqrtn n. Proof. by rewrite /sqrtn; case: ex_maxnP. Qed.
Lemma lesqrtn n : sqrtn n <= n.
Proof.
rewrite /sqrtn; case: ex_maxnP => j Pj _;apply: leq_trans Pj; exact: leq_expr.
Qed.
```

I can give a try

I initially had in mind to "mimic" c like code (which use float to float) but it turns out to be very complicated

Using what you suggest is probably better

Hey all, I have been working on a complex analysis package based on Coquelicot (https://github.com/zstone1/coq-complex), and have manged to prove some nice stuff, including "Holomorphic implies analytic". Now that I know what I'm doing (a little bit), I'd like to port the work to mathcomp analysis.

However, I need definite integrals. This is blocking me right now, as I am not sure where/if results like fundamental theorem of calculus live in mathcomp analysis. Can anyone help me to understand the current state of integration theorems in mathcomp/analysis? (FTC and exchanging limits and integrals are the only two thing I really need to do).

@zstone1 there is actually already some work in this direction performed on top of mathcomp-analysis

the branch analysis_270_integration provides the draft of a definition of integration and basic facts about holormophic functions

this is all very sketchy but this is also the focus of much attention right now

@zstone1 These have also been formalized in corn, math-classes, and there is a recent PR to the coq stdlib. There might be some posibilities to refactor things.

Consider contacting @vincentSe (vincent.semeria@gmail.com) https://github.com/coq/coq/pull/9185

The classical theory seems to factor quite well via the constructive one.

Thanks for the pointers. The proofs in analysis_270_integration do seem to be in the right direction. I can definitely merge some of my work is to that. For example, I have the reverse direction of Cauchy Riemann, which should port pretty well from coquelicot. I am also extremely agnostic to the definition of integral being used. I only integrate (uniformly) continuous functions over real intervals. Considering how uncertain all this work is, maybe I should just define an interface to decouple it?

As far math-classes and corn go, it appears they don't use filters to handle convergence. My work defines the topology of compact convergence, and proves compact limits exchange with contour integrals. So porting everything to an epsilon Delta world would be pretty tough.

Considering how uncertain all this work is, maybe I should just define an interface to decouple it?

The integral.v is intended to provide an interface to support other work; it would be great if you can plug on it, but if something is lacking or needs improvement your input is welcome and should be followed by quick action!

@zstone1 yes, these libraries use eps-delta.

In any case, it's nice to see some complex analysis. Is this your PhD-project?

@zstone1 Hi, I would be happy to discuss or help with your porting to mathcomp analysis. When porting the cauchyriemann equations to the recent PR270 some questions were raised on complex analysis, and on how to handle the various topologies on `C`

. Don't hesitate to ask if something seems obscure !

@affeldt-aist That sounds like a plan. I will start there, and we can figure out what I need to complete my proofs.

@Bas Spitters Not a PhD project, this is a side project for me. I'm just trying to learn about the intersection of computer science and analysis. If you are handing out graduate degrees, I'll take one though.

@mkerjean, thanks for the offer. I first need to bash my head against this new notation for a bit, then I might have some relevant questions. Dealing with multiple topologies wasn't too painful. I have some (hacky) tactics to automatically apply `forall (P:Prop) (x:C), locally_square x P <-> locally_circle x P`

. So I rarely cared which topology I was in. That being said, my proofs are... inelegant. So maybe not a great data point.

I have two questions. In cauchyetoile, which seems to be the right file, there is a comment that `differentiable in derive.v, means continuoulsy differentiable, not just that the limit exists`

. I'm pretty sure all it's doing is asking for the linear approximation to be continuous, not for `f'`

to be continuous. If I'm right, is there any need to define a separate difference quotient in `holomorphic`

? Your existing proofs need almost no change, as a short proof shows `holomorphic f z = derivable f z 1`

today.

Now the thing I really don't understand is why differentiable_def is coinductive. Why not just a normal inductive type?

Hi @zstone1 , `cauchyetoile`

is very much work in progress (and me learning mathcomp analysis) - I don't remember when I wrote this comment and you should be right about continuity.

@zstone1

Now the thing I really don't understand is why differentiable_def is coinductive. Why not just a normal inductive type?

Actually, is should be `Variant`

rather than `Inductive`

or `Coinductive`

(the latter was a "hack", because for non-recursive inductive types, it actually has the same semantics, except it does not generate (unused) induction principles). `Variant`

is the "clean" way to do that.

Hi, am I right if I say that no lemmas in `analysis`

shows the equivalence between continuous and bounded for linear maps between normed spaces ? Maybe we could add them to `normedtype`

( I needed them for Hahn-Banach here ) ?

@mkerjean one direction of this equivalence should be hidden in here https://github.com/math-comp/analysis/blob/master/theories/derive.v#L152-L166

@Cyril Cohen It seems to be it just shows that the identity is bounded ?

Hi everyone,

For several reasons, I would like to endow a `numFieldType`

with a (canonical) topological structure. This would for example allow for the use of multiplication instead of scalar multplication in some cases of complex theory, and makes us closer to maths.

If I understand well, it would be necessary to make a clone of `ssrnum`

in the analysis library, creating types as `PseudoMetricNormedZmodule`

. How close are we to have a viable Hierarchy Builder tool (@Cyril Cohen @Kazuhiko Sakaguchi ) ?

How "feasible" is it to prove something using à derivative ? In arithmetic there is the lia tactic which ease équation transformation to some extent, but it likely doesn't work for reals. Since it's tedious to transform expression by hand is there some recommanded way to do with mathcomp analysis ?

@vlj lia has relatives for reals https://coq.inria.fr/refman/addendum/micromega.html#short-description-of-the-tactics

(but never used any of the other ones)

It works with reals ? It's not limited to presburger arithmetic ?

It's a good new

There is a zify like mecanism

Hi folks, should `\max`

in order.v be generalized such that it works with `ring_display`

? (cc: @Cyril Cohen )

this would mean that \max would be defined with ringType ?

I think you need something higher, such as numField

Hi folks, should \max in order.v be generalized such that it works with ring_display? (cc: Cyril Cohen )

Sure!

What is the recommended way to make proof relying on formula on a field ? For instance I have a formula defined in numFieldType, and it has a nice composition property. If I use Coq.Reals the field tactic can be used ; I tried adding a custom field theory to the field database, but then I hit the bug

#11998 in coq

In this bug somebody mentions ssring which is part of a third party lib on elliptic curve, but elliptic curve by themselve seem to be too specific to be part of mathcomp

Should I just copy the file content and use it or is there another more "official" way of doing ?

Hi @vlj, sorry, there is no official way yet. Your question is a "generalization" of https://github.com/math-comp/math-comp/issues/401

Yes, that's where I found ssring.

It looks like there are several methods "floating around" but I'm not really sure which one to pick

If I have a topologyOfBaseMixin, how can I make a TopologicalType out of it ? in topology.v it's not directly considered as a topologicalType, it's used to create another mixin (topologyOfSubbaseMixin) which in turn is used to generate another mixin (sup_topologicalTypeMixin ) which has it's own type

here is the sample I'm using : https://gist.github.com/vlj/b45fb840764357d58c6d2e1ee4e501f1

btw is there a definition of "included" topology somewhere ?

eg coarser topology

classical_set means that Excluded Middle hold ? I miss a lemma "Lemma setCC: `~' ~' X = X`

I can write one, but I'd like to know if this I'm not mistaking something

I created a pull request : https://github.com/math-comp/analysis/pull/173 all comment welcome (I'm still not completly familiar with every mathcomp convention)

Hi everyone, I would like to create a PR getting rid of the `^o`

for analysis ( defined here ). In the current state of the library (branch `mathcomp master`

), the tag `^o`

is the only way to have a topology on a `numFieldType`

as well as a `lmodType`

structure on it.

As I see it, while it is understandable that no canonical algebra structure should be put on a ring, this became less clear in the case of fields, especially if one wants to deal with analysis. The inconvenient of `^o`

to me is that dealing with topology on it leads to multiplication of the tags `^o`

on a single type.

The solution would be the creation of an copy of the structure `numField`

endowed by inheritance with a `lmodType`

structure.

Does any of you have an opinion on that subject ?

Am I missing a Lemma saying that the complement of set0 is setT ? I dont find it in classical set

it seems so, here is a proposal: https://github.com/math-comp/analysis/pull/178

Thanks for the pr and merge !

I opened another pr : https://github.com/math-comp/analysis/pull/184 I'm less confident in it, there are a lot of split.

I have a maths question : is `<=`

a lattice ? in mathcomp it's not a subtype of lattice, and I'm not familiar with lattice, but it looks a lot like intersection and union may be meet and join in a top bottom lattice, maybe a distributed one

I had to prove that `A '<=' A | B`

and it looks a lot like `a <= max a b`

actually the wikipedia page answers it

I created another PR : https://github.com/math-comp/analysis/pull/186 I don't know if boolean reflection is the best way, I didn't find the exact demorgan law in boolp.

There has a substantial merge on master (of PR https://github.com/math-comp/analysis/pull/175), following the release of MathComp 1.11.0+beta1. It is documented here https://hal.inria.fr/hal-02463336v2/document.

You can enjoy better notations and more general lemmas but there might be unforeseen issues. Does not hesitate to report them here or on github. Thank you.

@Cyril Cohen is it reasoanble to assign PR #176 to milestone 0.3?

Yes, actually I am in favor of releasing 0.3.0 asap and working on 0.3.1 if needed

cool (I meant #177 of course)

I have a math question : in meetjoin theory , the mixin is built using a less or equal relation, and also a less than relation. Is there an exemple where the less than could not be deduced from less than ? An obligation of the mixin is to prove than less than is less or equal + not equal

https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/order.v#L4165

@vlj, yes, logically speaking, it can always be inferred thanks to the equation you cited. However, in some cases it is convenient to be able to choose another one. For example, for natural numbers, defining `lt`

as `ltn`

(where `ltn m n := (m.+1 <= n)`

) makes `(m <= n)%O`

convertible to `(m < n)%N`

.

![image.png](https://files.gitter.im/math-comp/analysis/d1rx/thumb/image.png)

We need to commit something! ;-)

Let's keep it that way :laughing:

I can't find lemmas on the monotonicity of limits (if f bounded by M, then lim f <= M). Are they missing or maybe I don't have the right keyword ?

Hi Marie, I think they are WIP in the sequence branch, and not general enough...

(yet)

thanks !

I can't find lemmas on the monotonicity of limits (if f bounded by M, then lim f <= M). Are they missing or maybe I don't have the right keyword ?

this one is for real numbers: https://github.com/math-comp/analysis/blob/mathcomp_master_sequences/theories/sequences.v#L561-L563

Last updated: Feb 09 2023 at 03:06 UTC