Constants and Parameters are shown again

coq/ErrorValidation.v

 Require Import Coq.QArith.QArith Coq.QArith.Qminmax Coq.QArith.Qabs Coq.QArith.Qreals.
 (*Coq.QArith.Qcanon.*)
-Require Import Coq.micromega.Psatz Coq.Reals.Reals .
-Require Import Daisy.Infra.Abbrevs Daisy.Infra.RationalSimps Daisy.Infra.RealRationalProps.
-Require Import Daisy.Expressions Daisy.Infra.RationalConstruction Daisy.Infra.RealSimps Daisy.IntervalArith Daisy.ErrorBounds.
+Require Import Coq.micromega.Psatz Coq.Reals.Reals Interval.Interval_tactic.
+Require Import Daisy.Infra.Abbrevs Daisy.Infra.RationalSimps Daisy.Infra.RealRationalProps  Daisy.Infra.RationalConstruction Daisy.Infra.RealSimps.
+Require Import Daisy.Infra.ExpressionAbbrevs Daisy.IntervalArith Daisy.ErrorBounds Daisy.IntervalValidation.
 
 Section ComputableErrors.
 
@@ -36,8 +36,9 @@ Section ComputableErrors.
             end
               in andb rec theVal
       end.
-
+  (*
   Functional Scheme validErrorbound_ind := Induction for validErrorbound Sort Prop.
+   *)
 
   Definition u:nat := 1.
   (** 1655/5 = 331; 0,4 = 2/5 **)
@@ -85,14 +86,15 @@ Section ComputableErrors.
       (Q2R ivlo <= cenv v <= Q2R ivhi)%R.
 
   Lemma validErrorboundCorrectConstant:
-    forall cenv absenv (n:Q) nR nF e nlo nhi,
+    forall cenv absenv (n:Q) nR nF e nlo nhi (P:precond),
       eval_exp 0%R cenv (Const (Q2R n)) nR ->
       eval_exp (Q2R machineEpsilon) cenv (Const (Q2R n)) nF ->
       validErrorbound (Const n) absenv = true ->
+      validIntervalbounds (Const n) absenv P = true ->
       absenv (Const n) = ((nlo,nhi),e) ->
       (Rabs (nR - nF) <= (Q2R e))%R.
   Proof.
-    intros cenv absenv n nR nF e nlo nhi eval_real eval_float error_valid absenv_const.
+    intros cenv absenv n nR nF e nlo nhi P eval_real eval_float error_valid intv_valid absenv_const.
     unfold validErrorbound in error_valid.
     rewrite absenv_const in error_valid.
     inversion eval_real; subst.
@@ -113,10 +115,21 @@ Section ComputableErrors.
     rewrite Q2R_mult in error_valid.
     eapply Rle_trans.
     eapply Rmult_le_compat_r.
-    (*
-    apply error_valid.
-  Qed. *)
-  Admitted.
+    rewrite <- Q2R0_is_0.
+    apply Qle_Rle.
+    unfold machineEpsilon.
+    assert (Qle_bool 0 (1 # (2^53)) = true) by (unfold Qle_bool; auto).
+    rewrite <- Qle_bool_iff; auto.
+    rewrite absenv_const in intv_valid.
+    simpl in intv_valid.
+    apply Is_true_eq_left in intv_valid.
+    apply andb_prop_elim in intv_valid.
+    destruct intv_valid as [valid_lo valid_hi]; unfold Is_true in *.
+    Focus 2. apply error_valid.
+    rewrite <- Rabs_eq_Qabs.
+    rewrite <- maxAbs_impl_RmaxAbs.
+    apply RmaxAbs; simpl; apply Qle_Rle; rewrite <- Qle_bool_iff; unfold Qleb in *; [ destruct (Qle_bool nlo n); auto | destruct (Qle_bool n nhi); auto].
+  Qed.
 
   Lemma validErrorboundCorrectParam:
     forall cenv absenv (v:nat) nR nF e P plo phi,
@@ -125,10 +138,11 @@ Section ComputableErrors.
       eval_exp 0%R cenv (Param R v) nR ->
       eval_exp (Q2R machineEpsilon) cenv (Param R v) nF ->
       validErrorbound (Param Q v) absenv = true ->
+      validIntervalbounds (Param Q v) absenv P = true ->
       absenv (Param Q v)  = ((plo,phi),e) ->
       (Rabs (nR - nF) <= (Q2R e))%R.
   Proof.
-    intros cenv absenv v nR nF e P plo phi absenv_approx_p cenv_approx_p eval_real eval_float error_valid absenv_param.
+    intros cenv absenv v nR nF e P plo phi absenv_approx_p cenv_approx_p eval_real eval_float error_valid intv_valid absenv_param.
     unfold validErrorbound in error_valid.
     rewrite absenv_param in error_valid.
     inversion eval_real; subst.

coq/IntervalValidation.v

 Require Import Coq.QArith.QArith Coq.QArith.Qreals.
-Require Import Daisy.Expressions Daisy.Infra.Abbrevs Daisy.Infra.RationalSimps Daisy.IntervalArithQ Daisy.Infra.RationalConstruction Daisy.Infra.RealRationalProps Daisy.IntervalArith.
+Require Import Daisy.Infra.Abbrevs Daisy.Infra.RationalSimps Daisy.Infra.RationalConstruction Daisy.Infra.RealRationalProps.
+Require Import Daisy.Expressions Daisy.IntervalArithQ.
 
 Fixpoint validIntervalbounds (e:exp Q) (absenv:analysisResult) (P:precond):=
   let (intv, _) := absenv e in
     match e with
     | Var v =>
       let bounds_v := P v in
-      andb (Qeqb (fst intv) (fst (bounds_v))) (Qeqb (snd intv) (snd (bounds_v)))
+      andb (Qeq_bool (fst intv) (fst (bounds_v))) (Qeq_bool (snd bounds_v) (snd (intv)))
     | Param v =>
       let bounds_v := P v in
-      andb (Qeq_bool (fst intv) (fst (bounds_v))) (Qeq_bool (snd intv) (snd (bounds_v)))
+      andb (Qeq_bool (fst intv) (fst (bounds_v))) (Qeq_bool (snd bounds_v) (snd (intv)))
     | Const n =>
-      andb (Qleb (fst intv) n) (Qleb (snd intv) n)
+      andb (Qleb (fst intv) n) (Qleb n (snd intv))
     | Binop b e1 e2 =>
       let rec := andb (validIntervalbounds e1 absenv P) (validIntervalbounds e2 absenv P) in
       let (iv1,_) := absenv e1 in
@@ -33,6 +34,7 @@ Fixpoint validIntervalbounds (e:exp Q) (absenv:analysisResult) (P:precond):=
       andb rec opres
     end.
 
+(*
 Lemma validIntervalbounds_correct (e:exp Q):
   forall (absenv:analysisResult) (P:precond) cenv vR,
   validIntervalbounds e absenv P = true ->
@@ -79,6 +81,7 @@ Proof.
       destruct valid_bounds.
       unfold Is_true in *; simpl in *. contradiction.
 Admitted.
+ *)
 
 Definition u:nat := 1.
 (** 1655/5 = 331; 0,4 = 2/5 **)