Commit 82239e90 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Update Coq realizations.

parent d3d7c7ac
...@@ -52,11 +52,13 @@ Defined. ...@@ -52,11 +52,13 @@ Defined.
(* Why3 goal *) (* Why3 goal *)
Lemma t'axiom : Lemma t'axiom :
forall (x:t), (t'isFinite x) -> forall (x:t), (t'isFinite x) ->
((-(16777215 * 20282409603651670423947251286016)%R)%R <= (t'real x))%R /\ ((-340282346638528859811704183484516925440%R)%R <= (t'real x))%R /\
((t'real x) <= (16777215 * 20282409603651670423947251286016)%R)%R. ((t'real x) <= 340282346638528859811704183484516925440%R)%R.
Proof. Proof.
intros x _. intros x _.
apply Rabs_le_inv. apply Rabs_le_inv.
change 340282346638528859811704183484516925440%Z with (16777215 * 20282409603651670423947251286016)%Z.
rewrite mult_IZR.
change (Rabs (B2R _ _ x) <= F2R (Float radix2 (Zpower radix2 24 - 1) (127 - 23)))%R. change (Rabs (B2R _ _ x) <= F2R (Float radix2 (Zpower radix2 24 - 1) (127 - 23)))%R.
destruct x as [s|s|s|s m e H] ; destruct x as [s|s|s|s m e H] ;
try (simpl ; rewrite Rabs_R0 ; now apply F2R_ge_0). try (simpl ; rewrite Rabs_R0 ; now apply F2R_ge_0).
......
...@@ -52,13 +52,16 @@ Defined. ...@@ -52,13 +52,16 @@ Defined.
(* Why3 goal *) (* Why3 goal *)
Lemma t'axiom : Lemma t'axiom :
forall (x:t), (t'isFinite x) -> forall (x:t), (t'isFinite x) ->
((-(9007199254740991 * 19958403095347198116563727130368385660674512604354575415025472424372118918689640657849579654926357010893424468441924952439724379883935936607391717982848314203200056729510856765175377214443629871826533567445439239933308104551208703888888552684480441575071209068757560416423584952303440099278848)%R)%R ((-179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368%R)%R
<= (t'real x))%R /\ <= (t'real x))%R /\
((t'real x) <= ((t'real x) <=
(9007199254740991 * 19958403095347198116563727130368385660674512604354575415025472424372118918689640657849579654926357010893424468441924952439724379883935936607391717982848314203200056729510856765175377214443629871826533567445439239933308104551208703888888552684480441575071209068757560416423584952303440099278848)%R)%R. 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368%R)%R.
Proof. Proof.
intros x _. intros x _.
apply Rabs_le_inv. apply Rabs_le_inv.
change 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368%Z
with (9007199254740991 * 19958403095347198116563727130368385660674512604354575415025472424372118918689640657849579654926357010893424468441924952439724379883935936607391717982848314203200056729510856765175377214443629871826533567445439239933308104551208703888888552684480441575071209068757560416423584952303440099278848)%Z.
rewrite mult_IZR.
change (Rabs (B2R _ _ x) <= F2R (Float radix2 (Zpower radix2 53 - 1) (1023 - 52)))%R. change (Rabs (B2R _ _ x) <= F2R (Float radix2 (Zpower radix2 53 - 1) (1023 - 52)))%R.
destruct x as [s|s|s|s m e H] ; destruct x as [s|s|s|s m e H] ;
try (simpl ; rewrite Rabs_R0 ; now apply F2R_ge_0). try (simpl ; rewrite Rabs_R0 ; now apply F2R_ge_0).
......
...@@ -105,7 +105,7 @@ Qed. ...@@ -105,7 +105,7 @@ Qed.
(* Why3 goal *) (* Why3 goal *)
Lemma Pow_half : Lemma Pow_half :
forall (x:R), (0%R < x)%R -> forall (x:R), (0%R < x)%R ->
((Reals.Rpower.Rpower x (05 / 10)%R) = (Reals.R_sqrt.sqrt x)). ((Reals.Rpower.Rpower x (5 / 10)%R) = (Reals.R_sqrt.sqrt x)).
Proof. Proof.
intros x h1. intros x h1.
replace (5 / 10)%R with (/ 2)%R by field. replace (5 / 10)%R with (/ 2)%R by field.
......
...@@ -103,7 +103,7 @@ Qed. ...@@ -103,7 +103,7 @@ Qed.
(* Why3 goal *) (* Why3 goal *)
Lemma Cos_pi2 : Lemma Cos_pi2 :
((Reals.Rtrigo_def.cos ((05 / 10)%R * Reals.Rtrigo1.PI)%R) = 0%R). ((Reals.Rtrigo_def.cos ((5 / 10)%R * Reals.Rtrigo1.PI)%R) = 0%R).
Proof. Proof.
replace (5 / 10 * PI)%R with (PI / 2)%R by field. replace (5 / 10 * PI)%R with (PI / 2)%R by field.
apply cos_PI2. apply cos_PI2.
...@@ -111,7 +111,7 @@ Qed. ...@@ -111,7 +111,7 @@ Qed.
(* Why3 goal *) (* Why3 goal *)
Lemma Sin_pi2 : Lemma Sin_pi2 :
((Reals.Rtrigo_def.sin ((05 / 10)%R * Reals.Rtrigo1.PI)%R) = 1%R). ((Reals.Rtrigo_def.sin ((5 / 10)%R * Reals.Rtrigo1.PI)%R) = 1%R).
Proof. Proof.
replace (5 / 10 * PI)%R with (PI / 2)%R by field. replace (5 / 10 * PI)%R with (PI / 2)%R by field.
apply sin_PI2. apply sin_PI2.
...@@ -140,7 +140,7 @@ Qed. ...@@ -140,7 +140,7 @@ Qed.
(* Why3 goal *) (* Why3 goal *)
Lemma Cos_plus_pi2 : Lemma Cos_plus_pi2 :
forall (x:R), forall (x:R),
((Reals.Rtrigo_def.cos (x + ((05 / 10)%R * Reals.Rtrigo1.PI)%R)%R) = ((Reals.Rtrigo_def.cos (x + ((5 / 10)%R * Reals.Rtrigo1.PI)%R)%R) =
(-(Reals.Rtrigo_def.sin x))%R). (-(Reals.Rtrigo_def.sin x))%R).
Proof. Proof.
intros x. intros x.
...@@ -152,7 +152,7 @@ Qed. ...@@ -152,7 +152,7 @@ Qed.
(* Why3 goal *) (* Why3 goal *)
Lemma Sin_plus_pi2 : Lemma Sin_plus_pi2 :
forall (x:R), forall (x:R),
((Reals.Rtrigo_def.sin (x + ((05 / 10)%R * Reals.Rtrigo1.PI)%R)%R) = ((Reals.Rtrigo_def.sin (x + ((5 / 10)%R * Reals.Rtrigo1.PI)%R)%R) =
(Reals.Rtrigo_def.cos x)). (Reals.Rtrigo_def.cos x)).
Proof. Proof.
intros x. intros x.
......
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