Stream: math-comp analysis

Topic: imported from gitter room math-comp/analysis


view this post on Zulip Cyril Cohen (Dec 12 2018 at 08:42):

Hello!

view this post on Zulip Reynald Affeldt (Dec 12 2018 at 08:42):

こんにちは

view this post on Zulip Cyril Cohen (Dec 13 2018 at 10:42):

does this mean "hello world"?

view this post on Zulip Reynald Affeldt (Dec 13 2018 at 12:31):

just "hello" :-)

view this post on Zulip 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.

view this post on Zulip Marie Kerjean (Jan 18 2019 at 15:12):

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

view this post on Zulip 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.

view this post on Zulip 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 !

view this post on Zulip 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.

view this post on Zulip Cyril Cohen (Jan 21 2019 at 13:07):

@Pierre-Yves Strub +1

view this post on Zulip Reynald Affeldt (Jan 21 2019 at 13:19):

agreed

view this post on Zulip 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?

view this post on Zulip Cyril Cohen (Mar 04 2019 at 17:43):

@affeldt-aist sorry for the late answer

view this post on Zulip 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 ?

view this post on Zulip 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.

view this post on Zulip Cyril Cohen (May 09 2019 at 11:40):

which version of Coq are you using?

view this post on Zulip Cyril Cohen (May 09 2019 at 11:40):

sorry, which version of mathcomp

view this post on Zulip 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 ?

view this post on Zulip Cyril Cohen (May 09 2019 at 14:37):

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

view this post on Zulip 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 ?

view this post on Zulip Cyril Cohen (May 23 2019 at 14:33):

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

view this post on Zulip Cyril Cohen (May 23 2019 at 14:33):

they are in mathcomp.algebra.ssralg

view this post on Zulip Cyril Cohen (May 23 2019 at 14:34):

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

view this post on Zulip Marie Kerjean (May 23 2019 at 14:36):

Thanks, I was missing addrC, lesson learned.

view this post on Zulip Cyril Cohen (May 23 2019 at 14:36):

:+1:

view this post on Zulip 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} ?

view this post on Zulip Cyril Cohen (May 24 2019 at 14:42):

@mkerjean they should coincide

view this post on Zulip 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 ?

view this post on Zulip Marie Kerjean (May 25 2019 at 20:27):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Cyril Cohen (May 28 2019 at 09:28):

@mkerjean can you show me?

view this post on Zulip 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 ?

view this post on Zulip 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

view this post on Zulip Cyril Cohen (May 28 2019 at 10:56):

which line?

view this post on Zulip Cyril Cohen (May 28 2019 at 10:56):

do you want to skype quickly?

view this post on Zulip Marie Kerjean (May 28 2019 at 11:29):

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

view this post on Zulip Cyril Cohen (May 28 2019 at 11:29):

ok

view this post on Zulip 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 ?

view this post on Zulip Marie Kerjean (May 28 2019 at 11:35):

(line 144 vs line 82 in the file)

view this post on Zulip 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: ...

view this post on Zulip Cyril Cohen (May 28 2019 at 12:03):

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

view this post on Zulip 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 :-/

view this post on Zulip Cyril Cohen (May 28 2019 at 12:05):

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

view this post on Zulip Cyril Cohen (May 28 2019 at 12:06):

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

view this post on Zulip Cyril Cohen (May 28 2019 at 12:07):

(line 144 vs line 82 in the file)

I cannot compile line 82 :-/

view this post on Zulip 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.
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.

view this post on Zulip 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

view this post on Zulip Marie Kerjean (May 28 2019 at 13:06):

Ok now I see your code

view this post on Zulip 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 ?

view this post on Zulip 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...

view this post on Zulip 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 ?

view this post on Zulip 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.

view this post on Zulip Reynald Affeldt (May 29 2019 at 15:57):

Maybe the lemma ler_lt_trans?

view this post on Zulip 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

view this post on Zulip Cyril Cohen (May 29 2019 at 16:01):

Maybe the lemma ler_lt_trans?

That would have been my answer as well.

view this post on Zulip Marie Kerjean (May 29 2019 at 16:03):

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

view this post on Zulip 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.

view this post on Zulip 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)).

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Cyril Cohen (Jun 12 2019 at 13:19):

@mkerjean you understand how to use it now?

view this post on Zulip Marie Kerjean (Jun 12 2019 at 22:43):

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

