Stream: math-comp analysis

Topic: Cannot use `continuous` on `f: R^n -> R`

abab9579 (Aug 20 2022 at 02:55):

Taking a baby step here. I found that the notion continuous does not work for the case I want.

I have:

From mathcomp Require Import all_ssreflect.
From mathcomp Require Import ssralg ssrnum matrix.
From mathcomp Require Import topology normedtype derive reals.

Set Implicit Arguments.

Import numFieldNormedType.Exports.

Section DiffSpace.
Context {R: realType} {n: nat}.
Let V := 'rV[R]_n.+1.

Definition conti (f: V -> R): Prop :=
  continuous f.

(Put the continuous f part out and made it into a definition to simplify the example)

And it errors out with:

The term
 "Phantom (classical_sets.set (classical_sets.set R)) (f x @[x --> x])"
has type
 "phantom (classical_sets.set (classical_sets.set (Real.sort R)))
    (@fmap V (Real.sort R) f
       (@filter_of V ?fX0 x (Phantom (@Filtered.sort V ?fX0) x)))"
while it is expected to have type "phantom (@Filtered.sort ?X ?fX) ?x".

1. Would you explain why this is happening?
2. How can I fix it to work? Am I missing some important imports?
3. How should I interpret such coq error messages, in general?

Thanks in advance!

Zachary Stone (Aug 20 2022 at 03:41):

Reading these error messages requires some expertise. If you haven't done so, take an hour to read about canonical structures. It's worth the effort. Of course, that won't help you solve the immediate problem. The solution is simple enough, it seems just importing classical_sets works. There must be some lower level canonicals (probably Pointed, I.E. a set with at least one point) that are required to bootstrap the whole canonical hierarchy.

As for how I figured that out, first I saw phantom (@Filtered.sort ?X ?fX) ?x, indicating it was expecting a canoncial Filtered. That makes sense given that you're working with continuity. Then I saw that there is a matrix_filtered canonical you already imported from topology, and got confused. So I cut-and-paste the header from sequence.v, which worked (that's my go-to file for these problems). Then just minimize the imports.

abab9579 (Aug 20 2022 at 04:24):

First of all, thank you! Now I could go further with my code.

I have read the Canonical section of the Coq documentation, but I did not know how to read phantom (@Filtered.sort ..) part - namely, I do not know how math-comp does canonical structures. I wish the error message were more direct about it...

For me, it is quite frustrating to figure out the imports. Is there more principled way for this?

By the way, Is it okay to take much time on setting up basic stuffs? I am starting to feel anxious.

Zachary Stone (Aug 20 2022 at 18:16):

I'm not aware of a more principled way to handle imports. I wouldn't worry too much about the time. Much effort is still going into some major renovations (E.G. hierarchy builder, measure theory), so I'm not surprised that new users would encounter some rough edges (I certainly did when I started).

But don't let that discourage you! We're still actively developing it, and happy to hear your about your experiences. Do you have any specific goals for using the library?

abab9579 (Aug 21 2022 at 02:01):

I see, so this is a byproduct of the project in early phase. That is reassuring to my anxiety, hope it would become much better in the future. Thanks!
My goal is to take notes on basic manifold stuffs, and wanted to do it formally. When done informally, the lack of typechecker let me make mistakes.

Zachary Stone (Aug 21 2022 at 19:09):

Ah, that makes sense. There's not much on manifolds right now, although most of the pieces are in place. There are a couple traps I can steer you away from.

1. If you're working with manifolds over R, you'll be fine. If you're working with manifolds over other things like C, see https://github.com/math-comp/analysis/issues/317.
2. Manifold theory is full of subspace topologies, but Coq makes this difficult by default. Textbooks often write f : [0.1] -> Vwith some implicit understands about subspace topologies. But sets and types are _not the same in mathcomp-analysis_. It's a bit awkward at first: R is a type, but [set x : R | 0 <= x <= 1] is a set. So f : [set x : R | 0 <= x <= 1] -> V isn't even well formed! Speaking of recent renovations, functions.v cleans this up elegantly. And that should compose correctly with the subspace topology in topology.v. As you work with this stuff, please let us know your experiences. This is an area I'm personally working on, so I'm eager to get some feedback.

abab9579 (Aug 22 2022 at 03:28):

I see, fortunately I am only dealing with R-manifolds here. I do want to avoid subspace stuffs in this notes if possible, but I'd try using functions.v to see the subspace stuffs. Thanks for the directions!

abab9579 (Aug 22 2022 at 03:30):

Also, I have this problem.

I am trying to make C^n(R) a vector space, but the typical approach does not seem to work well due to them designed for boolean predicates. How do I use the machinery with such a type derived from a set?
(The set is defined by induction, alike sig type)

Zachary Stone (Aug 22 2022 at 04:53):

Huh, that's funny. I'm not sure if there are any examples of explicitly finite dimensional vector space theory. Someone should correct me if I'm wrong. If I had unlimited time, I'd probably add N-dimensional to the hierarchy of normed types. That's certainly out of scope while other folks are doing hierarchy builder rewrites.

Assuming there's no existing way to do it, you could define it as Fin n -> Cin the pointwise topology, where Fin n is just some n element type in the discrete topology...

abab9579 (Aug 22 2022 at 04:58):

Oh.. Sorry, I should have elaborated, I did not mean finite dimention things.
by C^n(R), I mean the set of functions which are n-times continuously differentiable.
Similarly, there would be C^\infty (R).
So what I want is to register this subtype as a vector space. (Assign canonical vector space on the subtype)

Marie Kerjean (Aug 22 2022 at 12:58):

Zachary Stone said:

Huh, that's funny. I'm not sure if there are any examples of explicitly finite dimensional vector space theory. Someone should correct me if I'm wrong. If I had unlimited time, I'd probably add N-dimensional to the hierarchy of normed types. That's certainly out of scope while other folks are doing hierarchy builder rewrites.

Assuming there's no existing way to do it, you could define it as Fin n -> Cin the pointwise topology, where Fin n is just some n element type in the discrete topology...

If I'm not wrong, vector here in math-comp is doing finite dimensional vector spaces

Zachary Stone (Aug 22 2022 at 14:56):

Ah, that makes sense. I figured it lived in math-comp, but we don't seem to use that much in analysis yet. Thanks for the link!

For n-times continuously differentiable, derive1n is defined, but little is proved about it. I am not sure the right way to build a bunch of nested, sub-vector spaces like this.

abab9579 (Aug 22 2022 at 23:23):

I see. For me, derive1n would not suffice as I want to work with general normedModType (R^n, at least).

It seems hard to give canonical structures for subtypes generated from a -> Prop, not ssreflect's typical pred a..

Last updated: Feb 05 2023 at 13:02 UTC