FAQ

Table of Contents

Idioms
Others

##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 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.