view this post on Zulip Cyril Cohen (Jul 01 2019 at 14:44):

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

view this post on Zulip Marie Kerjean (Jul 02 2019 at 10:02):

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

view this post on 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.

view this post on Zulip 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.

view this post on Zulip Cyril Cohen (Jul 02 2019 at 21:47):

thanks for signaling

view this post on Zulip Marie Kerjean (Jul 03 2019 at 06:41):

@Cyril Cohen It's working, merci beaucoup !

view this post on Zulip Assia Mahboubi (Jul 03 2019 at 07:52):

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

view this post on Zulip Assia Mahboubi (Jul 03 2019 at 07:53):

I mean, how to upgrade nixpkgs.

view this post on Zulip 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)

view this post on Zulip Assia Mahboubi (Jul 03 2019 at 10:16):

Why changing this commit did solve Marie's issue?

view this post on Zulip 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

view this post on Zulip Assia Mahboubi (Jul 03 2019 at 11:58):

How did you add real-closed to nixpgs?

view this post on Zulip Cyril Cohen (Jul 03 2019 at 12:33):

How did you add real-closed to nixpgs?

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

view this post on Zulip 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").

view this post on Zulip 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?

view this post on Zulip 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...

view this post on Zulip 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?

view this post on Zulip Florent Hivert (Jul 10 2019 at 13:21):

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

view this post on Zulip Florent Hivert (Jul 10 2019 at 13:22):

But got:

view this post on Zulip 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.

view this post on Zulip 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...)

view this post on Zulip Reynald Affeldt (Jul 10 2019 at 14:42):

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

view this post on Zulip Florent Hivert (Jul 10 2019 at 14:45):

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

view this post on Zulip Florent Hivert (Jul 10 2019 at 14:45):

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

view this post on Zulip Reynald Affeldt (Jul 10 2019 at 14:47):

O_O

view this post on Zulip Florent Hivert (Jul 10 2019 at 14:47):

Now trying : opam install coq-mathcomp-ssreflect

view this post on Zulip Florent Hivert (Jul 10 2019 at 14:47):

- install coq-mathcomp-ssreflect dev

view this post on Zulip 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...

view this post on Zulip Reynald Affeldt (Jul 10 2019 at 14:50):

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

view this post on Zulip Florent Hivert (Jul 10 2019 at 14:50):

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

view this post on Zulip Reynald Affeldt (Jul 10 2019 at 14:50):

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

view this post on Zulip Reynald Affeldt (Jul 10 2019 at 14:51):

(but maybe you know all that)

view this post on Zulip Reynald Affeldt (Jul 10 2019 at 14:51):

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

view this post on Zulip Florent Hivert (Jul 10 2019 at 14:52):

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

view this post on Zulip 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 :-)

view this post on Zulip Florent Hivert (Jul 10 2019 at 14:52):

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

view this post on Zulip Florent Hivert (Jul 10 2019 at 14:53):

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

view this post on Zulip 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

view this post on Zulip Florent Hivert (Jul 10 2019 at 14:53):

Waiting some compilation to finish...

view this post on Zulip Florent Hivert (Jul 10 2019 at 14:55):

millsmess-~ $ opam info coq-mathcomp-analysis

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

<><> Version-specific details <><><><><><><><><><><><><><><><><><><><><><><><><>
[...]

view this post on Zulip Florent Hivert (Jul 10 2019 at 14:55):

Only the dev version is accessible...

view this post on Zulip Reynald Affeldt (Jul 10 2019 at 14:56):

(just to check: opam --version?)

view this post on Zulip Florent Hivert (Jul 10 2019 at 14:56):

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

view this post on Zulip Reynald Affeldt (Jul 10 2019 at 14:57):

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

view this post on Zulip Florent Hivert (Jul 10 2019 at 14:57):

It seem to be related to

view this post on Zulip Florent Hivert (Jul 10 2019 at 14:57):

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

view this post on Zulip Reynald Affeldt (Jul 10 2019 at 14:58):

ah!

view this post on Zulip Reynald Affeldt (Jul 10 2019 at 14:59):

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

view this post on Zulip Reynald Affeldt (Jul 10 2019 at 14:59):

maybe this would be better

view this post on Zulip 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

view this post on Zulip Reynald Affeldt (Jul 10 2019 at 15:03):

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

view this post on Zulip Florent Hivert (Jul 10 2019 at 15:04):

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

