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.

1 Introduction

Verifying the correctness of software is becoming increasingly important, in particular in safety critical application domains. Often, such programs need to interact in some way with the outside, physical world requiring numerical calculations over the real numbers and other uncountable mathematical entities. While proof assistants and formal methods are becoming more mature and are increasingly used in practical applications, verification of numerical programs remains extremely challenging [2]. One difficulty arises from the fact that in practice real numbers are commonly replaced by floating-point approximations, introducing rounding errors and uncertainties that pose additional problems for verification.

While there is active ongoing work on the verification of floating-point arithmetic [4, 15], we here consider a different approach known as exact real computation. In exact real computation, real numbers are basic entities that allow exact manipulation without rounding errors. Programs can output finite approximations up to any desired absolute precision. This is often realized by adding a datatype for reals and arithmetic operations on them as primitives in programming languages. Several implementations exist demonstrating the feasibility of the approach [1, 10, 16]. Although less efficient than optimized hardware-based floating-point calculations, implementations in exact real computation are by design more reliable than the former and are thus well-suited for situations where correctness is of high importance. Further, for efficient implementations there is often only a small overhead. However, subtilities of the semantics such as multivaluedness can still make writing correct programs difficult and stronger guarantees of correctness are highly desirable. One of the strongest such guarantees is a computer verified correctness proof e.g. in a proof assistant which however requires a sound model of the semantics. This poses some theoretical challenges as operations such as partial comparisons and multivalued branching are common in exact real computation and need to be computable [18].

Software packages for exact real computation often build on the theoretical framework of computable analysis and the theory of representations [13, 25]. In previous work [11] two of the authors of the present paper worked on verified exact real computation using the Incone library [23], which aims to directly formulate the model of computable analysis in Coq. Incone requires to define computational realizers, i.e. functions that work on low-level encodings of the reals e.g. by sequences of rational numbers. Working directly with such encodings facilitates high control over the algorithm and allows fine-grained optimizations. However, algorithms and their correctness proofs depend on the concrete encoding and the approach is therefore less elegant and more labour-intensive than working with a high-level abstract implementation of a real number type. While this issue has also been addressed in Incone by providing an abstract specification of some important real number operations, in this work we chose an even higher level of abstraction. That is, instead of reimplementing and verifying basic real number operations, we trust the implementation of a core of simple real number operations and to verify programs using those operations under the assumption that they are correctly implemented. The basic idea is to axiomatically model sophisticated implementations of exact real computation which exist for many modern programming languages, e.g. AERN [10] for Haskell or iRRAM for C++. This approach also provides a certain amount of independence of the concrete implementation of real numbers and thus allows to easily switch the underlying framework.

More concretely, we define a new constructive axiomatization that models the real numbers in a conceptually similar way as some mature implementations of exact real computation. We formally define our theory on top of a simple type theory inspired by the one used in Coq and prove its soundness with respect to the realizability interpretation used in computable analysis. We also give a theoretical foundation of relating proofs written over a classical theory of real numbers with our real numbers.

There are already several formalizations of real numbers and real analysis in most proof assistants (see e.g. [3] for an overview), including the C-CoRn library [6], a large constructive framework based on Coq setoids. Our axiomatization is different in that it very closely models classical reasoning used in computable analysis and concepts used in practical implementations of exact real computation, such as multivalued operations. We therefore think that it can be appealing to people working in this area.

Our approach further allows to easily map the constructive real type, and its axiomatically defined basic operations such as arithmetic or limits, to corresponding types and operations in an exact real computation framework. Concretely, utilising this mapping and program extraction techniques, we obtain certified programs over an implementation of exact real computation from correctness proofs.

We implemented the theory in the Coq proof assistant and extracted Haskell programs from our proofs using Coq code extraction. In the extracted programs, primitive operations on the reals are mapped to operations in the exact real computation framework AERN [10] which is written and maintained by one of the authors. Our first examples show that the extracted programs perform efficiently, having only a small overhead compared to hand-written implementations.

2 Computable Analysis and Exact Real Computation

In this section, we recap some essential concepts and limitations of computable analysis and exact real computation in order to justify our choice of axioms.

To compute over uncountable mathematical structures such as real numbers exactly, computable analysis takes assemblies over Kleene’s second algebra (assemblies for short) as the basic data type [8, 22].¹ An assembly is a pair of a set A and a relation $\Vdash \, \subseteq \mathbb {N}^\mathbb {N}\times A$, which is surjective in that $\forall x\in A.\ \exists \varphi .\ \varphi \Vdash x$. We call $\varphi \in \mathbb {N}^\mathbb {N}$ a realizer of an abstract entity $x \in A$ if $\varphi \Vdash x$ holds. Given two assemblies of A and B, a function $f : A \rightarrow B$ is said to be computable if there is a computable partial function $\tau :\subseteq \mathbb {N}^\mathbb {N}\rightarrow \mathbb {N}^\mathbb {N}$ that tracks f, i.e. for any $x \in A$ and its realizer $\varphi$, $\tau (\varphi )$ is a realizer of f(x).

