Quinn (Oct 15 2022 at 17:44): 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 }.
Two options I've used with various tradeoffs. So it depends what you're trying to do:
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.
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]?
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.
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...
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.
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].
ah! Open Scope ring_scope. was the missing ingredient
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
Julien Puydt (Oct 16 2022 at 17:34):Sometimes 0%:R is what it takes.
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 -module (not specifically R).
Quinn (Oct 17 2022 at 20:55):(I'm still failing to Check 0%:R. for R : realType)
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.
thanks! wow, that's subtle.
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: Oct 13 2024 at 01:02 UTC