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

Manajro Linux で TeamViewer が動かなかった

AUR からTeamViewer を入れてコンソールから TeamViewer を起動させたが起動に失敗した。

理由は Systemd のServiceを起動してないためだった。

そのため、次のようにServiceを起動させることによりTeamViewerが使えるようになった。

$sudo systemctl start teamviewd

ChromeOS に fedora 25 をインストール

ChromeOS で Linux 系 OS を使うにはCroutonで Debian, Ubuntu がよく使われる。
しかし、Debian Ubuntu は入るソフトが古く新しいソフトウェアが使えない、そこで、新しいパッケージを使える Fedora 25　を入れ VNC を使い GUI を実現した。


Fedora インストール方法は下のサイトを参考にした。
https://github.com/nmilosev/crouton-fedora

まず次のコマンドを実行する
$cd ~/Downloads
$wget https://github.com/nmilosev/crouton-fedora/archive/master.tar.gz -O crouton-fedora.tar.gz
$tar xvf crouton-fedora.tar.gz
$sudo sh ./crouton-fedora-master/installer/main.sh -r fedora -t fedora


このとき インストールした Fedore のユーザー名とパスワードはともにfedora になっている。
次にGUI の設定のスクリプトを実行するとハングアップしてしまった
$sudo sh /home/fedora/Downloads/crouton-fedora-master/freon-x/install.sh

そこで、
https://nmilosev.svbtle.com/crouton-with-fedora-chroot-chromebook
を参考にして VNC を使う。

次にwindow Manager を入れるがその前にFedora のパッケージを更新する。この作業を忘れるとパッケージの追加更新の際にエラーがたくさん出るようになった。
$sudo dnf upgrade

今回は Window manager に LXDE を使う
$sudo dnf install @lxde

次にVNC Sever を入れVNCのパスワードを設定する。
$sudo dnf install tigervnc-server
$vncpasswd

次に LXDE を起動する設定をする。
$echo '/usr/bin/startlxde' > ~/.vnc/xstartup && chmod +x ~/.vnc/xstartup

次に、VNCサーバーの起動は
$vncserver :1 -geometry 1360x768 -depth 24

VNC クライアントから
localhost :5901
で起動できる。