For real numbers, there is a unique assembly (up to isomorphism in the category of assemblies $\mathsf {Asm}(\mathcal {K}_2)$) that makes the model-theoretic structure [7] of real numbers computable: (1) $0, 1\in \mathbb {R}$ are computable, (2) field arithmetic is computable, (3) the order relation < that is undefined at $\{(x, x) \mid x \in \mathbb {R}\}$ is computable, and (4) the limit operation defined at rapidly converging sequences is computable. An example is the Cauchy reals where $\varphi$ is a realizer of $x \in \mathbb {R}$ if and only if $\varphi$ encodes a sequence of rationals converging rapidly towards x. An assembly of reals satisfying the above computability conditions is called effective.

An inevitable side-effect of this approach is partiality. Whichever realizability relation for reals we take, comparisons of real numbers are only partially computable [25, Theorem 4.1.16]. Let Kleenean $\mathbf {K}$ be the assembly of $\{ ff , tt , \bot \}$ where an infinite sequence of zeros realizes $\bot$, an infinite sequence that starts with 1 after a finite prefix of zeros realizes $ff$, and an infinite sequence that starts with 2 after a finite prefix of zeros realizes $tt$ (see e.g. [11, Example 3]). The assembly $\mathbf {K}$ can be seen as a generalization of the Booleans by adding an explicit state of divergence $\bot$. Comparison in any effective assembly of reals $\mathbf {R}$ is computable as a function $x< y = tt$ if $x < y$, $ff$ if $y < x$, and $\bot$ if $x = y$.

As the usual comparisons are partial, multivaluedness becomes essential in exact real computation [14]. For two assemblies of A and B, a multivalued function $f : A \rightrightarrows B$, which is basically a nonempty set-valued function, is computable if there is a computable function that takes a realizer $\varphi$ of $x \in A$ and computes a realizer of any $y \in f(x)$. An example is the multivalued soft comparison [5]:

$$ x<_k y = \{ tt \mid x< y + 2^{k}\} \cup \{ ff \mid y < x + 2^{k}\}. $$

The above total multivalued function approximates the order relation. It is tracked by evaluating two partial comparisons $x < y + 2^{k}$ and $y < x + 2^{k}$ in parallel, returning $tt$ if $x < y + 2^{k} = tt$, and $ff$ if $y < x + 2^{k} = tt$. It is nondeterministic in the sense that for the same x and y but with different realizers, which of the tests terminates first may vary. Exact real number computation software such as [10, 16] further offer operators like $\mathbf {select}:\subseteq \mathbf {K}\times \mathbf {K}\rightrightarrows \mathbf {K}$ such that $\mathbf {select}(k_1, k_2) \ni tt$ iff $k_1 = tt$ and $\mathbf {select}(k_1, k_2) \ni ff$ iff $k_2 = tt$ as a primitive operation for generating multivaluedness.

3 Axiomatization

In this section we give an overview of the formalization and the axioms we introduce. For space reasons we omit most axioms in the main part but provide a complete list in Appendix A. For those axioms that we do introduce here, we also reference the corresponding entry from the appendix.

Our theory is formalized in a type theory similar to the one of Coq. More precisely, we work with a dependent type theory with basic types $0, 1, 2, \mathsf {N}, \mathsf {Z}$, and a universe of classical propositions. That is, we have an impredicative à la Russel universe $\mathsf {Prop}$, closed under $\rightarrow , \wedge , \vee , \exists , \mathrm {\Pi }$, where the law of excluded middle $\mathrm {\Pi }( P : \mathsf {Prop}).\ P \vee \lnot P$ holds (Axiom TT1) [17]. We assume that the identity types belong to $\mathsf {Prop}$. Opposed to $\mathsf {Prop}$, $\mathsf {Type}$ is an à la Russel universe of types (with an implicit type level) with type constructors $\rightarrow , \times , +, \mathrm {\Sigma }, \mathrm {\Pi }$. We further suppose propositional extensionality in $\mathsf {Prop}$ (Axiom TT2) and function extensionality (Axiom TT3). Based on this setting, we propose an axiomatization for the assemblies $\mathbf {K}, \mathbf {R}$ and computable multivalued functions from Sect. 2.

