Stream: math-comp analysis

Topic: Ongoing work on filters?


view this post on Zulip Julien Puydt (Oct 18 2022 at 07:52):

I saw old PRs on working with filters, but they seem dormant. Is someone still working on them?

I have given some thought to filters, sequences and series lately, but things seem to be changing pretty fast in mc-analysis right now so I probably need to discuss with someone in the know.

view this post on Zulip Cyril Cohen (Oct 18 2022 at 09:50):

Sure, what do you want to know?

view this post on Zulip Julien Puydt (Oct 18 2022 at 12:32):

@Cyril Cohen Is someone actively working on them? Your PRs are pretty old... And I have ideas and sample code I'd like to discuss to see if there's interesting ideas in there in spite of my being a newbie.

view this post on Zulip Cyril Cohen (Oct 18 2022 at 12:38):

@Julien Puydt Indeed, I'm not working on them anymore because every attempt I made at trying to satisfy all the requirements failed. I now think the only fully satisfactory approach, goes through a big refactoring of the design patterns at use, and that it cannot work without HB giving the right abstraction level so that everything else does not break. If you have suggestions to improve things I'd be glad to read them.

view this post on Zulip Julien Puydt (Oct 18 2022 at 12:40):

My ideas were precisely about refactoring ; can I send you some code?

view this post on Zulip Cyril Cohen (Oct 18 2022 at 12:40):

Sure

view this post on Zulip Julien Puydt (Oct 18 2022 at 12:43):

I sent you a .tar.bz2 (8.4K) ; most of it doesn't compile

view this post on Zulip Julien Puydt (Oct 18 2022 at 12:43):

(so use make -k)

view this post on Zulip Cyril Cohen (Oct 18 2022 at 12:45):

Ok, I received it.

view this post on Zulip Cyril Cohen (Oct 18 2022 at 12:45):

What would help me would be to understand which problem you are trying to solve with this?

view this post on Zulip Julien Puydt (Oct 18 2022 at 12:47):

The biggest problem I have is topology.v is a big many-thousands lines ; I tried to make much smaller chunks.

view this post on Zulip Julien Puydt (Oct 18 2022 at 12:47):

And then I wanted most results to be first results about filters, and only then deduce results on limits.

view this post on Zulip Cyril Cohen (Oct 18 2022 at 12:48):

I was indeed going to propose to cut into 3 files topology / pseudometric / uniform

view this post on Zulip Julien Puydt (Oct 18 2022 at 12:49):

For example, in theories/filters/generalities, you'll find the notion of separated filtered set - a definition on filters. And from this notion (same file) I get unicity of limits. It's in theories/filters/reals.v that I show (or: will show...) that the considered structure is separated.

view this post on Zulip Cyril Cohen (Oct 18 2022 at 12:49):

Julien Puydt said:

And then I wanted most results to be first results about filters, and only then deduce results on limits.

Most things are already done this way, the last remaining bits that were not I'm preparing a PR to generalize cf math-comp/analysis#772

view this post on Zulip Julien Puydt (Oct 18 2022 at 12:54):

(I'm reading)

view this post on Zulip Cyril Cohen (Oct 18 2022 at 12:54):

Julien Puydt said:

For example, in theories/filters/generalities, you'll find the notion of separated filtered set - a definition on filters. And from this notion (same file) I get unicity of limits. It's in theories/filters/reals.v that I show (or: will show...) that the considered structure is separated.

Mmmh I'm not entirely sure what this notion of separated filtered set is? How is it related to ultrafilters?

view this post on Zulip Cyril Cohen (Oct 18 2022 at 12:54):

In MCA we currently get unicity of limits through https://github.com/math-comp/analysis/blob/cd8f5e1e04a503c5236efe00e98eae8e0eab9baf/theories/topology.v#L2630

view this post on Zulip Cyril Cohen (Oct 18 2022 at 12:56):

BTW the purpose of the old PRs on filters has nothing to do with logic properties of filters, most of which we already have in mathcomp/analysis, although we can always think of further generalizing many structures, or completing existing theories.

view this post on Zulip Julien Puydt (Oct 18 2022 at 12:57):

I define separated filtered set in generalities.v as the notion to get unique limits ; there's also a sequential filter notion to get sequential characterization (I didn't manage to finish the proof yet - not good enough with Coq+MC yet)

