Commit 1d920615 authored by Arthur Correnson's avatar Arthur Correnson Committed by François Bobot
Browse files

Bplus is compatible with Fle0

parent 28a6cacc
From Flocq Require Import IEEE754.BinarySingleNaN.
From Coq Require Import ZArith.
From F Require Import Utils.
From F Require Import Utils Correction_thms.
(**
The usual ordering relation on [binary_float] is [Bleb]. As defined
......@@ -106,20 +106,102 @@ Lemma Fle0_trans:
Fle0 x y = true -> Fle0 y z = true -> Fle0 x z = true.
Proof.
intros.
fdestruct y.
- fdestruct x; fdestruct z.
now destruct s, s0.
- fdestruct x; fdestruct z.
now destruct s, s0.
- fdestruct x; fdestruct z.
- fdestruct x; fdestruct z.
- fdestruct x; fdestruct z; simpl in *.
+ now destruct s, s0.
+ now destruct s.
+ now destruct s, s0.
+ now destruct s, s0.
+ now destruct s, s0.
+ apply (Bleb_trans _ _ _ H H0).
fdestruct y; fdestruct x; fdestruct z;
try (now destruct s, s0);
try (now destruct s).
apply (Bleb_trans _ _ _ H H0).
Qed.
End Fle0.
\ No newline at end of file
Lemma Fle0_refl:
forall (x : float),
is_nan x = false ->
Fle0 x x = true.
Proof.
intros. fdestruct x.
now apply Beqb_Bleb, Beqb_refl.
Qed.
Inductive interv : Type :=
| I_closed : forall (lo hi : float) (nan : bool) (H : Fle0 lo hi = true), interv
| I_nan : interv.
Definition contains (i : interv) (x : float) : Prop :=
match i with
| I_nan => x = NaN
| I_closed lo hi nan _ =>
(x = NaN /\ nan = true) \/ Fle0 lo x = true /\ Fle0 x hi = true
end.
Lemma contains_nan :
forall (i : interv), contains i NaN ->
(exists a b H, i = I_closed a b true H)
\/ i = I_nan.
Proof.
intros [ ].
+ intros [ [_ ->] | ]; try easy.
left; repeat eexists.
+ now right.
Qed.
Example szerop := I_closed (+0) (+0) false eq_refl.
Example szerom := I_closed (-0) (-0) false eq_refl.
Example contains_szerop :
forall x, contains szerop x -> x = +0.
Proof.
intros x [ [Hx ? ] | ]; try easy.
now apply Fle0_antysim.
Qed.
Example contains_szerom :
forall x, contains szerom x -> x = -0.
Proof.
intros x [ [Hx ? ] | ]; try easy.
now apply Fle0_antysim.
Qed.
Example szero := I_closed (-0) (+0) false eq_refl.
Example contains_szero:
forall x, contains szero x -> (x = -0 \/ x = +0).
Proof.
intros x [ [Hx ? ] | ]; try easy.
fdestruct x; cbn in *.
+ now left.
+ now right.
+ now destruct s.
Qed.
Theorem add_Fle0_mono :
forall (x y z : float) m,
Fle0 x y = true ->
is_nan (Bplus m x z) = false ->
is_nan (Bplus m y z) = false ->
Fle0 (Bplus m x z) (Bplus m y z) = true.
Proof.
intros.
fdestruct x; fdestruct y; try (fdestruct z; now destruct m).
- now apply Fle0_refl.
- fdestruct z; try now destruct m.
now apply Fle0_refl.
- fdestruct z. now destruct m.
apply Bplus_le_compat; try easy.
- now apply Fle0_refl.
- fdestruct z. now destruct m.
now apply Bplus_le_compat.
- fdestruct z.
now apply Bplus_le_compat.
- fdestruct z. now destruct m.
destruct s; simpl (Bplus m -0 _); admit.
- fdestruct z. now destruct m.
destruct s; simpl (Bplus m +0 _); admit.
- fdestruct z.
simpl (Bplus m +oo _).
admit.
- fdestruct z.
admit.
Admitted.
End Fle0.
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