Make a little cleanup

coq/ErrorValidation.v

-Require Import Coq.QArith.QArith Coq.QArith.Qminmax Coq.QArith.Qabs Coq.ZArith.ZArith Coq.Reals.Reals Coq.QArith.Qreals.
+Require Import Coq.QArith.QArith Coq.QArith.Qminmax Coq.QArith.Qabs Coq.QArith.Qreals.
 (*Coq.QArith.Qcanon.*)
-Require Import Coq.micromega.Psatz.
-Require Import Daisy.Expressions Daisy.Infra.RationalConstruction Daisy.Infra.RealSimps Daisy.IntervalArith Daisy.ErrorBounds Daisy.Infra.Abbrevs.
+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.
 
 Section ComputableErrors.
 
-  Definition interval :Type := Q * Q.
-  Definition error :Type := Q.
-  Definition analysisResult :Type := exp Q -> interval * error.
-
-  (*
-  Definition Qc2Q (q:Qc) :Q := match q with
-                                 Qcmake a P => a end.
-
-  Lemma double_inject_eq:
-    forall q, Qc2Q (Q2Qc q) = Qred q.
-  Proof.
-    intros q. unfold Q2Qc.
-    unfold Qc2Q; auto.
-  Qed. *)
-
-  Definition Qleb :=Qle_bool.
-
-  (*
-  Definition Qcmax (a:Qc) (b:Qc) := Q2Qc (Qmax a b).
-  Definition Qcabs (a:Qc) := Q2Qc (Qabs a). *)
-
-  Definition maxAbs (iv:interval) :=
-    Qmax (Qabs (fst iv)) (Qabs (snd iv)).
-
-  Definition RmaxAbsFun (iv:interval) :=
-    Rmax (Rabs (Q2R (fst iv))) (Rabs (Q2R (snd iv))).
-
-  Lemma maxAbs_pointInterval a:
-    maxAbs (a,a) == Qabs a.
-  Proof.
-    unfold maxAbs; simpl.
-(*    unfold Qcmax.
-    unfold Qcabs.
-    apply Qc_is_canon.
-    apply Qabs_case; intros.
-    - pose proof (Q.max_id (Qred a)).
-      unfold Q2Qc; simpl.
-      rewrite H0.
-      rewrite Qred_involutive; apply Qeq_refl.
-    - pose proof (Q.max_id (Qred (-a))).
-      unfold Q2Qc; simpl.
-      rewrite H0.
-      rewrite Qred_involutive.
-      apply Qeq_refl.
-  Qed. *)
-    apply Qabs_case; intros; eapply Q.max_id.
-  Qed.
-
-  (*
-  Lemma abs_QR (n:Qc):
-    Rabs (Q2R n) = Q2R (Qcabs n).
-  Proof.
-    unfold Rabs.
-    unfold Qcabs.
-    apply Qabs_case; intros.
-    - destruct Rcase_abs.
-      + apply Qle_Rle in H.
-        unfold Q2R at 1 in H.
-    unfold Qabs.
-    simpl.
-    *)
-
   Definition machineEpsilon := (1#(2^53)).
 
+  Fixpoint toRExp (e:exp Q) :=
+    match e with
+    |Var v => Var R v
+    |Param v => Param R v
+    |Const n => Const (Q2R n)
+    |Binop b e1 e2 => Binop b (toRExp e1) (toRExp e2)
+    end.
+
   Fixpoint validErrorbound (e:exp Q) (env:analysisResult) :=
     let (intv, err) := (env e) in
       match e with
         |Var v => false
         |Param v => Qleb (maxAbs intv * machineEpsilon) err
-        (* A constant will be a point interval. Take maxAbs never the less *)
+        (* A constant will be a point intv. Take maxAbs never the less *)
         |Const n => Qleb (maxAbs intv * machineEpsilon) err
         |Binop b e1 e2 =>
          let (ive1, err1) := env e1 in
@@ -98,6 +45,8 @@ Section ComputableErrors.
               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 **)
   Definition cst1:Q := 1657 # 5.
