Library Interval.Interval.Float
This file is part of the Coq.Interval library for proving bounds of
real-valued expressions in Coq: https://coqinterval.gitlabpages.inria.fr/
Copyright (C) 2007-2016, Inria
This library is governed by the CeCILL-C license under French law and
abiding by the rules of distribution of free software. You can use,
modify and/or redistribute the library under the terms of the CeCILL-C
license as circulated by CEA, CNRS and Inria at the following URL:
http://www.cecill.info/
As a counterpart to the access to the source code and rights to copy,
modify and redistribute granted by the license, users are provided
only with a limited warranty and the library's author, the holder of
the economic rights, and the successive licensors have only limited
liability. See the COPYING file for more details.
From Coq Require Import Bool Reals Psatz.
From Flocq Require Import Raux.
Require Import Stdlib.
Require Import Xreal.
Require Import Basic.
Require Import Sig.
Require Import Interval.
Definition output_bnd (fmt upp : bool) radix (s : bool) m e :=
let m := if s then Zneg m else Zpos m in
match e with
| 0%Z ⇒ BInteger m
| Zpos p ⇒ BInteger (m × Zaux.Zfast_pow_pos (Zaux.radix_val radix) p)
| Zneg p ⇒
if andb fmt (Zeq_bool (Zaux.radix_val radix) 2) then
let e' := Z.to_pos (Zpos p × 3 / 10) in
let m' := Z.mul m (Zaux.Zfast_pow_pos 5 e') in
let m'' := Z.div_eucl m' (Z.pow 2 (Zpos p - Zpos e')) in
let u := if upp then if Zeq_bool (snd m'') 0 then 0%Z else 1%Z else 0%Z in
let d := Z.to_pos (Zaux.Zfast_pow_pos 10 e') in
BDecimal (QArith_base.Qmake (fst m'' + u) d)
else
BFraction m (Zaux.Zfast_pow_pos (Zaux.radix_val radix) p)
end.
Theorem output_bnd_correct :
∀ fmt radix s m e,
(Interval.convert_bound (output_bnd fmt false radix s m e) ≤ FtoR radix s m e)%R ∧
(FtoR radix s m e ≤ Interval.convert_bound (output_bnd fmt true radix s m e))%R.
Inductive f_interval (A : Type) : Type :=
| Inan : f_interval A
| Ibnd (l u : A) : f_interval A.
Arguments Inan {A}.
Arguments Ibnd {A} _ _.
Definition le_lower' x y :=
match x with
| Xnan ⇒ True
| Xreal xr ⇒
match y with
| Xnan ⇒ False
| Xreal yr ⇒ Rle xr yr
end
end.
Module FloatInterval (F'' : FloatOps with Definition sensible_format := true) <: IntervalBasicOps with Module F := F''.
Module F := F''.
Module F' := FloatExt F.
Definition c1 := F.fromZ 1.
Definition cm1 := F.fromZ (-1).
Definition c2 := F.fromZ 2.
Definition p52 := F.PtoP 52.
Definition type := f_interval F.type.
Definition bound_type := F.type.
Definition precision := F.precision.
Definition valid_lb x := F.valid_lb x = true.
Definition valid_ub x := F.valid_ub x = true.
Definition nan := F.nan.
Definition convert_bound := F.toX.
Definition convert (xi : type) :=
match xi with
| Inan ⇒ Interval.Inan
| Ibnd l u ⇒
if (F.valid_lb l && F.valid_ub u)%bool then Interval.Ibnd (F.toX l) (F.toX u)
else Interval.Ibnd (Xreal 1) (Xreal 0)
end.
Definition nai : type := @Inan F.type.
Definition bnd l u : type := Ibnd l u.
Definition zero : type := Ibnd F.zero F.zero.
Definition empty : type := Ibnd c1 F.zero.
Definition real (xi : type) :=
match xi with
| Inan ⇒ false
| Ibnd _ _ ⇒ true
end.
Definition singleton b :=
if andb (F.valid_lb b) (F.valid_ub b) then @Ibnd F.type b b
else @Inan F.type.
Lemma valid_lb_real :
∀ b, F.toX b = Xreal (proj_val (F.toX b)) → F.valid_lb b = true.
Lemma valid_ub_real :
∀ b, F.toX b = Xreal (proj_val (F.toX b)) → F.valid_ub b = true.
Lemma bnd_correct :
∀ l u, valid_lb l → valid_ub u →
convert (bnd l u) = Interval.Ibnd (F.toX l) (F.toX u).
Lemma singleton_correct :
∀ b,
contains (convert (singleton b)) (Xreal (proj_val (convert_bound b))).
Lemma nai_correct :
convert nai = Interval.Inan.
Lemma zero_correct :
convert zero = Interval.Ibnd (Xreal 0) (Xreal 0).
Lemma empty_correct :
∀ x, contains (convert empty) x → False.
Lemma real_correct :
∀ xi, real xi = match convert xi with Interval.Inan ⇒ false | _ ⇒ true end.
Definition is_empty xi :=
match xi with
| Ibnd xl xu ⇒
match F.cmp xl xu with
| Xgt ⇒ true
| _ ⇒ false
end
| _ ⇒ false
end.
Definition bounded xi :=
match xi with
| Ibnd xl xu ⇒ F.real xl && F.real xu
| _ ⇒ false
end.
Definition lower_bounded xi :=
match xi with
| Ibnd xl _ ⇒ F.real xl
| _ ⇒ false
end.
Definition upper_bounded xi :=
match xi with
| Ibnd _ xu ⇒ F.real xu
| _ ⇒ false
end.
Definition output (fmt : bool) xi :=
match xi with
| Ibnd xl xu ⇒
match F.toF xl, F.toF xu with
| Float sl ml el, Float su mu eu ⇒
(Some (output_bnd fmt false F.radix sl ml el), Some (output_bnd fmt true F.radix su mu eu))
| Fzero, Float su mu eu ⇒
(Some (BInteger 0), Some (output_bnd fmt true F.radix su mu eu))
| Float sl ml el, Fzero ⇒
(Some (output_bnd fmt false F.radix sl ml el), Some (BInteger 0))
| Fzero, Fzero ⇒ (Some (BInteger 0), Some (BInteger 0))
| Fzero, Basic.Fnan ⇒ (Some (BInteger 0), None)
| Basic.Fnan, Fzero ⇒ (None, Some (BInteger 0))
| Basic.Fnan, Float su mu eu ⇒
(None, Some (output_bnd fmt true F.radix su mu eu))
| Float sl ml el, Basic.Fnan ⇒
(Some (output_bnd fmt false F.radix sl ml el), None)
| Basic.Fnan, Basic.Fnan ⇒ (None, None)
end
| Inan ⇒ (None, None)
end.
Definition subset xi yi :=
if is_empty xi then true else
match xi, yi with
| Ibnd xl xu, Ibnd yl yu ⇒
match F.cmp xl yl with
| Xund ⇒
match F.classify yl with
| Fnan | Fminfty ⇒ true
| Freal | Fpinfty ⇒ false
end
| Xlt ⇒ false
| _ ⇒ true
end &&
match F.cmp xu yu with
| Xund ⇒
match F.classify yu with
| Fnan | Fpinfty ⇒ true
| Freal | Fminfty ⇒ false
end
| Xgt ⇒ false
| _ ⇒ true
end
| _, Inan ⇒ true
| Inan, Ibnd _ _ ⇒ false
end.
Definition wider prec xi yi :=
match yi, xi with
| Inan, _ ⇒ false
| Ibnd yl yu, Inan ⇒ true
| Ibnd yl yu, Ibnd xl xu ⇒
let yw := F.sub_UP prec yu yl in
if F.real yw then
match F'.cmp (F.sub_UP prec xu xl) yw with
| Xlt | Xeq ⇒ false
| _ ⇒ true
end
else false
end.
Definition join xi yi :=
if is_empty xi then yi else
if is_empty yi then xi else
match xi, yi with
| Ibnd xl xu, Ibnd yl yu ⇒
Ibnd (F.min xl yl) (F.max xu yu)
| _, _ ⇒ Inan
end.
Definition meet xi yi :=
if is_empty xi then xi else
if is_empty yi then yi else
match xi, yi with
| Ibnd xl xu, Ibnd yl yu ⇒
let l :=
match F.is_nan xl, F.is_nan yl with
| true, _ ⇒ yl
| false, true ⇒ xl
| false, false ⇒ F.max xl yl
end in
let u :=
match F.is_nan xu, F.is_nan yu with
| true, _ ⇒ yu
| false, true ⇒ xu
| false, false ⇒ F.min xu yu
end in
Ibnd l u
| Inan, _ ⇒ yi
| _, Inan ⇒ xi
end.
Definition mask xi yi : type :=
match yi with
| Inan ⇒ yi
| _ ⇒ xi
end.
Definition lower_extent xi :=
match xi with
| Ibnd _ xu ⇒ Ibnd F.nan xu
| _ ⇒ Inan
end.
Definition upper_extent xi :=
match xi with
| Ibnd xl _ ⇒ Ibnd xl F.nan
| _ ⇒ Inan
end.
Definition lower_complement xi :=
match xi with
| Ibnd xl _ ⇒ if F.real xl then Ibnd F.nan xl else empty
| Inan ⇒ empty
end.
Definition upper_complement xi :=
match xi with
| Ibnd _ xu ⇒ if F.real xu then Ibnd xu F.nan else empty
| Inan ⇒ empty
end.
Definition whole := Ibnd F.nan F.nan.
Definition lower xi :=
match xi with
| Ibnd xl _ ⇒ xl
| _ ⇒ F.nan
end.
Definition upper xi :=
match xi with
| Ibnd _ xu ⇒ xu
| _ ⇒ F.nan
end.
Definition fromZ_small n :=
let f := F.fromZ n in Ibnd f f.
Definition fromZ prec n :=
Ibnd (F.fromZ_DN prec n) (F.fromZ_UP prec n).
Definition midpoint xi :=
match xi with
| Inan ⇒ F.zero
| Ibnd xl xu ⇒
match F.real xl, F.real xu with
| false, false ⇒ F.zero
| true, false ⇒
match F.cmp xl F.zero with
| Xund | Xlt ⇒ F.zero
| Xeq ⇒ c1
| Xgt ⇒ let m := F.mul_UP p52 xl c2 in if F.real m then m else xl
end
| false, true ⇒
match F.cmp xu F.zero with
| Xund | Xgt ⇒ F.zero
| Xeq ⇒ cm1
| Xlt ⇒ let m := F.mul_DN p52 xu c2 in if F.real m then m else xu
end
| true, true ⇒ F.midpoint xl xu
end
end.
Definition bisect xi :=
match xi with
| Inan ⇒ (Inan, Inan)
| Ibnd xl xu ⇒
let m := midpoint xi in (Ibnd xl m, Ibnd m xu)
end.
Definition extension f fi := ∀ b x,
contains (convert b) x → contains (convert (fi b)) (f x).
Definition extension_2 f fi := ∀ ix iy x y,
contains (convert ix) x →
contains (convert iy) y →
contains (convert (fi ix iy)) (f x y).
Definition sign_large_ xl xu :=
match F.cmp xl F.zero, F.cmp xu F.zero with
| Xeq, Xeq ⇒ Xeq
| _, Xlt ⇒ Xlt
| _, Xeq ⇒ Xlt
| Xgt, _ ⇒ Xgt
| Xeq, _ ⇒ Xgt
| _, _ ⇒ Xund
end.
Definition sign_large xi :=
match xi with
| Ibnd xl xu ⇒ sign_large_ xl xu
| Inan ⇒ Xund
end.
Definition sign_strict_ xl xu :=
match F.cmp xl F.zero, F.cmp xu F.zero with
| Xeq, Xeq ⇒ Xeq
| _, Xlt ⇒ Xlt
| Xgt, _ ⇒ Xgt
| _, _ ⇒ Xund
end.
Definition sign_strict xi :=
match xi with
| Ibnd xl xu ⇒ sign_strict_ xl xu
| Inan ⇒ Xund
end.
Definition neg xi :=
match xi with
| Ibnd xl xu ⇒ Ibnd (F.neg xu) (F.neg xl)
| Inan ⇒ Inan
end.
Definition abs xi :=
match xi with
| Ibnd xl xu ⇒
match sign_large_ xl xu with
| Xgt ⇒ xi
| Xeq ⇒ Ibnd F.zero F.zero
| Xlt ⇒ Ibnd (F.neg xu) (F.neg xl)
| Xund ⇒ Ibnd F.zero (F.max (F.neg xl) xu)
end
| Inan ⇒ Inan
end.
Definition mul2 prec xi :=
match xi with
| Ibnd xl xu ⇒
Ibnd (F.mul_DN prec xl c2) (F.mul_UP prec xu c2)
| Inan ⇒ Inan
end.
Definition sqrt prec xi :=
match xi with
| Ibnd xl xu ⇒
match F.cmp xl F.zero with
| Xgt ⇒ Ibnd (F.sqrt_DN prec xl) (F.sqrt_UP prec xu)
| _ ⇒ Ibnd F.zero (F.sqrt_UP prec xu)
end
| Inan ⇒ Inan
end.
Definition add prec xi yi :=
match xi, yi with
| Ibnd xl xu, Ibnd yl yu ⇒
Ibnd (F.add_DN prec xl yl) (F.add_UP prec xu yu)
| _, _ ⇒ Inan
end.
Definition sub prec xi yi :=
match xi, yi with
| Ibnd xl xu, Ibnd yl yu ⇒
Ibnd (F.sub_DN prec xl yu) (F.sub_UP prec xu yl)
| _, _ ⇒ Inan
end.
Definition cancel_add prec xi yi :=
match xi, yi with
| Ibnd xl xu, Ibnd yl yu ⇒
Ibnd (F.sub_DN prec xl yl) (F.sub_UP prec xu yu)
| _, _ ⇒ Inan
end.
Definition cancel_sub prec xi yi :=
match xi, yi with
| Ibnd xl xu, Ibnd yl yu ⇒
Ibnd (F.add_DN prec xl yu) (F.add_UP prec xu yl)
| _, _ ⇒ Inan
end.
Definition mul_mixed prec xi y :=
match xi with
| Ibnd xl xu ⇒
if F.real y then
match F.cmp y F.zero with
| Xlt ⇒ Ibnd (F.mul_DN prec xu y) (F.mul_UP prec xl y)
| Xeq ⇒ Ibnd F.zero F.zero
| Xgt ⇒ Ibnd (F.mul_DN prec xl y) (F.mul_UP prec xu y)
| Xund ⇒ Inan
end
else Inan
| Inan ⇒ Inan
end.
Definition div_mixed_r prec xi y :=
match xi with
| Ibnd xl xu ⇒
if F.real y then
match F.cmp y F.zero with
| Xlt ⇒ Ibnd (F.div_DN prec xu y) (F.div_UP prec xl y)
| Xgt ⇒ Ibnd (F.div_DN prec xl y) (F.div_UP prec xu y)
| _ ⇒ Inan
end
else Inan
| Inan ⇒ Inan
end.
Definition sqr prec xi :=
match xi with
| Ibnd xl xu ⇒
match sign_large_ xl xu with
| Xund ⇒
let xm := F.max (F.abs xl) xu in
Ibnd F.zero (F.mul_UP prec xm xm)
| Xeq ⇒ Ibnd F.zero F.zero
| Xlt ⇒
let lb := F.mul_DN prec xu xu in
match F.cmp lb F.zero with
| Xgt ⇒ Ibnd lb (F.mul_UP prec xl xl)
| _ ⇒ Ibnd F.zero (F.mul_UP prec xl xl)
end
| Xgt ⇒
let lb := F.mul_DN prec xl xl in
match F.cmp lb F.zero with
| Xgt ⇒ Ibnd lb (F.mul_UP prec xu xu)
| _ ⇒ Ibnd F.zero (F.mul_UP prec xu xu)
end
end
| _ ⇒ Inan
end.
Definition mul prec xi yi :=
match xi, yi with
| Ibnd xl xu, Ibnd yl yu ⇒
match sign_large_ xl xu, sign_large_ yl yu with
| Xeq, _ ⇒ Ibnd F.zero F.zero
| _, Xeq ⇒ Ibnd F.zero F.zero
| Xgt, Xgt ⇒ Ibnd (F.mul_DN prec xl yl) (F.mul_UP prec xu yu)
| Xlt, Xlt ⇒ Ibnd (F.mul_DN prec xu yu) (F.mul_UP prec xl yl)
| Xgt, Xlt ⇒ Ibnd (F.mul_DN prec xu yl) (F.mul_UP prec xl yu)
| Xlt, Xgt ⇒ Ibnd (F.mul_DN prec xl yu) (F.mul_UP prec xu yl)
| Xgt, Xund ⇒ Ibnd (F.mul_DN prec xu yl) (F.mul_UP prec xu yu)
| Xlt, Xund ⇒ Ibnd (F.mul_DN prec xl yu) (F.mul_UP prec xl yl)
| Xund, Xgt ⇒ Ibnd (F.mul_DN prec xl yu) (F.mul_UP prec xu yu)
| Xund, Xlt ⇒ Ibnd (F.mul_DN prec xu yl) (F.mul_UP prec xl yl)
| Xund, Xund ⇒ Ibnd (F.min (F.mul_DN prec xl yu) (F.mul_DN prec xu yl))
(F.max (F.mul_UP prec xl yl) (F.mul_UP prec xu yu))
end
| _, _ ⇒ Inan
end.
Definition Fdivz_UP prec x y :=
if F.real y then F.div_UP prec x y else F.zero.
Definition Fdivz_DN prec x y :=
if F.real y then F.div_DN prec x y else F.zero.
Definition inv prec xi :=
match xi with
| Ibnd xl xu ⇒
match sign_strict_ xl xu with
| Xund ⇒ Inan
| Xeq ⇒ Inan
| _ ⇒
Ibnd (Fdivz_DN prec c1 xu) (Fdivz_UP prec c1 xl)
end
| _ ⇒ Inan
end.
Definition invnz prec xi :=
match xi with
| Ibnd xl xu ⇒
match sign_strict_ xl xu with
| Xund ⇒
match sign_large_ xl xu with
| Xund ⇒ Inan
| Xeq ⇒ Inan
| Xlt ⇒ Ibnd F.nan (Fdivz_UP prec c1 xl)
| Xgt ⇒ Ibnd (Fdivz_DN prec c1 xu) F.nan
end
| Xeq ⇒ Inan
| _ ⇒
Ibnd (Fdivz_DN prec c1 xu) (Fdivz_UP prec c1 xl)
end
| _ ⇒ Inan
end.
Definition div prec xi yi :=
match xi, yi with
| Ibnd xl xu, Ibnd yl yu ⇒
match sign_strict_ xl xu, sign_strict_ yl yu with
| _, Xund ⇒ Inan
| _, Xeq ⇒ Inan
| Xeq, _ ⇒ Ibnd F.zero F.zero
| Xgt, Xgt ⇒ Ibnd (Fdivz_DN prec xl yu) (F.div_UP prec xu yl)
| Xlt, Xlt ⇒ Ibnd (Fdivz_DN prec xu yl) (F.div_UP prec xl yu)
| Xgt, Xlt ⇒ Ibnd (F.div_DN prec xu yu) (Fdivz_UP prec xl yl)
| Xlt, Xgt ⇒ Ibnd (F.div_DN prec xl yl) (Fdivz_UP prec xu yu)
| Xund, Xgt ⇒ Ibnd (F.div_DN prec xl yl) (F.div_UP prec xu yl)
| Xund, Xlt ⇒ Ibnd (F.div_DN prec xu yu) (F.div_UP prec xl yu)
end
| _, _ ⇒ Inan
end.
Fixpoint Fpower_pos_UP prec x n :=
match n with
| xH ⇒ x
| xO p ⇒ Fpower_pos_UP prec (F.mul_UP prec x x) p
| xI p ⇒ F.mul_UP prec x (Fpower_pos_UP prec (F.mul_UP prec x x) p)
end.
Fixpoint Fpower_pos_DN prec x n :=
match n with
| xH ⇒ x
| xO p ⇒
let xx := F.mul_DN prec x x in
match F.cmp xx F.zero with
| Xgt ⇒ Fpower_pos_DN prec xx p
| Xeq | Xlt ⇒ F.zero
| Xund ⇒ F.nan
end
| xI p ⇒
let xx := F.mul_DN prec x x in
match F.cmp xx F.zero with
| Xgt ⇒ F.mul_DN prec x (Fpower_pos_DN prec xx p)
| Xeq | Xlt ⇒ F.zero
| Xund ⇒ F.nan
end
end.
Definition power_pos prec xi n :=
match xi with
| Ibnd xl xu ⇒
match sign_large_ xl xu with
| Xund ⇒
match n with
| xH ⇒ xi
| xO _ ⇒
let xm := F.max (F.abs xl) xu in
Ibnd F.zero (Fpower_pos_UP prec xm n)
| xI _ ⇒ Ibnd (F.neg (Fpower_pos_UP prec (F.abs xl) n)) (Fpower_pos_UP prec xu n)
end
| Xeq ⇒ Ibnd F.zero F.zero
| Xlt ⇒
match n with
| xH ⇒ xi
| xO _ ⇒ Ibnd (Fpower_pos_DN prec (F.abs xu) n) (Fpower_pos_UP prec (F.abs xl) n)
| xI _ ⇒ Ibnd (F.neg (Fpower_pos_UP prec (F.abs xl) n)) (F.neg (Fpower_pos_DN prec (F.abs xu) n))
end
| Xgt ⇒ Ibnd (Fpower_pos_DN prec xl n) (Fpower_pos_UP prec xu n)
end
| _ ⇒ Inan
end.
Definition power_int prec xi n :=
match n with
| Zpos p ⇒ power_pos prec xi p
| Z0 ⇒ match xi with Inan ⇒ Inan | _ ⇒ Ibnd c1 c1 end
| Zneg p ⇒ inv prec (power_pos prec xi p)
end.
Definition nearbyint mode xi :=
match xi with
| Inan ⇒ Inan
| Ibnd xl xu ⇒ Ibnd (F.nearbyint_DN mode xl) (F.nearbyint_UP mode xu)
end.
Definition error_aux prec mode e :=
let e :=
match mode with
| rnd_NE ⇒ Z.pred e
| _ ⇒ e
end in
let err := F.pow2_UP prec (F.ZtoS e) in
match mode with
| rnd_NE ⇒ Ibnd (F.neg err) err
| rnd_UP ⇒ Ibnd F.zero err
| rnd_DN ⇒ Ibnd (F.neg err) F.zero
| rnd_ZR ⇒ Ibnd (F.neg err) err
end.
Definition error_fix prec mode emin (xi : type) :=
match xi with
| Inan ⇒ Inan
| Ibnd xl xu ⇒
error_aux prec mode emin
end.
Definition error_flt prec mode emin p xi :=
match xi with
| Inan ⇒ Inan
| Ibnd xl xu ⇒
let xu' := F.max (F.neg xl) xu in
if andb (F.real xu') (Z.eqb (Zaux.radix_val F.radix) 2) then
let e := FLT.FLT_exp emin (Z.pos p) (F.StoZ (F.mag xu')) in
error_aux prec mode e
else
Inan
end.
Ltac xreal_tac v :=
let X := fresh "X" in
case_eq (F.toX v) ;
[ intros X ; try exact I
| let r := fresh "r" in
intros r X ; try rewrite X in × ].
Ltac xreal_tac2 :=
match goal with
| H: F.toX ?v = Xreal _ |- context [F.toX ?v] ⇒
rewrite H
| |- context [F.toX ?v] ⇒ xreal_tac v
end.
Ltac xreal_tac3 v :=
match goal with
| H: F.toX v = Xreal _ |- _ ⇒ rewrite H
| H: F.toX v = Xnan |- _ ⇒ rewrite H
| _ ⇒ xreal_tac v
end.
Ltac bound_tac :=
unfold Xround, Xbind ;
match goal with
| |- (round ?r rnd_DN ?p ?v ≤ ?w)%R ⇒
apply Rle_trans with (1 := proj1 (proj2 (Generic_fmt.round_DN_pt F.radix (FLX.FLX_exp (Zpos p)) v)))
| |- (?w ≤ round ?r_UP ?p ?v)%R ⇒
apply Rle_trans with (2 := proj1 (proj2 (Generic_fmt.round_UP_pt F.radix (FLX.FLX_exp (Zpos p)) v)))
end.
Lemma is_empty_correct :
∀ xi x,
contains (convert xi) x →
is_empty xi = true →
False.
Lemma lower_correct :
∀ xi : type,
not_empty (convert xi) →
F.toX (lower xi) = Xlower (convert xi).
Lemma valid_lb_lower :
∀ xi : type,
not_empty (convert xi) →
valid_lb (lower xi).
Lemma upper_correct :
∀ xi : type,
not_empty (convert xi) →
F.toX (upper xi) = Xupper (convert xi).
Lemma valid_ub_upper :
∀ xi : type,
not_empty (convert xi) →
valid_ub (upper xi).
Theorem output_correct :
∀ fmt xi x, contains (convert xi) (Xreal x) → contains_output (output fmt xi) x.
Theorem subset_correct :
∀ xi yi v,
contains (convert xi) v →
subset xi yi = true →
contains (convert yi) v.
Lemma join_correct :
∀ xi yi v,
contains (convert xi) v ∨ contains (convert yi) v →
contains (convert (join xi yi)) v.
Theorem meet_correct :
∀ xi yi v,
contains (convert xi) v → contains (convert yi) v →
contains (convert (meet xi yi)) v.
Theorem meet_correct' :
∀ xi yi v,
contains (convert (meet xi yi)) v →
contains (convert xi) v ∧ contains (convert yi) v.
Definition bounded_prop xi :=
not_empty (convert xi) →
convert xi = Interval.Ibnd (F.toX (lower xi)) (F.toX (upper xi)).
Theorem lower_bounded_correct :
∀ xi,
lower_bounded xi = true →
F.toX (lower xi) = Xreal (proj_val (F.toX (lower xi))) ∧
bounded_prop xi.
Theorem upper_bounded_correct :
∀ xi,
upper_bounded xi = true →
F.toX (upper xi) = Xreal (proj_val (F.toX (upper xi))) ∧
bounded_prop xi.
Theorem bounded_correct :
∀ xi,
bounded xi = true →
lower_bounded xi = true ∧ upper_bounded xi = true.
Theorem lower_extent_correct :
∀ xi x y,
contains (convert xi) (Xreal y) →
(x ≤ y)%R →
contains (convert (lower_extent xi)) (Xreal x).
Theorem upper_extent_correct :
∀ xi x y,
contains (convert xi) (Xreal y) →
(y ≤ x)%R →
contains (convert (upper_extent xi)) (Xreal x).
Theorem lower_complement_correct :
∀ xi x y,
contains (convert xi) (Xreal x) →
contains (convert (lower_complement xi)) (Xreal y) →
(y ≤ x)%R.
Theorem upper_complement_correct :
∀ xi x y,
contains (convert xi) (Xreal x) →
contains (convert (upper_complement xi)) (Xreal y) →
(x ≤ y)%R.
Theorem whole_correct :
∀ x,
contains (convert whole) (Xreal x).
Lemma sign_large_correct_ :
∀ xl xu x,
contains (convert (Ibnd xl xu)) (Xreal x) →
match sign_large_ xl xu with
| Xeq ⇒ x = 0%R ∧ F.toX xl = Xreal 0 ∧ F.toX xu = Xreal 0
| Xlt ⇒ (x ≤ 0)%R ∧ (match F.toX xl with Xreal rl ⇒ (rl ≤ 0)%R | _⇒ True end) ∧ (∃ ru, F.toX xu = Xreal ru ∧ (ru ≤ 0)%R)
| Xgt ⇒ (0 ≤ x)%R ∧ (match F.toX xu with Xreal ru ⇒ (0 ≤ ru)%R | _⇒ True end) ∧ (∃ rl, F.toX xl = Xreal rl ∧ (0 ≤ rl)%R)
| Xund ⇒
match F.toX xl with Xreal rl ⇒ (rl ≤ 0)%R | _⇒ True end ∧
match F.toX xu with Xreal ru ⇒ (0 ≤ ru)%R | _⇒ True end
end.
Theorem sign_large_correct :
∀ xi,
match sign_large xi with
| Xeq ⇒ ∀ x, contains (convert xi) x → x = Xreal 0
| Xlt ⇒ ∀ x, contains (convert xi) x → x = Xreal (proj_val x) ∧ Rle (proj_val x) 0
| Xgt ⇒ ∀ x, contains (convert xi) x → x = Xreal (proj_val x) ∧ Rle 0 (proj_val x)
| Xund ⇒ True
end.
Lemma sign_strict_correct_ :
∀ xl xu x,
contains (convert (Ibnd xl xu)) (Xreal x) →
match sign_strict_ xl xu with
| Xeq ⇒ x = 0%R ∧ F.toX xl = Xreal 0 ∧ F.toX xu = Xreal 0
| Xlt ⇒ (x < 0)%R ∧ (match F.toX xl with Xreal rl ⇒ (rl < 0)%R | _⇒ True end) ∧ (∃ ru, F.toX xu = Xreal ru ∧ (ru < 0)%R)
| Xgt ⇒ (0 < x)%R ∧ (match F.toX xu with Xreal ru ⇒ (0 < ru)%R | _⇒ True end) ∧ (∃ rl, F.toX xl = Xreal rl ∧ (0 < rl)%R)
| Xund ⇒
match F.toX xl with Xreal rl ⇒ (rl ≤ 0)%R | _⇒ True end ∧
match F.toX xu with Xreal ru ⇒ (0 ≤ ru)%R | _⇒ True end
end.
Theorem sign_strict_correct :
∀ xi,
match sign_strict xi with
| Xeq ⇒ ∀ x, contains (convert xi) x → x = Xreal 0
| Xlt ⇒ ∀ x, contains (convert xi) x → x = Xreal (proj_val x) ∧ Rlt (proj_val x) 0
| Xgt ⇒ ∀ x, contains (convert xi) x → x = Xreal (proj_val x) ∧ Rlt 0 (proj_val x)
| Xund ⇒ True
end.
Theorem fromZ_small_correct :
∀ v,
(Z.abs v ≤ 256)%Z →
contains (convert (fromZ_small v)) (Xreal (IZR v)).
Theorem fromZ_correct :
∀ prec v,
contains (convert (fromZ prec v)) (Xreal (IZR v)).
Theorem midpoint_correct :
∀ xi,
not_empty (convert xi) →
F.toX (midpoint xi) = Xreal (proj_val (F.toX (midpoint xi))) ∧
contains (convert xi) (F.toX (midpoint xi)).
Theorem bisect_correct :
∀ xi x,
contains (convert xi) x →
contains (convert (fst (bisect xi))) x ∨ contains (convert (snd (bisect xi))) x.
Theorem mask_correct :
extension_2 Xmask mask.
Theorem mask_correct' :
∀ xi yi x,
contains (convert xi) x →
contains (convert (mask xi yi)) x.
Definition propagate_l fi :=
∀ xi yi : type, convert xi = Interval.Inan →
convert (fi xi yi) = Interval.Inan.
Definition propagate_r fi :=
∀ xi yi : type, convert yi = Interval.Inan →
convert (fi xi yi) = Interval.Inan.
Theorem neg_correct :
extension Xneg neg.
Theorem neg_correct' :
∀ xi x,
contains (convert (neg xi)) (Xneg x) →
contains (convert xi) x.
Theorem abs_correct :
extension Xabs abs.
Theorem abs_ge_0 :
∀ xi, not_empty (convert xi) → convert xi ≠ Interval.Inan →
le_lower' (Xreal 0) (F.toX (lower (abs xi))).
Theorem abs_ge_0' :
∀ xi, not_empty (convert xi) →
(0 ≤ proj_val (F.toX (lower (abs xi))))%R.
Lemma abs_correct_aux :
∀ xl xu x, contains (convert (Ibnd xl xu)) (Xreal x) →
let xm := F.max (F.neg xl) xu in le_upper (Xreal (Rabs x)) (F.toX xm).
Theorem mul2_correct :
∀ prec xi x,
contains (convert xi) x →
contains (convert (mul2 prec xi)) (Xmul x (Xreal 2)).
Theorem add_correct :
∀ prec,
extension_2 Xadd (add prec).
Theorem sub_correct :
∀ prec,
extension_2 Xsub (sub prec).
Theorem sqrt_correct :
∀ prec, extension Xsqrt (sqrt prec).
Ltac clear_complex_aux :=
match goal with
| H: Rle _ _ |- _ ⇒
generalize H ; clear H ; try clear_complex_aux
| H: (Rle _ _) ∧ _ |- _ ⇒
generalize (proj1 H) ;
destruct H as (_, H) ;
try clear_complex_aux
| H: Rlt _ _ |- _ ⇒
generalize H ; clear H ; try clear_complex_aux
| H: (Rlt _ _) ∧ _ |- _ ⇒
generalize (proj1 H) ;
destruct H as (_, H) ;
try clear_complex_aux
| H: ex (fun r : R ⇒ _ ∧ _) |- _ ⇒
let a := fresh "a" in
let K := fresh in
destruct H as (a, (K, H)) ;
injection K ; clear K ; intro K ;
rewrite <- K in H ;
clear K a ; try clear_complex_aux
| H: _ ∧ _ |- _ ⇒
destruct H as (_, H) ;
try clear_complex_aux
| H: _ |- _ ⇒
clear H ; try clear_complex_aux
end.
Ltac clear_complex :=
clear_complex_aux ; clear ; intros.
Local Hint Resolve Rlt_le : mulauto.
Local Hint Resolve Rle_trans : mulauto.
Local Hint Resolve Rmult_le_compat_l : mulauto.
Local Hint Resolve Rmult_le_compat_r : mulauto.
Local Hint Resolve Rmult_le_compat_neg_l : mulauto.
Local Hint Resolve Rmult_le_compat_neg_r : mulauto.
Theorem mul_mixed_correct :
∀ prec yf,
extension (fun x ⇒ Xmul x (F.toX yf)) (fun xi ⇒ mul_mixed prec xi yf).
Theorem mul_correct :
∀ prec,
extension_2 Xmul (mul prec).
Ltac simpl_is_zero :=
let X := fresh "X" in
match goal with
| H: Rlt ?v 0 |- context [is_zero ?v] ⇒
destruct (is_zero_spec v) as [X|X] ;
[ rewrite X in H ; elim (Rlt_irrefl _ H) | idtac ]
| H: Rlt 0 ?v |- context [is_zero ?v] ⇒
destruct (is_zero_spec v) as [X|X] ;
[ rewrite X in H ; elim (Rlt_irrefl _ H) | idtac ]
| H: Rlt ?v 0 ∧ _ |- context [is_zero ?v] ⇒
destruct (is_zero_spec v) as [X|X] ;
[ rewrite X in H ; elim (Rlt_irrefl _ (proj1 H)) | idtac ]
| H: _ ∧ (Rlt ?v 0 ∧ _) |- context [is_zero ?v] ⇒
destruct (is_zero_spec v) as [X|X] ;
[ rewrite X in H ; elim (Rlt_irrefl _ (proj1 (proj2 H))) | idtac ]
| H: Rlt 0 ?v ∧ _ |- context [is_zero ?v] ⇒
destruct (is_zero_spec v) as [X|X] ;
[ rewrite X in H ; elim (Rlt_irrefl _ (proj1 H)) | idtac ]
| H: _ ∧ (Rlt 0 ?v ∧ _) |- context [is_zero ?v] ⇒
destruct (is_zero_spec v) as [X|X] ;
[ rewrite X in H ; elim (Rlt_irrefl _ (proj1 (proj2 H))) | idtac ]
end.
Local Hint Resolve Rinv_lt_0_compat : mulauto.
Local Hint Resolve Rinv_0_lt_compat : mulauto.
Local Hint Resolve Rle_Rinv_pos : mulauto.
Local Hint Resolve Rle_Rinv_neg : mulauto.
Local Hint Resolve Rlt_le : mulauto2.
Local Hint Resolve Rinv_lt_0_compat : mulauto2.
Local Hint Resolve Rinv_0_lt_compat : mulauto2.
Local Hint Resolve Rmult_le_pos_pos : mulauto2.
Local Hint Resolve Rmult_le_neg_pos : mulauto2.
Local Hint Resolve Rmult_le_pos_neg : mulauto2.
Local Hint Resolve Rmult_le_neg_neg : mulauto2.
Theorem div_mixed_r_correct :
∀ prec yf,
extension (fun x ⇒ Xdiv x (F.toX yf)) (fun xi ⇒ div_mixed_r prec xi yf).
Theorem div_correct :
∀ prec,
extension_2 Xdiv (div prec).
Theorem inv_correct :
∀ prec,
extension Xinv (inv prec).
Theorem invnz_correct :
∀ prec xi x,
x ≠ Xreal 0 → contains (convert xi) x → contains (convert (invnz prec xi)) (Xinv x).
Theorem sqr_correct :
∀ prec,
extension Xsqr (sqr prec).
Lemma Fpower_pos_up_correct :
∀ prec x n,
F.valid_ub x = true →
le_upper (Xreal 0) (F.toX x) →
F.valid_ub (Fpower_pos_UP prec x n) = true
∧ le_upper (Xpower_int (F.toX x) (Zpos n)) (F.toX (Fpower_pos_UP prec x n)).
Lemma Fpower_pos_dn_correct :
∀ prec x n,
le_lower' (Xreal 0) (F.toX x) →
F.valid_lb (Fpower_pos_DN prec x n) = true
∧ le_lower' (F.toX (Fpower_pos_DN prec x n)) (Xpower_int (F.toX x) (Zpos n)).
Theorem power_pos_correct :
∀ prec n,
extension (fun x ⇒ Xpower_int x (Zpos n)) (fun x ⇒ power_pos prec x n).
Theorem power_int_correct :
∀ prec n,
extension (fun x ⇒ Xpower_int x n) (fun x ⇒ power_int prec x n).
Lemma mask_propagate_l : propagate_l mask.
Lemma mask_propagate_r : propagate_r mask.
Lemma add_propagate_l : ∀ prec, propagate_l (add prec).
Lemma sub_propagate_l : ∀ prec, propagate_l (sub prec).
Lemma mul_propagate_l : ∀ prec, propagate_l (mul prec).
Lemma div_propagate_l : ∀ prec, propagate_l (div prec).
Lemma add_propagate_r : ∀ prec, propagate_r (add prec).
Lemma sub_propagate_r : ∀ prec, propagate_r (sub prec).
Lemma mul_propagate_r : ∀ prec, propagate_r (mul prec).
Lemma div_propagate_r : ∀ prec, propagate_r (div prec).
Lemma nearbyint_correct :
∀ mode, extension (Xnearbyint mode) (nearbyint mode).
Lemma error_aux_correct_aux :
∀ prec mode fexp e x,
Generic_fmt.Valid_exp fexp →
(Ulp.ulp radix2 fexp x ≤ bpow radix2 e)%R →
contains (convert (error_aux prec mode e))
(Xreal (Generic_fmt.round radix2 fexp (rnd_of_mode mode) x - x)) ∧
contains (convert (error_aux prec mode e)) (Xreal 0).
Lemma error_fix_correct_aux :
∀ prec mode emin xi x,
contains (convert xi) x →
contains (convert (error_fix prec mode emin xi)) (Xerror_fix mode emin x) ∧
contains (convert (error_fix prec mode emin xi)) (Xreal 0).
Lemma error_fix_correct :
∀ prec mode emin, extension (Xerror_fix mode emin) (error_fix prec mode emin).
Lemma error_fix_contains_0 :
∀ prec mode emin x,
not_empty (convert x) → contains (convert (error_fix prec mode emin x)) (Xreal 0).
Lemma error_flt_correct_aux :
∀ prec mode emin p xi x,
contains (convert xi) x →
contains (convert (error_flt prec mode emin p xi)) (Xerror_flt mode emin p x) ∧
contains (convert (error_flt prec mode emin p xi)) (Xreal 0).
Lemma error_flt_correct :
∀ prec mode emin p, extension (Xerror_flt mode emin p) (error_flt prec mode emin p).
Lemma error_flt_contains_0 :
∀ prec mode emin p x,
not_empty (convert x) → contains (convert (error_flt prec mode emin p x)) (Xreal 0).
Definition valid_lb_nan := F'.valid_lb_nan.
Definition valid_ub_nan := F'.valid_ub_nan.
End FloatInterval.