view this post on Zulip Cyril Cohen (Oct 18 2022 at 12:57):

The purpose of theses old PRs was to attend extra-logic properties, such as which inference of Coq to trigger, to solve a maximum number of problems automatically, and give a consistent set of notations to filters (which is today very confusing), without losing the current expressivity. (Naming points instead of filters, automatically inferring that something is a filter, etc)

view this post on Zulip Julien Puydt (Oct 18 2022 at 13:00):

Yes, I saw topology.v had much material, and things with coercions to help smooth writing proofs (all things I'm not really able to do yet).

view this post on Zulip Julien Puydt (Oct 18 2022 at 13:03):

Do you have an ETA for this rework? Notice that my code is much more comments than code: I listed many properties which I thought would be helpful at the CPGE level...

view this post on Zulip Julien Puydt (Oct 18 2022 at 13:18):

Ah, cvg_unique is the unicity of limits, and uses Hypothesis sep a few lines above. And normed_hausdorff gives separation on complex numbers and ereal_hausdorff gives it for real numbers (and their infinities) ?

view this post on Zulip Cyril Cohen (Oct 18 2022 at 13:20):

Julien Puydt said:

Do you have an ETA for this rework? Notice that my code is much more comments than code: I listed many properties which I thought would be helpful at the CPGE level...

Which rework? The one from math-comp/analysis#772 ? Or the one from my old PRs on filters?

view this post on Zulip Julien Puydt (Oct 18 2022 at 13:21):

Is there a sequential characterization of limits somewhere? It's pretty important to use the dominated convergence theorem to prove continuous limit results (continuity of parameter integrals for example).

view this post on Zulip Cyril Cohen (Oct 18 2022 at 13:22):

And normed_hausdorff gives separation on complex numbers

For any normed vector space, including any R : numFieldType (seen as a 1-dimensional vector space on itself), which encompasses reals and complex numberS.

ereal_hausdorff gives it for real numbers (and their infinities) ?

This is specific for \bar R which has no algebraic structure (except a canonical ordering, as of today)

view this post on Zulip Julien Puydt (Oct 18 2022 at 13:26):

The fact that \bar R lacks structure is a bit annoying (see comments in theories/filters/reals.v) ; of course it can't have proper algebraic structures since +oo + -oo doesn't make sense, but when it works, it should work (not really clear, but I still mean it).

view this post on Zulip Cyril Cohen (Oct 18 2022 at 13:27):

Julien Puydt said:

The fact that \bar R lacks structure is a bit annoying (see comments in theories/filters/reals.v) ; of course it can't have proper algebraic structures since +oo + -oo doesn't make sense, but when it works, it should work (not really clear, but I still mean it).

I know, it might be solved with the ganularity HB will be able to introduce though...

view this post on Zulip Cyril Cohen (Oct 18 2022 at 13:28):

Note that filter_tends_to in MCA is F --> l

view this post on Zulip Julien Puydt (Oct 18 2022 at 13:30):

How are partial functions handled? I put (A: set X) and x\in A&... everywhere to cope with it, because it's not clear how it works in MCA.

view this post on Zulip Cyril Cohen (Oct 18 2022 at 13:30):

Note that the squeeze theorem is under generalization here:
https://github.com/math-comp/analysis/blob/082f934ba6b92679d4fa2bad0da39a94a984099d/theories/normedtype.v#L4176-L4185

view this post on Zulip Cyril Cohen (Oct 18 2022 at 13:31):

Julien Puydt said:

How are partial functions handled? I put (A: set X) and x\in A&... everywhere to cope with it, because it's not clear how it works in MCA.

Partial functions are handled using the function library https://github.com/math-comp/analysis/blob/master/classical/functions.v

view this post on Zulip Julien Puydt (Oct 18 2022 at 13:33):

and how is what I call "filter_is_adherent" handled?

view this post on Zulip Cyril Cohen (Oct 18 2022 at 13:37):

cluster F A I think

view this post on Zulip Cyril Cohen (Oct 18 2022 at 13:38):

It can be related to the usual notion of cluster points for sequences ("valeurs d'adhérence" in French) : u is a sequence,cluster (u @ \oo) is the set of cluster points of the sequence u.

view this post on Zulip Julien Puydt (Oct 18 2022 at 13:40):

Hmmm... that's only about points, isn't it? How does it make it easy to consider the limit of the mathematical sequence $(u_n)_{n\geqslant10}$, but not of $(u_n)_{n\leqslant10}$ ?

view this post on Zulip Cyril Cohen (Oct 18 2022 at 13:41):

Julien Puydt said:

Hmmm... that's only about points, isn't it? How does it make it easy to consider the limit of the mathematical sequence (un)n10(u_n)_{n\geqslant10}, but not of (un)n10(u_n)_{n\leqslant10} ?

I didn't understand your question

view this post on Zulip Julien Puydt (Oct 18 2022 at 13:46):

I meant I don't see where cvg_to gets limited to reasonable filters, ie: those clustering to the definition domain of the function.

view this post on Zulip Julien Puydt (Oct 18 2022 at 13:50):

In the topology.v from MCA 0.5.4, cvg_to appears line 652 while cluster is line 2557, so obviously there's something I don't get: in my experiments I had to define filter_is_adherent before I could turn to filter_tends_to...

view this post on Zulip Julien Puydt (Oct 18 2022 at 13:52):

(notice my comment before the definition of filter_tends_to: FIXME: I'm pretty clueless how to work with partial functions in Coq/MC -- I knew there was a catch and it was wooshing way over my head)

view this post on Zulip Cyril Cohen (Oct 18 2022 at 13:55):

Oh I see, I misread your definition of filter_is_adherent it has nothing to do with clustering does it?

view this post on Zulip Cyril Cohen (Oct 18 2022 at 13:55):

Since we allow filter to be non proper we do not really care in most cases. When a filter converges, we know it's proper

view this post on Zulip Julien Puydt (Oct 18 2022 at 13:57):

I use the word 'adherent' to make the link with topological adherence ; it's clustering indeed.

Ah, the fact that I force proper filters might explain why I have to add this condition. But I don't see why a converging filter needs to be proper.

view this post on Zulip Cyril Cohen (Oct 18 2022 at 13:57):

filter_tends_to f F G is denoted f @ F --> G in MC.

view this post on Zulip Cyril Cohen (Oct 18 2022 at 14:00):

Julien Puydt said:

I use the word 'adherent' to make the link with topological adherence ; it's clustering indeed.

Ah, the fact that I force proper filters might explain why I have to add this condition. But I don't see why a converging filter needs to be proper.

you are right... it's not convergence that makes it proper, I got confused. It's because most of the time we input proper filters, as in f @ x (neighborhoods filters are proper filters, hence image filter are too)

view this post on Zulip Julien Puydt (Oct 18 2022 at 14:01):

Neighborhood fiters are proper, but when restricted to a subset, that can disappear... unless the filter is "adherent"/"clustering"

view this post on Zulip Cyril Cohen (Oct 18 2022 at 14:03):

Oh I see where you're going...

view this post on Zulip Cyril Cohen (Oct 18 2022 at 14:03):

We have this definition of subspace : https://github.com/math-comp/analysis/blob/cd8f5e1e04a503c5236efe00e98eae8e0eab9baf/theories/topology.v#L6042

view this post on Zulip Julien Puydt (Oct 18 2022 at 14:03):

Yes, what prevents me to try a limit at 2 (proper filter) for a function defined on $[0;1]$?

view this post on Zulip Cyril Cohen (Oct 18 2022 at 14:04):

Nothing will prevent you... you will just obtain a result that makes no sense.

view this post on Zulip Julien Puydt (Oct 18 2022 at 14:05):

Hmmmm... and this subspace makes me wonder: what if I have a function $]0;1]$ and want to try a limit at 0? It's not in the subspace, but there's no issue with it per se.

