Merge pull request #16 from VeriNum/gentype

Generalized types (not limited to IEEE Binary)

FPBench/Makefile

@@ -9,7 +9,7 @@ _CoqProject: Makefile
 	echo $(COQFLAGS) >_CoqProject
 
 target: doppler1.vo doppler2.vo doppler3.vo predatorprey.vo verhulst.vo carbongas.vo t_div_t1.vo\
-     kepler0.vo kepler1.vo kepler2.vo rigid_body1.v rigid_body2.v turbine1.vo turbine2.vo\
+     kepler0.vo kepler1.vo kepler2.vo rigid_body1.vo rigid_body2.vo turbine1.vo turbine2.vo\
      turbine3.vo himmilbeau.vo jetengine.vo
 
 %.vo: %.v 

FPBench/carbongas.v

@@ -49,7 +49,7 @@ try match goal with |-Rabs ?a <= _ =>
   (i_taylor vxH, i_bisect vxH, i_depth 15) as H' ; apply H');
   try (interval_intro (Rabs a) upper as H' ; apply H') end;
   apply Rle_refl)).
-Qed.
+Time Qed.
 
 Lemma check_carbongas_bound: ltac:(CheckBound carbongas_b 2.5e-08%F64).
 Proof. reflexivity. Qed.

FPBench/doppler1.v

@@ -6,8 +6,14 @@ Section WITHNANS.
 Context {NANS:Nans}.
 Open Scope R_scope.
 
+Definition _u : ident := 1%positive.
+Definition _v : ident := 2%positive.
+Definition _t : ident := 3%positive.
 
-Definition doppler1_bmap_list := [Build_varinfo Tdouble 1%positive (-100) (100);Build_varinfo Tdouble 2%positive (20) (2e4);Build_varinfo Tdouble 3%positive (-30) (50)].
+Definition doppler1_bmap_list := [
+     Build_varinfo Tdouble _u (-100) (100);
+     Build_varinfo Tdouble _v (20) (2e4);
+     Build_varinfo Tdouble _t (-30) (50)].
 
 Definition doppler1_bmap :=
  ltac:(let z := compute_PTree (boundsmap_of_list doppler1_bmap_list) in exact z).
@@ -17,7 +23,7 @@ Definition doppler1 (u : ftype Tdouble) (v : ftype Tdouble) (t : ftype Tdouble)
   (((-t1) * v)%F64 / ((t1 + u)%F64 * (t1 + u)%F64)%F64)%F64.
 
 Definition doppler1_expr := 
- ltac:(let e' :=  HO_reify_float_expr constr:([1%positive;2%positive;3%positive]) doppler1 in exact e').
+ ltac:(let e' :=  HO_reify_float_expr constr:([_u;_v;_t]) doppler1 in exact e').
 
 Derive doppler1_b 
 SuchThat (forall vmap, prove_roundoff_bound doppler1_bmap vmap doppler1_expr doppler1_b)
@@ -38,14 +44,14 @@ try match goal with |- (Rabs ?e <= ?a - ?b)%R =>
                       eapply Rle_trans;
                       [apply G | apply Rminus_plus_le_minus; apply Rle_refl] end)));
 try match goal with |- Rabs ?a <= _ =>
-interval_intro (Rabs a) with (i_bisect v, 
+interval_intro (Rabs a) with (i_bisect v_v, 
  i_depth 17) as H'; apply H'; apply Rle_refl
 end;
 try match goal with |- Rabs ?a <= _ =>
-interval_intro (Rabs a) with (i_bisect vxH, 
-i_bisect v0, i_depth 17) as H'; apply H'; apply Rle_refl
+interval_intro (Rabs a) with (i_bisect v_u, 
+i_bisect v_t, i_depth 17) as H'; apply H'; apply Rle_refl
 end).
-Qed.
+Time Qed.
 
 Lemma check_doppler1_bound: ltac:(CheckBound doppler1_b 4.5e-13%F64).
 Proof. reflexivity. Qed.

FPBench/doppler2.v

@@ -6,7 +6,14 @@ Section WITHNANS.
 Context {NANS:Nans}.
 Open Scope R_scope.
 
-Definition doppler2_bmap_list := [Build_varinfo Tdouble 1%positive (-125) (125);Build_varinfo Tdouble 2%positive (15) (25000);Build_varinfo Tdouble 3%positive (-40) (60)].
+Definition _u : ident := 1%positive.
+Definition _v : ident := 2%positive.
+Definition _t : ident := 3%positive.
+
+Definition doppler2_bmap_list := [
+   Build_varinfo Tdouble _u (-125) (125);
+   Build_varinfo Tdouble _v (15) (25000);
+   Build_varinfo Tdouble _t (-40) (60)].
 
 Definition doppler2_bmap :=
  ltac:(let z := compute_PTree (boundsmap_of_list doppler2_bmap_list) in exact z).
