FAQ

About MathComp-Analysis Versions

Q: Which version is compatible with MathComp 1.XY.Z?

A: The last version of MathComp-Analysis compatible with MathComp 1 is release 0.7.0. Prior versions are also compatible with MathComp 1. Since [2024-01-24], the master branch of MathComp-Analysis requires MathComp 2.

MathComp-Analysis Idioms

Q: How to introduce a positive real number?

A: When introducing a positive real number, it is best to turn it into a posnum whose type is equipped with better automation. There is an idiomatic way to perform such an introduction. Given a goal of the form

==========================
forall e : R, 0 < e -> G

the tactic move=> _/posnumP[e] performs the following introduction

e : {posnum R}
==========================
G

Others

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

A: The following script provides an example (MathComp-Analysis 1.0.0) but this "feature" is not really used in MathComp-Analysis:

From Coq Require Import Reals.

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

From mathcomp Require Import
boolp ereal reals signed landau classical_sets Rstruct ereal 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 may use the view nbhs_normP.

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

A: This is by design.