3.1 Kleenean and Multivalued Lifting

First, we assume that there is a type $\mathsf {K}: \mathsf {Type}$ of Kleeneans (Axiom K1) and that there are two distinct elements $\textsf {true}: \mathsf {K}$ and $\textsf {false}: \mathsf {K}$ (Axioms K2, K3 and K4). Let us define the abbreviation $\lceil t \rceil : \mathsf {Prop}:\equiv t = \textsf {true}$. In many cases, we do not work directly with Kleeneans. Instead, we call a proposition $P : \mathsf {Prop}$ semi-decidable (in its free variables) if there is a Kleenean t that identifies P:

$$ \textsf {semiDec}(P) :\equiv \mathrm {\Sigma }( t : \textsf {K}).\ P = \lceil t \rceil $$

Multivalued computations are axiomatized by a monad $\mathsf {M}$ (Axioms M1–M9) such that a mapping $f : A \rightarrow B$ expresses a singlevalued function and $f : A \rightarrow \mathsf {M}\ B$ expresses a multivalued function. We assume the monad structure: (1) there is a type constructor $\mathsf {M}: \mathsf {Type}\rightarrow \mathsf {Type}$, (2) there is a unit $\textsf {unitM}: \mathrm {\Pi }( A : \mathsf {Type}).\ A \rightarrow \mathsf {M}\ A$, (3) a multiplication $\mathsf {multM}: \mathrm {\Pi }( A : \mathsf {Type}).\ \mathsf {M}(\mathsf {M}\ A) \rightarrow \mathsf {M}\ A$, (4) a function lifting $\mathsf {liftM}: \mathrm {\Pi }( A,B : \mathsf {Type}).\ (A \rightarrow B) \rightarrow \mathsf {M}\ A \rightarrow \mathsf {M}\ B$, (5) and the corresponding coherence conditions.

Intuitively, the monad can be understood as the nonempty power-set monad. In this sense, we assume that there is a mapping

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

which is an inverse of $\textsf {unitM}$ (Axioms M10–M11).

For any sequence of types $P : \mathsf {N}\rightarrow \mathsf {Type}$, we assume that the map

$$ \lambda ( X : \mathsf {M}(\mathrm {\Pi }( x : \mathsf {N}).\ P\ x) ).\ \lambda ( n : \mathsf {N} ).\ \mathsf {liftM}\big (\lambda ( f : \mathrm {\Pi }( x : \mathsf {N}).\ P\ x ).\ f\ n\big )\ X $$

which is of type $\mathsf {M}(\mathrm {\Pi }( x : \mathsf {N}).\ P\ x) \rightarrow \mathrm {\Pi }( x : \mathsf {N}).\ \mathsf {M}(P\ x)$ admits a section (Axioms M12–M13):

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

Intuitively, given a set of sequences S, the first map transforms it to a sequence of sets $(n \mapsto \bigcup _{f \in S}\{f(n)\})$. And, $\mathsf {\omega lift}$ is its section which transforms a sequence of sets f to a set of sequences $\{g \mid \forall n.\ g(n) \in f(n)\}$. This operation enables, for example, to interchange multivalued sequences of real numbers with sequences of multivalued real numbers.

The most important axiom we assume is multivalued branching (Axiom M14):

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

The above axiom yields the following, which we use more frequently:

$$ \textsf {choose}: \mathrm {\Pi }( P, Q : \mathsf {Prop}).\ P \vee Q \rightarrow \textsf {semiDec}(P) \rightarrow \textsf {semiDec}(Q) \rightarrow \mathsf {M}\big ( P + Q\big ). $$

Namely, given two semi-decidable propositions and at least one of them holds classically, we can nondeterministically decide if P holds or Q holds.

For any two types A, B, we write $f : A \rightrightarrows B$ to denote $f : A \rightarrow \mathsf {M}\ B$ and $\overline{\mathrm {\Sigma }}( x : A ).\ P(x)$ for $\mathsf {M}\ \mathrm {\Sigma }( x : A).\ P(x)$ (multivalued functions and existences).

Example 1 For any proposition P, suppose both $\textsf {semiDec}(P)$ and $\textsf {semiDec}(\lnot P)$ hold. As $P \vee \lnot P$ holds by the classical law of excluded middle, we have $\mathsf {M}( P + \lnot P)$ by applying $\textsf {choose}$. As it is provable that $P + \lnot P$ is subsingleton, using $\textsf {elimM}$, we have $P + \lnot P$, the decidability of the proposition P.

3.2 Real Numbers

