Skip to content
Snippets Groups Projects
Commit 67c5f554 authored by Arthur Correnson's avatar Arthur Correnson
Browse files

[ieee/coq] cleaning proofs

parent 5375de5a
No related branches found
No related tags found
1 merge request!16Fp/ieee
Pipeline #36205 waiting for manual action
Stage: test
Stage: deploy
Hide whitespace changes
Inline Side-by-side
src_common/ieee/coq/Finterval.v
+ 2
− 233
View file @ 67c5f554
......@@ -13,11 +13,6 @@ Variable emax : Z.
Context (Hprec : FLX.Prec_gt_0 prec).
Context (Hemax : Prec_lt_emax prec emax).
Notation "x <= y" := (Bleb x y = true).
Notation "x <= y <= z" := (Bleb x y = true /\ Bleb y z = true).
Notation "'+oo'" := (B754_infinity false).
Notation "'-oo'" := (B754_infinity true).
Definition float := binary_float prec emax.
Record Interval := MK_INTERVAL {
......@@ -166,232 +161,6 @@ Lemma Iadd2_correct :
x ∈ I1 -> y ∈ I2 ->
Bplus m x y ∈ Iadd2 m I1 I2.
Proof.
intros m x y I1 I2 [ ] [ ] [ [Hx1 Hx2] | Hx ] [ [Hy1 Hy2] | Hy ];
destruct I1 as [lo1 hi1 nan1] eqn:EI1;
destruct I2 as [lo2 hi2 nan2] eqn:EI2;
unfold γ in *;
simpl in *.
- destruct (is_nan (Bplus m lo1 lo2)) eqn:E1;
destruct (is_nan (Bplus m hi1 hi2)) eqn:E2.
+ unfold Iadd2; simpl.
rewrite (is_nan_inv _ _ _ E1).
rewrite (is_nan_inv _ _ _ E2).
simpl. right. easy.
End Finterval.
(* Module MakeI (F : B_FORMAT).
Module Float := MakeIEEE F.
Local Notation "x <= y" := (Float.le x y = true).
Local Notation "x <= y <= z" := (Float.le x y = true /\ Float.le y z = true).
Local Notation "'+oo'" := (B754_infinity false).
Local Notation "'-oo'" := (B754_infinity true).
Axiom Fadd_le_compat:
forall m (w x y z : Float.T),
is_nan w = false ->
is_nan x = false ->
is_nan y = false ->
is_nan z = false ->
w <= x -> y <= z ->
Float.add m w y <= Float.add m x z.
Record Interval := MK_INTERVAL {
lo : Float.T;
hi : Float.T;
infp : bool;
infm : bool;
nan : bool;
}.
Definition contains (I : Interval) (x : Float.T) :=
(lo I <= x <= hi I) \/
(Float.is_nan x = true /\ nan I = true) \/
(Float.is_infp x = true /\ infp I = true) \/
(Float.is_infm x = true /\ infm I = true).
Notation "x ∈ I" := (contains I x) (at level 80).
Definition orb2 (x y : bool) :=
match x with
| false => y
| true => true
end.
Lemma orb2_orb :
forall b1 b2, b1 || b2 = orb2 b1 b2.
Proof. now intros [ ] [ ]. Qed.
Definition andb2 (x y : bool) :=
match x, y with
| true, true => true
| _, _ => false
end.
Lemma andb2_andb :
forall b1 b2, b1 && b2 = andb2 b1 b2.
Proof. now intros [ ] [ ]. Qed.
Infix "or" := (orb2) (at level 50).
Infix "and" := (andb2) (at level 40).
Definition check (I : Interval) : bool :=
is_finite (lo I) and is_finite (hi I).
Definition Iadd (m : mode) (A B : Interval) : Interval :=
let (a1, b1) := (lo A, hi A) in
let (a2, b2) := (lo B, hi B) in
let a := Float.add m a1 a2 in
let b := Float.add m b1 b2 in
let nan := (nan A) or (nan B) or (infp A and infm B) or (infm A and infp B) in
MK_INTERVAL a b (infp A or infp B) (infm A or infm B) nan.
Ltac checked :=
match goal with
| [ H : check _ = true |- _ ] =>
unfold check in H;
rewrite <- andb2_andb in H;
rewrite Bool.andb_true_iff in H;
simpl in H;
destruct H;
checked
| _ => idtac
end.
Ltac contained :=
match goal with
| [ H : contains _ _ |- _ ] =>
case H; [ simpl; intros [ ] | simpl; intros [ ] ];
clear H;
contained
| _ => idtac
end.
Ltac classify_nan x :=
match goal with
| [ H : Float.is_nan x = true |- _ ] =>
rewrite (Float.is_nan_inv x H) in *
| [ H : _ <= x |- _ ] =>
assert (Float.is_nan x = false) by apply (Float.le_not_nan_r _ _ H)
| [ H : x <= _ |- _ ] =>
assert (Float.is_nan x = false) by apply (Float.le_not_nan_l _ _ H)
| _ => fail "can't determine if" x "is NaN"
end.
Ltac classify_inf x :=
match goal with
| [ H : Float.is_infp x = true |- _ ] =>
rewrite (Float.is_infp_inv x H) in *
| [ H : +oo <= x |- _ ] =>
rewrite (Float.infp_le_is_infp _ H) in *
| [ H : Float.is_infm x = true |- _ ] =>
rewrite (Float.is_infm_inv x H) in *
| [ H : x <= -oo |- _ ] =>
rewrite (Float.le_infm_is_infm x H) in *
| _ => fail "can't determine if" x "is +oo or -oo"
end.
Ltac feasy :=
try easy;
match goal with
| |- is_nan ?x = false => classify_nan x; (try easy; intuition)
end.
Ltac auto_contain :=
try easy; first [ progress (right; simpl; intuition) | progress (left; simpl; intuition) ].
Lemma contains_nan :
forall I, contains I Float.NaN <-> nan I = true.
Proof.
intros [ ? ? ? ? [ ] ]; simpl; split; intros; try auto_contain.
inversion H; try easy; intuition.
Qed.
Lemma bounded_finite :
forall m M x, m <= x <= M -> is_finite m = true -> is_finite M = true -> Float.is_finite x = true.
Proof.
intros m M x Hx Fm FM.
destruct Hx, x; try easy.
destruct s.
- classify_inf m; discriminate.
- classify_inf M; discriminate.
Qed.
Ltac boolean :=
match goal with
| [ |- true = _ ] => symmetry; boolean
| [ |- true or _ = true ] => simpl; reflexivity
| [ |- ?x or true = true ] =>
destruct x; simpl; reflexivity
| [ |- ?x or ?y = true ] =>
replace x with true by boolean; boolean
end.
Ltac irewrite :=
match goal with
| [ H : infp _ = _ |- _ ] => rewrite H; irewrite
| [ H : infm _ = _ |- _ ] => rewrite H; irewrite
| [ H : nan _ = _ |- _ ] => rewrite H; irewrite
| _ => idtac
end.
Ltac fdiscriminate x :=
(classify_inf x; discriminate) ||
(classify_nan x; discriminate).
Ltac fdestruct x :=
destruct (x : Float.T) as [ [ ] | [ ] | | ].
Lemma Iadd_correct :
forall m ix iy x y,
check ix = true ->
check iy = true ->
contains ix x ->
contains iy y ->
contains (Iadd m ix iy) (Float.add m x y).
Proof.
intros.
checked.
contained; intuition; unfold Iadd; irewrite.
+ left; split; simpl; apply Float.add_le_compat; eauto using bounded_finite.
+ classify_nan x; irewrite; auto_contain.
+ classify_inf x. fdestruct y; auto_contain.
classify_inf (lo iy); discriminate.
+ classify_inf x. fdestruct y;
try fdiscriminate (hi iy); auto_contain.
+ classify_nan y; fdestruct x; auto_contain.
+ classify_nan x; auto_contain.
+ classify_nan y; fdestruct x; auto_contain.
+ classify_nan y; fdestruct x; auto_contain.
+ classify_inf y; fdestruct x;
try fdiscriminate (lo ix); auto_contain.
+ classify_inf y; fdestruct x;
try fdiscriminate (hi ix); auto_contain.
+ classify_nan x; auto_contain.
+ classify_nan x; auto_contain.
+ classify_inf x; classify_inf y; auto_contain.
+ classify_inf x; classify_inf y; auto_contain.
+ classify_inf x; classify_inf y; auto_contain.
+ classify_inf x; classify_inf y; auto_contain.
Qed.
Lemma Iadd_check :
forall m ix iy,
check ix = true ->
check iy = true ->
Float.dont_overflow m Rplus (lo ix) (lo iy) = true ->
Float.dont_overflow m Rplus (hi ix) (hi iy) = true ->
check (Iadd m ix iy) = true.
Proof.
intros m ix iy Hx Hy; checked.
unfold check.
rewrite <- andb2_andb, Bool.andb_true_iff; split; now apply Float.add_finite.
Qed.
Admitted.
End MakeI. *)
\ No newline at end of file
End Finterval.
\ No newline at end of file
src_common/ieee/coq/Futils.v
+ 1
− 226
View file @ 67c5f554
......@@ -194,229 +194,4 @@ End Utils.
Arguments le_not_nan {prec} {emax}.
Arguments le_not_nan_l {prec} {emax}.
Arguments le_not_nan_r {prec} {emax}.
(* Class leb_op (A:Type) : Type := leb : A -> A -> bool.
Local Notation "x <= y" := (leb x y = true).
Class ltb_op (A:Type) : Type := ltb : A -> A -> bool.
Local Notation "x < y" := (ltb x y = true).
Class eqb_op (A:Type) : Type := eqb : A -> A -> bool.
Local Notation "x = y" := (eqb x y = true).
Class infp_symb (A:Type) : Type := infp : A.
Local Notation "+oo" := (infp).
Class infm_symb (A:Type) : Type := infm : A.
Local Notation "-oo" := (infm).
Module Type B_FORMAT.
Parameter prec : Z.
Parameter emax : Z.
Parameter Hprec : (0 < prec)%Z.
Parameter Hprec_emax : (prec < emax)%Z.
End B_FORMAT.
Module MakeIEEE (F : B_FORMAT).
Definition T := binary_float F.prec F.emax.
Definition NaN : T := B754_nan.
Definition add (m : mode) : T -> T -> T := @Bplus _ _ F.Hprec F.Hprec_emax m.
Definition sub (m : mode) : T -> T -> T := @Bminus _ _ F.Hprec F.Hprec_emax m.
Definition mul (m : mode) : T -> T -> T := @Bmult _ _ F.Hprec F.Hprec_emax m.
Definition div (m : mode) : T -> T -> T := @Bdiv _ _ F.Hprec F.Hprec_emax m.
Definition sqrt (m : mode) : T -> T := @Bsqrt _ _ F.Hprec F.Hprec_emax m.
Instance lt : ltb_op T := Bltb.
Instance le : leb_op T := Bleb.
#[global] Transparent leb.
Instance eq : eqb_op T := Beqb.
Instance infm : infm_symb T := B754_infinity true.
Instance infp : infp_symb T := B754_infinity false.
Definition is_inf (x : T) :=
match x with
| B754_infinity _ => true
| _ => false
end.
Definition is_infp (x : T) :=
match x with
| B754_infinity s => negb s
| _ => false
end.
Definition is_infm (x : T) :=
match x with
| B754_infinity s => s
| _ => false
end.
Definition is_finite (x : T) := is_finite x.
Definition is_nan (x : T) := is_nan x.
Lemma le_Rle :
forall (x y :T),
is_finite x = true ->
is_finite y = true ->
x <= y -> (B2R x <= B2R y)%R.
Proof.
intros x y Fx Fy Hxy.
unfold leb, le, Bleb, SpecFloat.SFleb in Hxy.
replace (SpecFloat.SFcompare (B2SF x) (B2SF y)) with (Bcompare x y) in Hxy by auto.
pose proof (Bcompare_correct _ _ x y Fx Fy).
rewrite H in Hxy.
destruct Raux.Rcompare eqn:E in Hxy.
- right. auto using Raux.Rcompare_Eq_inv.
- left. auto using Raux.Rcompare_Lt_inv.
- discriminate.
Qed.
Lemma Rle_le :
forall (x y :T),
is_finite x = true ->
is_finite y = true ->
(B2R x <= B2R y)%R -> x <= y.
Proof.
intros x y Fx Fy Hxy.
unfold leb, le, Bleb, SpecFloat.SFleb.
replace (SpecFloat.SFcompare (B2SF x) (B2SF y)) with (Bcompare x y) by auto.
rewrite (Bcompare_correct _ _ _); auto.
destruct Raux.Rcompare eqn:E; auto.
apply Raux.Rcompare_Gt_inv in E; lra.
Qed.
Definition add_to_nan (x y : T) :=
((is_infm x && is_infp y) || (is_infp x && is_infm y))%bool.
Definition dont_overflow (m : mode) (op : R -> R -> R) (x y : T) : bool :=
let fexp := @SpecFloat.fexp F.prec F.emax in
let fmax := Raux.bpow Zaux.radix2 F.emax in
let rsum := Generic_fmt.round Zaux.radix2 fexp (round_mode m) (op (B2R x) (B2R y)) in
Raux.Rlt_bool (Rabs rsum) fmax.
Lemma add_le_compat_aux :
forall m w x y z,
is_finite w = true ->
is_finite x = true ->
is_finite y = true ->
is_finite z = true ->
dont_overflow m Rplus w y = true ->
dont_overflow m Rplus x z = true ->
(B2R w <= B2R x)%R -> (B2R y <= B2R z)%R ->
(B2R (add m w y) <= B2R (add m x z))%R.
Proof.
intros m w x y z Fw Fx Fy Fz Ho1 Ho2 Hwx Hyz.
unfold dont_overflow in Ho1, Ho2; unfold add.
pose proof (Hc1 := Bplus_correct _ _ F.Hprec F.Hprec_emax m w y Fw Fy).
pose proof (Hc2 := Bplus_correct _ _ F.Hprec F.Hprec_emax m x z Fx Fz).
pose proof F.Hprec_emax; pose proof F.Hprec.
rewrite Ho1 in Hc1; rewrite Ho2 in Hc2.
rewrite (proj1 Hc1), (proj1 Hc2).
apply Generic_fmt.round_le;
unfold SpecFloat.fexp, SpecFloat.emin, Generic_fmt.Valid_exp in *;
intuition.
Qed.
Lemma add_le_compat_aux2 :
forall m w x y z,
is_nan w = false ->
is_nan x = false ->
is_nan y = false ->
is_nan z = false ->
add_to_nan w y = false ->
add_to_nan x z = false ->
dont_overflow m Rplus w y = true ->
dont_overflow m Rplus x z = true ->
(B2R w <= B2R x)%R -> (B2R y <= B2R z)%R ->
(B2R (add m w y) <= B2R (add m x z))%R.
Proof.
Lemma add_finite :
forall m x y,
is_finite x = true ->
is_finite y = true ->
dont_overflow m Rplus x y = true ->
is_finite (add m x y) = true.
Proof.
intros m x y Fx Fy Ho.
unfold dont_overflow in Ho; unfold add.
pose proof (Bplus_correct _ _ F.Hprec F.Hprec_emax m x y Fx Fy).
rewrite Ho in H. intuition.
Qed.
Lemma add_le_compat :
forall m w x y z,
is_finite w = true ->
is_finite x = true ->
is_finite y = true ->
is_finite z = true ->
dont_overflow m Rplus w y = true ->
dont_overflow m Rplus x z = true ->
w <= x -> y <= z ->
add m w y <= add m x z.
Proof.
intros m w x y z Fw Fx Fy Fz Ho1 Ho2 Hwx Hyz.
unfold dont_overflow in Ho1, Ho2; unfold add.
assert(Hwx': (B2R w <= B2R x)%R) by auto using le_Rle.
assert(Hyz': (B2R y <= B2R z)%R) by auto using le_Rle.
pose proof (add_le_compat_aux m w x y z Fw Fx Fy Fz Ho1 Ho2 Hwx' Hyz').
apply Rle_le; auto using add_finite.
Qed.
Lemma add_nan :
forall m x y,
is_finite x = true ->
is_finite y = true ->
is_nan (add m x y) = false.
Proof.
intros m [[ ] | [ ] | | ] [ [ ] | [ ] | | ] Fx Fy; try easy.
- now destruct m.
- now destruct m.
- unfold add, Bplus, is_nan.
auto using is_nan_binary_normalize.
Qed.
End MakeIEEE.
Module B32_FORMAT : B_FORMAT.
Definition emax := 128%Z.
Definition prec := 24%Z.
Lemma Hprec : (0 < prec)%Z.
Proof. reflexivity. Qed.
Lemma Hprec_emax : (prec < emax)%Z.
Proof. reflexivity. Qed.
End B32_FORMAT.
Module B32 := MakeIEEE (B32_FORMAT).
Module B64_FORMAT : B_FORMAT.
Definition emax := 1024%Z.
Definition prec := 53%Z.
Lemma Hprec : (0 < prec)%Z.
Proof. reflexivity. Qed.
Lemma Hprec_emax : (prec < emax)%Z.
Proof. reflexivity. Qed.
End B64_FORMAT.
Module B64 := MakeIEEE (B64_FORMAT). *)
\ No newline at end of file
Arguments le_not_nan_r {prec} {emax}.
\ No newline at end of file
src_common/ieee/coq/Rextended.v
+ 61
− 1
View file @ 67c5f554
From Flocq Require Import IEEE754.BinarySingleNaN.
From Coq Require Import ZArith Psatz Reals.
(*********************************************************
Extension of R with special values +oo, -oo
**********************************************************)
Set Implicit Arguments.
Section Rextended.
......@@ -99,18 +103,74 @@ Definition B2Rx (x : float) :=
| _ => Real (B2R x)
end.
Lemma B2Rx_finite :
forall (f : float),
is_finite f = true -> B2Rx f = Real (B2R f).
Proof. now destruct f. Qed.
Lemma B2Rx_le :
forall (x y : float),
is_nan x = false ->
is_nan y = false ->
leb (B2Rx x) (B2Rx y) = true ->
Bleb x y = true.
Proof.
intros.
destruct x as [[ ] | [ ] | | ] eqn:E1; destruct y as [ [ ] | [ ] | | ] eqn:E2; try easy;
rewrite <- E1, <- E2 in *;
rewrite B2Rx_finite in H1 by (rewrite E1; auto);
rewrite B2Rx_finite in H1 by (rewrite E2; auto);
unfold leb in H1;
unfold Bleb, SpecFloat.SFleb;
replace (SpecFloat.SFcompare (B2SF x) (B2SF y)) with (Bcompare x y) by auto;
assert (Fx: is_finite x = true) by (rewrite E1; auto);
assert (Fy: is_finite y = true) by (rewrite E2; auto);
rewrite (Bcompare_correct _ _ x y Fx Fy);
destruct Raux.Rcompare eqn:E; auto;
apply Raux.Rcompare_Gt_inv in E;
destruct (Raux.Rle_bool_spec (B2R x) (B2R y)); auto; lra.
Qed.
Ltac fdestruct f :=
destruct f as [ [ ] | [ ] | | ] eqn:?E; try easy.
Lemma B2Rx_B2R :
forall (x : float),
is_finite x = true ->
B2Rx x = Real (B2R x).
Proof. now intros [ ] Fx. Qed.
Lemma le_B2Rx :
forall (x y : float),
Bleb x y = true ->
leb (B2Rx x) (B2Rx y) = true.
Proof.
Ltac by_comparison :=
match goal with
| [ x : _, y : _, E : _, E0 : _, H : _ |- _ ] =>
rewrite <- E, <- E0 in H;
unfold Bleb, SpecFloat.SFleb in H;
replace (SpecFloat.SFcompare (B2SF _) (B2SF _)) with (Bcompare x y) in H by auto;
rewrite E, E0 in *;
rewrite Bcompare_correct in H by auto;
rewrite B2Rx_B2R by auto;
rewrite B2Rx_B2R, leb_real by auto;
destruct (Raux.Rcompare _) eqn:Cmp in H; try easy;
[ apply Raux.Rcompare_Eq_inv in Cmp | apply Raux.Rcompare_Lt_inv in Cmp ];
apply Raux.Rle_bool_true; lra
end.
Ltac by_computation :=
simpl; apply Raux.Rle_bool_true; lra.
intros.
fdestruct x; fdestruct y; try by_computation; by_comparison.
Qed.
End Rextended.
Arguments round {prec} {emax}.
Arguments B2Rx {prec} {emax}.
\ No newline at end of file
Arguments B2Rx {prec} {emax}.
Arguments B2Rx_le {prec} {emax}.
Arguments le_B2Rx {prec} {emax}.
Arguments B2Rx_B2R {prec} {emax}.
Arguments B2Rx_finite {prec} {emax}.
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