Commit 0abac1ea authored by Guillaume Melquiond's avatar Guillaume Melquiond

Add functions for erasing proof terms from binary_float.

parent 784678ee
......@@ -416,6 +416,29 @@ Proof.
easy.
Qed.
Definition erase (x : binary_float) : binary_float.
Proof.
destruct x as [s|s|s pl H|s m e H].
- exact (B754_zero s).
- exact (B754_infinity s).
- apply (B754_nan s pl).
destruct nan_pl.
apply eq_refl.
exact H.
- apply (B754_finite s m e).
destruct bounded.
apply eq_refl.
exact H.
Defined.
Theorem erase_correct :
forall x, erase x = x.
Proof.
destruct x as [s|s|s pl H|s m e H] ; try easy ; simpl.
- apply f_equal, eqbool_irrelevance.
- apply f_equal, eqbool_irrelevance.
Qed.
(** Opposite *)
Definition Bopp opp_nan x :=
......
......@@ -639,6 +639,7 @@ Definition binop_nan_pl32 (f1 f2 : binary32) : { nan : binary32 | is_nan 24 128
| _, _ => default_nan_pl32
end.
Definition b32_erase : binary32 -> binary32 := erase 24 128.
Definition b32_opp : binary32 -> binary32 := Bopp 24 128 unop_nan_pl32.
Definition b32_abs : binary32 -> binary32 := Babs 24 128 unop_nan_pl32.
Definition b32_sqrt : mode -> binary32 -> binary32 := Bsqrt _ _ Hprec Hprec_emax unop_nan_pl32.
......@@ -687,6 +688,7 @@ Definition binop_nan_pl64 (f1 f2 : binary64) : { nan : binary64 | is_nan 53 1024
| _, _ => default_nan_pl64
end.
Definition b64_erase : binary64 -> binary64 := erase 53 1024.
Definition b64_opp : binary64 -> binary64 := Bopp 53 1024 unop_nan_pl64.
Definition b64_abs : binary64 -> binary64 := Babs 53 1024 unop_nan_pl64.
Definition b64_sqrt : mode -> binary64 -> binary64 := Bsqrt _ _ Hprec Hprec_emax unop_nan_pl64.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment