-
Notifications
You must be signed in to change notification settings - Fork 43
FAQ
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.
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
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.