## Stream: math-comp analysis

### Topic: imported from gitter room math-comp/analysis

Hello!

こんにちは

#### Cyril Cohen (Dec 13 2018 at 10:42):

does this mean "hello world"?

just "hello" :-)

#### Marie Kerjean (Jan 18 2019 at 15:11):

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.

#### Marie Kerjean (Jan 18 2019 at 15:12):

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

#### Reynald Affeldt (Jan 18 2019 at 23:59):

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.

#### Marie Kerjean (Jan 19 2019 at 16:33):

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 !

#### Pierre-Yves Strub (Jan 21 2019 at 09:45):

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

#### Cyril Cohen (Jan 21 2019 at 13:07):

@Pierre-Yves Strub +1

agreed

#### Reynald Affeldt (Jan 28 2019 at 16:13):

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

#### Cyril Cohen (Mar 04 2019 at 17:43):

@affeldt-aist sorry for the late answer

#### Marie Kerjean (May 08 2019 at 19:30):

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 ?

#### Marie Kerjean (May 09 2019 at 11:39):

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

#### Cyril Cohen (May 09 2019 at 11:40):

which version of Coq are you using?

#### Cyril Cohen (May 09 2019 at 11:40):

sorry, which version of mathcomp

#### Marie Kerjean (May 09 2019 at 13:48):

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

#### Cyril Cohen (May 09 2019 at 14:37):

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

#### Marie Kerjean (May 23 2019 at 14:27):

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 ?

#### Cyril Cohen (May 23 2019 at 14:33):

add0r for neutrality (on the left) and addrC for commutativity should work, don't they?

#### Cyril Cohen (May 23 2019 at 14:33):

they are in mathcomp.algebra.ssralg

#### Cyril Cohen (May 23 2019 at 14:34):

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

#### Marie Kerjean (May 23 2019 at 14:36):

Thanks, I was missing addrC, lesson learned.

:+1:

#### Marie Kerjean (May 24 2019 at 13:43):

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} ?

#### Cyril Cohen (May 24 2019 at 14:42):

@mkerjean they should coincide

#### Marie Kerjean (May 25 2019 at 20:19):

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 ?

#### Marie Kerjean (May 25 2019 at 20:27):

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

#### Cyril Cohen (May 27 2019 at 07:32):

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

Yes but you can reuse the proof

#### Marie Kerjean (May 27 2019 at 19:28):

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

#### Cyril Cohen (May 28 2019 at 09:28):

@mkerjean can you show me?

#### Marie Kerjean (May 28 2019 at 10:31):

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

#### Marie Kerjean (May 28 2019 at 10:32):

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

which line?

#### Cyril Cohen (May 28 2019 at 10:56):

do you want to skype quickly?

#### Marie Kerjean (May 28 2019 at 11:29):

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

ok

#### Marie Kerjean (May 28 2019 at 11:34):

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 ?

#### Marie Kerjean (May 28 2019 at 11:35):

(line 144 vs line 82 in the file)

#### Cyril Cohen (May 28 2019 at 12:02):

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: ...

#### Cyril Cohen (May 28 2019 at 12:03):

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

#### Cyril Cohen (May 28 2019 at 12:04):

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 :-/

#### Cyril Cohen (May 28 2019 at 12:05):

When F = M = R everything has the same type...

#### Cyril Cohen (May 28 2019 at 12:06):

to use normm lemmas on R one has to annotate it like this R^o

#### Cyril Cohen (May 28 2019 at 12:07):

(line 144 vs line 82 in the file)

I cannot compile line 82 :-/

#### Cyril Cohen (May 28 2019 at 12:15):

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.

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.


#### Marie Kerjean (May 28 2019 at 13:06):

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

#### Marie Kerjean (May 28 2019 at 13:06):

Ok now I see your code

#### Marie Kerjean (May 28 2019 at 13:07):

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

#### Cyril Cohen (May 28 2019 at 14:09):

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...

#### Marie Kerjean (May 29 2019 at 15:34):

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 ?

#### Marie Kerjean (May 29 2019 at 15:36):

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.

