From 67c5f554b59362bf09c80bd04dbb18e45e55c3c6 Mon Sep 17 00:00:00 2001
From: Arthur Correnson <arthur.correnson@gmail.com>
Date: Tue, 29 Jun 2021 10:29:15 +0200
Subject: [PATCH] [ieee/coq] cleaning proofs
---
src_common/ieee/coq/Finterval.v | 235 +-------------------------------
src_common/ieee/coq/Futils.v | 227 +-----------------------------
src_common/ieee/coq/Rextended.v | 62 ++++++++-
3 files changed, 64 insertions(+), 460 deletions(-)
diff --git a/src_common/ieee/coq/Finterval.v b/src_common/ieee/coq/Finterval.v
index 333327025..67d8b7261 100644
--- a/src_common/ieee/coq/Finterval.v
+++ b/src_common/ieee/coq/Finterval.v
@@ -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
diff --git a/src_common/ieee/coq/Futils.v b/src_common/ieee/coq/Futils.v
index d7e87ca61..40ce8d3fe 100644
--- a/src_common/ieee/coq/Futils.v
+++ b/src_common/ieee/coq/Futils.v
@@ -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
diff --git a/src_common/ieee/coq/Rextended.v b/src_common/ieee/coq/Rextended.v
index ee50bf208..b93e3aedb 100644
--- a/src_common/ieee/coq/Rextended.v
+++ b/src_common/ieee/coq/Rextended.v
@@ -1,6 +1,10 @@
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}.
--
GitLab