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

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

Thanks in advance!

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.

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.

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 about your experiences. Do you have any specific goals for using the library?

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.

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.

- 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. - Manifold theory is full of subspace topologies, but Coq makes this difficult by default. Textbooks often write
`f : [0.1] -> V`

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

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!

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)

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 -> C`

in the pointwise topology, where `Fin n`

is just some n element type in the discrete topology...

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)

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 -> C`

in 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

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.

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`

..

Solved (from math-comp users channel)

abab9579 has marked this topic as resolved.

Last updated: Feb 27 2024 at 23:01 UTC