#### Reynald Affeldt (May 29 2019 at 15:57):

Maybe the lemma ler_lt_trans?

#### Cyril Cohen (May 29 2019 at 16:00):

@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

#### Cyril Cohen (May 29 2019 at 16:01):

Maybe the lemma ler_lt_trans?

That would have been my answer as well.

#### Marie Kerjean (May 29 2019 at 16:03):

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

#### Marie Kerjean (Jun 11 2019 at 09:34):

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.

#### Marie Kerjean (Jun 11 2019 at 09:37):

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


#### Cyril Cohen (Jun 12 2019 at 11:21):

Hi @mkerjean, I do not understand locally_restricted, where does it come from? Did you try to use within?

#### Marie Kerjean (Jun 12 2019 at 11:32):

@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.

#### Cyril Cohen (Jun 12 2019 at 13:19):

@mkerjean you understand how to use it now?

#### Marie Kerjean (Jun 12 2019 at 22:43):

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

#### Cyril Cohen (Jul 01 2019 at 14:44):

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

#### Marie Kerjean (Jul 02 2019 at 14:06):

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.

#### Cyril Cohen (Jul 02 2019 at 21:47):

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.

#### Cyril Cohen (Jul 02 2019 at 21:47):

thanks for signaling

#### Marie Kerjean (Jul 03 2019 at 06:41):

@Cyril Cohen It's working, merci beaucoup !

#### Assia Mahboubi (Jul 03 2019 at 07:52):

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

#### Assia Mahboubi (Jul 03 2019 at 07:53):

I mean, how to upgrade nixpkgs.

#### Cyril Cohen (Jul 03 2019 at 09:49):

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)

#### Assia Mahboubi (Jul 03 2019 at 10:16):

Why changing this commit did solve Marie's issue?

#### Cyril Cohen (Jul 03 2019 at 10:27):

Why changing this commit did solve Marie's issue?

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

#### Assia Mahboubi (Jul 03 2019 at 11:58):

How did you add real-closed to nixpgs?

#### Cyril Cohen (Jul 03 2019 at 12:33):

How did you add real-closed to nixpgs?

#### Marie Kerjean (Jul 08 2019 at 19:20):

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").

#### Assia Mahboubi (Jul 10 2019 at 09:43):

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

#### Florent Hivert (Jul 10 2019 at 12:16):

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

#### Assia Mahboubi (Jul 10 2019 at 12:20):

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?

#### Florent Hivert (Jul 10 2019 at 13:21):

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

But got:

#### Florent Hivert (Jul 10 2019 at 13:22):

The following dependencies couldn't be met:

- coq-mathcomp-analysis -> coq-mathcomp-field < 1.9.0~
no matching version
At step 3.

#### Reynald Affeldt (Jul 10 2019 at 14:36):

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

#### Reynald Affeldt (Jul 10 2019 at 14:42):

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

#### Florent Hivert (Jul 10 2019 at 14:45):

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

#### Florent Hivert (Jul 10 2019 at 14:45):

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

O_O

#### Florent Hivert (Jul 10 2019 at 14:47):

Now trying : opam install coq-mathcomp-ssreflect

#### Florent Hivert (Jul 10 2019 at 14:47):

- install coq-mathcomp-ssreflect dev

#### Reynald Affeldt (Jul 10 2019 at 14:48):

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

#### Reynald Affeldt (Jul 10 2019 at 14:50):

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

#### Florent Hivert (Jul 10 2019 at 14:50):

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

#### Reynald Affeldt (Jul 10 2019 at 14:50):

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

#### Reynald Affeldt (Jul 10 2019 at 14:51):

(but maybe you know all that)

#### Reynald Affeldt (Jul 10 2019 at 14:51):

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

#### Florent Hivert (Jul 10 2019 at 14:52):

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

#### Reynald Affeldt (Jul 10 2019 at 14:52):

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

#### Florent Hivert (Jul 10 2019 at 14:52):

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

#### Florent Hivert (Jul 10 2019 at 14:53):

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

#### Reynald Affeldt (Jul 10 2019 at 14:53):

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