We assume real numbers by declaring that there is a type $\mathsf {R}: \mathsf {Type}$ for real numbers (Axiom R1) and axiomatizing its model-theoretic structure. There are distinct constants $0 : \mathsf {R}$ and $1 : \mathsf {R}$, (infix) binary operators $+,\times : \mathsf {R}\rightarrow \mathsf {R}\rightarrow \mathsf {R}$, a unary operator $- : \mathsf {R}\rightarrow \mathsf {R}$, a term $/ : \mathrm {\Pi }( x : \mathsf {R}).\ x \ne 0 \rightarrow \mathsf {R}$, and a (infix) binary predicate $< : \mathsf {R}\rightarrow \mathsf {R}\rightarrow \mathsf {Prop}$ (Axioms R2–R8). We assume the properties of the structure classically in a safe way that does not damage constructivity (Axioms R11–R27). For example, trichotomy (Axiom R22) is assumed as a term of type

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

However, an inhabitant of the type $\mathrm {\Pi }( x, y : \mathsf {R}).\ (x< y) + (x = y) + (y < x)$ is not posed anywhere.

In addition to the axioms in $\mathsf {Prop}$, we assume $\mathrm {\Pi }( x, y : \mathsf {R}).\ \textsf {semiDec}(x < y)$ (Axiom R9). Namely, for any two real numbers its order, as a classical proposition, is semi-decidable.

Example 2 Using the classical trichotomy, we can construct a term of type

$$ \mathrm {\Pi }( x, y, \epsilon : \mathsf {R}).\ 0< \epsilon \rightarrow x< y + \epsilon \vee y < x + \epsilon . $$

Since the inequalities are semi-decidable, using $\textsf {choose}$, the multivalued version of the approximate splitting lemma [21, Lemma 1.23]

$$ \textsf {mSplit}: \mathrm {\Pi }( x, y, \epsilon : \mathsf {R}).\ 0< \epsilon \rightrightarrows \big ( (x< y + \epsilon ) + (y < x + \epsilon )\big ) $$

is obtainable, which roughly says, for any real numbers $x, y, \epsilon$, when $\epsilon$ is positive, we can nondeterministically decide if $x < y + \epsilon$ or $y < x + \epsilon$.

The set of classical axioms living in $\mathsf {Prop}$ includes the completeness of the set of real numbers (Axiom R27). For its constructive counterpart (Axiom R10), for any predicate $P : \mathsf {R}\rightarrow \mathsf {Prop}$ such that $p:\exists !(z : \mathsf {R} ).\ P\ z$ holds, we assume

$$ \textsf {lim}\ P\ p : \big (\mathrm {\Pi }( n :\mathsf {N}).\ \mathrm {\Sigma }( e :\mathsf {R}).\ \!\exists (a : \mathsf {R} ).\ P\ a \wedge - 2^{-n}< e - a < 2^{-n}\big ) \!\rightarrow \! \mathrm {\Sigma }( a : \mathsf {R}).\ P\ a. $$

Here, for any $n : \mathsf {N}$, $2^{-n} : \mathsf {R}$ is constructed by recursive division of $1 + 1$ on 1 and $\exists !( a : A ).\ P\ a$ stands for $\exists (a:A ).\ P\ a\wedge \mathrm {\Pi }( b : A).\ P\ b \rightarrow a = b$. Note that P can be seen as a data that classically defines a real number. The axiom says that when we have a procedure that computes a $2^{-n}$ approximation to the real number for each n, we have the real number constructively.

Example 3 In many cases, we compute an approximation of a real number using multivalued computation. Using $\textsf {elimM}$ and $\mathsf {\omega lift}$, we can define

$$ \overline{\textsf {lim}}\ P\ p: \big (\mathrm {\Pi }( n :\mathsf {N}).\ \overline{\mathrm {\Sigma }}( e :\mathsf {R} ).\ \!\exists (a : \mathsf {R} ).\ P\ a \wedge - 2^{-n}< e - a < 2^{-n}\big ) \!\rightarrow \! \mathrm {\Sigma }( a : \mathsf {R}).\ P\ a. $$

where $P : \mathsf {R}\rightarrow \mathsf {Prop}$ and $p:\exists !(z : \mathsf {R} ).\ P\ z$. Namely, when we have a procedure that computes a multivalued approximation to a real number, the procedure itself gets converted to the real number.

3.3 Soundness by Realizabiltiy

