Axiomatic Reals and Certified Efficient Exact Real Computation

Abstract

We introduce a new axiomatization of the constructive real numbers in a dependent type theory. Our main motivation is to provide a sound and simple to use backend for verifying algorithms for exact real number computation and the extraction of efficient certified programs from our proofs. We prove the soundness of our formalization with regards to the standard realizability interpretation from computable analysis. We further show how to relate our theory to a classical formalization of the reals to allow certain non-computational parts of correctness proofs to be non-constructive. We demonstrate the feasibility of our theory by implementing it in the Coq proof assistant and present several natural examples. From the examples we can automatically extract Haskell programs that use the exact real computation framework AERN for efficiently performing exact operations on real numbers. In experiments, the extracted programs behave similarly to hand-written implementations in AERN in terms of running time.

Holger Thies is supported by JSPS KAKENHI Grant Number JP20K19744. Sewon Park is supported by the National Research Foundation of Korea (NRF) grants funded by the Korea government (No. NRF-2016K1A3A7A03950702, NRF-2017R1E1A1A03071032 (MSIT) & No. NRF-2017R1D1A1B05031658 (MOE)).

This project has received funding from the EU’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie grant agreement No. 731143.

Appendices

A Full List of Axioms

Here we list all our axioms, grouped by the files in our implementation.

Base.v defines our base type theory, making it extensional and $\mathsf {Prop}$ classical:

• TT1 $\mathrm {\Pi }( P : \mathsf {Prop}).\ P \vee \lnot P$

• TT2 $\mathrm {\Pi }( P,Q: \mathsf {Prop}).\ (P \rightarrow Q) \rightarrow (Q \rightarrow P) \rightarrow P = Q$

• TT3 $\mathrm {\Pi }( A : \mathsf {Type}).\ \mathrm {\Pi }( P : A \rightarrow \mathsf {Type}).\ \mathrm {\Pi }( f, g : \mathrm {\Pi }( x : A).\ P(x)).\ (\mathrm {\Pi }( x: A).\ f\, x = g\, x) \rightarrow f = g$

Kleene.v axiomatizes the type of Kleeneans and the multivalued monad.

• K1 $\textsf {K}: \mathsf {Type}$

• K2 $\textsf {true}: \textsf {K}$

• K3 $\textsf {false}: \textsf {K}$

• K4 $\textsf {true}\ne \textsf {false}$

• K5 $\hat{\lnot }: \textsf {K}\rightarrow \textsf {K}$

• K6 $\mathrel {\hat{\vee }}: \textsf {K}\rightarrow \textsf {K}\rightarrow \textsf {K}$

• K7 $\mathrel {\hat{\wedge }}: \textsf {K}\rightarrow \textsf {K}\rightarrow \textsf {K}$

  Define $\lceil k :\mathsf {K} \rceil :\equiv k = \textsf {true}$, $\lfloor k : \mathsf {K} \rfloor :\equiv k = \textsf {false}$, and $(k : \mathsf {K}) \!\downarrow :\equiv \lceil k \rceil \vee \lfloor k \rfloor$.

• K8 $x \!\downarrow \rightarrow \lceil x \rceil + \lfloor x \rfloor$

  Kleene logic operations:

• K9 $\lceil \hat{\lnot }x \rceil = \lfloor x \rfloor$ and $\lfloor \hat{\lnot }x \rfloor = \lceil x \rceil$

• K10 $\lceil x \mathrel {\hat{\wedge }}y \rceil = (\lceil x \rceil \wedge \lceil y \rceil )$ and $\lfloor x \mathrel {\hat{\wedge }}y \rfloor = (\lfloor x \rfloor \vee \lfloor y \rfloor )$

• K11 $\lceil x \mathrel {\hat{\vee }}y \rceil = (\lceil x \rceil \vee \lceil y \rceil )$ and $\lfloor x \mathrel {\hat{\vee }}y \rfloor = (\lfloor x \rfloor \wedge \lfloor y \rfloor )$