#### Florent Hivert (Jul 10 2019 at 14:53):

Waiting some compilation to finish...

ah!

#### Reynald Affeldt (Jul 10 2019 at 14:59):

maybe this would be better

#### Florent Hivert (Jul 10 2019 at 15:01):

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

#### Reynald Affeldt (Jul 10 2019 at 15:03):

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

#### Florent Hivert (Jul 10 2019 at 15:04):

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

#### Reynald Affeldt (Jul 10 2019 at 15:04):

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

#### Florent Hivert (Jul 10 2019 at 15:04):

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

#### Florent Hivert (Jul 10 2019 at 15:05):

Please ignore my PR if you have something better.

#### Florent Hivert (Jul 10 2019 at 15:05):

Anyway, thanks for the help !

#### Marie Kerjean (Aug 20 2019 at 19:23):

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 ?

#### Cyril Cohen (Aug 23 2019 at 08:52):

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 absRingTypeshould 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...

#### Marie Kerjean (Aug 23 2019 at 15:07):

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 ?

#### Marie Kerjean (Aug 28 2019 at 19:17):

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 loctype but not for a topological mixin.

#### Cyril Cohen (Sep 06 2019 at 09:13):

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

#### Marie Kerjean (Sep 06 2019 at 09:26):

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.

#### Cyril Cohen (Sep 06 2019 at 09:26):

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.

#### Cyril Cohen (Sep 06 2019 at 09:29):

@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

#### Cyril Cohen (Sep 06 2019 at 09:29):

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

#### Marie Kerjean (Sep 06 2019 at 09:32):

@Cyril Cohen But uniform's mixin_of departs from this rule of thumb right? It has a locally parameter. (@Assia Mahboubi speaking)

#### Cyril Cohen (Sep 06 2019 at 09:35):

yes indeed, it is an exception

#### Cyril Cohen (Sep 06 2019 at 09:35):

because there is no way of writing the type of the structure that has a loc on itself...

#### Cyril Cohen (Sep 06 2019 at 09:35):

I will give more details

#### Cyril Cohen (Sep 06 2019 at 09:38):

Right now filteredTypeis very particuliar, it is sort of a mix between predTypeand 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

#### Cyril Cohen (Sep 06 2019 at 09:39):

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

#### Cyril Cohen (Sep 06 2019 at 09:40):

(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)

#### Marie Kerjean (Sep 06 2019 at 09:46):

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

#### Marie Kerjean (Sep 11 2019 at 08:31):

I have been working on holomorphic functions, and for this purpose working on the complex typeC (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 ?

#### Cyril Cohen (Sep 12 2019 at 13:18):

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

#### Marie Kerjean (Sep 12 2019 at 13:19):

@Cyril Cohen great, thanks

#### Florent Hivert (Sep 12 2019 at 15:17):

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 ?

#### Cyril Cohen (Sep 12 2019 at 16:57):

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

#### Florent Hivert (Sep 12 2019 at 21:40):

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...

#### Assia Mahboubi (Sep 16 2019 at 08:53):

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.

#### Assia Mahboubi (Sep 16 2019 at 11:41):

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

#### Assia Mahboubi (Sep 16 2019 at 11:42):

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)


#### Assia Mahboubi (Sep 16 2019 at 11:43):

This is blocking for us in the integral-draft branch when we need to import complex. Any hint ?

#### Assia Mahboubi (Sep 16 2019 at 11:49):

Note that trying to have mathcomp-multinomial or mathcomp-coqeal fails as well.

#### Cyril Cohen (Sep 16 2019 at 12:38):

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

#### Assia Mahboubi (Sep 17 2019 at 09:42):

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

#### Cyril Cohen (Sep 17 2019 at 14:44):

I will try now or tomorrow

#### Cyril Cohen (Sep 17 2019 at 15:08):

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

#### Assia Mahboubi (Sep 17 2019 at 15:58):

@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.

#### Assia Mahboubi (Sep 17 2019 at 15:59):

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

#### Assia Mahboubi (Sep 17 2019 at 16:01):

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?

#### Assia Mahboubi (Sep 17 2019 at 16:03):

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.