To prove soundness of the set of axioms, we extend the standard realizability interpretation of extensional dependent type theories to the category of assemblies over Kleene’s second algebra with computable morphisms $\mathsf {Asm}(\mathcal {K}_2)$ [19, § 4 and § 5]. That is, to each type constant $A : \mathsf {Type}$ we axiomatize, we designate an assembly $\llbracket A : \mathsf {Type} \rrbracket$ and to each axiomatic term constant c : A, we assign a morphism $\llbracket c:A \rrbracket : \mathbf {1}\rightarrow \llbracket A : \mathsf {Type} \rrbracket$ in $\mathsf {Asm}(\mathcal {K}_2)$ where $\mathbf {1}$ is a terminal object.

In consequence, by extending the interpretation, we not only prove soundness of the axiomatization but also argue that a closed term in our type theory automatically gives a construction of a computable function in the sense of computable analysis. For example, suppose we have a proof of the statement

$$ \mathrm {\Pi }( x : \mathsf {R}).\ P\ x \rightrightarrows \mathrm {\Sigma }( y : \mathsf {R}).\ Q\ x\ y $$

where $P : \mathsf {R}\rightarrow \mathsf {Prop}$ and $Q : \mathsf {R}\rightarrow \mathsf {R}\rightarrow \mathsf {Prop}$. The interpretation of the proof is a computable partial multifunction $f :\subseteq \mathbb {R}\rightrightarrows \mathbb {R}$ where for any $x \in \mathbb {R}$ such that $\llbracket P \rrbracket (x) = \mathbf {1}$, f(x) is well-defined and for any $y \in f(x)$, $\llbracket Q \rrbracket (x, y) = \mathbf {1}$.

For our axioms, we interpret $\mathsf {K}$ to the Kleenean assembly $\mathbf {K}$ and $\mathsf {R}$ to any effective assembly of real numbers $\mathbf {R}$. Mapping the axiomatic constants properly, e.g., $\textsf {true}$ to $tt$ and $\textsf {false}$ to $ff$, validates most of the axioms.

In order to interpret the multivaluedness, we specify the endofunctor $\mathbf {M}: \mathsf {Asm}(\mathcal {K}_2)\rightarrow \mathsf {Asm}(\mathcal {K}_2)$ such that for an assembly $\mathbf {A}$, $\mathbf {M}\ \mathbf {A}$ is an assembly of the set of nonempty subsets of $\mathbf {A}$ whose realization relation $\Vdash$ is defined by

$$ \varphi \Vdash _{\mathbf {M}\ \mathbf {A}} S \quad :\Leftrightarrow \quad \exists x.\ x\in S \wedge \varphi \Vdash _\mathbf {A}x. $$

In words, $\varphi$ realizes a nonempty subset S of $\mathbf {A}$ if $\varphi$ realized an element x of S in the original $\mathbf {A}$. Note that for any assemblies $\mathbf {A}, \mathbf {B}$, a multifunction $f : \mathbf {A}\rightrightarrows \mathbf {B}$ is computable if and only if it appears as a morphism $f : \mathbf {A}\rightarrow \mathbf {M}\ \mathbf {B}$.

The endofunctor $\mathbf {M}$ is a monad whose unit is $\eta _\mathbf {A}: x \mapsto \{x\}$, multiplication is $\mu _\mathbf {A}: S \mapsto \bigcup _{T \in S} T$, and its action on morphisms is $\mathbf {M}(f) : S \mapsto \bigcup _{x \in S}\{f(x)\}$.

When $\mathbf {A}$ is sub-singleton, $\mathbf {M}\ \mathbf {A}$ is isomorphic to $\mathbf {A}$. And, for any sequence of assemblies $(\mathbf {A}_i)_{i\in \mathbb {N}}$, there is a mapping $\mathrm {\Pi }_{i\in \mathbb {N}}\mathbf {M}(\mathbf {A}_i) \rightarrow \mathbf {M}(\mathrm {\Pi }_{i\in \mathbb {N}}\mathbf {A}_i)$ that collects all sections of $f \in \mathrm {\Pi }_{i\in \mathbb {N}}\mathbf {M}(\mathbf {A}_i)$. The axioms of multivalue types are validated by mapping the monad structure of $\mathsf {M}$ to the monad structure of $\mathbf {M}$ and mapping $\textsf {select}$ to $\mathbf {select}$.

Discussions thus far conclude the soundness of our axioms:

Lemma 1

The axiomatization is sound admitting a realizability interpretation.

4 Relating Classical Analysis

Although our axiomatization is constructive, in some cases we allow a certain amount of classical reasoning to prove non-computational properties. For example, in terms of program extraction (cf. Sect. 5) we often want to prove a statement of the form $\mathrm {\Pi }( x : \mathsf {R}).\ \mathrm {\Sigma }( y : \mathsf {R}).\ P\ x\ y$ where $P : \mathsf {R}\rightarrow \mathsf {R}\rightarrow \mathsf {Prop}$. To do this, we assume any $x : \mathsf {R}$, provide an explicit $y : \mathsf {R}$ and prove that $P\ x\ y$ holds. $P\ x\ y : \mathsf {Prop}$ is a classical statement and thus admits nonconstructive proofs.

