問題タブ [real-number]

Coqで実数の簡単な証明をしようとしています。たとえば、2 つの非負数の平均も非負であることを証明したいと考えています。

私の最初のステップは、次のように証明することr1 + r2 >=0です。

しかし、私は得ることができるだけです

仮説で。0 + 0H1 の RHS を に変更できません0。simpl in H1.示されているように試しましたが、何もしませんでした。実数が と違うのはわかりましたnat。しかし、ここで物事をどのように単純化すればよいでしょうか?

(注: 私は実数の初心者です。また、上記のコードはナイーブ/非効率的である可能性があります。改善のための提案は大歓迎です。) また:

Choco Solver で数式をエンコードする方法を探しています。次のような制約をエンコードする方法があることがわかりました。

しかし、私は次のようなものをエンコードしようとしています

ここでx、 とyは int 変数で、係数は実数です。

Matlab には、閉区間でランダムな実数を生成する関数があります。で何かを見つけましたunifrnd()が、開いた間隔で数値を生成しています。使用するunifrnd(x,y);と、[x,y] の代わりに (x,y) 間隔が得られます。

Verilog でガウス ノイズ ジェネレーターを作成しています。

出力がロジックのベクトル (16 ビット) の場合、コードは正常に機能します。

しかし、実数入力を使用している別のブロックと通信するには、このコードが必要です

$bitstoreal 関数を試してみましたが、機能していません。出力は常に O です

私が行ったことは、モジュールの in/out 宣言で output [16, 0] data_out1 を output real data_out1 に置き換え、「assign data_out1 = $bitstoreal(data_out);」を追加することです。data_out は、他のモジュールからのビット ベクトルです。

どんな助けでも

pi を 8087 のレジスタ スタックの一番上にロードし、その定数を短い実メモリ変数に返す簡単なプログラムを作成しました。

shortReal に格納される値は 40 49 0F DB hex です。これは、バイナリで 0100000001001001111111011011 に変換されます。

最初のビットは 0 なので、正の数です。バイアスされた指数部分は 1 に変換されます。

したがって、実際の数値は次のようになります。

1(暗示点)10010010000111111011011

1(暗黙のポイント)1 は 3. に変換されるため、これは PI の正しい整数部分ですが、このポイント以降、私の理解は崩壊します。

現在、次の番号が残っています。

0010010000111111011011

001 は 1 に変換できますが、これは正しいでしょう。ただし、これは、次の番号が 001 になり、これが再び 1 になることを意味します。これは間違っています。または、0010 で 2 になる可能性もありますが、それも間違っています。

小数部分の各桁をどのように区切りますか。