#### Gaëtan Gilbert (Sep 17 2019 at 16:50):

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

#### Cyril Cohen (Sep 17 2019 at 16:53):

@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...

#### Cyril Cohen (Sep 17 2019 at 16:53):

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

#### Cyril Cohen (Sep 17 2019 at 16:56):

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

#### Cyril Cohen (Sep 17 2019 at 17:01):

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

So do I

#### Théo Zimmermann (Sep 17 2019 at 17:21):

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.

#### Théo Zimmermann (Sep 17 2019 at 17:21):

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

#### Théo Zimmermann (Sep 17 2019 at 17:22):

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.

#### Théo Zimmermann (Sep 17 2019 at 17:23):

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

#### Cyril Cohen (Sep 17 2019 at 17:33):

@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

#### Cyril Cohen (Sep 17 2019 at 17:33):

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

#### Reynald Affeldt (Sep 18 2019 at 02:13):

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
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)
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


#### Cyril Cohen (Sep 18 2019 at 08:31):

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

#### Reynald Affeldt (Sep 18 2019 at 08:50):

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

#### Pierre-Yves Strub (Sep 26 2019 at 13:50):

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

#### Pierre-Yves Strub (Sep 26 2019 at 13:51):

dev is not working, mathcomp is incompatible with finmap 1.2

#### Pierre-Yves Strub (Sep 26 2019 at 13:51):

Are we stuck with mathcomp 1.8 ?

#### Pierre-Yves Strub (Sep 26 2019 at 13:52):

Ah sorry, 1.2.1 seems to be the solution

#### Reynald Affeldt (Sep 26 2019 at 15:20):

compiles with mathcomp 1.9 (and Coq 8.10beta3)

#### Pierre-Yves Strub (Sep 26 2019 at 15:25):

The problem was finmap.dev

#### Assia Mahboubi (Sep 27 2019 at 07:45):

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.

#### Reynald Affeldt (Sep 27 2019 at 09:29):

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

#### Cyril Cohen (Oct 02 2019 at 11:32):

@Pierre-Yves Strub

The problem was finmap.dev

#### Cyril Cohen (Oct 02 2019 at 11:32):

did I screw up with the dependencies?

#### Cyril Cohen (Oct 02 2019 at 11:33):

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...)

#### Marie Kerjean (Oct 03 2019 at 12:34):

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 ...

#### Pierre-Yves Strub (Oct 03 2019 at 19:01):

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.

#### Pierre-Yves Strub (Oct 03 2019 at 19:03):

I am going to look at multinomials VS finmap

#### Marie Kerjean (Oct 04 2019 at 11:07):

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.

#### Assia Mahboubi (Oct 04 2019 at 22:14):

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

#### Assia Mahboubi (Oct 04 2019 at 22:17):

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.

#### Reynald Affeldt (Oct 05 2019 at 09:30):

We are in the process of removing Require reals from normedType.v.

#### Reynald Affeldt (Oct 05 2019 at 09:31):

Eudoxus reals came after normedType.v was "completed".

#### Pierre-Yves Strub (Oct 05 2019 at 09:32):

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

#### Reynald Affeldt (Oct 05 2019 at 09:37):

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

#### Reynald Affeldt (Oct 05 2019 at 09:48):

Ah, there is Require Reals and Require reals. :-)

#### Pierre-Yves Strub (Oct 05 2019 at 10:16):

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

#### Pierre-Yves Strub (Oct 05 2019 at 10:16):

There is not that much to do.

#### Pierre-Yves Strub (Oct 05 2019 at 10:16):

I plan to be done with it within 2 weeks

#### Marie Kerjean (Oct 05 2019 at 12:50):

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

#### Marie Kerjean (Oct 05 2019 at 12:51):

@Assia Mahboubi thanks for the answers !

#### Reynald Affeldt (Oct 05 2019 at 13:09):

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

#### vlj (Oct 26 2019 at 21:50):

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

#### vlj (Oct 26 2019 at 21:51):

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

#### Damien Rouhling (Oct 28 2019 at 08:03):

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