As mentioned in the introduction, most proof assistants already provide formalizations of classical reals and some theory upon them. Instead of rebuilding all this theory on top of our axiomatization, in the above situation it would be more practical to have a way to carefully apply classical results to our type without breaking constructivity.

More concretely, let us assume a Coq-like dependent type theory that already provides a rich theory of classical analysis through a type $\tilde{\mathsf {R}}$. Here, by classical analysis, we mean that classical statements such as $\mathrm {\Pi }( x : \tilde{\mathsf {R}}).\ x> 0 + \lnot (x > 0)$ hold in the type theory. We want to embed our axiomatization and apply theorems proven over the classical theory to our formalization while separating the constructive part and the classical part of the type theory correctly so that realizability results like those from Sect. 3.3 still hold.

Even though the type theory provides classical types and terms, it stays fully constructive for the terms that do not access the classical axioms. That means, a term in the type theory can be formally interpreted into two different models. We have two type judgements saying that t of type A may rely on classical axioms and saying that $t'$ of type $A'$ is free from any classical axioms. When , we interpret it in the category of sets $\mathsf {Set}$ and when , we interpret it in $\mathsf {Asm}(\mathcal {K}_2)$. For example, is derivable for some t, but is not for the same t.

The goal is to correctly relate the two type judgements. One way is obvious: when is derivable, then so is .² However, we are more interested in the other direction, i.e. how we can get a constructively well-typed term from classical well-typedness.

Recall that $\mathsf {Set}$ is a reflective subcategory of $\mathsf {Asm}(\mathcal {K}_2)$ by the forgetful functor $\mathbf {\Gamma }: \mathsf {Asm}(\mathcal {K}_2)\rightarrow \mathsf {Set}$ and its right adjoint $\boldsymbol{\nabla }: \mathsf {Set}\rightarrow \mathsf {Asm}(\mathcal {K}_2)$ where for any set A, $\boldsymbol{\nabla }A$ is the assembly of A with the trivial realization relation [24, Theorem 1.5.2].

For each type A, define

$$ \nabla A :\equiv \mathrm {\Sigma }( P : A \rightarrow \mathsf {Prop}).\ \exists !( x : A ).\ P\ x. $$

See that for any type A, is isomorphic to in $\mathsf {Set}$ and is isomorphic to in $\mathsf {Asm}(\mathcal {K}_2)$. It can be understood as a functor that erases all the computational structure of A while keeping its set-theoretic structure.

It is provable in the type theory using the assumptions of $\mathsf {Prop}$ being the type of classical propositions admitting propositional extensionality that $\nabla$ is an idempotent monad where its unit $\textsf {unit}_{\nabla }\!: \mathrm {\Pi }( A : \mathsf {Type}).\ A \rightarrow \nabla A$ on $\nabla A$, is an equivalence with the inverse being the multiplication. Moreover, it holds that $\textsf {unit}_{\nabla }\!\ \mathsf {Prop}: \mathsf {Prop}\rightarrow \nabla \mathsf {Prop}$ is an equivalence. That means, given a mapping $f : A_1 \rightarrow A_2 \rightarrow \cdots \rightarrow A_d$, there is a naturally defined lifting $\mathrel {{f}^{\dagger _{\nabla }}} : \nabla A_1 \rightarrow \nabla A_2 \rightarrow \cdots \rightarrow \nabla A_d$ and given a predicate $P : A_1 \rightarrow A_2 \rightarrow \cdots \rightarrow \mathsf {Prop}$, there is $\mathrel {{P}^{\dagger _{\nabla }}} :\nabla A_1 \rightarrow \nabla A_2 \rightarrow \cdots \rightarrow \mathsf {Prop}$.

We add the type judgement rule:

saying that when t is a classically constructed term of a transferable type A, we have a constructive term t of type A. A type is transferable if it is of the form $\nabla c$ for a constant type, a $\mathsf {Type}$, or a $\mathsf {Prop}$ variable c; $A \rightarrow B$, $A \times B$, $A \wedge B$, $A \vee B$, or $\nabla (A + B)$ for transferable types A and B; $\mathrm {\Pi }( x : A).\ P(x)$, $\mathrm {\Sigma }( x : A).\ P(x)$, or $\exists (x : A ).\ P(x)$ for transferable types A and P(x); $x = y$, $x < y$, or $x <^\dagger y$; or is $\mathsf {Type}$ or $\mathsf {Prop}$. Roughly speaking, a type is transferable if its subexpressions in the construction of the type are guarded by $\nabla$.