view this post on Zulip Cyril Cohen (Oct 18 2022 at 14:06):

if you have f : subspace `[0, 1] -> T and try f @ 2, nbhs 2 will be interpreted as the filter generated by [set 2], it will be proper.

view this post on Zulip Cyril Cohen (Oct 18 2022 at 14:06):

Same with your example, if you have f : subspace `]0, 1] -> T and try f @ 0, nbhs 0 will be interpreted as the trivial filter generated by [set 0], it will be proper too...

view this post on Zulip Cyril Cohen (Oct 18 2022 at 14:07):

Oops I did a mistake, I'm going to correct it.

view this post on Zulip Julien Puydt (Oct 18 2022 at 14:07):

The first objection is fair (though students usually don't mind computing limits far outside the domain), but the second looks pretty annoying.

view this post on Zulip Zachary Stone (Oct 18 2022 at 14:12):

For what it's worth, I've done some work with things like subspace `]0,1] and it's not a problem (for local properties). That 0 is in the R limit of the domain never comes up, because all the theorems about subspace let you aggresively intersect with `]0,1] as you work.

view this post on Zulip Zachary Stone (Oct 18 2022 at 14:13):

For things like compactness, second countable, simply connected, and other global properties, our subspace topology is quite annoying.

view this post on Zulip Julien Puydt (Oct 18 2022 at 14:13):