#### vlj (Oct 29 2019 at 20:30):

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

#### vlj (Oct 29 2019 at 20:31):

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

#### vlj (Oct 29 2019 at 23:07):

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

#### vlj (Oct 29 2019 at 23:11):

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

#### vlj (Oct 29 2019 at 23:12):

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

#### Damien Rouhling (Oct 30 2019 at 07:56):

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.

#### Damien Rouhling (Oct 30 2019 at 08:00):

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

#### vlj (Oct 30 2019 at 20:49):

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

#### vlj (Nov 04 2019 at 22:17):

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

#### vlj (Nov 04 2019 at 22:19):

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

#### vlj (Nov 04 2019 at 22:21):

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).

#### vlj (Nov 04 2019 at 22:21):

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

#### Emilio Jesús Gallego Arias (Nov 05 2019 at 00:42):

@vlj I dunno, this works for me:

#### Emilio Jesús Gallego Arias (Nov 05 2019 at 00:42):

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


#### Florent Hivert (Nov 05 2019 at 07:49):

@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.

#### Damien Rouhling (Nov 05 2019 at 07:50):

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.

#### Damien Rouhling (Nov 05 2019 at 07:53):

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.


#### Assia Mahboubi (Nov 05 2019 at 07:58):

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?

#### Damien Rouhling (Nov 05 2019 at 08:08):

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

#### Cyril Cohen (Nov 05 2019 at 12:23):

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

#### Pierre-Yves Strub (Nov 05 2019 at 12:32):

I can write something with my experience on summability.

#### Pierre-Yves Strub (Nov 05 2019 at 12:32):

And positive stuffs.

#### Pierre-Yves Strub (Nov 05 2019 at 12:32):

Where should we put our stuffs?

#### Cyril Cohen (Nov 05 2019 at 12:33):

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

#### Pierre-Yves Strub (Nov 05 2019 at 12:35):

Any solution will do. Decide, I obey :)

#### Cyril Cohen (Nov 05 2019 at 12:37):

Then a subdirectory

#### vlj (Nov 05 2019 at 17:54):

@Emilio Jesús Gallego Arias thanks !

Is there à

#### vlj (Nov 05 2019 at 18:08):

Docker script to build analysis ?

#### vlj (Nov 05 2019 at 18:09):

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

#### Pierre-Yves Strub (Nov 06 2019 at 05:57):

You can have a look at the travis script

#### Pierre-Yves Strub (Nov 06 2019 at 05:58):

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

Ok

#### Reynald Affeldt (Nov 06 2019 at 13:28):

@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?

#### Damien Rouhling (Nov 06 2019 at 13:30):

oh… we definitely should do some clean up

let me check

:-)

#### Damien Rouhling (Nov 06 2019 at 13:36):

none of the above ! :-)

#### Reynald Affeldt (Nov 06 2019 at 13:36):

I would have said entourages_bigmaxr_mem :-/

#### Damien Rouhling (Nov 06 2019 at 13:37):

the latest code is in uniform-entourages

thanks!

#### vlj (Nov 09 2019 at 18:13):

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

#### Cyril Cohen (Nov 15 2019 at 10:16):

I can write something with my experience on summability.

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

#### vlj (Nov 17 2019 at 00:41):

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

#### vlj (Nov 17 2019 at 00:42):

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


#### vlj (Nov 17 2019 at 00:43):

the [set X] seti means that X = seti and thus goal is solved

#### vlj (Nov 17 2019 at 00:43):

I tried with in_setE or things like that

#### vlj (Nov 17 2019 at 00:50):

[set X] is a notation for set1 X ie [set a : _ | a = X]. but I dont know how to "destruct" set1 X seti

#### Emilio Jesús Gallego Arias (Nov 17 2019 at 05:11):

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

#### Reynald Affeldt (Nov 17 2019 at 08:05):

@vlj Maybe you want to do this

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


#### Reynald Affeldt (Nov 17 2019 at 08:06):

(which can be of course shortened to by move=> -> and furthermore streamlined into the previous line of script)

#### vlj (Nov 17 2019 at 15:34):

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

