This webpage contains some information on how to access the Coq development for our paper “ Continuous and monotone machines”. The formal development has been made part of incone, a Coq library for computable analysis.

Installation instructions

You should have coq (8.9.0) running with the Coquelicot library (3.0) and from math-comp (1.9.0) the packages ssreflect and algebra.

The following libraries have to be installed in this order:

• mf
• rlzrs
• metric
• incone

You can just clone this github repository using git clone --recurse-submodules, change into the top directory and run make to install all four libraries.

Alternatively if you are using opam you can also run opam install . --working-dir to install all necessary libraries.

The contents of the paper

Formal proofs of statements in the paper have been made part of the library and are scattered across several files and folders.

A good overview over how many of the main concepts from the paper are formalized can be ganed by looking at the example of representing real numbers using rational approximations (Example 2.2 in the paper) contained in examples/Q_reals.v in the incone library.

Further results and examples of the paper can be roughly related to the formalization as follows:

• Represented spaces as introduced in Section 2 are called continuity spaces in incone. Results on continuity spaces are contained in the continuity_spaces folder of the incone library.
  • The notion of representation and other basic definitions are contained in the file continuity_spaces/representation.v
  • The representation for discrete spaces (Example 2.1) is contained in the file continuity_spaces/discr.v
  • Continuity is defined in continuity_spaces/cont.v.
  • the Kleeneans as defined in Example 2.3 are introduced in the file continuity_spaces/hyperspaces.v in the Section Kleeneans. This file also contains Example 2.4.
  • The second part of Example 2.3 (the sign function) is defined in the beginning of the examples/Q_reals.v file.
  • Isomorphy (Section 2.2) is defined in continuity_spaces/iso.v
• Statements and Definitions about multifunctions described in the first part of Section 3 are contained in the mf sublibrary.
• Realizability (Section 3.1) is contained in the rlzrs sublibrary.
• The definition of the modulus function from Section 4 can be found in continuity_spaces/cont.v.
• The results in Sections 3 and 4 concerning continuous and monotone machines are mostly contained in the computability subfolder of incone.
  • The F operator from Section 3.2 is defined in computability/FMop.v.
  • The extensive example in Section 3.3 (Inversion in the rational representation) is contained in the file examples/reals/division_for_Q_reals.v.
  • Continuous machines (Section 4) are defined in computabiliy/continuous_machines.v
  • The main results in this chapter are formalized in computability/classical_mach.v.
  • Montone machines and their composition (Chapter 4.2) are treated in computability/monotone_machines.v.