Commit 53bba4a2 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Update parts of Coq realizations whose printing looks sane.

parent da025ed3
......@@ -15,7 +15,8 @@ Require Import BuiltIn.
Require BuiltIn.
(* Why3 goal *)
Lemma andb_def : forall (x:bool) (y:bool),
Lemma andb_def :
forall (x:bool) (y:bool),
((Init.Datatypes.andb x y) = match x with
| true => y
| false => false
......@@ -26,7 +27,8 @@ apply refl_equal.
Qed.
(* Why3 goal *)
Lemma orb_def : forall (x:bool) (y:bool),
Lemma orb_def :
forall (x:bool) (y:bool),
((Init.Datatypes.orb x y) = match x with
| false => y
| true => true
......@@ -37,7 +39,8 @@ apply refl_equal.
Qed.
(* Why3 goal *)
Lemma notb_def : forall (x:bool),
Lemma notb_def :
forall (x:bool),
((Init.Datatypes.negb x) = match x with
| false => true
| true => false
......@@ -48,7 +51,8 @@ apply refl_equal.
Qed.
(* Why3 goal *)
Lemma xorb_def : forall (x:bool) (y:bool),
Lemma xorb_def :
forall (x:bool) (y:bool),
((Init.Datatypes.xorb x y) = match x with
| false => y
| true => (Init.Datatypes.negb y)
......@@ -59,7 +63,8 @@ destruct x; destruct y; auto.
Qed.
(* Why3 goal *)
Lemma implb_def : forall (x:bool) (y:bool),
Lemma implb_def :
forall (x:bool) (y:bool),
((Init.Datatypes.implb x y) = match x with
| false => true
| true => y
......
This diff is collapsed.
......@@ -16,7 +16,7 @@ Require BuiltIn.
Require int.Int.
(* Why3 goal *)
Definition pow2: Z -> Z.
Definition pow2 : Z -> Z.
exact (two_p).
Defined.
......@@ -26,8 +26,8 @@ Lemma Power_0 : ((pow2 0%Z) = 1%Z).
Qed.
(* Why3 goal *)
Lemma Power_s : forall (n:Z), (0%Z <= n)%Z ->
((pow2 (n + 1%Z)%Z) = (2%Z * (pow2 n))%Z).
Lemma Power_s :
forall (n:Z), (0%Z <= n)%Z -> ((pow2 (n + 1%Z)%Z) = (2%Z * (pow2 n))%Z).
apply two_p_S.
Qed.
......@@ -37,7 +37,9 @@ Lemma Power_1 : ((pow2 1%Z) = 2%Z).
Qed.
(* Why3 goal *)
Lemma Power_sum : forall (n:Z) (m:Z), ((0%Z <= n)%Z /\ (0%Z <= m)%Z) ->
Lemma Power_sum :
forall (n:Z) (m:Z),
((0%Z <= n)%Z /\ (0%Z <= m)%Z) ->
((pow2 (n + m)%Z) = ((pow2 n) * (pow2 m))%Z).
unfold pow2.
intros n m [H1 H2].
......
......@@ -24,31 +24,31 @@ Require floating_point.DoubleFormat.
Require Import floating_point.GenFloat.
(* Why3 goal *)
Definition round: floating_point.Rounding.mode -> R -> R.
Definition round : floating_point.Rounding.mode -> R -> R.
exact (round 53 1024).
Defined.
(* Why3 goal *)
Definition value: floating_point.DoubleFormat.double -> R.
Definition value : floating_point.DoubleFormat.double -> R.
exact (value 53 1024).
Defined.
(* Why3 goal *)
Definition exact: floating_point.DoubleFormat.double -> R.
Definition exact : floating_point.DoubleFormat.double -> R.
exact (exact 53 1024).
Defined.
(* Why3 goal *)
Definition model: floating_point.DoubleFormat.double -> R.
Definition model : floating_point.DoubleFormat.double -> R.
exact (model 53 1024).
Defined.
(* Why3 assumption *)
Definition round_error (x:floating_point.DoubleFormat.double): R :=
Definition round_error (x:floating_point.DoubleFormat.double) : R :=
(Reals.Rbasic_fun.Rabs ((value x) - (exact x))%R).
(* Why3 assumption *)
Definition total_error (x:floating_point.DoubleFormat.double): R :=
Definition total_error (x:floating_point.DoubleFormat.double) : R :=
(Reals.Rbasic_fun.Rabs ((value x) - (model x))%R).
(* Why3 assumption *)
......@@ -57,15 +57,16 @@ Definition no_overflow (m:floating_point.Rounding.mode) (x:R): Prop :=
x)) <= (9007199254740991 * 19958403095347198116563727130368385660674512604354575415025472424372118918689640657849579654926357010893424468441924952439724379883935936607391717982848314203200056729510856765175377214443629871826533567445439239933308104551208703888888552684480441575071209068757560416423584952303440099278848)%R)%R.
(* Why3 goal *)
Lemma Bounded_real_no_overflow : forall (m:floating_point.Rounding.mode)
(x:R),
Lemma Bounded_real_no_overflow :
forall (m:floating_point.Rounding.mode) (x:R),
((Reals.Rbasic_fun.Rabs x) <= (9007199254740991 * 19958403095347198116563727130368385660674512604354575415025472424372118918689640657849579654926357010893424468441924952439724379883935936607391717982848314203200056729510856765175377214443629871826533567445439239933308104551208703888888552684480441575071209068757560416423584952303440099278848)%R)%R ->
(no_overflow m x).
exact (Bounded_real_no_overflow 53 1024 (refl_equal true) (refl_equal true)).
Qed.
(* Why3 goal *)
Lemma Round_monotonic : forall (m:floating_point.Rounding.mode) (x:R) (y:R),
Lemma Round_monotonic :
forall (m:floating_point.Rounding.mode) (x:R) (y:R),
(x <= y)%R -> ((round m x) <= (round m y))%R.
now apply Round_monotonic.
Qed.
......@@ -99,14 +100,14 @@ now apply Exact_rounding_for_integers.
Qed.
(* Why3 goal *)
Lemma Round_down_le : forall (x:R), ((round floating_point.Rounding.Down
x) <= x)%R.
Lemma Round_down_le :
forall (x:R), ((round floating_point.Rounding.Down x) <= x)%R.
now apply Round_down_le.
Qed.
(* Why3 goal *)
Lemma Round_up_ge : forall (x:R), (x <= (round floating_point.Rounding.Up
x))%R.
Lemma Round_up_ge :
forall (x:R), (x <= (round floating_point.Rounding.Up x))%R.
now apply Round_up_ge.
Qed.
......@@ -123,13 +124,14 @@ now apply Round_up_neg.
Qed.
(* Why3 goal *)
Definition round_logic: floating_point.Rounding.mode -> R ->
floating_point.DoubleFormat.double.
Definition round_logic :
floating_point.Rounding.mode -> R -> floating_point.DoubleFormat.double.
exact (round_logic 53 1024 (refl_equal true) (refl_equal true)).
Defined.
(* Why3 goal *)
Lemma Round_logic_def : forall (m:floating_point.Rounding.mode) (x:R),
Lemma Round_logic_def :
forall (m:floating_point.Rounding.mode) (x:R),
(no_overflow m x) -> ((value (round_logic m x)) = (round m x)).
Proof.
exact (Round_logic_def 53 1024 (refl_equal true) (refl_equal true)).
......
......@@ -24,37 +24,36 @@ Require floating_point.SingleFormat.
Require Import floating_point.GenFloat.
(* Why3 goal *)
Definition round: floating_point.Rounding.mode -> R -> R.
Definition round : floating_point.Rounding.mode -> R -> R.
exact (round 24 128).
Defined.
(* Why3 goal *)
Definition value: floating_point.SingleFormat.single -> R.
Definition value : floating_point.SingleFormat.single -> R.
exact (value 24 128).
Defined.
(* Why3 goal *)
Definition exact: floating_point.SingleFormat.single -> R.
Definition exact : floating_point.SingleFormat.single -> R.
exact (exact 24 128).
Defined.
(* Why3 goal *)
Definition model: floating_point.SingleFormat.single -> R.
Definition model : floating_point.SingleFormat.single -> R.
exact (model 24 128).
Defined.
(* Why3 assumption *)
Definition round_error (x:floating_point.SingleFormat.single): R :=
Definition round_error (x:floating_point.SingleFormat.single) : R :=
(Reals.Rbasic_fun.Rabs ((value x) - (exact x))%R).
(* Why3 assumption *)
Definition total_error (x:floating_point.SingleFormat.single): R :=
Definition total_error (x:floating_point.SingleFormat.single) : R :=
(Reals.Rbasic_fun.Rabs ((value x) - (model x))%R).
(* Why3 assumption *)
Definition no_overflow (m:floating_point.Rounding.mode) (x:R): Prop :=
((Reals.Rbasic_fun.Rabs (round m
x)) <= (33554430 * 10141204801825835211973625643008)%R)%R.
Definition no_overflow (m:floating_point.Rounding.mode) (x:R) : Prop :=
((Reals.Rbasic_fun.Rabs (round m x)) <= (33554430 * 10141204801825835211973625643008)%R)%R.
Lemma max_single_eq: (33554430 * 10141204801825835211973625643008 = max 24 128)%R.
unfold max, Fcore_defs.F2R; simpl.
......@@ -62,8 +61,8 @@ ring.
Qed.
(* Why3 goal *)
Lemma Bounded_real_no_overflow : forall (m:floating_point.Rounding.mode)
(x:R),
Lemma Bounded_real_no_overflow :
forall (m:floating_point.Rounding.mode) (x:R),
((Reals.Rbasic_fun.Rabs x) <= (33554430 * 10141204801825835211973625643008)%R)%R ->
(no_overflow m x).
intros m x Hx.
......@@ -73,7 +72,8 @@ exact (Bounded_real_no_overflow 24 128 (refl_equal true) (refl_equal true) m x H
Qed.
(* Why3 goal *)
Lemma Round_monotonic : forall (m:floating_point.Rounding.mode) (x:R) (y:R),
Lemma Round_monotonic :
forall (m:floating_point.Rounding.mode) (x:R) (y:R),
(x <= y)%R -> ((round m x) <= (round m y))%R.
apply Round_monotonic.
easy.
......@@ -93,7 +93,8 @@ now apply Round_value.
Qed.
(* Why3 goal *)
Lemma Bounded_value : forall (x:floating_point.SingleFormat.single),
Lemma Bounded_value :
forall (x:floating_point.SingleFormat.single),
((Reals.Rbasic_fun.Rabs (value x)) <= (33554430 * 10141204801825835211973625643008)%R)%R.
rewrite max_single_eq.
now apply Bounded_value.
......@@ -109,14 +110,14 @@ now apply Exact_rounding_for_integers.
Qed.
(* Why3 goal *)
Lemma Round_down_le : forall (x:R), ((round floating_point.Rounding.Down
x) <= x)%R.
Lemma Round_down_le :
forall (x:R), ((round floating_point.Rounding.Down x) <= x)%R.
now apply Round_down_le.
Qed.
(* Why3 goal *)
Lemma Round_up_ge : forall (x:R), (x <= (round floating_point.Rounding.Up
x))%R.
Lemma Round_up_ge :
forall (x:R), (x <= (round floating_point.Rounding.Up x))%R.
now apply Round_up_ge.
Qed.
......
......@@ -38,13 +38,13 @@ Proof.
Defined.
(* Why3 goal *)
Definition t'real: t -> R.
Definition t'real : t -> R.
Proof.
apply B2R.
Defined.
(* Why3 goal *)
Definition t'isFinite: t -> Prop.
Definition t'isFinite : t -> Prop.
Proof.
apply is_finite.
Defined.
......@@ -81,153 +81,153 @@ now apply bpow_le.
Qed.
(* Why3 goal *)
Definition zeroF: t.
Definition zeroF : t.
Proof.
apply zeroF.
Defined.
(* Why3 goal *)
Definition add: ieee_float.RoundingMode.mode -> t -> t -> t.
Definition add : ieee_float.RoundingMode.mode -> t -> t -> t.
Proof.
now apply add.
Defined.
(* Why3 goal *)
Definition sub: ieee_float.RoundingMode.mode -> t -> t -> t.
Definition sub : ieee_float.RoundingMode.mode -> t -> t -> t.
Proof.
now apply sub.
Defined.
(* Why3 goal *)
Definition mul: ieee_float.RoundingMode.mode -> t -> t -> t.
Definition mul : ieee_float.RoundingMode.mode -> t -> t -> t.
Proof.
now apply mul.
Defined.
(* Why3 goal *)
Definition div: ieee_float.RoundingMode.mode -> t -> t -> t.
Definition div : ieee_float.RoundingMode.mode -> t -> t -> t.
Proof.
now apply div.
Defined.
(* Why3 goal *)
Definition abs: t -> t.
Definition abs : t -> t.
Proof.
apply abs.
Defined.
(* Why3 goal *)
Definition neg: t -> t.
Definition neg : t -> t.
Proof.
apply neg.
Defined.
(* Why3 goal *)
Definition fma: ieee_float.RoundingMode.mode -> t -> t -> t -> t.
Definition fma : ieee_float.RoundingMode.mode -> t -> t -> t -> t.
Proof.
now apply fma.
Defined.
(* Why3 goal *)
Definition sqrt: ieee_float.RoundingMode.mode -> t -> t.
Definition sqrt : ieee_float.RoundingMode.mode -> t -> t.
Proof.
now apply GenericFloat.sqrt.
Defined.
(* Why3 goal *)
Definition roundToIntegral: ieee_float.RoundingMode.mode -> t -> t.
Definition roundToIntegral : ieee_float.RoundingMode.mode -> t -> t.
Proof.
now apply roundToIntegral.
Defined.
(* Why3 goal *)
Definition min: t -> t -> t.
Definition min : t -> t -> t.
Proof.
now apply min.
Defined.
(* Why3 goal *)
Definition max: t -> t -> t.
Definition max : t -> t -> t.
Proof.
now apply max.
Defined.
(* Why3 goal *)
Definition le: t -> t -> Prop.
Definition le : t -> t -> Prop.
Proof.
apply le.
Defined.
(* Why3 goal *)
Definition lt: t -> t -> Prop.
Definition lt : t -> t -> Prop.
Proof.
apply lt.
Defined.
(* Why3 goal *)
Definition eq: t -> t -> Prop.
Definition eq : t -> t -> Prop.
Proof.
apply eq.
Defined.
(* Why3 goal *)
Definition is_normal: t -> Prop.
Definition is_normal : t -> Prop.
Proof.
apply is_normal.
Defined.
(* Why3 goal *)
Definition is_subnormal: t -> Prop.
Definition is_subnormal : t -> Prop.
Proof.
apply is_subnormal.
Defined.
(* Why3 goal *)
Definition is_zero: t -> Prop.
Definition is_zero : t -> Prop.
Proof.
apply is_zero.
Defined.
(* Why3 goal *)
Definition is_infinite: t -> Prop.
Definition is_infinite : t -> Prop.
Proof.
apply is_infinite.
Defined.
(* Why3 goal *)
Definition is_nan: t -> Prop.
Definition is_nan : t -> Prop.
Proof.
apply is_nan.
Defined.
(* Why3 goal *)
Definition is_positive: t -> Prop.
Definition is_positive : t -> Prop.
Proof.
apply is_positive.
Defined.
(* Why3 goal *)
Definition is_negative: t -> Prop.
Definition is_negative : t -> Prop.
Proof.
apply is_negative.
Defined.
(* Why3 assumption *)
Definition is_plus_infinity (x:t): Prop := (is_infinite x) /\ (is_positive
x).
Definition is_plus_infinity (x:t) : Prop :=
(is_infinite x) /\ (is_positive x).
(* Why3 assumption *)
Definition is_minus_infinity (x:t): Prop := (is_infinite x) /\ (is_negative
x).
Definition is_minus_infinity (x:t) : Prop :=
(is_infinite x) /\ (is_negative x).
(* Why3 assumption *)
Definition is_plus_zero (x:t): Prop := (is_zero x) /\ (is_positive x).
Definition is_plus_zero (x:t) : Prop := (is_zero x) /\ (is_positive x).
(* Why3 assumption *)
Definition is_minus_zero (x:t): Prop := (is_zero x) /\ (is_negative x).
Definition is_minus_zero (x:t) : Prop := (is_zero x) /\ (is_negative x).
(* Why3 assumption *)
Definition is_not_nan (x:t): Prop := (t'isFinite x) \/ (is_infinite x).
Definition is_not_nan (x:t) : Prop := (t'isFinite x) \/ (is_infinite x).
(* Why3 goal *)
Lemma is_not_nan1 : forall (x:t), (is_not_nan x) <-> ~ (is_nan x).
......@@ -236,8 +236,8 @@ Proof.
Qed.
(* Why3 goal *)
Lemma is_not_finite : forall (x:t), (~ (t'isFinite x)) <-> ((is_infinite
x) \/ (is_nan x)).
Lemma is_not_finite :
forall (x:t), (~ (t'isFinite x)) <-> ((is_infinite x) \/ (is_nan x)).
Proof.
apply is_not_finite.
Qed.
......@@ -262,13 +262,13 @@ Proof.
Qed.
(* Why3 goal *)
Definition of_int: ieee_float.RoundingMode.mode -> Z -> t.
Definition of_int : ieee_float.RoundingMode.mode -> Z -> t.
Proof.
now apply z_to_fp.
Defined.
(* Why3 goal *)
Definition to_int: ieee_float.RoundingMode.mode -> t -> Z.
Definition to_int : ieee_float.RoundingMode.mode -> t -> Z.
Proof.
now apply fp_to_z.
Defined.
......@@ -281,7 +281,7 @@ Proof.
Qed.
(* Why3 goal *)
Definition round: ieee_float.RoundingMode.mode -> R -> R.
Definition round : ieee_float.RoundingMode.mode -> R -> R.
Proof.
apply (round 8 24).
Defined.
......@@ -296,7 +296,7 @@ Proof.
Qed.
(* Why3 goal *)
Definition max_int: Z.
Definition max_int : Z.
Proof.
exact (33554430 * 10141204801825835211973625643008)%Z.
Defined.
......@@ -309,7 +309,7 @@ Proof.
Qed.
(* Why3 assumption *)
Definition in_range (x:R): Prop :=
Definition in_range (x:R) : Prop :=
((-(33554430 * 10141204801825835211973625643008)%R)%R <= x)%R /\
(x <= (33554430 * 10141204801825835211973625643008)%R)%R.
......@@ -327,7 +327,7 @@ Proof.
Qed.
(* Why3 assumption *)
Definition no_overflow (m:ieee_float.RoundingMode.mode) (x:R): Prop :=
Definition no_overflow (m:ieee_float.RoundingMode.mode) (x:R) : Prop :=
(in_range (round m x)).
(* Why3 goal *)
......
......@@ -38,13 +38,13 @@ Proof.
Defined.
(* Why3 goal *)
Definition t'real: t -> R.
Definition t'real : t -> R.
Proof.
apply B2R.
Defined.
(* Why3 goal *)
Definition t'isFinite: t -> Prop.
Definition t'isFinite : t -> Prop.
Proof.
apply is_finite.
Defined.
......@@ -81,153 +81,153 @@ now apply bpow_le.
Qed.
(* Why3 goal *)
Definition zeroF: t.
Definition zeroF : t.
Proof.
apply zeroF.
Defined.
(* Why3 goal *)
Definition add: ieee_float.RoundingMode.mode -> t -> t -> t.
Definition add : ieee_float.RoundingMode.mode -> t -> t -> t.
Proof.
now apply add.
Defined.
(* Why3 goal *)
Definition sub: ieee_float.RoundingMode.mode -> t -> t -> t.
Definition sub : ieee_float.RoundingMode.mode -> t -> t -> t.
Proof.
now apply sub.
Defined.
(* Why3 goal *)
Definition mul: ieee_float.RoundingMode.mode -> t -> t -> t.
Definition mul : ieee_float.RoundingMode.mode -> t -> t -> t.
Proof.
now apply mul.
Defined.
(* Why3 goal *)
Definition div: ieee_float.RoundingMode.mode -> t -> t -> t.
Definition div : ieee_float.RoundingMode.mode -> t -> t -> t.
Proof.
now apply div.
Defined.
(* Why3 goal *)
Definition abs: t -> t.
Definition abs : t -> t.
Proof.
apply abs.
Defined.
(* Why3 goal *)
Definition neg: t -> t.
Definition neg : t -> t.
Proof.
apply neg.
Defined.
(* Why3 goal *)
Definition fma: ieee_float.RoundingMode.mode -> t -> t -> t -> t.
Definition fma : ieee_float.RoundingMode.mode -> t -> t -> t -> t.
Proof.
now apply fma.
Defined.
(* Why3 goal *)
Definition sqrt: ieee_float.RoundingMode.mode -> t -> t.
Definition sqrt : ieee_float.RoundingMode.mode -> t -> t.
Proof.
now apply GenericFloat.sqrt.
Defined.
(* Why3 goal *)
Definition roundToIntegral: ieee_float.RoundingMode.mode -> t -> t.
Definition roundToIntegral : ieee_float.RoundingMode.mode -> t -> t.
Proof.
now apply roundToIntegral.
Defined.
(* Why3 goal *)
Definition min: t -> t -> t.
Definition min : t -> t -> t.
Proof.
now apply min.
Defined.
(* Why3 goal *)
Definition max: t -> t -> t.
Definition max : t -> t -> t.
Proof.
now apply max.
Defined.
(* Why3 goal *)
Definition le: t -> t -> Prop.
Definition le : t -> t -> Prop.
Proof.
apply le.
Defined.
(* Why3 goal *)
Definition lt: t -> t -> Prop.
Definition lt : t -> t -> Prop.
Proof.
apply lt.
Defined.
(* Why3 goal *)
Definition eq: t -> t -> Prop.
Definition eq : t -> t -> Prop.
Proof.
apply eq.
Defined.
(* Why3 goal *)
Definition is_normal: t -> Prop.
Definition is_normal : t -> Prop.
Proof.
apply is_normal.
Defined.
(* Why3 goal *)
Definition is_subnormal: t -> Prop.
Definition is_subnormal : t -> Prop.
Proof.
apply is_subnormal.
Defined.
(* Why3 goal *)
Definition is_zero: t -> Prop.
Definition is_zero : t -> Prop.
Proof.
apply is_zero.
Defined.
(* Why3 goal *)
Definition is_infinite: t -> Prop.
Definition is_infinite : t -> Prop.
Proof.
apply is_infinite.
Defined.
(* Why3 goal *)
Definition is_nan: t -> Prop.
Definition is_nan : t -> Prop.
Proof.
apply is_nan.
Defined.
(* Why3 goal *)
Definition is_positive: t -> Prop.
Definition is_positive : t -> Prop.
Proof.
apply is_positive.
Defined.
(* Why3 goal *)
Definition is_negative: t -> Prop.
Definition is_negative : t -> Prop.
Proof.
apply is_negative.
Defined.
(* Why3 assumption *)
Definition is_plus_infinity (x:t): Prop := (is_infinite x) /\ (is_positive