• The monad structure:

• M1 $\mathsf {M}: \mathsf {Type}\rightarrow \mathsf {Type}$

• M2 $\textsf {unitM}: \mathrm {\Pi }( A : \mathsf {Type}).\ A \rightarrow \mathsf {M}\ A$

• M3 $\mathsf {multM}: \mathrm {\Pi }( A : \mathsf {Type}).\ \mathsf {M}\ (\mathsf {M}\ A) \rightarrow \mathsf {M}\ A$

• M4 $\mathsf {liftM}: \mathrm {\Pi }( A, B : \mathsf {Type}).\ (A \rightarrow B) \rightarrow (\mathsf {M}\ A \rightarrow \mathsf {M}\ B)$

  $\textsf {unitM}$ and $\mathsf {multM}$ are natural transformations:

• M5 $\mathrm {\Pi }( A, B : \mathsf {Type}).\ \mathrm {\Pi }( f : A \rightarrow B).\ \mathrm {\Pi }( x : A).\ \mathsf {liftM}\ A\ B\ f(\textsf {unitM}\ A\ x) = \textsf {unitM} B\ (f\ x)$

• M6 $\mathrm {\Pi }( A, B : \mathsf {Type}).\ \mathrm {\Pi }( f : A \rightarrow B).\ \mathrm {\Pi }( x : \mathsf {M}\ (\mathsf {M}\ A)).\$

  $\mathsf {multM}\ B ((\mathsf {liftM}\ (\mathsf {M}\ A)\ (\mathsf {M}\ B)\ (\mathsf {liftM}\ A\ B\ f))\ x) = (\mathsf {liftM}\ A\ B\ f) (\mathsf {multM}\ A\ x)$

  The coherence conditions:

• M7 $\mathrm {\Pi }( A:\mathsf {Type}).\ \mathrm {\Pi }( x : \mathsf {M}\ A).\ \mathsf {multM}\ A\ (\textsf {unitM}\ (\mathsf {M}\ A)\ x) = x$

• M8 $\mathrm {\Pi }( A :\mathsf {Type}).\ \mathrm {\Pi }( x : \mathsf {M}\ A).\ \mathsf {multM}\ A\ (\mathsf {liftM}\ A\ (\mathsf {M}\ A)\ (\textsf {unitM}\ A)\ x) = x$

• M9 $\mathrm {\Pi }( A : \mathsf {Type}).\ \mathrm {\Pi }( x : \mathsf {M}\ (\mathsf {M}\ (\mathsf {M}\ A))).\ \mathsf {multM}\ A\ (\mathsf {multM}\ (\mathsf {M}\ A)\ x) =$

  $\mathsf {multM}\ A\ (\mathsf {liftM}\ (\mathsf {M}\ (\mathsf {M}\ A)) (\mathsf {M}\ A) (\mathsf {multM}\ A)\ x)$

  Further characterization of the monad:

• M10 $\textsf {elimM}:\mathrm {\Pi }( A : \mathsf {Type}).\ (\mathrm {\Pi }( x, y : A).\ x = y) \rightarrow \mathsf {M}\ A \rightarrow A$

• M11 $\mathrm {\Pi }( A : \mathsf {Type}).\ \mathrm {\Pi }( p : \big (\mathrm {\Pi }( x, y : A).\ x = y\big )).\ \mathrm {\Pi }( a : \mathsf {M}\, A).\ \textsf {unitM}\, A\, \big ( \textsf {elimM}\, A p\, a\big ) = a$

• M12 $\mathsf {\omega lift}: \mathrm {\Pi }( P : \mathsf {N}\rightarrow \mathsf {Type}).\ \big (\mathrm {\Pi }( x : \mathsf {N}).\ \mathsf {M}\ P(x)\big ) \rightarrow \mathsf {M}\big (\mathrm {\Pi }( x : \mathsf {N}).\ P(x)\big )$