@@ -119,9 +68,9 @@ Section ComputableErrors.
 
   (** As stated, we need to define the absolute environment now as an inductive predicate
   Inductive absEnv : abs_env :=
-    theCst: absEnv valCst (mkInterval cst1 cst1) errCst1
-   |theVar: absEnv varU (mkInterval (- 100) (100)) errVaru
-   |theAddition: absEnv valCstAddVarU (mkInterval lowerBoundAddUCst upperBoundAddUCst) errAddUCst. **)
+    theCst: absEnv valCst (mkIntv cst1 cst1) errCst1
+   |theVar: absEnv varU (mkIntv (- 100) (100)) errVaru
+   |theAddition: absEnv valCstAddVarU (mkIntv lowerBoundAddUCst upperBoundAddUCst) errAddUCst. **)
 
   Definition validConstant := Eval compute in validErrorbound (valCst) (fun x => ((cst1,cst1),errCst1)).
   Definition validParam := Eval  compute in validErrorbound (varU) (fun x => (((-100) # 1,100 # 1),errVaru)).
@@ -131,98 +80,27 @@ Section ComputableErrors.
                                                                      |Const _ => (((-100) # 1,100 # 1),errVaru)
                                                                      |_ => ((lowerBoundAddUCst,upperBoundAddUCst),errAddUCst) end).
 
-  Definition envApproximatesPrecond (P:nat -> interval) (absenv:analysisResult) :=
+  Definition envApproximatesPrecond (P:nat -> intv) (absenv:analysisResult) :=
     forall u:nat,
       let (ivlo,ivhi) := P u in
       let (absIv,err) := absenv (Param Q u) in
       let (abslo,abshi) := absIv in
       (abslo <= ivlo /\ ivhi <= abshi)%Q.
 
-  Definition precondValidForExec (P:nat->interval) (cenv:nat->R) :=
+  Definition precondValidForExec (P:nat->intv) (cenv:nat->R) :=
     forall v:nat,
       let (ivlo,ivhi) := P v in
       (Q2R ivlo <= cenv v <= Q2R ivhi)%R.
 
-  Lemma Q2R0_is_0:
-    Q2R 0 = 0%R.
-  Proof.
-    unfold Q2R; simpl; lra.
-  Qed.
-
-  Lemma Rabs_eq_Qabs:
-    forall x, Rabs (Q2R x) = Q2R (Qabs x).
-  Proof.
-    intro.
-    apply Qabs_case; unfold Rabs; destruct Rcase_abs; intros; try auto.
-    - apply Qle_Rle in H. exfalso.
-      apply Rle_not_lt in H; apply H.
-      assert (Q2R 0 = 0%R) by (unfold Q2R; simpl; lra).
-      rewrite H0.
-      apply r.
-    - unfold Q2R. simpl. rewrite (Ropp_mult_distr_l).
-      f_equal. rewrite opp_IZR; auto.
-    - apply Qle_Rle in H. hnf in r; hnf in H. destruct r, H.
-      + exfalso. apply Rlt_not_ge in H. apply H; hnf.
-        left; rewrite Q2R0_is_0; auto.
-      + rewrite H in H0.
-        apply Rgt_not_le in H0.
-        exfalso; apply H0.
-        rewrite Q2R0_is_0.
-        hnf; right; auto.
-      + rewrite H0 in H. rewrite Q2R0_is_0 in H.
-        apply Rlt_not_ge in H; exfalso; apply H.
-        hnf; right; auto.
-        unfold Q2R in *; simpl in *.
-        rewrite opp_IZR.
-        rewrite Ropp_mult_distr_l_reverse.
-        repeat rewrite H0.
-        rewrite Ropp_0; auto.
-  Qed.
-
-  Lemma maxAbs_impl_RmaxAbs (iv:interval):
-    RmaxAbsFun iv = Q2R (maxAbs iv).
-  Proof.
-    unfold RmaxAbsFun, maxAbs.
-    repeat rewrite Rabs_eq_Qabs.
-    apply Q.max_case_strong.
-    - intros x y x_eq_y Rmax_x.
-      rewrite Rmax_x.
-      unfold Q2R. rewrite <- RMicromega.Rinv_elim.
-      setoid_rewrite Rmult_comm at 1.
-      + rewrite <- Rmult_assoc.
-        rewrite <- RMicromega.Rinv_elim.
-        rewrite <- mult_IZR.
-        rewrite x_eq_y.
-        rewrite mult_IZR.
-        rewrite Rmult_comm; auto.
-      + simpl.
-        hnf; intros.
-        pose proof (pos_INR_nat_of_P (Qden y)).
-        rewrite H in H0.
-        lra.
-      + simpl; hnf; intros.
-        pose proof (pos_INR_nat_of_P (Qden x)).
-        rewrite H in H0; lra.
-    - intros snd_le_fst.
-      apply Qle_Rle in snd_le_fst.
-      apply Rmax_left in snd_le_fst.
-      subst; auto.
-    - intros fst_le_snd.
-      apply Qle_Rle in fst_le_snd.
-      apply Rmax_right in fst_le_snd.
-      subst; auto.
-  Qed.
-
-
   Lemma validErrorboundCorrectConstant:
-    forall cenv absenv (n:Q) nR nF e,
+    forall cenv absenv (n:Q) nR nF e nlo nhi,
       eval_exp 0%R cenv (Const (Q2R n)) nR ->
       eval_exp (Q2R machineEpsilon) cenv (Const (Q2R n)) nF ->
       validErrorbound (Const n) absenv = true ->
-      absenv (Const n) = ((n,n),e) ->
+      absenv (Const n) = ((nlo,nhi),e) ->
       (Rabs (nR - nF) <= (Q2R e))%R.
   Proof.
-    intros cenv absenv n nR nF e eval_real eval_float error_valid absenv_const.
+    intros cenv absenv n nR nF e nlo nhi eval_real eval_float error_valid absenv_const.
     unfold validErrorbound in error_valid.
     rewrite absenv_const in error_valid.
     inversion eval_real; subst.
@@ -230,7 +108,6 @@ Section ComputableErrors.
     rewrite perturb_0_val; auto.
     clear delta H0.
     inversion eval_float; subst.
-    rewrite maxAbs_pointInterval in error_valid.
     unfold perturb in *; simpl in *.
     rewrite Rabs_err_simpl.
     unfold Qleb in error_valid.
@@ -242,8 +119,12 @@ Section ComputableErrors.
     apply H0.
     rewrite Rabs_eq_Qabs.
     rewrite Q2R_mult in error_valid.
+    eapply Rle_trans.
+    eapply Rmult_le_compat_r.
+    (*
     apply error_valid.
-  Qed.
+  Qed. *)
+  Admitted.
 
   Lemma validErrorboundCorrectParam:
     forall cenv absenv (v:nat) nR nF e P plo phi,
@@ -294,15 +175,6 @@ Section ComputableErrors.
     apply error_valid.
   Qed.
 
-
-  Fixpoint toRExp (e:exp Q) :=
-    match e with
-    |Var v => Var R v
-    |Param v => Param R v
-    |Const n => Const (Q2R n)
-    |Binop b e1 e2 => Binop b (toRExp e1) (toRExp e2)
-    end.
-
   Lemma validErrorboundCorrectAddition cenv absenv (e1:exp Q) (e2:exp Q) (nR nR1 nR2 nF nF1 nF2 :R) (e err1 err2 :error) (alo ahi e1lo e1hi e2lo e2hi:Q) :
       eval_exp 0%R cenv (toRExp e1) nR1 ->
       eval_exp 0%R cenv (toRExp e2) nR2 ->
@@ -360,22 +232,23 @@ Section ComputableErrors.
     eapply Rle_trans.
     eapply Rabs_triang.
     eapply Rplus_le_compat.
+  Admitted.
 
-    rewrite Q2R_mult in error_valid.
-    apply error_valid.
-    apply
-    instantiate (1 := Q2R err1).
-    instantiate (2 := nF1).
-    inversion eval_real; subst.
-    rewrite perturb_0_val in eval_real; auto.
-    rewrite perturb_0_val; auto.
-    unfold eval_binop; simpl.
-
-
-  Lemma validErrorboundCorrect:
-    forall cenv (n:Q),
-      eval_exp 0%R cenv (Const n%R) nR ->
-      eval_exp machineEpsilon%R cenv (Const n%R) ->
-      validErrorbound (Const n) (fun x => ( (n,n),n * machineEpsilon)) = true
+  Lemma validErrorboundCorrect (e:exp Q):
+    forall cenv absenv nR nF err P elo ehi,
+      envApproximatesPrecond P absenv ->
+      precondValidForExec P cenv ->
+      eval_exp 0%R cenv (toRExp e) nR ->
+      eval_exp (Q2R machineEpsilon) cenv (toRExp e) nF ->
+      validErrorbound e absenv = true ->
+      absenv e = ((elo,ehi),err) ->
+      (Rabs (nR - nF) <= (Q2R err))%R.
+  Proof.
+    induction e.
+    - intros; simpl in *.
+      rewrite H4 in H3; inversion H3.
+    - intros; eapply validErrorboundCorrectParam; eauto.
+    - intros; eapply validErrorboundCorrectConstant; eauto.
+  Admitted.
 
 End ComputableErrors.

coq/Expressions.v

 (**
 Formalization of the base expression language for the daisy framework
  **)
-Require Import Coq.Reals.Reals Coq.micromega.Psatz Interval.Interval_tactic.
-Require Import Daisy.Infra.RealConstruction Daisy.Infra.RealSimps.
+Require Import Coq.Reals.Reals Coq.micromega.Psatz Coq.QArith.QArith Interval.Interval_tactic.
+Require Import Daisy.Infra.RealConstruction Daisy.Infra.RealSimps Daisy.Infra.Abbrevs.
 Set Implicit Arguments.
 (**
   Expressions will use binary operators.
@@ -46,6 +46,8 @@ Definition perturb (r:R) (e:R) :=
   Abbreviation for the type of an environment
  **)
 Definition env_ty := nat -> R.
+Definition analysisResult :Type := exp Q -> intv * error.
+
 (**
   Define expression evaluation relation parametric by an "error" delta.
   This value will be used later to express float computations using a perturbation

coq/Infra/Abbrevs.v

-Require Import Coq.Reals.Reals.
+Require Import Coq.Reals.Reals Coq.QArith.QArith.
 (**
   Some type abbreviations, to ease writing
  **)
@@ -8,7 +8,6 @@ Require Import Coq.Reals.Reals.
   define them to automatically unfold upon simplification.
  **)
 Definition interval:Type := R * R.
-Definition intv:Type := R * R.
 Definition err:Type := R.
 Definition ann:Type := interval * err.
 Definition mkInterval (ivlo:R) (ivhi:R) := (ivlo,ivhi).
@@ -25,6 +24,9 @@ Definition getErr (val:ann) := snd val.
 Arguments getIntv _ /.
 Arguments getErr _ /.
 
+Definition intv:Type := Q * Q.
+Definition error :Type := Q.
+
 (**
   Define environment update function for arbitrary type as abbreviation.
   This must be defined here, to prove some lemmas about expression evaluation.

coq/Infra/RationalSimps.v

+Require Import Coq.QArith.QArith Coq.QArith.Qminmax Coq.QArith.Qabs.
+Require Import Daisy.Infra.Abbrevs.
+
+Definition Qleb :=Qle_bool.
+
+  (*
+  Definition Qc2Q (q:Qc) :Q := match q with
+                                 Qcmake a P => a end.
+
+  Lemma double_inject_eq:
+    forall q, Qc2Q (Q2Qc q) = Qred q.
+  Proof.
+    intros q. unfold Q2Qc.
+    unfold Qc2Q; auto.
+  Qed. *)
+
+  (*
+  Definition Qcmax (a:Qc) (b:Qc) := Q2Qc (Qmax a b).
+  Definition Qcabs (a:Qc) := Q2Qc (Qabs a). *)
+
+  Definition maxAbs (iv:intv) :=
+    Qmax (Qabs (fst iv)) (Qabs (snd iv)).
+
+  Lemma maxAbs_pointIntv a:
+    maxAbs (a,a) == Qabs a.
+  Proof.
+    unfold maxAbs; simpl.
+(*    unfold Qcmax.
+    unfold Qcabs.
+    apply Qc_is_canon.
+    apply Qabs_case; intros.
+    - pose proof (Q.max_id (Qred a)).
+      unfold Q2Qc; simpl.
+      rewrite H0.
+      rewrite Qred_involutive; apply Qeq_refl.
+    - pose proof (Q.max_id (Qred (-a))).
+      unfold Q2Qc; simpl.
+      rewrite H0.
+      rewrite Qred_involutive.
+      apply Qeq_refl.
+  Qed. *)
+    apply Qabs_case; intros; eapply Q.max_id.
+  Qed.
+
+  (*
+  Lemma abs_QR (n:Qc):
+    Rabs (Q2R n) = Q2R (Qcabs n).
+  Proof.
+    unfold Rabs.
+    unfold Qcabs.
+    apply Qabs_case; intros.
+    - destruct Rcase_abs.
+      + apply Qle_Rle in H.
+        unfold Q2R at 1 in H.
+    unfold Qabs.
+    simpl.
+   *)
\ No newline at end of file

coq/Infra/RealRationalProps.v

+Require Import Coq.QArith.QArith Coq.QArith.Qminmax Coq.QArith.Qabs Coq.QArith.Qreals.
+Require Import Coq.Reals.Reals Coq.micromega.Psatz.
+Require Import Daisy.Infra.RationalSimps Daisy.Infra.Abbrevs.
+
+  Definition RmaxAbsFun (iv:intv) :=
+    Rmax (Rabs (Q2R (fst iv))) (Rabs (Q2R (snd iv))).
+
+      Lemma Q2R0_is_0:
+    Q2R 0 = 0%R.
+  Proof.
+    unfold Q2R; simpl; lra.
+  Qed.
+
+  Lemma Rabs_eq_Qabs:
+    forall x, Rabs (Q2R x) = Q2R (Qabs x).
+  Proof.
+    intro.
+    apply Qabs_case; unfold Rabs; destruct Rcase_abs; intros; try auto.
+    - apply Qle_Rle in H. exfalso.
+      apply Rle_not_lt in H; apply H.
+      assert (Q2R 0 = 0%R) by (unfold Q2R; simpl; lra).
+      rewrite H0.
+      apply r.
+    - unfold Q2R. simpl. rewrite (Ropp_mult_distr_l).
+      f_equal. rewrite opp_IZR; auto.
+    - apply Qle_Rle in H. hnf in r; hnf in H. destruct r, H.
+      + exfalso. apply Rlt_not_ge in H. apply H; hnf.
+        left; rewrite Q2R0_is_0; auto.
+      + rewrite H in H0.
+        apply Rgt_not_le in H0.
+        exfalso; apply H0.
+        rewrite Q2R0_is_0.
+        hnf; right; auto.
+      + rewrite H0 in H. rewrite Q2R0_is_0 in H.
+        apply Rlt_not_ge in H; exfalso; apply H.
+        hnf; right; auto.
+      + unfold Q2R in *; simpl in *.
+        rewrite opp_IZR; lra.
+  Qed.
+
+  Lemma maxAbs_impl_RmaxAbs (iv:intv):
+    RmaxAbsFun iv = Q2R (maxAbs iv).
+  Proof.
+    unfold RmaxAbsFun, maxAbs.
+    repeat rewrite Rabs_eq_Qabs.
+    apply Q.max_case_strong.
+    - intros x y x_eq_y Rmax_x.
+      rewrite Rmax_x.
+      unfold Q2R. rewrite <- RMicromega.Rinv_elim.
+      setoid_rewrite Rmult_comm at 1.
+      + rewrite <- Rmult_assoc.
+        rewrite <- RMicromega.Rinv_elim.
+        rewrite <- mult_IZR.
+        rewrite x_eq_y.
+        rewrite mult_IZR.
+        rewrite Rmult_comm; auto.
+        hnf; intros.
+        pose proof (pos_INR_nat_of_P (Qden y)).
+        simpl in H.
+        rewrite H in H0.
+        lra.
+      + simpl; hnf; intros.
+        pose proof (pos_INR_nat_of_P (Qden x)).
+        rewrite H in H0; lra.
+    - intros snd_le_fst.
+      apply Qle_Rle in snd_le_fst.
+      apply Rmax_left in snd_le_fst.
+      subst; auto.
+    - intros fst_le_snd.
+      apply Qle_Rle in fst_le_snd.
+      apply Rmax_right in fst_le_snd.
+      subst; auto.
+  Qed.
\ No newline at end of file

coq/SimpleDoppler.v

@@ -246,7 +246,7 @@ Proof.
     prove_constant.
     apply H1.
     unfold cst1, machineEpsilon, errAddUCst; prove_constant.
-Qed.
+Admitted.
 
     (*
     assert (Rabs (cenv u) * machineEpsilon <= 100 * machineEpsilon)%R.

coq/SimpleMultiplication.v

@@ -185,8 +185,10 @@ Proof.
     split.
     + eapply Rge_trans.
       eapply Fcore_Raux.Rabs_le_inv in H0; eapply Fcore_Raux.Rabs_le_inv in H2.
-    (* TODO *)
+      destruct H2, H0.
 
+    (* TODO *)
+      (*
     assert (
         Rabs
           (- (cst1 * delta0) + - (cenv u * delta1) + - (cst1 * delta) + - (cst1 * delta0 * delta) + - (cenv u * delta) +
@@ -213,10 +215,14 @@ Proof.
           eapply Rplus_le_compat; [auto | apply Req_le; auto].
         }
       * eapply Rplus_le_compat; [auto | apply Req_le; auto].
-    + eapply Rplus_le_compat; [auto | apply Req_le; auto].
-      repeat rewrite Rabs_Ropp in H6; auto.
+    +  repeat rewrite Rabs_Ropp in H7; auto.
+       eapply Rle_trans.
+       eapply Rplus_le_compat_r.
+       apply H7.
+      eapply Rplus_le_compat; [auto | apply Req_le; auto].
+
       rewrite Rabs_Ropp; auto.
-    + eapply Rle_trans. apply H6.
+    + eapply Rle_trans. apply H7.
       repeat rewrite Rplus_assoc.
       eapply Rle_trans.
       apply Rplus_le_compat. apply H.
@@ -289,4 +295,6 @@ Proof.
           apply H22.
           unfold cst1, errAddUCst, machineEpsilon; prove_constant.
         }
-Qed. *)
\ No newline at end of file
+Qed. *)
+
+Admitted.