#### vlj (Nov 17 2019 at 15:36):

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

#### vlj (Nov 17 2019 at 15:37):

the rewrite is not necessary actually

#### Damien Rouhling (Nov 18 2019 at 07:45):

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

#### vlj (Nov 18 2019 at 21:50):

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

#### vlj (Nov 18 2019 at 21:52):

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

#### Reynald Affeldt (Nov 19 2019 at 06:09):

The command Unset Printing Notations reveals what is behind notations.

Thanks

#### vlj (Nov 19 2019 at 12:15):

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

#### vlj (Nov 19 2019 at 12:16):

but actually it showed me that I need to rewrite rewrite /classical_sets.set1and not just rewrite /set1so that's useful.

#### vlj (Nov 19 2019 at 12:51):

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.

#### vlj (Nov 19 2019 at 12:54):

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

#### vlj (Nov 19 2019 at 19:48):

err nvm it works with classical_sets.setT

#### vlj (Nov 19 2019 at 19:49):

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

#### Reynald Affeldt (Nov 19 2019 at 20:12):

maybe Local Open Scope classical_set_scope. ?

Yes

#### vlj (Nov 21 2019 at 17:10):

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.

#### vlj (Nov 21 2019 at 17:13):

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

#### vlj (Nov 21 2019 at 17:15):

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

#### vlj (Nov 21 2019 at 19:16):

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

#### Damien Rouhling (Nov 22 2019 at 08:31):

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 Fto be of type set B which makes preimage_bigsetU not very interesting: when P is non-empty, \bigcup_(i in P) F = Fso this lemma almost just states that g @^-1 F = g @^-1 F

#### vlj (Nov 22 2019 at 21:13):

Ho yes you're right

#### vlj (Nov 22 2019 at 21:35):

I though F was a type in the notation indeed

#### vlj (Nov 26 2019 at 21:26):

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

#### vlj (Nov 26 2019 at 21:38):

Ssrnum has a sqrt but not for nat

#### Reynald Affeldt (Dec 05 2019 at 17:29):

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)

#### vlj (Dec 09 2019 at 22:40):

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

#### vlj (Dec 09 2019 at 22:41):

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

#### vlj (Dec 09 2019 at 22:42):

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

#### vlj (Dec 09 2019 at 22:42):

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

#### Assia Mahboubi (Dec 10 2019 at 07:38):

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.

#### Pierre-Yves Strub (Dec 10 2019 at 07:42):

S.t. n >= i * i, no ?

Yes, sorry

#### Assia Mahboubi (Dec 10 2019 at 14:55):

@vlj, what about using ex_maxn as provided in ssrnat?

#### Assia Mahboubi (Dec 10 2019 at 14:55):

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

#### vlj (Dec 10 2019 at 21:24):

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

#### vlj (Dec 10 2019 at 21:24):

Using what you suggest is probably better

#### zstone1 (Gitter import) (Jan 07 2020 at 01:01):

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).

#### Reynald Affeldt (Jan 07 2020 at 09:48):

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

#### Reynald Affeldt (Jan 07 2020 at 09:54):

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

#### Reynald Affeldt (Jan 07 2020 at 09:55):

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

#### Bas Spitters (Jan 07 2020 at 12:45):

@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.

#### zstone1 (Gitter import) (Jan 07 2020 at 15:41):

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?

#### zstone1 (Gitter import) (Jan 07 2020 at 15:46):

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.

#### Reynald Affeldt (Jan 07 2020 at 16:59):

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!

#### Bas Spitters (Jan 07 2020 at 17:19):

@zstone1 yes, these libraries use eps-delta.
In any case, it's nice to see some complex analysis. Is this your PhD-project?

#### Marie Kerjean (Jan 07 2020 at 18:52):

@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 !

#### zstone1 (Gitter import) (Jan 08 2020 at 00:35):

@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.

#### zstone1 (Gitter import) (Jan 11 2020 at 00:57):

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?

#### Marie Kerjean (Jan 11 2020 at 07:14):

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.

#### Cyril Cohen (Jan 29 2020 at 23:36):

