Coq formalization of constructive reals for exact real computation and code extraction to Haskell/AERN.
- 1. Installation instructions
- 2. Code extraction to Haskell/AERN
- 3. Executing extracted code
- 4. Benchmark measurements
Our formalization is implemented in the Coq proof assistant.
You should have Coq installed and running, with the option to install further packages via opam.
We tested our code with Coq version 8.18.0 installed via opam.
To build the code you can just clone this repository, install the below packages, and run make in the formalization subfolder.
Most of the implementation does not have any additional dependencies.
The only exception is the file sqrt.v which uses some libraries for classical analysis.
To execute sqrt.v you additionally need to install the following Coq packages:
These libraries can be installed e.g. using opam install.
Code extraction is defined in the following file:
Extract.v
After processing this file, Coq produces Haskell files, one for each example. The files need minor mechanical post-processing described below. The extracted post-processed compilable code is also readily available in folder extracted-examples/src.
For example, the extracted version of real_max is in file Max.hs.
-
Add the following statements after the last import statement in the generated file:
import Prelude ((+),(-),(/)) import qualified Prelude as P import MixedTypesNumPrelude (ifThenElse) import Numeric.CollectErrors (unCNfn2) import qualified Numeric.OrdGenericBool as OGB import qualified Unsafe.Coerce as UC import qualified Control.Monad import qualified Data.Functor import qualified MixedTypesNumPrelude as MNP import qualified Math.NumberTheory.Logarithms as Logs import qualified AERN2.Real as AERN2 import qualified AERN2.Continuity.Principles as AERN2Principles
-
Install
stack(a Haskell build tool). -
Locate the folder
extracted-examples -
(optional) Check that the provided
stack.yamlmeets your needs.
$ stack repl src/Max.hs --ghci-options "-Wno-unused-matches -Wno-unused-imports -Wno-type-defaults"
ghci> import Prelude
ghci> import AERN2.Real hiding (pi)
ghci>
ghci> real_max ((sqrt 2)/2) (1/(sqrt 2)) ? (bits 1000)
[0.70710678118654752440084436... ± ~0.0000 ~2^(-1229)]
ghci>
ghci> (real_max (pi-pi) 0) ? (bits 1000)
[0 ± ~0.0000 ~2^(-1228)]
- The examples
ode_exp.hsandode_tan.hsin theextracted-examples/srcfolder are extracted from the examples in theode.vscript. - The extracted programs demonstrate the step wise ODE solver for the initial value problems
y' = y; y(0) =1which is solved by the exponential function andy' = 1+y^2; y(0) = 0which is solved by the tan function. - See the below example on how to execute the example interactively for an arbitrary number of steps.
- The program returns a list of real number pairs corresponding to (t, y(t)).
$ stack repl src/ode_exp.hs --ghci-options "-Wno-unused-matches -Wno-unused-imports -Wno-type-defaults" *> exp_example 100
-
Run
stack installin theextracted-examplesfolder.- The first time round it may take long time and install a large number of packages.
-
Test the executable:
$ coq-aern-extracted-bench realmaxE 100 [0 ± ~2.2569e-36 ~2^(-118)] accuracy: bits 118
The file all.ods in folder extracted-examples/bench summarises our benchmark measurements. The measurements were made on a Lenovo T440p laptop with Intel i7-4710MQ CPU and 16GB RAM, OS Ubuntu 18.04, compiled using Haskell Stackage LTS 17.2.
The benchmarks measurements can be reproduced using the provided bash script runBench.sh:
$ mkdir -pv logs/{civt{1,2,3},sqrt{1,2},realmax}
...
mkdir: created directory 'logs/realmax'
$ bash bench/runBench.sh my_all.csv
/usr/bin/time -v coq-aern-extracted-bench realmaxE 1000000 (running and logging in logs/realmax/run-realmax-1000000-E.log)
...