• M13 $\mathrm {\Pi }( P : \mathsf {N}\rightarrow \mathsf {Type}).\ \mathrm {\Pi }( f : \big (\mathrm {\Pi }( x : \mathsf {N}).\ \mathsf {M}\ P(x)\big )).\ f\ n = \lambda ( n : \mathsf {N} ).\ \mathsf {liftM}\big (\lambda ( f : \big (\mathrm {\Pi }( x : \mathsf {N}).\ P(x)\big ) ).\ f\ n\big )\ (\mathsf {\omega lift}\ P\ f)$

• M14 $\textsf {select}: \mathrm {\Pi }( x, y : \mathsf {K}).\ (\lceil x \rceil \vee \lceil y \rceil ) \rightarrow \mathsf {M}\ \big (\lceil x \rceil + \lceil y \rceil \big )$

RealAxioms.v axiomatizes the real numbers:

• The structure of real numbers:

• R1 $\mathsf {R}: \mathsf {Type}$

• R2 $0 : \mathsf {R}$

• R3 $1 : \mathsf {R}$

• R4 $+ : \mathsf {R}\rightarrow \mathsf {R}\rightarrow \mathsf {R}$

• R5 $\times : \mathsf {R}\rightarrow \mathsf {R}\rightarrow \mathsf {R}$

• R6 $- : \mathsf {R}\rightarrow \mathsf {R}$

• R7 $/ : \mathrm {\Pi }( x : \mathsf {R}).\ x \ne 0 \rightarrow \mathsf {R}$

• R8 $< : \mathsf {R}\rightarrow \mathsf {R}\rightarrow \mathsf {Prop}$

  Semi-decidability of comparison tests:

• R9 $\mathrm {\Pi }( x, y : \mathsf {R}).\ \textsf {semiDec}(x < y)$

  Constructive completeness:

• R10 $\mathrm {\Pi }( P : \mathsf {R}\rightarrow \mathsf {Prop}).\ (\exists !( x :\mathsf {R} ).\ P\ x) \rightarrow (\mathrm {\Pi }( n :\mathsf {N}).\ \mathrm {\Sigma }( x : \mathsf {R}).\ \exists (\tilde{x} : \mathsf {R} ).\ P\ x \wedge - 2^{-n}< x - \tilde{x} < 2^{-n}) \rightarrow \mathrm {\Sigma }( x : \mathsf {R}).\ P\ x$

  Classical axioms in $\mathsf {Prop}$:

• R11 $\mathrm {\Pi }( x, y:\mathsf {R}).\ x + y = y + x$

• R12 $\mathrm {\Pi }( x, y,z:\mathsf {R}).\ (x + y) + z = x + (y + z)$

• R13 $\mathrm {\Pi }( x:\mathsf {R}).\ x + - x = 0$

• R14 $\mathrm {\Pi }( x:\mathsf {R}).\ 0 + x = x$

• R15 $\mathrm {\Pi }( x, y:\mathsf {R}).\ x \times y = y \times x$

• R16 $\mathrm {\Pi }( x, y, z : \mathsf {R}).\ (x \times y) \times z = x \times (y \times z)$

• R17 $\mathrm {\Pi }( x:\mathsf {R}).\ \mathrm {\Pi }( p : x \ne 0).\ (/\ x\ p) \times x = 1$

• R18 $\mathrm {\Pi }( x:\mathsf {R}).\ 1 \times x= x$

• R19 $\mathrm {\Pi }( x,y,z:\mathsf {R}).\ x \times (y + z) = x \times y + x \times z$

• R20 $1 \ne 0$

• R21 $1 > 0$

• R22 $\mathrm {\Pi }( x, y :\mathsf {R}).\ x < y \vee x = y \vee x > y$