Well, I tend to consider the domain of definition of a function to be more on the side of brutally tyrannic rather than just aggressive...

view this post on Zulip Zachary Stone (Oct 18 2022 at 14:14):

Yeah, that's fair. It tends to feel like you have to specify the domain of your function twice. First the underlying Type, then the underlying Set. In typical textbook topology, there is no such distinction.

view this post on Zulip Cyril Cohen (Oct 18 2022 at 14:15):

We could add an additional test in nbhs_subspace to detect if the restriction still keeps the filter proper and return the restriction if appropriate.

view this post on Zulip Zachary Stone (Oct 18 2022 at 14:17):

What do you mean? I think nbhs_subspace always returns a proper filter.

view this post on Zulip Cyril Cohen (Oct 18 2022 at 14:18):

But it's true that nbhs_subspace `]0,1] 0 should return a filter provably equal to at_right 0.

view this post on Zulip Zachary Stone (Oct 18 2022 at 14:19):

It currently returns the principle filter of 0. Isn't that what you want? 0 should be totally separated from ]0,1] in this topology.

view this post on Zulip Cyril Cohen (Oct 18 2022 at 14:20):

I think it will be useful for theorems about convergences/divergence of integral for e.g. x^-1 near 0.

view this post on Zulip Cyril Cohen (Oct 18 2022 at 14:21):

Even though 0 is not inbounds we want to consider the neighborhoods of 0

view this post on Zulip Cyril Cohen (Oct 18 2022 at 14:22):

