What's the proper way to make the unit interval, as a type? I'm not familiar with mathcomp.

The way I'd do it in coq standard library is something like

```
Definition closed_unit_interval : Ensemble R := fun x => 0 <= x <= 1.
Record compact_unit := { x : R; H :> closed_unit_interval x }.
```

Two options I've used with various tradeoffs. So it depends what you're trying to do:

- The sigma type with the weak topology. The upside is it has the true subspace topology. The downside is it doesn't inherit any algebra.
- The type
`subspace [0,1]`

is technically an alias of`R`

with a subspace-like topology. The benefit is this inherits all the algebra of`R`

. The downside is it contains points you don't care about. It works great for local properties like continuity, though.

I find `subspace`

to be far more useful in practice than sigma types. And its theory is better developed. You need to add the occasional `{in [0,1],...}`

and `{fun [0,1] >-> B}`

. But it's all worth it to be able to add numbers directly. Lots of examples of this in the code. In full disclosure I also wrote much of the subspace stuff, so I may have a bias.

What do I need to import to type `subspace [0,1]`

? where are the notations for `[0,1]`

?

I have `From mathcomp Require Import classical_sets.`

and I'm trying these notations and nothing is working.

@Quinn you can improve matters using `Open Scope classical_set_scope.`

.

I have to admit I haven't been able to use MC-analysis yet...

Oh, sorry about that. I missed an important backtick. There's ``[a, b]`

, which gives an `interval R`

normally. And there's ` `[a, b]%classic`

which gives a `set R`

. Most things prefer the `%classic`

version, although there is some converting back and forth. The `set_interval.v`

file has good examples of both. And the `subspace`

definition lives in `topology.v`

.

This works:

```
From mathcomp Require Import classical_sets interval.
Open Scope classical_set_scope.
Open Scope ring_scope.
Check `[0, 1].
```

ah! `Open Scope ring_scope.`

was the missing ingredient

The other thing I've been struggling with is coercing `0`

and `1`

to `R`

for some `R : realType`

Sometimes `0%:R`

is what it takes.

It would rather be `0 : R`

in the scope `ring_scope`

(or `0%R : R`

is the top scope is `nat_scope`

or another scope which poses the notaiton `0`

).

On the other hand `0%:R`

works indeed but is an explicit coercion of `0%N`

(of type `nat`

) to a $\mathbb{Z}$-module (not specifically `R`

).

(I'm still failing to `Check 0%:R.`

for `R : realType`

)

Here it is:

```
From mathcomp Require Import all_ssreflect all_algebra.
From mathcomp.analysis Require Import reals.
Open Scope ring_scope.
Section Foo.
Variable R: realType.
Check (0 :R).
Check (0%:R).
End Foo.
```

thanks! wow, that's subtle.

I wonder if there's a way to make it more intuitive that `Open Scope ring_scope`

is needed to be working with items of `R : realType`

Last updated: Jun 22 2024 at 15:01 UTC