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

[farith2] rewrite Assert

parent 68a05f02
......@@ -65,6 +65,26 @@ module Intv32 =
| B754_nan -> Inan
| _ -> Intv (x, x, false)
(** val s00 : t **)
let s00 =
Intv ((B754_zero false), (B754_zero false), false)
(** val s01 : t **)
let s01 =
Intv ((B754_zero false), (B754_zero true), false)
(** val s10 : t **)
let s10 =
Intv ((B754_zero true), (B754_zero false), false)
(** val s11 : t **)
let s11 =
Intv ((B754_zero true), (B754_zero true), false)
(** val ge : t -> t_opt **)
let ge =
......
......@@ -27,6 +27,14 @@ module Intv32 :
val singleton : float32 -> t
val s00 : t
val s01 : t
val s10 : t
val s11 : t
val ge : t -> t_opt
val le : t -> t_opt
......
......@@ -26,6 +26,7 @@ Module Assert (M : Inhabited).
End Assert.
Module GenericFloat.
Record F : Type := {
prec : Z;
emax : Z;
......@@ -33,6 +34,21 @@ Module GenericFloat.
Hemax : Prec_lt_emax prec emax;
value : binary_float prec emax;
}.
Require Import Bool.
Program Definition unify (p e p' e' : Z) (f : binary_float p' e') (Hp : p = p') (Hp : e = e') : binary_float p e := f.
Program Definition same_format_cast {p e p' e' : Z} (H : ((p =? p') && (e =? e') = true)%Z) (f : binary_float p' e') : binary_float p e := f.
Next Obligation.
apply andb_true_iff in H as [A _].
now rewrite (proj1 (Z.eqb_eq _ _) A).
Defined.
Next Obligation.
apply andb_true_iff in H as [_ B].
now rewrite (proj1 (Z.eqb_eq _ _) B).
Defined.
Module F_inhab.
Definition t : Type := F.
Program Definition dummy := {|
......@@ -44,38 +60,39 @@ Module GenericFloat.
|}.
Solve All Obligations with easy.
End F_inhab.
Module AssertF := Assert (F_inhab).
Definition same_format (x y : F) : bool :=
Z.eqb (prec x) (prec y) && Z.eqb (emax x) (emax y).
Z.eqb (prec x) (prec y) && Z.eqb (emax x) (emax y).
Program Definition add (m : mode) (x y : F) :=
match same_format x y with
| true => Some {|
prec := prec x;
emax := emax x;
Hprec := Hprec x;
Hemax := Hemax x;
value := @Bplus _ _ (Hprec x) (Hemax x) m (value x) (same_format_cast _ (value y))
|}
| false => None
end.
Program Definition Fadd (m : mode) (x y : F) : F :=
AssertF.assert (same_format x y) (fun _ => {|
Definition Fadd (m : mode) (x y : F) : F :=
AssertF.assert (same_format x y) (fun H => {|
prec := prec x;
emax := emax x;
Hprec := Hprec x;
Hemax := Hemax x;
value := _;
value := @Bplus _ _ (Hprec x) (Hemax x) m (value x) (same_format_cast H (value y));
|}).
Next Obligation.
apply andb_prop in H as [Hp He].
rewrite Z.eqb_eq in Hp, He.
destruct x as [ ? ? ? ? vx ], y as [ ? ? ? ? vy ]; simpl in *; subst.
apply (Bplus m vx vy).
Defined.
Program Definition Fsub (m : mode) (x y : F) : F :=
AssertF.assert (same_format x y) (fun _ => {|
Definition Fsub (m : mode) (x y : F) : F :=
AssertF.assert (same_format x y) (fun H => {|
prec := prec x;
emax := emax x;
Hprec := Hprec x;
Hemax := Hemax x;
value := _;
value := @Bminus _ _ (Hprec x) (Hemax x) m (value x) (same_format_cast H (value y));
|}).
Next Obligation.
apply andb_prop in H as [Hp He].
rewrite Z.eqb_eq in Hp, He.
destruct x as [ ? ? ? ? vx ], y as [ ? ? ? ? vy ]; simpl in *; subst.
apply (Bminus m vx vy).
Defined.
End GenericFloat.
\ No newline at end of file
......@@ -669,13 +669,8 @@ Proof.
replace 0%R with (@B2R prec emax +0) by auto.
rewrite <- B2R_Bopp.
apply Bleb_Rle; auto.
*
(* *
simpl in Hxy.
destruct (Raux.Req_bool r 0) eqn:E.
- now destruct b.
......@@ -690,16 +685,9 @@ Proof.
destruct (Raux.Req_bool_spec r 0); try easy.
rewrite Raux.Rlt_bool_true by lra.
unfold Rx0le.
destruct Raux.Req_bool.
destruct Raux.Req_bool. *)
Admitted.
Theorem add_Fle0_mono :
forall (x y z : float) m,
......@@ -739,7 +727,6 @@ Proof.
- fdestruct z.
apply B2Rx0_Fle0.
apply Fle0_B2Rx0 in H.
eapply add_Rx0le_mono_l.
Admitted.
End Fle0.
......
......@@ -2,6 +2,8 @@ From Coq Require Import ZArith Extraction Bool Psatz ExtrOcamlBasic.
From Flocq Require Import IEEE754.BinarySingleNaN FLX.
From F Require Import Utils Interval B32.
Notation "x '+⊥'" := (option x) (at level 80).
Module Intv32.
......@@ -102,10 +104,23 @@ Module Intv32.
fdestruct x.
Defined.
Program Example s00 : t := Intv prec emax (B754_zero false) (B754_zero false) false.
Program Example s01 : t := Intv prec emax (B754_zero false) (B754_zero true) false.
Program Example s10 : t := Intv prec emax (B754_zero true) (B754_zero false) false.
Program Example s11 : t := Intv prec emax (B754_zero true) (B754_zero true) false.
(** /!\ Série alternante !!! *)
Compute (proj1_sig (inter s10 s00)) (* s00*).
Compute (proj1_sig (inter s00 s10)) (* s10 *).
Compute (proj1_sig (inter s00 s10)) (* s10*).
Compute (proj1_sig (inter s10 s00)) (* s00 *).
Program Theorem singleton_correct :
forall (x : float32), Beqb x (B754_zero true) = false -> is_singleton (singleton x) = Some x.
Proof.
intros [ [ ] | [ ] | | [ ] ] H; try easy; cbn.
intros [ [ ] | [ ] | | [ ] ] H; try easy; cbn.
- rewrite Z.compare_refl, Pcompare_refl; reflexivity.
- rewrite Z.compare_refl, Pcompare_refl; reflexivity.
Qed.
......@@ -164,7 +179,7 @@ Module Intv32.
Proof. apply (@Ige_correct prec emax). Qed.
Theorem gt_correct :
forall (I : t) (x y : float32), contains I y -> Bltb y x = true -> contains_opt (gt I) x.
forall (I : t) (x y : float32), contains I y -> Bltb y x = true -> contains_opt (gt I) x.
Proof. apply (@Igt_correct prec emax). Qed.
End Intv32.
\ 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