view this post on Zulip Reynald Affeldt (Jul 10 2019 at 15:04):

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

view this post on Zulip Florent Hivert (Jul 10 2019 at 15:04):

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

view this post on Zulip Florent Hivert (Jul 10 2019 at 15:05):

Please ignore my PR if you have something better.

view this post on Zulip Florent Hivert (Jul 10 2019 at 15:05):

Anyway, thanks for the help !

view this post on Zulip Reynald Affeldt (Jul 10 2019 at 15:05):

Thanks for your patience!

view this post on Zulip 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 ?

view this post on Zulip 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...

view this post on Zulip 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 ?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Cyril Cohen (Sep 06 2019 at 09:35):

yes indeed, it is an exception

view this post on Zulip 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...

view this post on Zulip Cyril Cohen (Sep 06 2019 at 09:35):

I will give more details

view this post on Zulip 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

view this post on Zulip 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))

view this post on Zulip 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)

view this post on Zulip Marie Kerjean (Sep 06 2019 at 09:46):

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

view this post on Zulip 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 ?

view this post on Zulip 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.

view this post on Zulip Marie Kerjean (Sep 12 2019 at 13:19):

@Cyril Cohen great, thanks

view this post on Zulip 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 ?

view this post on Zulip Cyril Cohen (Sep 12 2019 at 16:57):

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

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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 ?

view this post on Zulip Assia Mahboubi (Sep 16 2019 at 11:49):

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

view this post on Zulip 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

view this post on Zulip Assia Mahboubi (Sep 17 2019 at 09:42):

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

view this post on Zulip Cyril Cohen (Sep 17 2019 at 14:44):

I will try now or tomorrow

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Assia Mahboubi (Sep 17 2019 at 15:59):

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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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...

view this post on Zulip 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

view this post on Zulip 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...

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Cyril Cohen (Sep 17 2019 at 17:33):

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

view this post on Zulip 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
                                 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

view this post on Zulip Cyril Cohen (Sep 18 2019 at 08:31):

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

view this post on Zulip Reynald Affeldt (Sep 18 2019 at 08:50):

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

view this post on Zulip 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 ?

view this post on Zulip Pierre-Yves Strub (Sep 26 2019 at 13:51):

dev is not working, mathcomp is incompatible with finmap 1.2

view this post on Zulip Pierre-Yves Strub (Sep 26 2019 at 13:51):

Are we stuck with mathcomp 1.8 ?

view this post on Zulip Pierre-Yves Strub (Sep 26 2019 at 13:52):

Ah sorry, 1.2.1 seems to be the solution

view this post on Zulip Reynald Affeldt (Sep 26 2019 at 15:20):

compiles with mathcomp 1.9 (and Coq 8.10beta3)

view this post on Zulip Pierre-Yves Strub (Sep 26 2019 at 15:25):

The problem was finmap.dev

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Cyril Cohen (Oct 02 2019 at 11:32):

@Pierre-Yves Strub

The problem was finmap.dev

view this post on Zulip Cyril Cohen (Oct 02 2019 at 11:32):

did I screw up with the dependencies?

view this post on Zulip 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...)

view this post on Zulip 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 ...

view this post on Zulip 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.

view this post on Zulip Pierre-Yves Strub (Oct 03 2019 at 19:03):

I am going to look at multinomials VS finmap

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Reynald Affeldt (Oct 05 2019 at 09:30):

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

view this post on Zulip Reynald Affeldt (Oct 05 2019 at 09:31):

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

view this post on Zulip 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?

view this post on Zulip Reynald Affeldt (Oct 05 2019 at 09:37):

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

view this post on Zulip Reynald Affeldt (Oct 05 2019 at 09:48):

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

view this post on Zulip Pierre-Yves Strub (Oct 05 2019 at 10:16):

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

view this post on Zulip Pierre-Yves Strub (Oct 05 2019 at 10:16):

There is not that much to do.

view this post on Zulip Pierre-Yves Strub (Oct 05 2019 at 10:16):

I plan to be done with it within 2 weeks

view this post on Zulip Marie Kerjean (Oct 05 2019 at 12:50):

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

view this post on Zulip Marie Kerjean (Oct 05 2019 at 12:51):

@Assia Mahboubi thanks for the answers !

view this post on Zulip 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

view this post on Zulip vlj (Oct 26 2019 at 21:50):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Cyril Cohen (Oct 28 2019 at 10:46):