@@ -16,7 +23,7 @@ Definition doppler2 (u : ftype Tdouble) (v : ftype Tdouble) (t : ftype Tdouble)
   (((-t1) * v)%F64 / ((t1 + u)%F64 * (t1 + u)%F64)%F64)%F64).
 
 Definition doppler2_expr := 
- ltac:(let e' :=  HO_reify_float_expr constr:([1%positive;2%positive;3%positive]) doppler2 in exact e').
+ ltac:(let e' :=  HO_reify_float_expr constr:([_u;_v;_t]) doppler2 in exact e').
 
 Derive doppler2_b 
 SuchThat (forall vmap, prove_roundoff_bound doppler2_bmap vmap doppler2_expr doppler2_b)
@@ -37,14 +44,14 @@ try match goal with |- (Rabs ?e <= ?a - ?b)%R =>
                       eapply Rle_trans;
                       [apply G | apply Rminus_plus_le_minus; apply Rle_refl] end)));
 try match goal with |- Rabs ?a <= _ =>
-interval_intro (Rabs a) with (i_bisect v, 
+interval_intro (Rabs a) with (i_bisect v_v, 
  i_depth 17) as H'; apply H'; apply Rle_refl
 end;
 try match goal with |- Rabs ?a <= _ =>
-interval_intro (Rabs a) with (i_bisect vxH, 
-i_bisect v0, i_depth 17) as H'; apply H'; apply Rle_refl
+interval_intro (Rabs a) with (i_bisect v_u, 
+i_bisect v_t, i_depth 17) as H'; apply H'; apply Rle_refl
 end).
-Qed.
+Time Qed.
 
 Lemma check_doppler2_bound: ltac:(CheckBound doppler2_b 1.2e-12%F64).
 Proof. reflexivity. Qed.

FPBench/doppler3.v

@@ -1,12 +1,17 @@
 Require Import vcfloat.VCFloat.
 Require Import Interval.Tactic.
-Import Binary List ListNotations.
+Import Binary Coq.Lists.List ListNotations.
 Set Bullet Behavior "Strict Subproofs".
 Section WITHNANS.
 Context {NANS:Nans}.
 Open Scope R_scope.
 
-Definition doppler3_bmap_list := [Build_varinfo Tdouble 1%positive (-30) (120);Build_varinfo Tdouble 2%positive (320) (20300);Build_varinfo Tdouble 3%positive (-50) (30)].
+
+Definition _u : ident := 1%positive.
+Definition _v : ident := 2%positive.
+Definition _t : ident := 3%positive.
+
+Definition doppler3_bmap_list := [Build_varinfo Tdouble _u (-30) (120);Build_varinfo Tdouble _v (320) (20300);Build_varinfo Tdouble _t (-50) (30)].
 
 Definition doppler3_bmap :=
  ltac:(let z := compute_PTree (boundsmap_of_list doppler3_bmap_list) in exact z).
@@ -16,7 +21,7 @@ Definition doppler3 (u : ftype Tdouble) (v : ftype Tdouble) (t : ftype Tdouble)
   (((-t1) * v)%F64 / ((t1 + u)%F64 * (t1 + u)%F64)%F64)%F64).
 
 Definition doppler3_expr := 
- ltac:(let e' :=  HO_reify_float_expr constr:([1%positive;2%positive;3%positive]) doppler3 in exact e').
+ ltac:(let e' :=  HO_reify_float_expr constr:([_u;_v;_t]) doppler3 in exact e').
 
 Derive doppler3_b 
 SuchThat (forall vmap, prove_roundoff_bound doppler3_bmap vmap doppler3_expr doppler3_b)
@@ -37,14 +42,14 @@ try match goal with |- (Rabs ?e <= ?a - ?b)%R =>
                       eapply Rle_trans;
                       [apply G | apply Rminus_plus_le_minus; apply Rle_refl] end)));
 try match goal with |- Rabs ?a <= _ =>
