Stream: math-comp analysis

Topic: the unit interval


view this post on Zulip Quinn (Oct 15 2022 at 17:44):

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

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

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

  1. 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.
  2. 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.

view this post on Zulip Quinn (Oct 15 2022 at 20:23):

What do I need to import to type subspace [0,1]? where are the notations for [0,1]?

view this post on Zulip Quinn (Oct 16 2022 at 02:05):

I have From mathcomp Require Import classical_sets. and I'm trying these notations and nothing is working.

view this post on Zulip Julien Puydt (Oct 16 2022 at 07:11):

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

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

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.

view this post on Zulip Julien Puydt (Oct 16 2022 at 14:27):

This works:

From mathcomp Require Import classical_sets interval.

Open Scope classical_set_scope.
Open Scope ring_scope.

Check `[0, 1].

view this post on Zulip Quinn (Oct 16 2022 at 17:19):

ah! Open Scope ring_scope. was the missing ingredient

view this post on Zulip Quinn (Oct 16 2022 at 17:20):

The other thing I've been struggling with is coercing 0 and 1 to R for some R : realType

view this post on Zulip Julien Puydt (Oct 16 2022 at 17:34):

Sometimes 0%:R is what it takes.

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

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 Z\mathbb{Z}-module (not specifically R).

view this post on Zulip Quinn (Oct 17 2022 at 20:55):

(I'm still failing to Check 0%:R. for R : realType)

view this post on Zulip Julien Puydt (Oct 17 2022 at 20:59):

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.

view this post on Zulip Quinn (Oct 17 2022 at 22:48):

thanks! wow, that's subtle.

view this post on Zulip Quinn (Oct 17 2022 at 22:49):

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: Jan 30 2023 at 11:03 UTC