:thumbsup:

view this post on Zulip vlj (Oct 29 2019 at 20:28):

Ok

view this post on Zulip 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

view this post on Zulip vlj (Oct 29 2019 at 20:31):

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

view this post on Zulip vlj (Oct 29 2019 at 23:07):

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

view this post on Zulip 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

view this post on Zulip 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 ?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip vlj (Oct 30 2019 at 20:49):

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

view this post on Zulip vlj (Nov 04 2019 at 22:17):

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

view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Nov 05 2019 at 00:42):

@vlj I dunno, this works for me:

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Damien Rouhling (Nov 05 2019 at 08:08):

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

view this post on Zulip Cyril Cohen (Nov 05 2019 at 12:23):

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

view this post on Zulip Pierre-Yves Strub (Nov 05 2019 at 12:32):

I can write something with my experience on summability.

view this post on Zulip Pierre-Yves Strub (Nov 05 2019 at 12:32):

And positive stuffs.

view this post on Zulip Pierre-Yves Strub (Nov 05 2019 at 12:32):

Where should we put our stuffs?

view this post on Zulip Cyril Cohen (Nov 05 2019 at 12:33):

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

view this post on Zulip Pierre-Yves Strub (Nov 05 2019 at 12:35):

Any solution will do. Decide, I obey :)

view this post on Zulip Cyril Cohen (Nov 05 2019 at 12:37):

Then a subdirectory

view this post on Zulip vlj (Nov 05 2019 at 17:54):

@Emilio Jesús Gallego Arias thanks !

view this post on Zulip vlj (Nov 05 2019 at 18:07):

Is there à

view this post on Zulip vlj (Nov 05 2019 at 18:08):

Docker script to build analysis ?

view this post on Zulip vlj (Nov 05 2019 at 18:09):

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

view this post on Zulip Pierre-Yves Strub (Nov 06 2019 at 05:57):

You can have a look at the travis script

view this post on Zulip Pierre-Yves Strub (Nov 06 2019 at 05:58):

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

view this post on Zulip vlj (Nov 06 2019 at 08:03):

Ok

view this post on Zulip 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?

view this post on Zulip Damien Rouhling (Nov 06 2019 at 13:30):

oh… we definitely should do some clean up

view this post on Zulip Damien Rouhling (Nov 06 2019 at 13:30):

let me check

view this post on Zulip Reynald Affeldt (Nov 06 2019 at 13:31):

:-)

view this post on Zulip Damien Rouhling (Nov 06 2019 at 13:36):

none of the above ! :-)

view this post on Zulip Reynald Affeldt (Nov 06 2019 at 13:36):

I would have said entourages_bigmaxr_mem :-/

view this post on Zulip Damien Rouhling (Nov 06 2019 at 13:37):

the latest code is in uniform-entourages

view this post on Zulip Reynald Affeldt (Nov 06 2019 at 13:38):

thanks!

view this post on Zulip vlj (Nov 09 2019 at 18:13):

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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip vlj (Nov 17 2019 at 00:43):

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

view this post on Zulip vlj (Nov 17 2019 at 00:43):

I tried with in_setE or things like that

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Nov 17 2019 at 05:11):

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

view this post on Zulip Reynald Affeldt (Nov 17 2019 at 08:05):

@vlj Maybe you want to do this

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

view this post on Zulip 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)

view this post on Zulip vlj (Nov 17 2019 at 15:34):

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

view this post on Zulip vlj (Nov 17 2019 at 15:36):

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

view this post on Zulip vlj (Nov 17 2019 at 15:37):

the rewrite is not necessary actually

view this post on Zulip 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<-.

view this post on Zulip vlj (Nov 18 2019 at 21:46):

Thanks

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Reynald Affeldt (Nov 19 2019 at 06:09):

The command Unset Printing Notations reveals what is behind notations.

view this post on Zulip vlj (Nov 19 2019 at 08:01):

Thanks

view this post on Zulip vlj (Nov 19 2019 at 12:15):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip vlj (Nov 19 2019 at 12:54):

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

view this post on Zulip vlj (Nov 19 2019 at 19:48):

err nvm it works with classical_sets.setT

view this post on Zulip 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

view this post on Zulip Reynald Affeldt (Nov 19 2019 at 20:12):

maybe Local Open Scope classical_set_scope. ?

view this post on Zulip vlj (Nov 20 2019 at 11:37):

