-
Notifications
You must be signed in to change notification settings - Fork 0
Library for floating point numbers
License
coq-contribs/float
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Folders and files
Name | Name | Last commit message | Last commit date | |
---|---|---|---|---|
Repository files navigation
This directory contains a library for floating point numbers. - This library is described in `A generic library of floating-point number and its application to exact computing' in TPHOLs 2001. To build the directory, do coq_makefile *.v > Makefile Then make depend;make all Laurent Thery & Sylvie Boldo & Laurence Rideau thery@sophia.inria.fr Sylvie.Boldo@ens-lyon.fr lrg@sophia.inria.fr Summary of what is in the library: AllFloat.v : load all the definitions and theorems of the library Float.v : definition of floating point number as pair of mantissa and exponent Record float : Set := Float { Fnum: Z; Fexp: Z }. Fop.v : usual operation on floats: +, -, * Fbound.v: Definition of a bound and what it is to be bounded for a float Record Fbound : Set := Bound { vNum: nat; dExp: nat }. Definition Fbounded := [b : Fbound] [d : float] ((Zle (Zopp (vNum b)) (Fnum d)) /\ (Zle (Fnum d) (vNum b))) /\ (Zle (Zopp (dExp b)) (Fexp d)). Fnorm.v: Definition of normal, subnormal and canonical numbers FSucc.v : The successor function for bounded numbers FPred.v : The predecessor function for bounded numbers Fprop.v : The proof of Sternbenz property MSB.v : Definition of Most Signigicant Bit and Least Significant Bit Fround.v: Defintion of rounding as a relation between a real and a float: (P r f) means f is a rounded value of r Definitions of the usual rounding modes. FroundProp.v: Standard properties of rounding FroundPlus.v: Standard properties of rounding for addition FroundMult.v: Standard properties of rounding for multiplication Closest.v: Definition of rounding to the closest ClosestProp.v: Standard properties of rounding to the closest ClosestPlus.v: Standard properties of rounding to the closest for addition ClosestMult.v: Standard properties of rounding to the closest for multiplication Closest2Prop.v: Standard properties of rounding to the closest in base 2 Closest2Plus.v: Standard properties of rounding to the closest for addition in base 2 Pradix.v : a simple verification of a program that computes the base.
About
Library for floating point numbers
Resources
License
Stars
Watchers
Forks
Packages 0
No packages published