in the same way for [1, +oo[ we want to consider the neighborhoods of +oo (and that's why we have a special definition for it), but in the case of ]0, 1] we could make it so that nbhs 0 = at_right 0.

view this post on Zulip Julien Puydt (Oct 18 2022 at 14:22):

Definitely that, yes

view this post on Zulip Zachary Stone (Oct 18 2022 at 14:22):

The fully closed subspace nbhs_subspace `[0,1] 0 is also at_right 0, though.

view this post on Zulip Julien Puydt (Oct 18 2022 at 14:22):

at_right is ambiguous - is it pointed or not?

view this post on Zulip Cyril Cohen (Oct 18 2022 at 14:23):

in the current definition it is an unpointed one.

view this post on Zulip Julien Puydt (Oct 18 2022 at 14:23):

(depending on the convention, a function can be continuous at a point iff it has the same finite limit at right and at left)

view this post on Zulip Cyril Cohen (Oct 18 2022 at 14:24):

So for nbhs_subspace `[0,1] 0 is would be the generalized of at_right 0 to a pointed version.

view this post on Zulip Zachary Stone (Oct 18 2022 at 14:25):

It sounds like the filter you'd want for x^-1 is within `]0,1] (nbhs 0).

view this post on Zulip Cyril Cohen (Oct 18 2022 at 14:27):

Zachary Stone said:

It sounds like the filter you'd want for x^-1 is within `]0,1] (nbhs 0).

yes indeed, but isn't it equal to at_right 0?

view this post on Zulip Zachary Stone (Oct 18 2022 at 14:28):

Oh, yeah that's right. I wonder if the filters fun x => within A (nbhs x) even forms a topology.

view this post on Zulip Zachary Stone (Oct 18 2022 at 14:29):

I have a feeling it's just subspace (closure A), although I don't have a proof off the top of my head.

view this post on Zulip Julien Puydt (Oct 18 2022 at 14:30):

In my experiments, I defined:

Definition filter_tends_to
  {X Y: Type}
  (A: set X) (f: X -> Y)
  (F: Filter X)
  (G: Filter Y) :=
  filter_is_adherent F A
  -> forall W, G W
  -> exists V, F V /\ forall x, x \in A `&` V -> (f x) \in W.

but I could also have defined it by asking G to be finer than the image by f of the restriction of F to A.

view this post on Zulip Cyril Cohen (Oct 18 2022 at 14:30):

@Zachary Stone just so you know, I'm doing a big refactor accross topology, normedtype and sequences, to perform some generalizations and complete with some missing lemmas.

view this post on Zulip Zachary Stone (Oct 18 2022 at 14:32):

Excellent, thank you. Let me know if you need any help/review on it.

view this post on Zulip Zachary Stone (Oct 18 2022 at 14:39):

A couple observations to make sure I'm understanding that definition:

  1. When X = Y and f is the identity, I think this is the same as G `=>` within A F
  2. if F is nbhs x, and G is nbhs (f x), this says that f is continuous at x from the subspace A (excluding the awkward boundary conditions issues above)

Are these accurate?

view this post on Zulip Julien Puydt (Oct 18 2022 at 14:41):

Yes ; notice I defined my filters to be proper and added filter_is_adherent conditions everywhere to enforce the domains of definitions of functions. It's a bit worrying me that MCA seems to not enforce it very clearly.

view this post on Zulip Julien Puydt (Oct 18 2022 at 14:59):

@Cyril Cohen you didn't comment on sequential characterization, did you?

view this post on Zulip Cyril Cohen (Oct 18 2022 at 15:00):

Julien Puydt said:

Cyril Cohen you didn't comment on sequential characterization, did you?

No, I didn't,... actually I'm not sure anyone did it so far. But it should be very easy.

view this post on Zulip Zachary Stone (Oct 18 2022 at 15:00):

You are right that domains are weird in MCA. They are often not enforced. It has the obvious downside that it's possible (E.G. dangerously easy) to write well-typed statements with garbage semantic content. From a software engineering perspective, this delays error reporting until theorem application time. Then you'll get a subgoal like 0 \in `]0,1]. Delayed errors are usually indicative of deeper problem. (I'm a software engineer in my day-job, so this stuff pains me to see)

On the other hand, I totally understand why it's like this. Even the definition of filter_tends_to doesn't prevent f from taking values far from A. I believe this whole class of issues needs a solution. The subspace topology was designed as a compromise, but certainly doesn't work everywhere.

By the way, the issue with the sigma type {x : R |x \in `[0,1]} not inheriting algebra is a bit tragic. I recently updated realfun.v to use the {within `[0,1], continuous f} instead of {in `[0,1], continuous f} which fixes issues at the boundary points. The proofs involved a lot of arithmetic in the domain. It's a _huge_ effort saver to have separate subgoals for x + eps/2 \in `[0,1] and f (x + eps/2) ... , which wouldn't work if f had {x : R |x \in `[0,1]} as its domain.

view this post on Zulip Zachary Stone (Oct 18 2022 at 15:01):

For sequential characterization, does having a "countable filterbase" suffice?

view this post on Zulip Julien Puydt (Oct 18 2022 at 15:03):

@Zachary Stone In my experimental code, I defined a "sequential filter" as one obtained through a nonincreasing sequence of nonempty subsets, and tried to prove a sequential characterisation result from that (failed because I'm not good enough with Coq+MC), so I guess the answer is yes.

view this post on Zulip Julien Puydt (Oct 18 2022 at 15:05):

The statement I was aiming for:

Lemma sequential_characterisation:
  filter_tends_to A f F G
  <-> forall (u: nat -> X),
    (forall n, (u n) \in A)
    -> filter_tends_to setT u inftyN F
    -> filter_tends_to setT (f \o u) inftyN G.

view this post on Zulip Zachary Stone (Oct 18 2022 at 15:09):

I recently did some closely related stuff to prove uniform spaces, with a countably-based entourage, are metrizable. See the section countable_uniform. It takes a similar approach

Context {T : uniformType} (f_ : nat -> set (T * T)).

Hypothesis countableBase : forall A, entourage A -> exists N, f_ N `<=` A.

view this post on Zulip Julien Puydt (Oct 18 2022 at 15:12):

I guess you need some kind of AC at some point?

view this post on Zulip Zachary Stone (Oct 18 2022 at 15:13):

Very much yes. There's also some heavy constructible_indefinite_description.

view this post on Zulip Zachary Stone (Oct 18 2022 at 15:15):

But yeah, I'd take the approach of

  1. Defining filter base
  2. Using cardinality.v to define "countably_based"
  3. Prove that if F tend to G, and B is a filter base for F, then f @ B forms a filter base for G. (I think this is true?)

view this post on Zulip Julien Puydt (Oct 18 2022 at 15:23):

I think 1-3 are true, but I don't see how they give the characterization

view this post on Zulip Zachary Stone (Oct 18 2022 at 15:28):

If you've got a countable filter base {U_n , n : nat}, then U_1, U_1 `&` U_2, ... gives a non-increasing, sequence of non-empty subsets inside the filter. Is that strong enough? I guess a follow up question might be, what results are you trying to prove about sequential convergence that aren't true for general filter convergence?

view this post on Zulip Julien Puydt (Oct 18 2022 at 15:43):

@Zachary Stone To prove the continuity theorem for integrals with parameter, you need to be able to convert this continuous problem to a discrete one using sequential characterization ; then you apply the dominated convergence theorem and you're done.

view this post on Zulip Zachary Stone (Oct 18 2022 at 15:47):

Ah, I see. Then the existence of this countable basis + AC for picking a point from each set should be good enough to build a sequence of points. You'll need to work in a T1 space, that is where neighborhood filters have a countable basis. Metric spaces are easily T1.

view this post on Zulip Julien Puydt (Oct 20 2022 at 11:15):

Yes. But first I have to figure out how to play with negation of complex propositions...

view this post on Zulip Julien Puydt (Oct 21 2022 at 20:14):

I figured out how to play with the negation of complex propositions ; so now I'm on my next issue: is there some place where a countable choice axiom is used that I could study?

view this post on Zulip Zachary Stone (Oct 22 2022 at 15:10):

Excellent. I've used cid or "constructive_indefinite_description" for this. There are lots of examples in the code of its applications.

F := forall x : X , exists y : Y, P x y

to functions

f := forall x, { y | P x y}

So that

(projT1 \o f) : X -> Y

This mirrors the "products of non-empty sets are non-empty" representation of choice. If someone else knows of a more elegant way to achieve this, I'd be eager to know.

view this post on Zulip Julien Puydt (Oct 22 2022 at 18:28):

@Zachary Stone Thanks, with this information I should be able to go further. For the moment, I found how to get from 7 to what I want... now I should be able to turn that into a nat -> X with the right property...

view this post on Zulip Julien Puydt (Oct 23 2022 at 07:58):

Ok, I have modified my proof using 7 to a proof using a parametric n and obtained:

v_by_exists : forall n : nat, exists vn : X, P vn

and I want to turn it into:

exists (v: nat -> X), forall n, P (v n)

but I don't see how constructive_indefinite_description does that.

view this post on Zulip abab9579 (Oct 23 2022 at 10:11):

I am not expert in this, but it seems that it would work.
Applying constructive_indefinite_description onto v_by_exists it should give

fn :  nat -> {vn : X | P vn}

Then, you should have

projT1 \o fn : nat -> X
projT2 \o fn : \forall n : nat, P (projT1 (fn n))

Providing the witness projT1 \o fn, you can prove the statement by projT2 \o fn.

view this post on Zulip Pierre Jouvelot (Oct 23 2022 at 11:20):

Is there a reason for not using functional_choice, in the same library Coq.Logic.IndefiniteDescription as constructive_indefinite_description?

view this post on Zulip Pierre Roux (Oct 23 2022 at 11:42):

The "philosophy" of Analysis is to use its boolp.vfile, not the standard library.

view this post on Zulip Julien Puydt (Oct 23 2022 at 12:30):

@abab9579 constructive_indefinite_description will turn an exists x, P x into a {x | P x}, but that's not exactly what I want.

The best I managed was:

pose raw := fun n => constructive_indefinite_description (v_by_exists n).
pose v := fun n => projT1 (raw n).

but it gave raw: forall n, {x: X | P x} which isn't the exists v: nat -> X, forall n, P (v n) I'm looking for! And v has a type forall nat, [eta [eta crazy_stuff which doesn't cut my bread.

view this post on Zulip abab9579 (Oct 23 2022 at 12:56):

The raw is the fn : (forall n : nat, {x : X | P x}) one. (the type is identical to nat -> {vn : X | P vn})
Interesting how applying projT1 blew the type up. Maybe it is from kind mismatch, proj1_sig might work to give nat -> X or forall n: nat, X. Otherwise, I would suspect raw might not have the intended type.

view this post on Zulip abab9579 (Oct 23 2022 at 13:05):

[eta f] is also eta expanded version of f, ideally something like simpl should simplify the type.

view this post on Zulip Julien Puydt (Oct 23 2022 at 13:36):

@abab9579 Perfect! I got the result I wanted to prove!

Here is how it works on a simpler case, for reference:

From mathcomp Require Import ssreflect.

From mathcomp.analysis Require Import boolp.

Section Foo.

Variable X Y: Type.
Variable P: Y -> Prop.

Lemma foo: (forall x: X, exists y, P y) -> exists (f: X -> Y), forall x, P (f x).
Proof.
  move=> H.
  pose raw := fun x => cid (H x).
  pose v := fun x => proj1_sig (raw x).
  exists v.
  move=> x.
  by apply: proj2_sig (raw x).
Qed.

End Foo.

view this post on Zulip Julien Puydt (Oct 23 2022 at 14:03):

@Cyril Cohen I'm quite annoyed that uniqueness of limits comes this high in the concept hierarchy ; it really should come much lower. Students encounter unicity of limits with sequences in december when they met mathematics for the first time in september -- so it's really a core principle!


Last updated: Feb 05 2023 at 14:02 UTC