• R23 $\mathrm {\Pi }( x,y : \mathsf {R}).\ x< y \rightarrow \lnot (y < x)$

• R24 $\mathrm {\Pi }( x,z,y :\mathsf {R}).\ x< y \rightarrow y< z \rightarrow x < z$

• R25 $\mathrm {\Pi }( x, y, z :\mathsf {R}).\ y< z \rightarrow x + y < x + z$

• R26 $\mathrm {\Pi }( x, y, z : \mathsf {R}).\ 0< x \rightarrow y< z \rightarrow x\times y < x \times z$

  Define $x \le y :\equiv x < y \vee x = y$. For each $P : \mathsf {R}\rightarrow \mathsf {Prop}$ and $x : \mathsf {R}$, define $P < x : \equiv \mathrm {\Pi }( y : \mathsf {R}).\ P\ y \rightarrow y \le x$.

• R27 $\mathrm {\Pi }( P : \mathsf {R}\rightarrow \mathsf {Prop}).\ (\exists (x : \mathsf {R} ).\ P\ x) \rightarrow (\exists (x : \mathsf {R} ).\ P \le x ) \rightarrow \exists (x : \mathsf {R} ).\ P \le x \wedge \mathrm {\Pi }( y : \mathsf {R}).\ P \le y \rightarrow x \le y$.

Nabla.v defines the idempotent monad $\nabla$ and RealCoqReal.v axiomatizes the relator:

$\nabla$1:

$\textsf {relator}: \mathsf {R}\rightarrow \nabla \tilde{\mathsf {R}}$

$\nabla$2:

$\mathrm {\Pi }( x, y :\mathsf {R}).\ \textsf {relator}\ x = \textsf {relator}\ y \rightarrow x = y$

$\nabla$3:

$\mathrm {\Pi }( y : \nabla \tilde{\mathsf {R}}).\ \exists (x :\mathsf {R} ).\ y = \textsf {relator}\ x$

$\nabla$4:

$\textsf {relator}\ 0 = \textsf {unit}_{\nabla }\!\ \tilde{\mathsf {R}}\ 0$

$\nabla$5:

$\textsf {relator}\ 1 = \textsf {unit}_{\nabla }\!\ \tilde{\mathsf {R}}\ 1$

$\nabla$6:

$\mathrm {\Pi }( x, y : \mathsf {R}).\ \textsf {relator}\ (x + y) = (\textsf {relator}\ x) \mathrel {{+}^{\dagger _{\nabla }}} (\textsf {relator}\ y)$

$\nabla$7:

$\mathrm {\Pi }( x, y : \mathsf {R}).\ \textsf {relator}\ (x \times y) = (\textsf {relator}\ x) \mathrel {{\times }^{\dagger _{\nabla }}} (\textsf {relator}\ y)$

$\nabla$8:

$\mathrm {\Pi }( x : \mathsf {R}).\ \textsf {relator}\ (-x) = \mathrel {{-}^{\dagger _{\nabla }}} (\textsf {relator}\ x)$

$\nabla$9:

$\mathrm {\Pi }( x : \mathsf {R}).\ \mathrm {\Pi }( p : x \ne 0).\ \textsf {relator}\ (/x\ p) = \mathrel {{/}^{\dagger _{\nabla }}} (\textsf {relator}\ x)$

$\nabla$10:

$\mathrm {\Pi }( x, y : \mathsf {R}).\ (x< y) = (\textsf {relator}\ x) \mathrel {{<}^{\dagger _{\nabla }}} (\textsf {relator}\ y)$

B Code Extraction

Extraction is defined in file Extract.v, including the following key mappings:

Note that the monad $\mathsf {M}$ does not appear in the extracted programs. Multivaluedness is intrinsic thanks to redundancy in the underlying representations.

The AERN comparison OGB.< returns a (lazy) Kleenean for real numbers.

Running the extracted code requires adding a few import statements, which are specified in file Extract.v.