FAQ

(see also Idioms in the contribution guide)

Q: How to use MathComp-Analysis' Boolean operators with the real numbers of the Coq standard library?

A: The following script provides an example but this "feature" is untested:

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.

Local Open Scope ring_scope.

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

Q: How to prove that a given subset is a neighbourhood of a point?

A: Typically, for R: numDomainType V: pseudoMetricType R A : set V x : V, proving nbhs x A can be done by applying the view nbhs_ballP. Then one uses the tactic exists to input the strictly positive radius r : R of a ball of radius r and of center x included in A.

R: numDomainType
V: pseudoMetricType R
A : set V
x : V
r : R
r0: (0%R < r)%O
============================
nbhs x A 

applying apply/nbhs_ballP; exists r; first by exact: r0. move => y By leads to

R: numDomainType
V: pseudoMetricType R
A : set V
x : V
r : R

y : V
By: ball x r y 
============================
A y

If V : normedModType R, then you maye use the view nbhs_normP.

Q: Why does the notation @` print as [set E | x in A]?

A: This is by design.