Stream: math-comp analysis

Topic: Boolean R comparisons in notations


view this post on Zulip Karl Palmskog (Aug 18 2020 at 20:57):

I tried a bunch of different requires, scopes, etc., but is it currently at all supported to get the usual infix notations for the boolean versions of the comparison operators on R, like how ssrnat gives you the boolean ones for nat? For example:

Variable r1 r2 : R.
Check r1 <= r2.
(*
should show:
r1 <= r2 : bool

as opposed to:
r1 <= r2 : Prop
*)

view this post on Zulip Reynald Affeldt (Aug 18 2020 at 23:30):

Since I seldom deal directly with Reals in mathcomp-analysis, I have no default recipe but for example the following has type bool:

Require Import Rstruct.

Check Rdefinitions.R0 <= Rdefinitions.R1.
(* Rdefinitions.RbaseSymbolsImpl.R0 <= Rdefinitions.RbaseSymbolsImpl.R1
     : bool *)

view this post on Zulip Reynald Affeldt (Aug 18 2020 at 23:32):

Or this:

Require Import Rstruct.

Check (0 <= 1 :> Rdefinitions.R).
(* (0 : Rdefinitions.RbaseSymbolsImpl.R) <= (1 : Rdefinitions.RbaseSymbolsImpl.R)
     : bool *)

view this post on Zulip Reynald Affeldt (Aug 18 2020 at 23:33):

Or this:

Require Import Reals.
Require Import Rstruct.

Check (0 <= 1 :> R).
(* (0 : R) <= (1 : R)
     : bool *)

view this post on Zulip Reynald Affeldt (Aug 18 2020 at 23:35):

(let's say in a context that Require Import the files up to normedtype.v)

view this post on Zulip Karl Palmskog (Aug 18 2020 at 23:56):

hmm, so like this?

From Coq Require Import Reals.

From mathcomp.analysis Require Import
boolp ereal reals posnum landau classical_sets Rstruct Rbar topology prodnormedzmodule normedtype.
(*
this gives using release 0.3.2:
Error:
Level 2 is already declared right associative while it is now expected to be left associative.
*)

view this post on Zulip Reynald Affeldt (Aug 19 2020 at 00:16):

Maybe insert this in-between:

From Coq Require Import ssreflect ssrfun ssrbool.
From mathcomp Require Import all_ssreflect.
From mathcomp Require Import ssralg ssrnum.

(only the first line is sufficient to get rid of the error)

view this post on Zulip Karl Palmskog (Aug 19 2020 at 00:25):

I may be missing something:

From Coq Require Import Reals.

From mathcomp Require Import all_ssreflect.
From mathcomp Require Import ssralg ssrnum.

From mathcomp.analysis Require Import
boolp ereal reals posnum landau classical_sets Rstruct Rbar topology prodnormedzmodule normedtype.

Fail Check (0 <= 1 :> Rdefinitions.R). (* Unknown interpretation for notation "_ <= _ :> _". *)
Fail Check (0 <= 1 :> R). (* Unknown interpretation for notation "_ <= _ :> _". *)

view this post on Zulip Reynald Affeldt (Aug 19 2020 at 00:32):

Local Open Scope ring_scope. before the Checks

view this post on Zulip Reynald Affeldt (Aug 19 2020 at 00:35):

(with my apologies: I should have prepared a minimal example from the start but I was not in a working environment)


Last updated: Aug 11 2022 at 01:03 UTC