Coq で小数演算

Coq で小数を含む演算を行う。

次のような小数点を含む数値はエラーが出て使えなかった。

Compute 3.3.


そこで、Coq の標準ライブラリ Float で 浮動小数点 の規格 IEEE754 をサポートしている.

IEEE 754 は符号s（0または1）、仮数 c、指数 q の3つの整数で表現し、(−1)^s × c × b^q　
で表される。
Float を使い  c q を設定し、 FtoR 関数を用いて b を決め実数型 R へ変換する.

Require Import Float.Float.
Variable c q b:Z.
Compute (Float c q).
Compute (FtoR b (Float c q).

参考
Mare Daumas, Laurence Rideau, Laurent Thery:A Generic Library of Floating-Point Numbers and its Application to Exact Computing

ftp://ftp-sop.inria.fr/marelle/Laurent.Thery/float.ppt