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

quick fix of the bug with fp singleton {0}

parent b032b78a
......@@ -47,7 +47,17 @@ module Intv32 =
let is_singleton = function
| Inan -> Some B754_nan
| Intv (a, b, n) ->
if (&&) (coq_Beqb prec emax a b) (Pervasives.not n) then Some a else None
if (&&)
((&&) (coq_Beqb prec emax a b)
(Pervasives.not (coq_Beqb prec emax a (B754_zero false))))
(Pervasives.not n)
then Some a
else None
(** val s0 : coq_Interval **)
let s0 =
Intv ((B754_zero false), (B754_zero true), false)
(** val singleton : float32 -> t **)
......
......@@ -23,6 +23,8 @@ module Intv32 :
val is_singleton : t -> float32 option
val s0 : coq_Interval
val singleton : float32 -> t
val ge : t -> t_opt
......
......@@ -70,30 +70,29 @@ Module Intv32.
match I with
| Inan _ _ => Some NaN
| Intv _ _ a b n =>
if Beqb a b && negb n then Some a
if Beqb a b && (negb (Beqb a (B754_zero false))) && negb n then Some a
else None
end.
Program Lemma is_singleton_eq_aux :
forall (I : t) (x a b : float32) n H, is_singleton (exist (fun I : Interval' prec emax => valid prec emax I)
(Intv prec emax a b n) H) = Some x -> x = a.
Proof.
cbn; intros.
destruct Beqb, negb; simpl in *; congruence.
Qed.
Program Definition s0 : Interval prec emax := Intv _ _ (B754_zero false) (B754_zero true) false.
Compute (is_singleton s0).
Program Theorem is_singleton_correct :
forall (I : t) (x : float32), (is_singleton I = Some x) -> (forall y, contains I y -> Beqb x y = true \/ (is_nan x && is_nan y = true)).
forall (I : t) (x : float32), (is_singleton I = Some x) -> (forall y, contains I y -> x = y).
Proof.
intros [[| a b n] H] x; cbn.
+ intros. inversion H0; fdestruct y; now right.
+ intros. destruct (Beqb a b) eqn:E1, (negb n) eqn:E; try easy; simpl in *.
inversion H0; subst. left.
destruct H1 as [ [H1 H2] | H1 ].
- assert (b <= y <= b) by eauto using E1, Beqb_symm, Beqb_Bleb, Bleb_trans.
apply Bleb_antisymm in H3.
eapply Beqb_trans; eauto using Beqb_symm.
- destruct n; fdestruct y.
- intros H1; inversion H1; fdestruct y.
- intros H' y [[H1 H2] | H2].
+ destruct (Beqb a b) eqn:?E, (negb n) eqn:?E, (negb (Beqb a (B754_zero false))) eqn:?; try easy; simpl in *.
assert (a <= y <= a) by eauto using E, Beqb_symm, Beqb_Bleb, Bleb_trans.
apply Bleb_antisymm_strict in H0.
* inversion H'; subst; reflexivity.
* now apply Bool.negb_true_iff in Heqb0.
+ destruct (Beqb a b) eqn:?E, (negb n) eqn:?E, (negb (Beqb a (B754_zero false))) eqn:?; try easy; simpl in *.
destruct n; try easy.
fdestruct y.
Qed.
Program Definition singleton (x : float32) : t :=
......@@ -107,10 +106,11 @@ Module Intv32.
Defined.
Program Theorem singleton_correct :
forall x, is_singleton (singleton x) = Some x.
forall (x : float32), Beqb x (B754_zero true) = false -> is_singleton (singleton x) = Some x.
Proof.
intros [ [ ] | [ ] | | [ ] ]; try easy; cbn;
rewrite Z.compare_refl, Pcompare_refl; reflexivity.
intros [ [ ] | [ ] | | [ ] ] H; try easy; cbn.
- rewrite Z.compare_refl, Pcompare_refl; reflexivity.
- rewrite Z.compare_refl, Pcompare_refl; reflexivity.
Qed.
Program Definition ge : t -> t_opt := @Ige prec emax.
......
......@@ -400,6 +400,37 @@ Proof.
lra.
Qed.
Axiom proof_irr :
forall m e (H H' : SpecFloat.bounded prec emax m e = true), H = H'.
Lemma Bleb_antisymm_strict :
forall x y : float, x <= y <= x -> Beqb x (B754_zero true) = false -> x = y.
Proof.
intros x y [H1 H2].
fdestruct x; fdestruct y;
try (destruct s; try easy);
try (destruct s0; try easy).
- intros _.
cbn in H1, H2.
destruct (e ?= e1)%Z eqn:E1; rewrite (Z.compare_antisym _ _), E1 in H2; simpl in H2; try discriminate.
rewrite <- ZC4 in H1.
destruct (Pos.compare_cont Eq m0 m) eqn:E2; try easy.
apply (Pcompare_Eq_eq _ _) in E2; subst.
apply (Z.compare_eq) in E1; subst; cbn.
rewrite (proof_irr _ _ e0 e2).
reflexivity.
- intros _.
cbn in H1, H2.
rewrite ZC4 in H2.
destruct (e1 ?= e)%Z eqn:E1; rewrite (Z.compare_antisym _ _), E1 in H1; simpl in H2; try discriminate.
destruct (Pos.compare_cont Eq m m0) eqn:E2; try easy.
+ apply (Pcompare_Eq_eq _ _) in E2; subst.
apply (Z.compare_eq) in E1; subst; cbn.
rewrite (proof_irr _ _ e0 e2).
reflexivity.
Qed.
Lemma Bleb_antisymm :
forall x y : float, x <= y <= x -> Beqb x y = true.
Proof.
......
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