diff --git a/lecture1.v b/lecture1.v index 2d7b2ff..db1fac4 100644 --- a/lecture1.v +++ b/lecture1.v @@ -7,27 +7,27 @@ (* - - How to define real numbers? - - Wikipedia: - - The discovery of a suitably rigorous definition of the real numbers - — indeed, the realization that a better definition was needed — was one of - the most important developments of 19th century mathematics. The currently - standard axiomatic definition is that real numbers form the unique Archimedean + + How to define real numbers? + + Wikipedia: + + The discovery of a suitably rigorous definition of the real numbers + — indeed, the realization that a better definition was needed — was one of + the most important developments of 19th century mathematics. The currently + standard axiomatic definition is that real numbers form the unique Archimedean complete totally ordered field (R,+,·,<), up to isomorphism,[1] whereas popular - constructive definitions of real numbers include declaring them as equivalence - classes of Cauchy sequences of rational numbers, Dedekind cuts, or certain - infinite "decimal representations", together with precise interpretations for - the arithmetic operations and the order relation. These definitions are - equivalent in the realm of classical mathematics. - + constructive definitions of real numbers include declaring them as equivalence + classes of Cauchy sequences of rational numbers, Dedekind cuts, or certain + infinite "decimal representations", together with precise interpretations for + the arithmetic operations and the order relation. These definitions are + equivalent in the realm of classical mathematics. + *) -(* - In Coq, real numbers are axiomatised +(* + In Coq, real numbers are axiomatised *) Require Import Reals. @@ -40,8 +40,8 @@ Check Rmult. Check Rgt. (* - We want to use the usual notations but the default interpretion is the one - for natural numbers nat + We want to use the usual notations but the default interpretion is the one + for natural numbers (nat) *) Check fun x => x + x. @@ -61,8 +61,8 @@ Check fun x => (x + x)%R. (******************************************************************************) Check R. (* the reals *) -Check R0. (* zero *) -Check R1. (* one *) +Check R0. (* zero *) +Check R1. (* one *) Check Rplus. (* addition *) Check Ropp. (* opposite *) Print Rminus. (* subtraction *) @@ -70,10 +70,10 @@ Check Rmult. (* multiplication *) (* Addition 4 axioms *) -Check Rplus_comm. (* commutativity *) -Check Rplus_assoc. (* associativity *) -Check Rplus_opp_l. (* right inverse *) -Check Rplus_0_l. (* left neutral element *) +Check Rplus_comm. (* commutativity *) +Check Rplus_assoc. (* associativity *) +Check Rplus_opp_l. (* right inverse *) +Check Rplus_0_l. (* left neutral element *) (* We can already derive some facts *) @@ -86,12 +86,12 @@ Qed. (* Multiplication 4 axioms *) -Check Rmult_comm. (* commutativity *) -Check Rmult_assoc. (* associativity *) -Check Rmult_1_l. (* left neutral element *) -Check Rmult_plus_distr_l. (* right distributivity *) +Check Rmult_comm. (* commutativity *) +Check Rmult_assoc. (* associativity *) +Check Rmult_1_l. (* left neutral element *) +Check Rmult_plus_distr_l. (* right distributivity *) -(* Non triviality 1 axiome *) +(* Non triviality 1 axiom *) Check R1_neq_R0. @@ -104,7 +104,7 @@ Fact ex2 : 121 = 11 * 11. Proof. ring. Qed. -(* Easy exercise +(* Easy exercise Fact ex3 : forall x y, (x = y) \/ (x = -y) -> x * x = y * y. Proof. @@ -138,12 +138,12 @@ Print IZR. Compute IZR (-11). Check plus_IZR. -(* - Easy exercise: Prove that INR 42 = 42. +(* + Easy exercise: Prove that INR 42 = 42. *) -(* - Easy exercise: Prove that IZR(-42) = -42. +(* + Easy exercise: Prove that IZR(-42) = -42. *) (******************************************************************************) @@ -162,49 +162,49 @@ Proof. intros. field. auto. Qed. Fact ex5 : 121 / 11 = 11. Proof. intros. field. Qed. -(* - Exercise - - Fact ex6 : forall x y, x <> y -> (x * x - y * y) / (x - y) = y + x. - Proof. - .... - Qed. - - Hint : given a goal - - H : ~ a - ----------------- - ~ b - - the tactic contradict returns the contrapose of a goal - - contradict H - - H : b - ----------------- - a - - +(* + Exercise + + Fact ex6 : forall x y, x <> y -> (x * x - y * y) / (x - y) = y + x. + Proof. + .... + Qed. + + Hint : given a goal + + H : ~ a + ----------------- + ~ b + + the tactic "contradict" returns the contrapose of a goal + + contradict H + + H : b + ----------------- + a + + *) (******************************************************************************) (* Ordering *) (******************************************************************************) -Check Rlt. (* strictly smaller *) -Print Rgt. (* strictly greater *) -Print Rle. (* smaller or equal *) -Print Rge. (* greater or equal *) +Check Rlt. (* strictly smaller *) +Print Rgt. (* strictly greater *) +Print Rle. (* smaller or equal *) +Print Rge. (* greater or equal *) -Check Rlt_asym. (* antisymmetry *) -Check Rlt_trans. (* transitivity *) -Check Rplus_lt_compat_l. (* left compatibility *) - (* with addition *) -Check Rmult_lt_compat_l. (* left compatibility *) - (* with multiplication *) +Check Rlt_asym. (* antisymmetry *) +Check Rlt_trans. (* transitivity *) +Check Rplus_lt_compat_l. (* left compatibility *) + (* with addition *) +Check Rmult_lt_compat_l. (* left compatibility *) + (* with multiplication *) -(* The tactic "lra" let us prove linear inequalities *) +(* The tactic "lra" lets us prove linear inequalities *) Require Import Psatz. @@ -212,7 +212,7 @@ Fact ex7 x : 0 < x -> 2 * x - 1 < 6 * x + 7. Proof. lra. Qed. Fact ex8 : 12 / 15 < 37 / 45. -Proof. intros. lra. Qed. +Proof. lra. Qed. Check total_order_T. (* The order is total *) Print sumbool. @@ -233,27 +233,27 @@ Print Rmax2. Lemma Rmax2_comm x y : Rmax2 x y = Rmax2 y x. Proof. unfold Rmax2. -destruct (total_order_T x y) as [[xLy |xEy] | xGy]; +destruct (total_order_T x y) as [[xLy |xEy] | xGy]; destruct (total_order_T y x) as [[yLx |yEx] | yGx]; lra. Qed. -(* - Exercise : define Rmax3 that takes 3 numbers and returns the greates of - three +(* + Exercise : define Rmax3 that takes 3 numbers and returns the greatest of + three *) -(* We can test equality on real number. Propositional version *) +(* We can test equality on real numbers. Propositional version *) Check Req_dec. -(* - Exercise : Build a computation version of Req_dec +(* + Exercise : Build a computational version of Req_dec *) (* Integrality of R can be proved *) Check Rmult_integral. -(* - Exercise : Reprove integrality without using Rmult_integral +(* + Exercise : Reprove integrality without using Rmult_integral *) Fact ex9 x : x ^ 2 - 2 * x + 1 = 0 <-> x = 1. @@ -273,35 +273,35 @@ Check Rabs. Check Rcase_abs. Print Rabs. -(* - The tactic split_Rabs let us remove the absolute value by generating - all the possible cases +(* + The tactic "split_Rabs" lets us remove the absolute value by generating + all the possible cases *) Fact ex10 x y z : Rabs (x - z) <= Rabs (x - y) + Rabs (y - z). Proof. split_Rabs. lra. lra. lra. lra. lra. lra. lra. lra. Qed. -(* - Exercise : Prove that (x * x = y * y) is equivalent to (Rabs x = Rabs y) +(* + Exercise : Prove that (x * x = y * y) is equivalent to (Rabs x = Rabs y) *) -(* Property of being archimedian *) +(* Property of being archimedean *) Check up. (* an uppper bound *) Check archimed. (* the characteristic property *) -(* Completness *) +(* Completeness *) Check is_upper_bound. (* to be an upper bound *) Print is_upper_bound. Check bound. (* to be bounded *) Print bound. -Check is_lub. (* to be the smallest bound *) +Check is_lub. (* to be the least bound *) Print is_lub. -Check completeness. (* completness *) +Check completeness. (* completeness *) -(* From this 24 axioms we can build the usual functions *) +(* From these 24 axioms we can build the usual functions *) Check IVT. (* intermediate value theorem *) Check cos_plus. (* some trigonometry *) @@ -318,24 +318,23 @@ Search _ (0 < _) (_ * _) outside Fourier_util. (* without fourier *) SearchPattern (0 < _ * _). (* filtering the conclusion *) -(* - Resume - - we can play formally with the reals - - two automatic tactics - field to prove equalities - lra to prove linear inequalities - - split_Rabs to remove the absolute values - - set (x := ....) to name a subterm - - assert (H : ....) to introduce an intermediate result - - Search, SearchPattern to search in the library +(* + Resume + - we can play formally with the reals + - two automatic tactics + field to prove equalities + lra to prove linear inequalities + - split_Rabs to remove the absolute values + - set (x := ....) to name a subterm + - assert (H : ....) to introduce an intermediate result + - Search, SearchPattern to search in the library *) -(* - Exercise, - given two real numbers x and y such that 0 < x < y, show that - if A is the arithmetic mean and G the geometric one then we have - x < G < A < y +(* + Exercise, + given two real numbers x and y such that 0 < x < y, show that + if A is the arithmetic mean and G the geometric one then we have + x < G < A < y *) End Lecture1. - diff --git a/lecture2.v b/lecture2.v index 6be7351..3b03f9a 100644 --- a/lecture2.v +++ b/lecture2.v @@ -5,12 +5,12 @@ (* *) (******************************************************************************) -(* - - How to define floating point numbers ? - - We are going to use the flocq library at http://flocq.gforge.inria.fr/ - +(* + + How to define floating point numbers ? + + We are going to use the Flocq library at http://flocq.gforge.inria.fr/ + *) Require Import Psatz Reals. @@ -31,7 +31,7 @@ Variables vx vy : R. (* Some values for our examples *) Check F vx. (* vx is a floating-point number *) -Variable P : R -> R -> Prop. (* The relation +Variable P : R -> R -> Prop. (* The relation "to be a rounded value" *) Check P vx vy. (* vy is a rounded value of vx *) @@ -52,7 +52,7 @@ Qed. Definition rnd := let (f, _) := round_fun_of_pred P round_pred_P in f. -Check rnd. (* the function associated with the +Check rnd. (* the function associated with the relation *) Lemma rndP : forall x, P x (rnd x). (* its associated relation *) @@ -89,7 +89,7 @@ Eval lazy beta delta [Rnd_ZR] in Rnd_ZR F rnd. (******************************************************************************) Fact ex1 : forall x, F x -> Rnd_DN_pt F x x. (* Rnd_Dn_pt idempotent on F *) -Proof. +Proof. intros x Fx; repeat split. - assumption. - lra. @@ -104,35 +104,35 @@ destruct Rxg as [Fg [gLy gdown]]. apply gdown; try lra; assumption. Qed. -(* - Prove that UP is also idempotent and monotone - -Fact ex3 : forall x, F x -> Rnd_UP_pt F x x. -Proof. -... -Qed. - -Fact ex4 : round_pred_monotone (Rnd_UP_pt F). -Proof. -... -Qed. - - Prove that ZR is idempotent but only monotone if 0 is a float - -Fact ex5 : forall x, F x -> Rnd_ZR_pt F x x. -Proof. -... -Qed. - -Fact ex6 : F 0 -> round_pred_monotone (Rnd_ZR_pt F). -Proof. -... -Qed. - -Hint: - In order to perform a case analysis on the fact that x is smaller to y or not - one can use the tactic "destruct (Rle_lt_dec x y) as [xLy | yLx]" - +(* + Prove that UP is also idempotent and monotone + +Fact ex3 : forall x, F x -> Rnd_UP_pt F x x. +Proof. +... +Qed. + +Fact ex4 : round_pred_monotone (Rnd_UP_pt F). +Proof. +... +Qed. + + Prove that ZR is idempotent but only monotone if 0 is a float + +Fact ex5 : forall x, F x -> Rnd_ZR_pt F x x. +Proof. +... +Qed. + +Fact ex6 : F 0 -> round_pred_monotone (Rnd_ZR_pt F). +Proof. +... +Qed. + +Hint: + In order to perform a case analysis on the fact that x is smaller than y or not + one can use the tactic "destruct (Rle_lt_dec x y) as [xLy | yLx]" + *) (******************************************************************************) @@ -143,8 +143,7 @@ Hint: Fact ex7 : (forall x, F x -> F (-x)) -> (* the format is symmetric *) round_pred_total (Rnd_DN_pt F) -> round_pred_total (Rnd_UP_pt F). Proof. -intros sym tDN. -intros x. +intros sym tDN x. destruct (tDN (-x)) as [y [Fy [yLx yM]]]. exists (-y); repeat split. - apply sym; auto. @@ -158,24 +157,24 @@ Print satisfies_any. Hypothesis SAF : satisfies_any F. -(* - Prove that DN, UP, ZR are rounding predicates - -Fact ex8 : round_pred (Rnd_DN_pt F). -Proof. -... -Qed. - -Fact ex9 : round_pred (Rnd_UP_pt F). -Proof. -... -Qed. - -Fact ex10 : round_pred (Rnd_ZR_pt F). -Proof. -... -Qed. - +(* + Prove that DN, UP, ZR are rounding predicates + +Fact ex8 : round_pred (Rnd_DN_pt F). +Proof. +... +Qed. + +Fact ex9 : round_pred (Rnd_UP_pt F). +Proof. +... +Qed. + +Fact ex10 : round_pred (Rnd_ZR_pt F). +Proof. +... +Qed. + *) @@ -189,42 +188,42 @@ Eval lazy beta delta [Rnd_N_pt] in Rnd_N_pt F vx vy. Check Rnd_N. Eval lazy beta delta [Rnd_N] in Rnd_N F rnd. -(* - - Prove that N is idempotent, that is either UP or DOWN and that it is strictly - monotone - -Fact ex11 : forall x, F x -> Rnd_N_pt F x x. -Proof. -... -Qed. - -Fact ex12 : forall x f, Rnd_N_pt F x f -> Rnd_DN_pt F x f \/ Rnd_UP_pt F x f. -Proof. -... -Qed. - -Fact ex13 : forall x y f g, - Rnd_N_pt F x f -> Rnd_N_pt F y g -> x < y -> f <= g. -Proof. -... -Qed. - -Hints : some theorems about absolute values -Check Rabs_R0. -Check Rabs_pos. -Check Rabs_right. -Check Rabs_left. - +(* + + Prove that N is idempotent, that is either UP or DOWN and that it is strictly + monotone + +Fact ex11 : forall x, F x -> Rnd_N_pt F x x. +Proof. +... +Qed. + +Fact ex12 : forall x f, Rnd_N_pt F x f -> Rnd_DN_pt F x f \/ Rnd_UP_pt F x f. +Proof. +... +Qed. + +Fact ex13 : forall x y f g, + Rnd_N_pt F x f -> Rnd_N_pt F y g -> x < y -> f <= g. +Proof. +... +Qed. + +Hints : some theorems about absolute values +Check Rabs_R0. +Check Rabs_pos. +Check Rabs_right. +Check Rabs_left. + *) - + Variable T : R -> R -> Prop. (* Tie-break rule *) Check Rnd_NG_pt F T vx vy. Eval lazy beta delta [Rnd_NG_pt] in Rnd_NG_pt F T vx vy. -Check NG_existence_prop F T. (* condition to ensure existance *) +Check NG_existence_prop F T. (* condition to ensure existence *) Eval lazy beta delta [NG_existence_prop] in NG_existence_prop F T. Search NG_existence_prop. @@ -239,29 +238,29 @@ Search Rnd_NG_pt_unique_prop. Definition Taway x f := Rabs f >= Rabs x. -(* - Prove that Taway verifies the two properties to build a rounding mode - - -Fact ex14 : NG_existence_prop F Taway. -Proof. -... -Qed. - -Fact ex15 : F 0 -> Rnd_NG_pt_unicity_prop F Taway. -Proof. -... -Qed. - +(* + Prove that Taway verifies the two properties to build a rounding mode + + +Fact ex14 : NG_existence_prop F Taway. +Proof. +... +Qed. + +Fact ex15 : F 0 -> Rnd_NG_pt_unique_prop F Taway. +Proof. +... +Qed. + *) (* - Resume - - - "generic" version of format and roundind modes - - 4 rounding functions : up, down, to zero, to the nearest. - + Resume + + - "generic" version of format and rounding modes + - 4 rounding functions : up, down, to zero, to the nearest. + *) End Lecture2. \ No newline at end of file diff --git a/lecture3.v b/lecture3.v index 56f16d6..b2731f9 100644 --- a/lecture3.v +++ b/lecture3.v @@ -6,9 +6,9 @@ (******************************************************************************) -(* - After having seeen the rounding mode, we are going to see the formats for - our floating point numbers. We start from a very generic representation +(* + After having seen the rounding mode, we are going to see the formats for + our floating point numbers. We start from a very generic representation *) Require Import Psatz ZArith Reals. @@ -24,23 +24,23 @@ Section Lecture3. Check radix. (* A basis *) Print radix. -Definition radix2 : radix. exists 2%Z. auto. Defined. +Definition radix2 : radix. exists 2%Z. auto. Defined. Definition radix10 : radix. exists 10%Z. auto. Defined. Print Coercion Paths radix Z. Compute (radix2 + 2)%Z. - + Check float. -Check float radix2. (* Floating point number as +Check float radix2. (* Floating point number as pair of integers *) -Check float radix10. +Check float radix10. Print float. -Definition val1 : float radix2 := {| Fnum := 7; Fexp := 1 |}. +Definition val1 : float radix2 := {| Fnum := 7; Fexp := 1 |}. Compute Fnum val1. Compute Fexp val1. -Definition val2 : float radix2 := {| Fnum := 7; Fexp := 0 |}. +Definition val2 : float radix2 := {| Fnum := 7; Fexp := 0 |}. Compute Fnum val2. Compute Fexp val2. @@ -54,14 +54,14 @@ Compute F2R val3. Variable r : radix. -(* +(* Prove that the positivity of a floating point number is the one of its matissa - -Fact ex1 : forall (f : float r), (0 <= Fnum f)%Z <-> 0 <= F2R f. -Proof. -... -Qed. - + +Fact ex1 : forall (f : float r), (0 <= Fnum f)%Z <-> 0 <= F2R f. +Proof. +... +Qed. + *) (******************************************************************************) @@ -106,15 +106,15 @@ Search Fmult. Variable e : Z. (* Bound on the exponent *) Variable p : Z. (* Precision for the mantissa *) -Variables x y : R. +Variables x y : R. (* Format with a fixed exponent *) Check FIX_format r e x. Check FIX_spec. -(* - Prove that zero is in the FIX format and that this format is symmetric -*) +(* + Prove that zero is in the FIX format and that this format is symmetric +*) Fact ex2 : FIX_format r e 0. Proof. exists {| Fnum := 0; Fexp := e |}. @@ -137,57 +137,57 @@ Qed. Check FLX_format r p x. Check FLX_spec. -(* - Prove that zero is in the FLX format and that this format is symmetric - -Fact ex4 : (0 <= p)%Z -> FLX_format r p 0. -Proof. -... -Qed. - -Fact ex5 : FLX_format r p x -> FLX_format r p (- x). -Proof. -... -Qed. - +(* + Prove that zero is in the FLX format and that this format is symmetric + +Fact ex4 : (0 <= p)%Z -> FLX_format r p 0. +Proof. +... +Qed. + +Fact ex5 : FLX_format r p x -> FLX_format r p (- x). +Proof. +... +Qed. + *) (* Format with normalised numbers but without bound on the exponent *) Check FLXN_format r p x. Check FLXN_spec. -(* - Prove that zero is in the FLXN format and that this format is symmetric - -Fact ex6 : FLXN_format r p 0. -Proof. -... -Qed. - -Fact ex7 : FLXN_format r p x -> FLXN_format r p (- x). -Proof. -... -Qed. - +(* + Prove that zero is in the FLXN format and that this format is symmetric + +Fact ex6 : FLXN_format r p 0. +Proof. +... +Qed. + +Fact ex7 : FLXN_format r p x -> FLXN_format r p (- x). +Proof. +... +Qed. + *) (* Format with denormalised numbers and with bound on the exponent *) Check FLT_format r e p x. Check FLT_spec. -(* - Prove that zero is in the FLT format and that this format is symmetric - -Fact ex8 : (0 <= p)%Z -> FLT_format r e p 0. -Proof. -... -Qed. - -Fact ex9 : FLT_format r e p x -> FLT_format r e p (- x). -Proof. -... -Qed. - +(* + Prove that zero is in the FLT format and that this format is symmetric + +Fact ex8 : (0 <= p)%Z -> FLT_format r e p 0. +Proof. +... +Qed. + +Fact ex9 : FLT_format r e p x -> FLT_format r e p (- x). +Proof. +... +Qed. + *) (* Format without denormalised numbers but with bound on the exponent *) @@ -195,19 +195,19 @@ Qed. Check FTZ_format r e p x. Check FTZ_spec. -(* - Prove that zero is in the FTZ format and that this format is symmetric - -Fact ex10 : (0 <= p)%Z -> FTZ_format r e p 0. -Proof. -... -Qed. - -Fact ex11 : FTZ_format r e p x -> FTZ_format r e p (- x). -Proof. -... -Qed. - +(* + Prove that zero is in the FTZ format and that this format is symmetric + +Fact ex10 : (0 <= p)%Z -> FTZ_format r e p 0. +Proof. +... +Qed. + +Fact ex11 : FTZ_format r e p x -> FTZ_format r e p (- x). +Proof. +... +Qed. + *) (******************************************************************************) @@ -226,7 +226,7 @@ Print Coercion Paths mag_prop Z. Check (mag r x + 2)%Z. Check (bpow_mag_gt r x). (* lemma for the upper bound *) -Check archimed. (* Archimedian property *) +Check archimed. (* Archimedean property *) Check Zfloor. (* The floor function *) Print Zfloor. Check Zceil. (* The ceiling function *) @@ -244,14 +244,14 @@ Eval lazy beta delta [scaled_mantissa] in scaled_mantissa r phi x. Check generic_format r phi x. (* Generic format that depends only on phi *) Eval lazy beta delta [generic_format] in generic_format r phi x. -Eval lazy beta delta [generic_format F2R Fnum Fexp] iota in +Eval lazy beta delta [generic_format F2R Fnum Fexp] iota in generic_format r phi x. -Eval lazy beta delta [generic_format F2R scaled_mantissa Fnum Fexp] iota in +Eval lazy beta delta [generic_format F2R scaled_mantissa Fnum Fexp] iota in generic_format r phi x. -(* - Prove that the generic format contains zero and is symmetric +(* + Prove that the generic format contains zero and is symmetric *) Fact ex12 : generic_format r phi 0. @@ -260,7 +260,7 @@ unfold generic_format, F2R, scaled_mantissa; simpl. todo. Qed. -Fact ex13 : forall z, z <> 0 -> mag r (- z) = mag r z :> Z. +Fact ex13 : forall z, z <> 0 -> mag r (- z) = mag r z :> Z. Proof. Search mag inside Raux. todo. @@ -272,12 +272,12 @@ intros z; unfold generic_format, scaled_mantissa, cexp, F2R; simpl. todo. Qed. -(* -Hint : we can rely on the following properties of Ztrunc and mag - -Search Ztrunc inside Fcore_Raux. -Search mag inside Fcore_Raux. - +(* +Hint : we can rely on the following properties of Ztrunc and mag + +Search Ztrunc inside Fcore_Raux. +Search mag inside Fcore_Raux. + *) (* We can revisit the previous format using the algorithmic version *) @@ -309,55 +309,55 @@ Check FLT_format_generic r e p x. Check FTZ_exp e p z. Eval lazy beta delta [FTZ_exp] in FTZ_exp e p z. -(* - Prove Sterbenz lemma using the only property that phi is monotone - -Fact ex15 : - Monotone_exp phi -> - generic_format r phi x -> generic_format r phi y -> - (y / 2 <= x <= 2 * y)%R -> - generic_format r phi (x - y)%R. -Proof. -... -Qed. - -For this proof, we use the following lemma that gives a simple criterion to -ensure that a float is in the format - -Check generic_format_F2R. - -Here is the informal proof : - From (y / 2 <= x <= 2 * y) we deduce that - - 0 <= y (1) - - 0 <= x (2) - - x - y <= x (3) - - x - y <= y. (4) - generic_format r phi x can be rewritten as - x = F2R {| Fnum := mx; Fexp := phi (mag r x) |} - generic_format r phi y can be rewritten as - y = F2R {| Fnum := my, Fexp := phi (mag r y) |} - using Fopp, we can rewrite x - y as - x - y = - F2R {|Fnum := mz, Fexp := Z.min (phi (mag r x), phi (mag r y) |} - so in order to have generic_format r phi (x - y) using generic_format_F2R, - it is sufficient that - - phi (mag r (x - y)) <= Z.min (phi (mag r x), phi (mag r y)) - - so that - - phi (mag r (x - y)) <= phi (mag r x) - and - phi (mag r (x - y)) <= phi (mag r y) - - but mag is monotone so is phi, it is then sufficient to prove that - - x - y <= x - and - x - y <= y - - that come from (3) and (4). - +(* + Prove Sterbenz lemma using the only property that phi is monotone + +Fact ex15 : + Monotone_exp phi -> + generic_format r phi x -> generic_format r phi y -> + (y / 2 <= x <= 2 * y)%R -> + generic_format r phi (x - y)%R. +Proof. +... +Qed. + +For this proof, we use the following lemma that gives a simple criterion to +ensure that a float is in the format + +Check generic_format_F2R. + +Here is the informal proof : + From (y / 2 <= x <= 2 * y) we deduce that + - 0 <= y (1) + - 0 <= x (2) + - x - y <= x (3) + - x - y <= y. (4) + generic_format r phi x can be rewritten as + x = F2R {| Fnum := mx; Fexp := phi (mag r x) |} + generic_format r phi y can be rewritten as + y = F2R {| Fnum := my, Fexp := phi (mag r y) |} + using Fopp, we can rewrite x - y as + x - y = + F2R {|Fnum := mz, Fexp := Z.min (phi (mag r x), phi (mag r y) |} + so in order to have generic_format r phi (x - y) using generic_format_F2R, + it is sufficient that + + phi (mag r (x - y)) <= Z.min (phi (mag r x), phi (mag r y)) + + so that + + phi (mag r (x - y)) <= phi (mag r x) + and + phi (mag r (x - y)) <= phi (mag r y) + + but mag is monotone so is phi, it is then sufficient to prove that + + x - y <= x + and + x - y <= y + + that come from (3) and (4). + *) @@ -372,7 +372,7 @@ Check round r phi Zfloor x. (* Rounding down *) Eval lazy beta delta [round] in round r phi Zfloor x. Check round r phi Zceil x. (* Rounding up *) -Eval lazy beta delta [round] in round r phi Zfloor x. +Eval lazy beta delta [round] in round r phi Zceil x. Check round r phi Ztrunc x. (* Rounding to zero *) Eval lazy beta delta [round] in round r phi Ztrunc x. @@ -401,86 +401,86 @@ Check valid_rnd_ZR. Check valid_rnd_N choice. -(* - Prove that the error resulting of an addition in rounded to the nearest - can always be represented exactly - - We first prove a first general result on how a rounded value can be - represented - - Fact ex16 : - forall (f : float r) rnd, Valid_rnd rnd -> - exists m', - round r phi rnd (F2R f) = - F2R ({| Fnum := m'; Fexp := Fexp f |} : float r). - Proof. - ... - Qed. - - Informal proof - we can rewrite the rounded value as: - - round r phi rnd (F2R f) = - F2R {| Fnum := m; Fexp := phi (mag r (Fexp f)) |} - - if phi (mag r (Fexp f)) <= Fexp f - - we can choose m' = (Fnum f) - - if phi (mag r (Fexp f)) > Fexp f - - we can choose m' = m * r ^ (phi (mag r (Fexp f)) - Fexp f). - - Fact ex17 : - Monotone_exp phi -> - generic_format r phi x -> generic_format r phi y -> - generic_format r phi (round r phi (Znearest choice) (x + y) - (x + y))%R. - Proof. - .... - Qed. - - Informal proof - - generic_format r phi x can be rewritten as - x = F2R {| Fnum := mx; Fexp := phi (mag r x) |} - - generic_format r phi y, can be rewritten as - y = F2R {| Fnum := my; Fexp := phi (mag r y) |} - - without loss of generality we can suppose that - phi (mag r x) <= phi (mag r y) - - so using Fplus we have - x + y = F2R {| Fnum := mx + - my * r ^ (phi (mag r y) - phi (mag r x)); - Fexp := phi (mag x) |} - - applyin ex16 we get - round r phi (Znearest choice) (F2R (x + y)) = - F2R {| Fnum := m; Fexp := phi (mag r x) |} - - the definition of Fopp gives - round r phi (Znearest choice) (x + y) - (x + y) = +(* + Prove that the error resulting from an addition in rounded to the nearest + can always be represented exactly + + We first prove a general result on how a rounded value can be + represented + + Fact ex16 : + forall (f : float r) rnd, Valid_rnd rnd -> + exists m', + round r phi rnd (F2R f) = + F2R ({| Fnum := m'; Fexp := Fexp f |} : float r). + Proof. + ... + Qed. + + Informal proof + we can rewrite the rounded value as: + + round r phi rnd (F2R f) = + F2R {| Fnum := m; Fexp := phi (mag r (Fexp f)) |} + + if phi (mag r (Fexp f)) <= Fexp f + + we can choose m' = (Fnum f) + + if phi (mag r (Fexp f)) > Fexp f + + we can choose m' = m * r ^ (phi (mag r (Fexp f)) - Fexp f). + + Fact ex17 : + Monotone_exp phi -> + generic_format r phi x -> generic_format r phi y -> + generic_format r phi (round r phi (Znearest choice) (x + y) - (x + y))%R. + Proof. + ... + Qed. + + Informal proof + + generic_format r phi x can be rewritten as + x = F2R {| Fnum := mx; Fexp := phi (mag r x) |} + + generic_format r phi y can be rewritten as + y = F2R {| Fnum := my; Fexp := phi (mag r y) |} + + without loss of generality we can suppose that + phi (mag r x) <= phi (mag r y) + + so using Fplus we have + x + y = F2R {| Fnum := mx + + my * r ^ (phi (mag r y) - phi (mag r x)); + Fexp := phi (mag x) |} + + applyin ex16 we get + round r phi (Znearest choice) (F2R (x + y)) = + F2R {| Fnum := m; Fexp := phi (mag r x) |} + + the definition of Fopp gives + round r phi (Znearest choice) (x + y) - (x + y) = F2R {| Fnum := m - mx + my * r ^ (phi (mag r y) - phi (mag r x)); - Fexp := phi (mag r x) |} - - using generic_format_F2R, a sufficient condition for this float to be in - the format is : - - phi (mag r (round r phi (Znearest choice) (x + y) - (x + y))) <= - phi (mag r x) - - phi and mag are monotone so it is sufficient that - - |round r phi (Znearest choice) (x + y) - (x + y))| <= |x| - - so - - |round r phi (Znearest choice) (x + y) - (x + y))| <= |y - (x + y)| - - but y is a float so its distance to x + y must be greater or equal to the one - of the rounded value to the nearest of x + y. - + Fexp := phi (mag r x) |} + + using generic_format_F2R, a sufficient condition for this float to be in + the format is : + + phi (mag r (round r phi (Znearest choice) (x + y) - (x + y))) <= + phi (mag r x) + + phi and mag are monotone so it is sufficient that + + |round r phi (Znearest choice) (x + y) - (x + y))| <= |x| + + so + + |round r phi (Znearest choice) (x + y) - (x + y))| <= |y - (x + y)| + + but y is a float so its distance to x + y must be greater or equal to the one + of the rounded value to the nearest of x + y. + *) End Lecture3. \ No newline at end of file diff --git a/lecture4.v b/lecture4.v index 96c43aa..73e5967 100644 --- a/lecture4.v +++ b/lecture4.v @@ -5,8 +5,8 @@ (* *) (******************************************************************************) -(* - we present the notion of ulp and the concrete IEEE 754 format +(* + we present the notion of ulp and the concrete IEEE 754 format *) Require Import Psatz ZArith Reals SpecFloat. @@ -20,7 +20,7 @@ Section Lecture4. Variable vx vy : R. (* Basis *) Variable r : radix. -(* Translating funtion for the exponent *) +(* Translating function for the exponent *) Variable phi : Z -> Z. Hypothesis vPhi : Valid_exp phi. (* Rounding function *) @@ -36,67 +36,89 @@ Eval lazy beta delta [ulp cexp] in ulp r phi vx. Check ulp_neq_0. -(* - Prove that if phi is monotone so is ulp - -Fact ex1 x y : - x <> 0 -> Monotone_exp phi -> Rabs x <= Rabs y -> ulp r phi x <= ulp r phi y. - -Hints: - -Check mag_le_abs. -Check bpow_le. - +(* + Prove that if phi is monotone so is ulp + +Fact ex1 x y : + x <> 0 -> Monotone_exp phi -> Rabs x <= Rabs y -> ulp r phi x <= ulp r phi y. +Proof. +... +Qed. + +Hints: + +Check mag_le_abs. +Check bpow_le. + *) Check round_UP_DN_ulp. Check round_UP_DN_ulp r phi vx. -(* - Reprove round_UP_DN_ulp - -Fact ext2 x : - ~ generic_format r phi x -> - round r phi Zceil x = round r phi Zfloor x + ulp r phi x. - -Hints: - -Check scaled_mantissa_mult_bpow. -Check Zceil_floor_neq. -Check Ztrunc_IZR. - +(* + Reprove round_UP_DN_ulp + +Fact ext2 x : + ~ generic_format r phi x -> + round r phi Zceil x = round r phi Zfloor x + ulp r phi x. +Proof. +... +Qed. + +Hints: + +Check scaled_mantissa_mult_bpow. +Check Zceil_floor_neq. +Check Ztrunc_IZR. + *) Check error_lt_ulp. -(* - Reprove error_lt_ulp : - Fact ext3 x : x <> 0 -> Rabs (round r phi rnd x - x) < ulp r phi x. - -Hints : - -Check round_DN_UP_lt. -Check round_DN_or_UP. -Check round_UP_DN_ulp. - +(* Helper lemma *) + +Lemma format_dec x : generic_format r phi x \/ ~ generic_format r phi x. +Proof. +unfold generic_format, F2R; simpl. +set (y := _ * _); case (Req_dec x y); auto. +Qed. + +(* + Reprove error_lt_ulp : + + Fact ext3 x : x <> 0 -> Rabs (round r phi rnd x - x) < ulp r phi x. + Proof. + ... + Qed. + +Hints : + +Check round_DN_UP_lt. +Check round_DN_or_UP. +Check round_UP_DN_ulp. + *) Check error_le_half_ulp. -(* - Reprove error_le_half_ulp : - Fact ext4 x : - Rabs (round r phi (Znearest choice) x - x) <= / 2 * ulp r phi x. - -Hints: - -Check round_N_pt. -Check generic_format_round. -Check round_DN_UP_lt. -Check round_DN_or_UP. -Check round_UP_DN_ulp. - +(* + Reprove error_le_half_ulp : + + Fact ext4 x : + Rabs (round r phi (Znearest choice) x - x) <= / 2 * ulp r phi x. + Proof. + ... + Qed. + +Hints: + +Check round_N_pt. +Check generic_format_round. +Check round_DN_UP_lt. +Check round_DN_or_UP. +Check round_UP_DN_ulp. + *) (* The IEEE 754 norm *) @@ -120,7 +142,7 @@ Print binary64. Check binary_float. -(* Generic float *) +(* Generic float *) (* Variables for the precision and the exponent range *) Variable vp ve : Z. @@ -136,11 +158,11 @@ Check is_finite vp ve. Compute is_finite vp ve f. (* Checking bound *) -Eval lazy beta zeta iota delta [bounded] in +Eval lazy beta zeta iota delta [bounded] in (bounded vp ve m e). (* Test on the mantissa *) -Check canonical_canonical_mantissa vp ve s m e. +Check canonical_canonical_mantissa vp ve s m e. Print canonical. Print cexp.