Определение поплавков и доказательств с помощью flocq - PullRequest
Новая
       8

Определение поплавков и доказательств с помощью flocq

0 голосов
/ 04 мая 2018

Я пытаюсь понять, как использовать пакет flocq . Ниже у меня есть простой скрипт, в котором я создал простую функцию. Однако я не могу понять, как создать два binary32 , которые я могу использовать для оценки этой функции. Я застрял на том, как создать доказательство «ограниченного». Я также хотел бы иметь возможность доказать, что, например, для определенного x и y я не получу NaN . Это то, что хорошо для flocq ? Или мог бы быть другой пакет, в который я должен смотреть? Любая помощь приветствуется! 

Require Import Psatz.
From Flocq Require Import Fcore_FTZ Fcore Fcalc_ops Fappli_IEEE Fappli_IEEE_bits.

Definition b32_my_fun (x y : binary32) : binary32 :=
  b32_div mode_NE (b32_plus mode_NE x y) y.

1 Ответ

0 голосов
/ 04 мая 2018

Я соединил этот ответ, изучая копию flocq, которая включена в CompCert. Возможно, вам будет интересно взглянуть на lib/Floats.v CompCert и особенно lib/Fappli_IEEE_extra.v, который накладывает некоторые удобные функции поверх flocq. (Это также означает, что мой ответ может не применим к ванильному флоку, но я думаю, что должен.)

Чтобы создать binary32, используйте функцию flocq binary_normalize из Fappli_IEEE. Вот его тип: 

binary_normalize
     : forall prec emax : Z,
       Prec_gt_0 prec -> prec < emax -> mode -> Z -> Z -> bool -> binary_float prec emax

Для 32-разрядного числа с плавающей запятой IEEE prec равно 24 (биты точности в мантиссе), а emax равно 128 (максимальное значение показателя степени). Аргумент mode является режимом округления, mode_NE должен быть разумным выбором. Два аргумента Z являются значениями мантиссы и показателя степени соответственно; последний бул, по-видимому, является признаком для использования, если мантисса равна 0.

Таким образом, для 32-разрядного числа с плавающей точкой с мантиссой 42 и показателем 32 мы можем попробовать следующее: 

Check (binary_normalize 24 128 _ _ mode_NE 42 23 false).
binary_normalize 24 128 ?prec_gt_0_ ?Hmax mode_NE 42 23 false
     : binary_float 24 128
where
?prec_gt_0_ : [ |- Prec_gt_0 24] 
?Hmax : [ |- 24 < 128]

Осталось предоставить доказательства двух простых целей: Prec_gt_0 24 и 24 < 128. В интерактивном режиме оба из них могут быть доказаны просто reflexivity: 

Goal Prec_gt_0 24.
Proof.
  reflexivity.
Qed.

Термин для таких доказательств просто eq_refl (например, вы можете проверить с помощью Show Proof. перед Qed.). Итак, мы приходим к: 

Check (binary_normalize 24 128 eq_refl eq_refl mode_NE 42 23 false).
binary_normalize 24 128 eq_refl eq_refl mode_NE 42 23 false
     : binary_float 24 128

И мы можем взглянуть на реальное внутреннее представление этого: 

Eval simpl in (binary_normalize 24 128 eq_refl eq_refl mode_NE 42 23 false).
     = B754_finite 24 128 false 11010048 (FLT_exp (-149) 24 29)
         (proj1 (binary_round_correct 24 128 eq_refl eq_refl mode_NE false 42 23))
     : binary_float 24 128

Eval compute in (binary_normalize 24 128 eq_refl eq_refl mode_NE 42 23 false).
     = B754_finite 24 128 false 11010048 5
         (proj1 (binary_round_correct 24 128 eq_refl eq_refl mode_NE false 42 23))
     : binary_float 24 128

И, наконец, мы можем упаковать это в симпатичную маленькую функцию: 

Definition my_binary32 (mantissa exponent: Z): binary32 :=
  binary_normalize 24 128 eq_refl eq_refl mode_NE mantissa exponent false.

И проверить это: 

Eval simpl in (my_binary32 42 23).
     = B754_finite 24 128 false 11010048 (FLT_exp (-149) 24 29)
         (proj1 (binary_round_correct 24 128 eq_refl eq_refl mode_NE false 42 23))
     : binary32

Eval simpl in (my_binary32 42 230).
     = B754_infinity 24 128 false
     : binary32
...