Commit 82e06000 authored by Arthur Correnson's avatar Arthur Correnson Committed by François Bobot
Browse files

introducing the relation Fle0

parent 1959b7d8
......@@ -8,4 +8,5 @@
./thry/Utils.v
./thry/B32.v
./thry/Correction_thms.v
./thry/Test.v
./extraction.v
\ No newline at end of file
From Flocq Require Import IEEE754.BinarySingleNaN.
From Coq Require Import ZArith.
From F Require Import Utils.
(**
The usual ordering relation on [binary_float] is [Bleb]. As defined
in IEEE754, [Bleb] does'nt discriminate the signed zeros and thus
zeros are always in relation regardless of the sign.
We introduce a new relation [Fle0] that extends [Bleb] but discriminates
signed zeros. [Fle0] can be proven to be antisymmetric whereas [Bleb] is not.
*)
Section Fle0.
Variable prec : Z.
Variable emax : Z.
Context (Hprec : FLX.Prec_gt_0 prec).
Context (Hemax : Prec_lt_emax prec emax).
Definition float := binary_float prec emax.
Definition Fle0 (x y : float) :=
match x, y with
| B754_zero s1, B754_zero s2 =>
if negb s1 then negb s2
else true
| _, _ => Bleb x y
end.
Notation "+0" := (B754_zero false).
Notation "-0" := (B754_zero true).
Example Fle0_PP :
Fle0 +0 +0 = true.
Proof.
reflexivity.
Qed.
Example Fle0_PN :
Fle0 +0 -0 = false.
Proof.
reflexivity.
Qed.
Example Fle0_NP :
Fle0 -0 +0 = true.
Proof.
reflexivity.
Qed.
Example Fle0_NN :
Fle0 -0 -0 = true.
Proof.
reflexivity.
Qed.
Example Fle0_sign_true:
forall (x y : float),
x <> NaN ->
y <> NaN ->
Bsign x = true ->
Bsign y = false ->
Fle0 x y = true.
Proof.
intros.
fdestruct x; fdestruct y.
- now destruct s.
- now destruct s.
- now destruct s, s0.
Qed.
(**
Contrary to Bleb, Fle0 is antisymmetric
with respect to Coq's default equality
*)
Lemma Fle0_antysim:
forall (x y : float),
Fle0 x y = true ->
Fle0 y x = true ->
x = y.
Proof.
intros x y Hxy Hyx.
fdestruct x; fdestruct y; try now destruct s.
simpl in Hxy, Hyx.
apply (Bleb_antisymm_strict _ _ _ _ (conj Hxy Hyx)).
now destruct s.
Qed.
End Fle0.
\ No newline at end of file
Supports Markdown
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