This judgement rule is validated in our interpretation. First, note that $\boldsymbol{\nabla }\{*\} \simeq \mathbf {1}$. And, when a type A is transferable, holds. When , we have a function in $\mathsf {Set}$. Hence, we define by pre and postcomposing the above isomorphisms to .

We assume the map $\textsf {relator}: \mathsf {R}\rightarrow \nabla \tilde{\mathsf {R}}$ to relate our axiomatic real numbers with classical analysis (Axiom $\nabla$1). Its interpretation in $\mathsf {Set}$ is the identity map . We assume enough axioms that characterize the mapping (Axiom $\nabla$1–$\nabla$10). For example, $\textsf {relator}\ 0 = \textsf {unit}_{\nabla }\!\ \tilde{\mathsf {R}}\ 0$ (Axiom $\nabla$4), $\mathrm {\Pi }( x, y: \mathsf {R}).\ \textsf {relator}(x + y) = (\textsf {relator}\ x) \mathrel {{+}^{\dagger _{\nabla }}} (\textsf {relator}\ y)$ (Axiom $\nabla$6), $\mathrm {\Pi }( x, y: \mathsf {R}).\ (x< y) = (\textsf {relator}\ x) \mathrel {{<}^{\dagger _{\nabla }}} (\textsf {relator}\ y)$ (Axiom $\nabla$10), and so on.

Example 4 Suppose from the theory of classical analysis, we have a term f saying that for any positive real number, there is a square root:

As $\textsf {unit}_{\nabla }\!\ A : A \rightarrow \nabla A$ is an equivalence in the classical type theory, we can derive

As the type of the above judgement is transferable, we have

Using the axioms of the relator, we can obtain a term of type

It illustrates how we can transport a classical proof of the existence of square root based on $\tilde{\mathsf {R}}$ to a constructive proof of the classical existence of square root based on $\mathsf {R}$. This existence result is used when verifying our implementation of the square root function as described in Sect. 5.3.

Note that in Coq we can not formally deal with having two independent type theories simultaneously and therefore a complete correctness proof when applying the relator notion can only be proven on the meta-level. We plan to address this issue in future work e.g. by writing a Coq plugin that would allow this distinction.

5 Implementation and Examples

We implemented the above theory in the Coq proof assistant.³ From a correctness proof in our implementation, we can extract Haskell code that uses the AERN library to perform basic real number arithmetic operations. For this, we introduce several extraction rules replacing operations on the constructive reals with the corresponding AERN function. The extracted code requires only minor mechanical editing, namely adding import statements (cf. Appendix B for details of the extraction process).

Let us present the main features of our implementation by giving some examples of operations on real numbers.

5.1 Maximization

A simple example of an operation that requires multivaluedness in its definition is the maximization operator that takes to real numbers x and y and returns their maximum. We can define it by the following Coq statement.⁴

The statement can be proven by applying the limit operator defined in Example 3. That is, we have to show that there exists exactly one z: Real for which the condition in the above statement holds and that for each n : nat we can construct a e : Real multivaluedly that approximates z up to error $2^{-n}$. The first part can be easily concluded from the axioms over the Real type. The approximation can be constructed by concurrently testing whether $x > y - 2^{-n}$ or $x < y + 2^{-n}$, i.e. by multivalued branching from Example 2. In the first case, x can be used as the desired approximation and in the second case y.

Extracting code from this proof yields a maximization operator in AERN. Figure 1 shows parts of the Coq proof and the extracted Haskell code.

Fig. 1.

Outline of a Coq proof and corresponding extracted Haskell code

5.2 Intermediate Value Theorem (IVT)

A classical example from computable analysis (see e.g. [25, Chapter 6.3]) is finding the zero of a continuous, real valued function $f: [0,1] \rightarrow \mathbb {R}$ with $f(0) < 0$ and $f(1) > 0$ under the assumption that there is exactly one zero in the interval (i.e. a constructive version of the intermediate value theorem from analysis).

More precisely, we prove the following statement in Coq.