@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.

#### Marie Kerjean (Feb 05 2020 at 19:31):

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 ) ?

#### Cyril Cohen (Feb 05 2020 at 21:13):

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

#### Marie Kerjean (Feb 06 2020 at 09:32):

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

#### Marie Kerjean (Feb 11 2020 at 19:38):

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 ) ?

#### vlj (Mar 06 2020 at 21:47):

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 ?

#### Paolo Giarrusso (Mar 06 2020 at 21:51):

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

#### Paolo Giarrusso (Mar 06 2020 at 21:52):

(but never used any of the other ones)

#### vlj (Mar 06 2020 at 22:21):

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

It's a good new

#### vlj (Mar 06 2020 at 22:24):

There is a zify like mecanism

#### Emilio Jesús Gallego Arias (Mar 07 2020 at 00:39):

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

#### vlj (Mar 08 2020 at 16:43):

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

#### Emilio Jesús Gallego Arias (Mar 08 2020 at 20:09):

I think you need something higher, such as numField

#### Cyril Cohen (Mar 09 2020 at 09:36):

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

Sure!

#### vlj (Apr 05 2020 at 21:08):

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

#### vlj (Apr 05 2020 at 21:09):

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

#### vlj (Apr 05 2020 at 21:10):

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

#### Cyril Cohen (Apr 05 2020 at 22:49):

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

#### vlj (Apr 05 2020 at 23:10):

Yes, that's where I found ssring.

#### vlj (Apr 05 2020 at 23:11):

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

#### vlj (Apr 06 2020 at 17:29):

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

#### vlj (Apr 06 2020 at 17:31):

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

#### vlj (Apr 06 2020 at 20:49):

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

#### vlj (Apr 06 2020 at 20:52):

eg coarser topology

#### vlj (Apr 08 2020 at 18:26):

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

#### vlj (Apr 08 2020 at 18:27):

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

#### vlj (Apr 11 2020 at 17:07):

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)

#### Marie Kerjean (Apr 12 2020 at 19:43):

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.

#### Marie Kerjean (Apr 12 2020 at 19:43):

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.

#### Marie Kerjean (Apr 12 2020 at 19:45):

The solution would be the creation of an copy of the structure numField endowed by inheritance with a lmodType structure.

#### Marie Kerjean (Apr 12 2020 at 19:45):

Does any of you have an opinion on that subject ?

#### vlj (Apr 12 2020 at 21:47):

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

#### Reynald Affeldt (Apr 13 2020 at 17:26):

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

#### vlj (Apr 14 2020 at 17:28):

Thanks for the pr and merge !

#### vlj (Apr 16 2020 at 18:35):

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

#### vlj (Apr 20 2020 at 20:27):

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

#### vlj (Apr 20 2020 at 20:28):

I had to prove that A '<=' A | B and it looks a lot like a <= max a b

#### vlj (Apr 20 2020 at 21:21):

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.

#### Reynald Affeldt (Apr 24 2020 at 16:05):

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.

#### Reynald Affeldt (Apr 24 2020 at 16:07):

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.

#### Reynald Affeldt (Apr 27 2020 at 11:35):

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

#### Cyril Cohen (Apr 27 2020 at 12:42):

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

#### Reynald Affeldt (Apr 27 2020 at 12:51):

cool (I meant #177 of course)

#### vlj (Apr 29 2020 at 20:55):

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

#### vlj (Apr 29 2020 at 20:56):

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

#### Cyril Cohen (Apr 30 2020 at 00:35):

@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.

#### Reynald Affeldt (Apr 30 2020 at 15:10):

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

#### Reynald Affeldt (Apr 30 2020 at 15:10):

We need to commit something! ;-)

#### Cyril Cohen (Apr 30 2020 at 17:26):

Let's keep it that way :laughing:

#### Marie Kerjean (May 01 2020 at 14:56):

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 ?

#### Cyril Cohen (May 01 2020 at 16:59):

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

(yet)

thanks !

#### Reynald Affeldt (May 03 2020 at 23:23):

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: Aug 11 2022 at 02:03 UTC