-interval_intro (Rabs a) with (i_bisect v, 
+interval_intro (Rabs a) with (i_bisect v_v, 
  i_depth 14) as H'; apply H'; apply Rle_refl
 end;
 try match goal with |- Rabs ?a <= _ =>
-interval_intro (Rabs a) with (i_bisect vxH, 
-i_bisect v0, i_depth 14) as H'; apply H'; apply Rle_refl
+interval_intro (Rabs a) with (i_bisect v_t, 
+i_bisect v_u, i_depth 14) as H'; apply H'; apply Rle_refl
 end).
-Qed.
+Time Qed.
 
 Lemma check_doppler3_bound: ltac:(CheckBound doppler3_b 2.0e-13%F64).
 Proof. reflexivity. Qed.

FPBench/himmilbeau.v

@@ -28,7 +28,7 @@ time "himmilbeau" (
 try (subst himmilbeau_b; intro; prove_roundoff_bound);
 try (prove_rndval; interval);
 try (prove_roundoff_bound2; prune_terms (cutoff 30); do_interval)).
-Qed.
+Time Qed.
 
 Lemma check_himmilbeau_bound: ltac:(CheckBound himmilbeau_b 2.31e-12%F64).
 Proof. reflexivity. Qed.

FPBench/jetengine.v

@@ -6,7 +6,11 @@ Section WITHNANS.
 Context {NANS:Nans}.
 Open Scope R_scope.
 
-Definition jetengine_bmap_list := [Build_varinfo Tdouble 1%positive (-5) (5);Build_varinfo Tdouble 2%positive (-20) (5)].
+Definition _x1: ident := 1%positive.
+Definition _x2: ident := 2%positive.
+
+Definition jetengine_bmap_list := [Build_varinfo Tdouble _x1 (-5) (5);
+    Build_varinfo Tdouble _x2 (-20) (5)].
 
 Definition jetengine_bmap :=
  ltac:(let z := compute_PTree (boundsmap_of_list jetengine_bmap_list) in exact z).
@@ -20,7 +24,7 @@ Definition jetengine (x1 : ftype Tdouble) (x2 : ftype Tdouble) :=
   (x1 + ((((((((((2)%F64 * x1)%F64 * s)%F64 * (s - (3)%F64)%F64)%F64 + ((x1 * x1)%F64 * (((4)%F64 * s)%F64 - (6)%F64)%F64)%F64)%F64 * d)%F64 + ((((3)%F64 * x1)%F64 * x1)%F64 * s)%F64)%F64 + ((x1 * x1)%F64 * x1)%F64)%F64 + x1)%F64 + ((3)%F64 * s_42_)%F64)%F64)%F64).
 
 Definition jetengine_expr := 
- ltac:(let e' :=  HO_reify_float_expr constr:([1%positive;2%positive]) jetengine in exact e').
+ ltac:(let e' :=  HO_reify_float_expr constr:([_x1;_x2]) jetengine in exact e').
 
 Derive jetengine_b 
 SuchThat (forall vmap, prove_roundoff_bound jetengine_bmap vmap jetengine_expr jetengine_b)
@@ -32,15 +36,17 @@ try (subst jetengine_b; intro; prove_roundoff_bound);
 try (prove_rndval; interval);
 try (prove_roundoff_bound2);
 try match goal with |- Rabs ?a <= _ =>
-interval_intro (Rabs a) with (i_bisect vxH, i_bisect v, i_depth 17) as H
+interval_intro (Rabs a) with (i_bisect v_x1, i_bisect v_x2, i_depth 12) as H
 end;
+(*match type of H with _ <= _ <= ?A => pose (b := ltac:(ShowBound A)) end.
+ unify (Binary.Bcompare _ _ b 2.13e3%F64) (Some Lt).*)
 try (
 eapply Rle_trans;
 try apply H;
 try apply Rle_refl)).
-Qed.
+Time Qed.
 
-Lemma check_jetengine_bound: ltac:(CheckBound jetengine_b 1.4e02%F64).
+Lemma check_jetengine_bound: ltac:(CheckBound jetengine_b 2.13e3%F64).
 Proof. reflexivity. Qed.
 
 End WITHNANS.

FPBench/kepler0.v

@@ -24,12 +24,11 @@ Proof.
 idtac "Starting kepler0".
 time "kepler0" (
 try (subst kepler0_b; intro; prove_roundoff_bound);
-try (prove_rndval; interval));
-try (prove_roundoff_bound2; error_rewrites;
-try (field_simplify_Rabs);
+try (prove_rndval; interval);
+try (prove_roundoff_bound2; 
 try ((prune_terms (cutoff 30));
- do_interval)).
-Qed.
+ do_interval))).
+Time Qed.
 
 Lemma check_kepler0_bound: ltac:(CheckBound kepler0_b 2.2005e-13%F64).
 Proof. reflexivity. Qed.