Here, continuous is defined using the usual $\epsilon$-$\delta$-criterion and uniq f a b is the statement that f has exactly one zero in the interval [a, b]. The statement can be proven using the trisection method which is similar to the classical bisection method but avoids uncomputable comparison to 0. That is we inductively define sequences $a_i, b_i$ with $f(a_i)*f(b_i) < 0$ and $b_i - a_i \le (2/3)^i$. In each step we let $a_i' := (2a_i + b_i)/3$, $b_i' := (a_i +2b_i)/3$ and in parallel check if $f(a_i')*f(b_i) < 0$ or $f(a_i)*f(b_i') < 0$. In the first case we set $a_{i+1} := a_i'$, $b_{i+1} := b_i$, in the second case $a_{i+1} := a_i$, $b_{i+1} := b_i'$. As at least one of the inequalities is true by the assumptions, this selection can be done using the multivalued choose operator from Sect. 3.1. The zero can then be defined using the limit operator. Again, we can extract an AERN program from the proof. The extracted program is an implementation of root finding using the above algorithm.

5.3 Classical Proofs and a Fast Square Root Algorithm

As a final example let us look at how to use the relator operation defined in Sect. 4 to prove facts about our constructive real type using classical results from the Coq standard library. We follow an example from [11] that implements the Heron method to compute the square root of a real number in the Incone library. The proof is interesting as it is mostly classical and makes use of some of the theory and external libraries for classical analysis that are already available for Coq. Making use of this huge repertoire on theory already formalized in Coq vastly simplifies the proof. We repeated the example using our new implementation and compared it to the implementation in Incone.

The Heron method is an approximation scheme for the square root of a real $x \in \mathbb {R}$ by the sequence inductively defined by $x_0 := 1$ and $x_{i+1} := \frac{1}{2} \left( x_i + \frac{x}{x_i} \right)$. In this work we only consider a restricted version where $\frac{1}{4} \le x \le 2$. In this interval, the sequence converges quadratically to $\sqrt{x}$, i.e. $\left| x_i - \sqrt{x}\right| \le 2^{-2^{i}}$. This restricted version can be expanded to all non-negative reals (see the aforementioned work on Incone).

We prove the following statement in Coq.

The Coq standard library already contains a (non-constructive) definition of a function sqrt and proves many of its properties. To prove our statement, we construct a real number y by applying the limit operator to the sequence defined by the Heron iteration scheme. We then relate it to the classical real number sqrt(x) and use the characteristics of sqrt to show the condition. All necessary properties to show that the relation holds are again proven purely classical using tools from the standard library and other libraries building upon it.

The proof is very similar to the one in Incone and we could reuse large parts of it without major adaptions. It should be noted though, that Incone additionally requires to prove the existence of a realizer in the sense of computable analysis which adds an additional layer of complexity that is not required with our axiomatic approach and the new proof therefore becomes significantly simpler.

5.4 Performance Measurements

Since our axiomatization of constructive reals is built on a datatype similar to that used by AERN, we expect the performance of the extracted programs to be similar to that of hand-written AERN code. The measurements summarized below are consistent with our hypothesis.⁵ iRRAM is known to be one of the most efficient implementations of exact real computation and thus we also included hand-written iRRAM versions for calibration. The last three rows are examples of root finding by trisection. The iRRAM trisection code benefits from in-place update.

Benchmark		Average execution time (s)
Formula	Accuracy	Extracted	Hand-written AERN	iRRAM
$\max (0,\pi -\pi )$	$10^6$ bits	16.8	16.2	1.59
$\sqrt{2}$	$10^6$ bits	0.72	0.72	0.62
$\sqrt{\sqrt{2}}$	$10^6$ bits	1.51	1.54	1.15
$x-0.5=0$	$10^3$ bits	3.57	2.3	0.03
$x(2-x)-0.5=0$	$10^3$ bits	4.30	3.08	0.04
$\sqrt{x+0.5}-1=0$	$10^3$ bits	19.4	17.8	0.29

6 Conclusion and Future Work

We presented a new axiomatization of constructive reals in a type theory and proved its soundness with respect to the standard realizability interpretation from computable analysis. We implemented our theory in Coq and used Coq’s code extraction features to generate efficient Haskell programs for exact real computation based on the AERN library.

We think our new axiomatization is particularly well-suited for verifying exact real computation programs built on top of the theory of computable analysis. Nevertheless, we plan to more thoroughly compare our implementation with other implementations of constructive reals in Coq and other proof assistants in the future. In particular, we plan to take a deeper look at the C-CoRn library and how it differs from our implementation. Relating to other constructive formalization would also allow execution directly in the proof assistant.

From a more practical point of view, we plan to extend our implementation by other important operations on real numbers such as trigonometric and exponential functions and mathematical constants such as $\pi$ and e. Such extensions should be straight-forward and we do not expect any major difficulties in their implementation. Maybe more interestingly, we also plan to extend to more complicated operations such as solution operators for ordinary or partial differential equations by applying recent ideas from real complexity theory [9, 12].

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.