Commit a90ca0c2 authored by BOLDO Sylvie's avatar BOLDO Sylvie

More comments (and used by coqdoc)

parent aac8298e
(*
(**
This file is part of the Flocq formalization of floating-point
arithmetic in Coq: http://flocq.gforge.inria.fr/
Copyright (C) 2010 Sylvie Boldo
#<br />#
Copyright (C) 2010 Guillaume Melquiond
This library is free software; you can redistribute it and/or
......@@ -16,6 +17,7 @@ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
*)
(** * To ease the import *)
Require Export Fcore_Raux.
Require Export Fcore_defs.
Require Export Fcore_float_prop.
......
(*
(**
This file is part of the Flocq formalization of floating-point
arithmetic in Coq: http://flocq.gforge.inria.fr/
Copyright (C) 2010 Sylvie Boldo
#<br />#
Copyright (C) 2010 Guillaume Melquiond
This library is free software; you can redistribute it and/or
......@@ -16,6 +17,7 @@ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
*)
(** * Fixed-point format *)
Require Import Fcore_Raux.
Require Import Fcore_defs.
Require Import Fcore_rnd.
......@@ -30,7 +32,7 @@ Notation bpow := (bpow beta).
Variable emin : Z.
(* fixed-point format *)
(* fixed-point format with exponent emin *)
Definition FIX_format (x : R) :=
exists f : float beta,
x = F2R f /\ (Fexp f = emin)%Z.
......@@ -40,6 +42,7 @@ Definition FIX_RoundingModeP (rnd : R -> R):=
Definition FIX_exp (e : Z) := emin.
(** Properties of the FIX format *)
Theorem FIX_exp_correct : valid_exp FIX_exp.
Proof.
intros k.
......
(*
(**
This file is part of the Flocq formalization of floating-point
arithmetic in Coq: http://flocq.gforge.inria.fr/
Copyright (C) 2010 Sylvie Boldo
#<br />#
Copyright (C) 2010 Guillaume Melquiond
This library is free software; you can redistribute it and/or
......@@ -16,6 +17,7 @@ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
*)
(** * Floating-point format with gradual underflow *)
Require Import Fcore_Raux.
Require Import Fcore_defs.
Require Import Fcore_rnd.
......@@ -44,6 +46,7 @@ Definition FLT_RoundingModeP (rnd : R -> R):=
Definition FLT_exp e := Zmax (e - prec) emin.
(** Properties of the FLT format *)
Theorem FLT_exp_correct : valid_exp FLT_exp.
Proof.
intros k.
......@@ -148,6 +151,7 @@ apply Rle_lt_trans with (1 := Hx).
apply He.
Qed.
(** Links between FLT and FLX *)
Theorem FLT_generic_format_FLX :
forall x : R,
(bpow (emin + prec - 1) <= Rabs x)%R ->
......@@ -200,7 +204,7 @@ apply bpow_gt_0.
Qed.
(** Links between FLT and FIX (underflow) *)
Theorem FLT_canonic_FIX :
forall x, x <> R0 ->
(Rabs x < bpow (emin + prec))%R ->
......@@ -261,6 +265,7 @@ apply iff_sym.
now apply FIX_format_generic.
Qed.
(** FLT is a nice format which is not FTZ and that allows a rounding to nearest, ties to even *)
Theorem FLT_not_FTZ :
not_FTZ_prop FLT_exp.
Proof.
......
(*
(**
This file is part of the Flocq formalization of floating-point
arithmetic in Coq: http://flocq.gforge.inria.fr/
Copyright (C) 2010 Sylvie Boldo
#<br />#
Copyright (C) 2010 Guillaume Melquiond
This library is free software; you can redistribute it and/or
......@@ -16,6 +17,7 @@ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
*)
(** * Floating-point format without underflow *)
Require Import Fcore_Raux.
Require Import Fcore_defs.
Require Import Fcore_rnd.
......@@ -43,6 +45,7 @@ Definition FLX_RoundingModeP (rnd : R -> R):=
Definition FLX_exp (e : Z) := (e - prec)%Z.
(** Properties of the FLX format *)
Theorem FLX_exp_correct : valid_exp FLX_exp.
Proof.
intros k.
......@@ -142,7 +145,7 @@ apply FLX_format_generic.
exact FLX_exp_correct.
Qed.
(* unbounded floating-point format with normal mantissas *)
(** unbounded floating-point format with normal mantissas *)
Definition FLXN_format (x : R) :=
exists f : float beta,
x = F2R f /\ (x <> R0 ->
......@@ -238,6 +241,7 @@ now apply <- FLX_format_FLXN.
exact FLX_exp_correct.
Qed.
(** FLX is a nice format which is not FTZ and that allows a rounding to nearest, ties to even *)
Theorem FLX_not_FTZ :
not_FTZ_prop FLX_exp.
Proof.
......
(*
(**
This file is part of the Flocq formalization of floating-point
arithmetic in Coq: http://flocq.gforge.inria.fr/
Copyright (C) 2010 Sylvie Boldo
#<br />#
Copyright (C) 2010 Guillaume Melquiond
This library is free software; you can redistribute it and/or
......@@ -16,6 +17,7 @@ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
*)
(** * Floating-point format with abrupt underflow *)
Require Import Fcore_Raux.
Require Import Fcore_defs.
Require Import Fcore_rnd.
......@@ -43,6 +45,7 @@ Definition FTZ_RoundingModeP (rnd : R -> R):=
Definition FTZ_exp e := if Zlt_bool (e - prec) emin then (emin + prec - 1)%Z else (e - prec)%Z.
(** Properties of the FTZ format *)
Theorem FTZ_exp_correct : valid_exp FTZ_exp.
Proof.
intros k.
......@@ -235,6 +238,7 @@ Qed.
Section FTZ_round.
(** Rounding with FTZ *)
Hypothesis rnd : Zround.
Definition Zrnd_FTZ x :=
......
(*
(**
This file is part of the Flocq formalization of floating-point
arithmetic in Coq: http://flocq.gforge.inria.fr/
Copyright (C) 2010 Sylvie Boldo
#<br />#
Copyright (C) 2010 Guillaume Melquiond
This library is free software; you can redistribute it and/or
......@@ -16,11 +17,13 @@ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
*)
(** * Missing definitions/lemmas *)
Require Export Reals.
Require Export ZArith.
Section Rmissing.
(** About R *)
Theorem Rle_0_minus :
forall x y, (x <= y)%R -> (0 <= y - x)%R.
Proof.
......@@ -296,6 +299,7 @@ End Rmissing.
Section Zmissing.
(** About Z *)
Theorem Zopp_le_cancel :
forall x y : Z,
(-y <= -x)%Z -> Zle x y.
......@@ -327,6 +331,7 @@ End Zmissing.
Section Z2R.
(** Z2R function (Z -> R) *)
Fixpoint P2R (p : positive) :=
match p with
| xH => 1%R
......@@ -505,6 +510,7 @@ End Z2R.
Section Zcompare.
(** Useful comparisons *)
Inductive Zeq_bool_prop (x y : Z) : bool -> Prop :=
| Zeq_bool_true : x = y -> Zeq_bool_prop x y true
| Zeq_bool_false : x <> y -> Zeq_bool_prop x y false.
......@@ -910,6 +916,7 @@ Qed.
End Req_bool.
Section Floor_Ceil.
(** Zfloor and Zceil *)
Definition Zfloor (x : R) := (up x - 1)%Z.
Theorem Zfloor_lb :
......@@ -1193,6 +1200,7 @@ End Floor_Ceil.
Section Even_Odd.
(** Zeven, used for rounding to nearest, ties to even *)
Definition Zeven (n : Z) :=
match n with
| Zpos (xO _) => true
......@@ -1287,6 +1295,7 @@ End Proof_Irrelevance.
Section pow.
(** The radix must be greater than 1 *)
Record radix := { radix_val :> Z ; radix_prop : Zle_bool 2 radix_val = true }.
Theorem radix_val_inj :
......@@ -1320,6 +1329,7 @@ easy.
now apply Zle_bool_imp_le.
Qed.
(** Well-used function called bpow for computing the power function #&beta;#^e *)
Definition bpow e :=
match e with
| Zpos p => Z2R (Zpower_pos r p)
......@@ -1559,6 +1569,7 @@ rewrite <- Ropp_mult_distr_l_reverse.
now rewrite <- Z2R_opp.
Qed.
(** Another well-used function for having the logarithm of a real number x to the base #&beta;# *)
Record ln_beta_prop x := {
ln_beta_val :> Z ;
_ : (x <> 0)%R -> (bpow (ln_beta_val - 1)%Z <= Rabs x < bpow ln_beta_val)%R
......
(*
(**
This file is part of the Flocq formalization of floating-point
arithmetic in Coq: http://flocq.gforge.inria.fr/
Copyright (C) 2010 Sylvie Boldo
#<br />#
Copyright (C) 2010 Guillaume Melquiond
This library is free software; you can redistribute it and/or
......@@ -16,10 +17,12 @@ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
*)
(** * Basic definitions: float and rounding property *)
Require Import Fcore_Raux.
Section Def.
(** Definition of a floating-point number *)
Record float (beta : radix) := Float { Fnum : Z ; Fexp : Z }.
Implicit Arguments Fnum [[beta]].
......@@ -30,6 +33,7 @@ Variable beta : radix.
Definition F2R (f : float beta) :=
(Z2R (Fnum f) * bpow beta (Fexp f))%R.
(** Requirements on a rounding mode property *)
Definition MonotoneP (rnd : R -> R) :=
forall x y : R,
(x <= y)%R -> (rnd x <= rnd y)%R.
......@@ -59,7 +63,7 @@ Implicit Arguments F2R [[beta]].
Section RND.
(* property of being a round toward -inf *)
(** property of being a round toward -inf *)
Definition Rnd_DN_pt (F : R -> Prop) (x f : R) :=
F f /\ (f <= x)%R /\
forall g : R, F g -> (g <= x)%R -> (g <= f)%R.
......@@ -67,7 +71,7 @@ Definition Rnd_DN_pt (F : R -> Prop) (x f : R) :=
Definition Rnd_DN (F : R -> Prop) (rnd : R -> R) :=
forall x : R, Rnd_DN_pt F x (rnd x).
(* property of being a round toward +inf *)
(** property of being a round toward +inf *)
Definition Rnd_UP_pt (F : R -> Prop) (x f : R) :=
F f /\ (x <= f)%R /\
forall g : R, F g -> (x <= g)%R -> (f <= g)%R.
......@@ -75,7 +79,7 @@ Definition Rnd_UP_pt (F : R -> Prop) (x f : R) :=
Definition Rnd_UP (F : R -> Prop) (rnd : R -> R) :=
forall x : R, Rnd_UP_pt F x (rnd x).
(* property of being a round toward zero *)
(** property of being a round toward zero *)
Definition Rnd_ZR_pt (F : R -> Prop) (x f : R) :=
( (0 <= x)%R -> Rnd_DN_pt F x f ) /\
( (x <= 0)%R -> Rnd_UP_pt F x f ).
......@@ -83,7 +87,7 @@ Definition Rnd_ZR_pt (F : R -> Prop) (x f : R) :=
Definition Rnd_ZR (F : R -> Prop) (rnd : R -> R) :=
forall x : R, Rnd_ZR_pt F x (rnd x).
(* property of being a round to nearest *)
(** property of being a round to nearest *)
Definition Rnd_N_pt (F : R -> Prop) (x f : R) :=
F f /\
forall g : R, F g -> (Rabs (f - x) <= Rabs (g - x))%R.
......
(*
(**
This file is part of the Flocq formalization of floating-point
arithmetic in Coq: http://flocq.gforge.inria.fr/
Copyright (C) 2010 Sylvie Boldo
#<br />#
Copyright (C) 2010 Guillaume Melquiond
This library is free software; you can redistribute it and/or
......@@ -16,6 +17,7 @@ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
*)
(** * Basic properties of floating-point formats: lemmas about mantissa, exponent... *)
Require Import Fcore_Raux.
Require Import Fcore_defs.
......@@ -25,6 +27,7 @@ Variable beta : radix.
Notation bpow e := (bpow beta e).
(** Basic facts *)
Theorem F2R_le_reg :
forall e m1 m2 : Z,
(F2R (Float beta m1 e) <= F2R (Float beta m2 e))%R ->
......@@ -85,6 +88,32 @@ apply Zle_antisym ;
apply Rle_refl.
Qed.
Theorem abs_F2R :
forall m e : Z,
Rabs (F2R (Float beta m e)) = F2R (Float beta (Zabs m) e).
Proof.
intros m e.
unfold F2R.
rewrite Rabs_mult.
rewrite <- Z2R_abs.
simpl.
apply f_equal.
apply Rabs_right.
apply Rle_ge.
apply bpow_ge_0.
Qed.
Theorem opp_F2R :
forall m e : Z,
Ropp (F2R (Float beta m e)) = F2R (Float beta (Zopp m) e).
Proof.
intros m e.
unfold F2R. simpl.
rewrite <- Ropp_mult_distr_l_reverse.
now rewrite Z2R_opp.
Qed.
(** Sign facts *)
Theorem F2R_0 :
forall e : Z,
F2R (Float beta 0 e) = R0.
......@@ -184,6 +213,7 @@ rewrite <- F2R_0 with (Fexp f).
now apply F2R_lt_compat.
Qed.
(** Floats and bpow *)
Theorem F2R_bpow :
forall e : Z,
F2R (Float beta 1 e) = bpow e.
......@@ -276,54 +306,6 @@ apply Z2R_le.
omega.
Qed.
Theorem ln_beta_F2R_bounds :
forall x m e, (0 < m)%Z ->
(F2R (Float beta m e) <= x < F2R (Float beta (m + 1) e))%R ->
ln_beta beta x = ln_beta beta (F2R (Float beta m e)) :> Z.
Proof.
intros x m e Hp (Hx,Hx2).
destruct (ln_beta beta (F2R (Float beta m e))) as (ex, He).
simpl.
apply ln_beta_unique.
assert (Hp1: (0 < F2R (Float beta m e))%R).
now apply F2R_gt_0_compat.
specialize (He (Rgt_not_eq _ _ Hp1)).
rewrite Rabs_pos_eq in He. 2: now apply Rlt_le.
destruct He as (He1, He2).
assert (Hx1: (0 < x)%R).
now apply Rlt_le_trans with (2 := Hx).
rewrite Rabs_pos_eq. 2: now apply Rlt_le.
split.
now apply Rle_trans with (1 := He1).
apply Rlt_le_trans with (1 := Hx2).
now apply F2R_p1_le_bpow.
Qed.
Theorem abs_F2R :
forall m e : Z,
Rabs (F2R (Float beta m e)) = F2R (Float beta (Zabs m) e).
Proof.
intros m e.
unfold F2R.
rewrite Rabs_mult.
rewrite <- Z2R_abs.
simpl.
apply f_equal.
apply Rabs_right.
apply Rle_ge.
apply bpow_ge_0.
Qed.
Theorem opp_F2R :
forall m e : Z,
Ropp (F2R (Float beta m e)) = F2R (Float beta (Zopp m) e).
Proof.
intros m e.
unfold F2R. simpl.
rewrite <- Ropp_mult_distr_l_reverse.
now rewrite Z2R_opp.
Qed.
Theorem F2R_lt_bpow :
forall f : float beta, forall e',
(Zabs (Fnum f) < Zpower beta (e' - Fexp f))%Z ->
......@@ -385,6 +367,30 @@ now apply Z2R_lt.
exact Hp.
Qed.
(** Floats and ln_beta *)
Theorem ln_beta_F2R_bounds :
forall x m e, (0 < m)%Z ->
(F2R (Float beta m e) <= x < F2R (Float beta (m + 1) e))%R ->
ln_beta beta x = ln_beta beta (F2R (Float beta m e)) :> Z.
Proof.
intros x m e Hp (Hx,Hx2).
destruct (ln_beta beta (F2R (Float beta m e))) as (ex, He).
simpl.
apply ln_beta_unique.
assert (Hp1: (0 < F2R (Float beta m e))%R).
now apply F2R_gt_0_compat.
specialize (He (Rgt_not_eq _ _ Hp1)).
rewrite Rabs_pos_eq in He. 2: now apply Rlt_le.
destruct He as (He1, He2).
assert (Hx1: (0 < x)%R).
now apply Rlt_le_trans with (2 := Hx).
rewrite Rabs_pos_eq. 2: now apply Rlt_le.
split.
now apply Rle_trans with (1 := He1).
apply Rlt_le_trans with (1 := Hx2).
now apply F2R_p1_le_bpow.
Qed.
Theorem ln_beta_F2R :
forall m e : Z,
m <> Z0 ->
......
(*
(**
This file is part of the Flocq formalization of floating-point
arithmetic in Coq: http://flocq.gforge.inria.fr/
Copyright (C) 2010 Sylvie Boldo
#<br />#
Copyright (C) 2010 Guillaume Melquiond
This library is free software; you can redistribute it and/or
......@@ -16,6 +17,7 @@ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
*)
(** * What is a real number belonging to a format, and many properties. *)
Require Import Fcore_Raux.
Require Import Fcore_defs.
Require Import Fcore_rnd.
......@@ -29,6 +31,7 @@ Notation bpow e := (bpow beta e).
Variable fexp : Z -> Z.
(** To be a good fexp *)
Definition valid_exp :=
forall k : Z,
( (fexp k < k)%Z -> (fexp (k + 1) <= k)%Z ) /\
......@@ -50,6 +53,7 @@ Definition scaled_mantissa x :=
Definition generic_format (x : R) :=
x = F2R (Float beta (Ztrunc (scaled_mantissa x)) (canonic_exponent x)).
(** Basic facts *)
Theorem generic_format_0 :
generic_format 0.
Proof.
......@@ -228,6 +232,7 @@ apply Rle_trans with (2 := proj1 Hx).
apply bpow_ge_0.
Qed.
(** Properties when the real number is "small" (kind of subnormal) *)
Theorem mantissa_small_pos :
forall x ex,
(bpow (ex - 1) <= x < bpow ex)%R ->
......@@ -297,6 +302,7 @@ assert (H := mantissa_small_pos x ex Hx He).
split ; try apply Rlt_le ; apply H.
Qed.
(** Generic facts about any format *)
Theorem generic_format_discrete :
forall x m,
let e := canonic_exponent x in
......@@ -386,6 +392,7 @@ Qed.
Section Fcore_generic_round_pos.
(** * Rounding functions: R -> Z *)
Record Zround := mkZround {
Zrnd : R -> Z ;
Zrnd_monotone : forall x y, (x <= y)%R -> (Zrnd x <= Zrnd y)%Z ;
......@@ -420,6 +427,7 @@ rewrite Zfloor_Z2R, Zrnd_Z2R in Hx.
apply Zlt_irrefl with (1 := Hx).
Qed.
(** * the most useful one: R -> F *)
Definition round x :=
F2R (Float beta (Zrnd (scaled_mantissa x)) (canonic_exponent x)).
......@@ -698,6 +706,7 @@ Qed.
End Zround_opp.
(** IEEE-754 roundings: up, down and to zero *)
Definition rndDN := mkZround Zfloor Zfloor_le Zfloor_Z2R.
Definition rndUP := mkZround Zceil Zceil_le Zceil_Z2R.
Definition rndZR := mkZround Ztrunc Ztrunc_le Ztrunc_Z2R.
......@@ -1066,6 +1075,7 @@ End not_FTZ.
Section Znearest.
(** Roundings to nearest: when in the middle, use the choice function *)
Variable choice : R -> bool.
Definition Znearest x :=
......
(*
(**
This file is part of the Flocq formalization of floating-point
arithmetic in Coq: http://flocq.gforge.inria.fr/
Copyright (C) 2010 Sylvie Boldo
#<br />#
Copyright (C) 2010 Guillaume Melquiond
This library is free software; you can redistribute it and/or
......@@ -16,6 +17,7 @@ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
*)
(** * Roundings: properties and/or functions *)
Require Import Fcore_Raux.
Require Import Fcore_defs.
......
(*
(**
This file is part of the Flocq formalization of floating-point
arithmetic in Coq: http://flocq.gforge.inria.fr/
Copyright (C) 2010 Sylvie Boldo
#<br />#
Copyright (C) 2010 Guillaume Melquiond
This library is free software; you can redistribute it and/or
......@@ -16,6 +17,7 @@ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
*)
(** * Rounding to nearest, ties to even: existence, unicity... *)
Require Import Fcore_Raux.
Require Import Fcore_defs.
Require Import Fcore_rnd.
......
(*
(**
This file is part of the Flocq formalization of floating-point
arithmetic in Coq: http://flocq.gforge.inria.fr/
Copyright (C) 2010 Sylvie Boldo
#<br />#
Copyright (C) 2010 Guillaume Melquiond
This library is free software; you can redistribute it and/or
......@@ -16,6 +17,7 @@ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
*)
(** * Unit in the Last Place: our definition using fexp and its properties *)
Require Import Fcore_Raux.
Require Import Fcore_defs.
Require Import Fcore_rnd.
......@@ -122,6 +124,7 @@ rewrite H.
now rewrite scaled_mantissa_bpow.
Qed.
(** The successor of x is x + ulp x *)
Theorem succ_le_bpow :
forall x e, (0 < x)%R -> F x ->
(x < bpow e)%R ->
......@@ -325,7 +328,7 @@ split; trivial.
apply Rlt_le; now apply Rlt_Rminus.
Qed.
(** Error of a rounding, expressed in number of ulps *)
Theorem ulp_error :
forall Zrnd x,
(Rabs (round beta fexp Zrnd x - x) < ulp x)%R.
......@@ -568,6 +571,7 @@ apply ulp_half_error.
rewrite round_DN_opp; apply Ropp_0_gt_lt_contravar; apply Rlt_gt; assumption.
Qed.
(** Predecessor *)
Definition pred x :=
if Req_bool x (bpow (ln_beta beta x - 1)) then
(x - bpow (fexp (ln_beta beta x - 1)))%R
......
Markdown is supported
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