Yes

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip vlj (Nov 21 2019 at 19:16):

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

view this post on Zulip 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

view this post on Zulip vlj (Nov 22 2019 at 21:13):

Ho yes you're right

view this post on Zulip vlj (Nov 22 2019 at 21:35):

I though F was a type in the notation indeed

view this post on Zulip 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

view this post on Zulip vlj (Nov 26 2019 at 21:38):

Ssrnum has a sqrt but not for nat

view this post on Zulip 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)

view this post on Zulip vlj (Dec 09 2019 at 22:40):

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

view this post on Zulip vlj (Dec 09 2019 at 22:41):

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

view this post on Zulip 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

view this post on Zulip vlj (Dec 09 2019 at 22:42):

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

view this post on Zulip 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.

view this post on Zulip Pierre-Yves Strub (Dec 10 2019 at 07:42):

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

view this post on Zulip Assia Mahboubi (Dec 10 2019 at 08:45):

Yes, sorry

view this post on Zulip Assia Mahboubi (Dec 10 2019 at 14:55):

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

view this post on Zulip 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.

view this post on Zulip vlj (Dec 10 2019 at 21:22):

I can give a try

view this post on Zulip 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

view this post on Zulip vlj (Dec 10 2019 at 21:24):

Using what you suggest is probably better

view this post on Zulip 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).

view this post on Zulip Reynald Affeldt (Jan 07 2020 at 09:48):

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

view this post on Zulip 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

view this post on Zulip Reynald Affeldt (Jan 07 2020 at 09:55):

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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip 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?

view this post on Zulip 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 !

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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 ) ?

view this post on Zulip 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

view this post on Zulip Marie Kerjean (Feb 06 2020 at 09:32):

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

view this post on Zulip 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 ) ?

view this post on Zulip 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 ?

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Mar 06 2020 at 21:52):

(but never used any of the other ones)

view this post on Zulip vlj (Mar 06 2020 at 22:21):

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

view this post on Zulip vlj (Mar 06 2020 at 22:22):

It's a good new

view this post on Zulip vlj (Mar 06 2020 at 22:24):

There is a zify like mecanism

view this post on Zulip 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 )

view this post on Zulip vlj (Mar 08 2020 at 16:43):

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 08 2020 at 20:09):

I think you need something higher, such as numField

view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip vlj (Apr 05 2020 at 21:08):

#11998 in coq

view this post on Zulip 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

view this post on Zulip 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 ?

view this post on Zulip 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

view this post on Zulip vlj (Apr 05 2020 at 23:10):

Yes, that's where I found ssring.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip vlj (Apr 06 2020 at 17:31):

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

view this post on Zulip vlj (Apr 06 2020 at 20:49):

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

view this post on Zulip vlj (Apr 06 2020 at 20:52):

eg coarser topology

view this post on Zulip vlj (Apr 08 2020 at 18:26):

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

view this post on Zulip vlj (Apr 08 2020 at 18:27):

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

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Marie Kerjean (Apr 12 2020 at 19:45):

Does any of you have an opinion on that subject ?

view this post on Zulip 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

view this post on Zulip Reynald Affeldt (Apr 13 2020 at 17:26):

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

view this post on Zulip vlj (Apr 14 2020 at 17:28):

Thanks for the pr and merge !

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip vlj (Apr 20 2020 at 20:29):

actually the wikipedia page answers it

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Reynald Affeldt (Apr 27 2020 at 11:35):

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

view this post on Zulip 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

view this post on Zulip Reynald Affeldt (Apr 27 2020 at 12:51):

cool (I meant #177 of course)

view this post on Zulip 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

view this post on Zulip vlj (Apr 29 2020 at 20:56):

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

view this post on Zulip 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.

view this post on Zulip Reynald Affeldt (Apr 30 2020 at 15:10):

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

view this post on Zulip Reynald Affeldt (Apr 30 2020 at 15:10):

We need to commit something! ;-)

view this post on Zulip Cyril Cohen (Apr 30 2020 at 17:26):

Let's keep it that way :laughing:

view this post on Zulip 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 ?

view this post on Zulip Cyril Cohen (May 01 2020 at 16:59):

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

view this post on Zulip Cyril Cohen (May 01 2020 at 16:59):

(yet)

view this post on Zulip Marie Kerjean (May 01 2020 at 17:00):

thanks !

view this post on Zulip 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