FPBench/kepler1.v

@@ -6,7 +6,15 @@ Section WITHNANS.
 Context {NANS:Nans}.
 Open Scope R_scope.
 
-Definition kepler1_bmap_list := [Build_varinfo Tdouble 1%positive (4) (636e-2);Build_varinfo Tdouble 2%positive (4) (636e-2);Build_varinfo Tdouble 3%positive (4) (636e-2);Build_varinfo Tdouble 4%positive (4) (636e-2)].
+Definition _x1: ident := 1%positive.
+Definition _x2: ident := 2%positive.
+Definition _x3: ident := 3%positive.
+Definition _x4: ident := 4%positive.
+
+Definition kepler1_bmap_list := [Build_varinfo Tdouble _x1 (4) (636e-2);
+   Build_varinfo Tdouble _x2 (4) (636e-2);
+   Build_varinfo Tdouble _x3 (4) (636e-2);
+   Build_varinfo Tdouble _x4 (4) (636e-2)].
 
 Definition kepler1_bmap :=
  ltac:(let z := compute_PTree (boundsmap_of_list kepler1_bmap_list) in exact z).
@@ -15,23 +23,20 @@ Definition kepler1 (x1 : ftype Tdouble) (x2 : ftype Tdouble) (x3 : ftype Tdouble
   cast Tdouble (((((((((x1 * x4)%F64 * ((((-x1) + x2)%F64 + x3)%F64 - x4)%F64)%F64 + (x2 * (((x1 - x2)%F64 + x3)%F64 + x4)%F64)%F64)%F64 + (x3 * (((x1 + x2)%F64 - x3)%F64 + x4)%F64)%F64)%F64 - ((x2 * x3)%F64 * x4)%F64)%F64 - (x1 * x3)%F64)%F64 - (x1 * x2)%F64)%F64 - x4)%F64).
 
 Definition kepler1_expr := 
- ltac:(let e' :=  HO_reify_float_expr constr:([1%positive;2%positive;3%positive;4%positive]) kepler1 in exact e').
+ ltac:(let e' :=  HO_reify_float_expr constr:([_x1;_x2;_x3;_x4]) kepler1 in exact e').
 
 Derive kepler1_b 
 SuchThat (forall vmap, prove_roundoff_bound kepler1_bmap vmap kepler1_expr kepler1_b)
 As kepler1_bound.
 Proof.
-idtac "Starting kepler1".
-time "kepler1" (
-try (subst kepler1_b; intro; prove_roundoff_bound);
-try (prove_rndval; interval));
-try (prove_roundoff_bound2; error_rewrites;
-try (field_simplify_Rabs);
-try ((prune_terms (cutoff 30));
- do_interval)).
-Qed.
-
-Lemma check_kepler1_bound: ltac:(CheckBound kepler1_b 1.6e-12%F64).
+idtac "Starting kepler1";
+time "kepler1"
+ (subst kepler1_b; intro; prove_roundoff_bound;
+  [ prove_rndval; interval
+  | prove_roundoff_bound2; prune_terms (cutoff 50); do_interval]).
+Time Qed.
+
+Lemma check_kepler1_bound: ltac:(CheckBound kepler1_b 1.644e-12%F64).
 Proof. reflexivity. Qed.
 
 End WITHNANS.

FPBench/kepler2.v

@@ -24,12 +24,11 @@ Proof.
 idtac "Starting kepler2".
 time "kepler2" (
 try (subst kepler2_b; intro; prove_roundoff_bound);
-try (prove_rndval; interval));
-try (prove_roundoff_bound2; error_rewrites;
-try (field_simplify_Rabs);
+try (prove_rndval; interval);
+try (prove_roundoff_bound2;
 try ((prune_terms (cutoff 60));
- do_interval)).
-Qed.
+ do_interval))).
+Time Qed.
 
 Lemma check_kepler2_bound: ltac:(CheckBound kepler2_b 6.2e-12%F64).
 Proof. reflexivity. Qed.

FPBench/multivar_6.v

@@ -29,7 +29,7 @@ time "prove_rndval" prove_rndval; time "interval" interval.
 time "prove_roundoff_bound2" prove_roundoff_bound2;
 time "prune_terms" (prune_terms (cutoff 30)).
 time "do_interval" do_interval.
-Qed.
+Time Qed.
 
 Lemma check_delta4_bound: ltac:(CheckBound delta4_b 2.51e-13%F64).
 Proof. reflexivity. Qed.
@@ -57,7 +57,7 @@ time "prove_rndval" prove_rndval; time "interval" interval.
 time "prove_roundoff_bound2" prove_roundoff_bound2;
 time "prune_terms" (prune_terms (cutoff 30)).
 time "do_interval" do_interval.
-Qed.
+Time Qed.
 
 Lemma check_delta_bound: ltac:(CheckBound delta_b 6.2e-12%F64).
 Proof. reflexivity. Qed.

FPBench/predatorprey.v

@@ -49,7 +49,7 @@ try match goal with |-Rabs ?a <= _ =>
 interval_intro (Rabs a) upper with 
 (i_bisect vxH, i_depth 17) as H'
 end; apply H')).
-Qed.
+Time Qed.
 
 Lemma check_predatorprey_bound: ltac:(CheckBound predatorprey_b 3.1e-16%F64).
 Proof. reflexivity. Qed.

FPBench/rigid_body1.v

@@ -26,7 +26,7 @@ time "rigidbody1" (
 try (subst rigidbody1_b; intro; prove_roundoff_bound);
 try (prove_rndval; interval);
 try (prove_roundoff_bound2; prune_terms (cutoff 30); do_interval)).
-Qed.
+Time Qed.
 
 Lemma check_rigidbody1_bound: ltac:(CheckBound rigidbody1_b 3.1e-13%F64).
 Proof. reflexivity. Qed.

FPBench/rigid_body2.v

@@ -6,35 +6,6 @@ Section WITHNANS.
 Context {NANS:Nans}.
 Open Scope R_scope.
 
-<<<<<<< HEAD:FPBench/rigid_body.v
-Definition rigidbody1_bmap_list := [Build_varinfo Tdouble 1%positive (-15) (15);Build_varinfo Tdouble 2%positive (-15) (15);Build_varinfo Tdouble 3%positive (-15) (15)].
-
-Definition rigidbody1_bmap :=
- ltac:(let z := compute_PTree (boundsmap_of_list rigidbody1_bmap_list) in exact z).
-
-Definition rigidbody1 (x1 : ftype Tdouble) (x2 : ftype Tdouble) (x3 : ftype Tdouble) := 
-  cast Tdouble (((((-(x1 * x2)%F64) - (((2)%F64 * x2)%F64 * x3)%F64)%F64 - x1)%F64 - x3)%F64).
-
-Definition rigidbody1_expr := 
- ltac:(let e' :=  HO_reify_float_expr constr:([1%positive;2%positive;3%positive]) rigidbody1 in exact e').
-
-
-Derive rigidbody1_b 
-SuchThat (forall vmap, prove_roundoff_bound rigidbody1_bmap vmap rigidbody1_expr rigidbody1_b)
-As rigidbody1_bound.
-Proof.
-idtac "Starting rigidbody1".
-time "rigidbody1" (
-try (subst rigidbody1_b; intro; prove_roundoff_bound);
-try (prove_rndval; interval);
-try (prove_roundoff_bound2; prune_terms (cutoff 30); do_interval)).
-Qed.
-
-Lemma check_rigidbody1_bound: ltac:(CheckBound rigidbody1_b 3.1e-13%F64).
-Proof. reflexivity. Qed.
-
-=======
->>>>>>> b35234fce9cbf03ede4c0bfc4b61d33d055eb550:FPBench/rigid_body2.v
 Definition rigidbody2_bmap_list := [Build_varinfo Tdouble 1%positive (-15) (15);Build_varinfo Tdouble 2%positive (-15) (15);Build_varinfo Tdouble 3%positive (-15) (15)].
 
 Definition rigidbody2_bmap :=
@@ -55,7 +26,7 @@ time "rigidbody2" (
 try (subst rigidbody2_b; intro; prove_roundoff_bound);
 try (prove_rndval; interval);
 try (prove_roundoff_bound2; prune_terms (cutoff 30); do_interval)).
-Qed.
+Time Qed.
 
 Lemma check_rigidbody2_bound: ltac:(CheckBound rigidbody2_b 3.9e-11%F64).
 Proof. reflexivity. Qed.

FPBench/t_div_t1.v

@@ -36,7 +36,7 @@ try (
 eapply Rle_trans;
 try apply H;
 try apply Rle_refl)).
-Qed.
+Time Qed.
 
 Lemma check_t_div_t1_bound: ltac:(CheckBound t_div_t1_b 4.4e-16%F64).
 Proof. reflexivity. Qed.