Proof interval validation sound

coq/Infra/ExpressionAbbrevs.v

-Require Import Coq.QArith.QArith.
-
+Require Import Coq.QArith.QArith Coq.Reals.Reals Coq.QArith.Qreals.
 Require Export Daisy.Infra.Abbrevs Daisy.Expressions.
 
-Definition analysisResult :Type := exp Q -> intv * error.
\ No newline at end of file
+Definition analysisResult :Type := exp Q -> intv * error.
+
+
+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->intv) (cenv:nat->R) :=
+  forall v:nat,
+    let (ivlo,ivhi) := P v in
+    (Q2R ivlo <= cenv v <= Q2R ivhi)%R.
\ No newline at end of file

coq/Infra/RealRationalProps.v

@@ -78,4 +78,66 @@ Proof.
     apply Qle_Rle in fst_le_snd.
     apply Rmax_right in fst_le_snd.
     subst; auto.
+Qed.
+
+Lemma Q2R_max (a:Q) (b:Q) :
+  Rmax (Q2R a) (Q2R b) = Q2R (Qmax a b).
+Proof.
+  apply Q.max_case_strong.
+  - intros c d eq_c_d 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 eq_c_d.
+      rewrite mult_IZR.
+      rewrite Rmult_comm; auto.
+      hnf; intros.
+      pose proof (pos_INR_nat_of_P (Qden d)).
+      simpl in H.
+      rewrite H in H0.
+      lra.
+    + simpl; hnf; intros.
+      pose proof (pos_INR_nat_of_P (Qden c)).
+      rewrite H in H0; lra.
+  - intros less. apply Qle_Rle in less.
+    assert (Rmax (Q2R a) (Q2R b) = Q2R a) by (apply Rmax_left; auto).
+    rewrite H; auto.
+  - intros less. apply Qle_Rle in less.
+    assert (Rmax (Q2R a) (Q2R b) = Q2R b) by (apply Rmax_right; auto).
+    rewrite H; auto.
+Qed.
+
+Lemma Q2R_min (a:Q) (b:Q) :
+    Rmin (Q2R a) (Q2R b) = Q2R (Qmin a b).
+Proof.
+  apply Q.min_case_strong.
+  - intros c d eq_c_d Rmin_x.
+    rewrite Rmin_x.
+    unfold Q2R.
+    rewrite <- RMicromega.Rinv_elim.
+    setoid_rewrite Rmult_comm at 1.
+    + rewrite <- Rmult_assoc.
+      rewrite <- RMicromega.Rinv_elim.
+      rewrite <- mult_IZR.
+      rewrite eq_c_d.
+      rewrite mult_IZR.
+      rewrite Rmult_comm; auto.
+      hnf; intros.
+      pose proof (pos_INR_nat_of_P (Qden d)).
+      simpl in H.
+      rewrite H in H0.
+      lra.
+    + simpl; hnf; intros.
+      pose proof (pos_INR_nat_of_P (Qden c)).
+      rewrite H in H0; lra.
+  - intros less. apply Qle_Rle in less.
+    assert (Rmin (Q2R a) (Q2R b) = Q2R a) by (apply Rmin_left; auto).
+    rewrite H; auto.
+  - intros less. apply Qle_Rle in less.
+    assert (Rmin (Q2R a) (Q2R b) = Q2R b) by (apply Rmin_right; auto).
+    rewrite H; auto.
 Qed.
\ No newline at end of file

coq/IntervalValidation.v

-Require Import Coq.QArith.QArith Coq.QArith.Qreals.
+Require Import Coq.QArith.QArith Coq.QArith.Qreals QArith.Qminmax.
 Require Import Daisy.Infra.Abbrevs Daisy.Infra.RationalSimps Daisy.Infra.RationalConstruction Daisy.Infra.RealRationalProps.
-Require Import Daisy.Expressions Daisy.IntervalArithQ.
+Require Import Daisy.Infra.ExpressionAbbrevs Daisy.IntervalArithQ Daisy.IntervalArith Daisy.Infra.RealSimps.
 
 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 (Qeq_bool (fst intv) (fst (bounds_v))) (Qeq_bool (snd bounds_v) (snd (intv)))
+    | Var v => false
+                (* let bounds_v := P v in
+      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 bounds_v) (snd (intv)))
@@ -34,82 +34,178 @@ Fixpoint validIntervalbounds (e:exp Q) (absenv:analysisResult) (P:precond):=
       andb rec opres
     end.
 
-(*
+
+Corollary Q2R_max4 a b c d:
+  Q2R (IntervalArithQ.max4 a b c d) = max4 (Q2R a) (Q2R b) (Q2R c) (Q2R d).
+Proof.
+  unfold IntervalArithQ.max4, max4; repeat rewrite Q2R_max; auto.
+Qed.
+
+Corollary Q2R_min4 a b c d:
+  Q2R (IntervalArithQ.min4 a b c d) = min4 (Q2R a) (Q2R b) (Q2R c) (Q2R d).
+Proof.
+  unfold IntervalArith.min4, min4; repeat rewrite Q2R_min; auto.
+Qed.
+
+Ltac env_assert absenv e name :=
+  assert (exists iv err, absenv e = (iv,err)) as name by (destruct (absenv e); repeat eexists; auto).
+
 Lemma validIntervalbounds_correct (e:exp Q):
   forall (absenv:analysisResult) (P:precond) cenv vR,
-  validIntervalbounds e absenv P = true ->
-  eval_exp 0%R cenv (toRExp e) vR ->
-  contained vR (Q2R (fst (fst(absenv e))), Q2R (snd (fst (absenv e)))).
+    envApproximatesPrecond P absenv ->
+    precondValidForExec P cenv ->
+    validIntervalbounds e absenv P = true ->
+    eval_exp 0%R cenv (toRExp e) vR ->
+    (Q2R (fst (fst(absenv e))) <= vR <= Q2R (snd (fst (absenv e))))%R.
 Proof.
   induction e.
-  - intros absenv P cenv vR valid_bounds eval_e.
+  - intros absenv P cenv vR env_approx_p precond_valid valid_bounds eval_e.
     unfold validIntervalbounds in valid_bounds.
-    destruct (absenv (Var Q n)) as [intv err].
-    simpl.
-    (* needs that Precond approximates value *)
-    admit.
-  - intros absenv P cenv vR valid_bounds eval_e.
+    destruct (absenv (Var Q n)); inversion valid_bounds.
+  - intros absenv P cenv vR env_approx_p precond_valid valid_bounds eval_e.
     unfold validIntervalbounds in valid_bounds.
-    destruct (absenv (Param Q n)) as [intv err].
-    (* same *)
-    admit.
-  - intros absenv P cenv vR valid_bounds eval_e.
+    assert (exists intv err, absenv (Param Q n) = (intv,err))
+      as absenv_n
+        by (destruct (absenv (Param Q n)); repeat eexists; auto).
+    destruct absenv_n as [intv [err absenv_n]].
+    rewrite absenv_n in valid_bounds.
+    unfold precondValidForExec in precond_valid.
+    unfold envApproximatesPrecond in env_approx_p.
+    specialize (env_approx_p n).
+    assert (exists ivlo ivhi, P n = (ivlo, ivhi)) as p_n
+        by (destruct (P n); repeat eexists; auto).
+    destruct p_n as [ivlo [ivhi p_n]].
+    rewrite p_n, absenv_n in env_approx_p.
+    specialize (precond_valid n); rewrite p_n in precond_valid.
+    inversion eval_e; subst.
+    rewrite absenv_n; simpl.
+    rewrite perturb_0_val; auto.
+    destruct intv as [abslo abshi]; simpl in *.
+    destruct env_approx_p as [abslo_le_ivlo ivhi_le_abshi].
+    destruct precond_valid as [ivlo_le_env env_le_ivhi].
+    apply Qle_Rle in abslo_le_ivlo; apply Qle_Rle in ivhi_le_abshi.
+    split.
+    + eapply Rle_trans.
+      apply abslo_le_ivlo.
+      apply ivlo_le_env.
+    + eapply Rle_trans.
+      apply env_le_ivhi.
+      apply ivhi_le_abshi.
+  - intros absenv P cenv vR env_approx_p valid_precond valid_bounds eval_e.
     unfold validIntervalbounds in valid_bounds.
     destruct (absenv (Const v)) as [intv err].
     simpl.
     apply Is_true_eq_left in valid_bounds.
     apply andb_prop_elim in valid_bounds.
-    destruct valid_bounds.
+    destruct valid_bounds as [valid_lo valid_hi].
+    inversion eval_e; subst.
+    rewrite perturb_0_val; auto.
     unfold contained; simpl.
     split.
-    + apply Is_true_eq_true in H.
+    + apply Is_true_eq_true in valid_lo.
       unfold Qleb in *.
-      apply Qle_bool_iff in H.
-      admit.
-    + admit.
-  - destruct b.
-    + admit.
-    + admit.
-    + admit.
-    + intros absenv P cenv vR valid_bounds eval_e.
-      simpl in valid_bounds.
-      destruct (absenv (Binop Div e1 e2));
-        destruct (absenv e1);
-        destruct (absenv e2).
-      apply Is_true_eq_left in valid_bounds.
-      apply andb_prop_elim in valid_bounds.
-      destruct valid_bounds.
-      unfold Is_true in *; simpl in *. contradiction.
-Admitted.
- *)
-
-Definition u:nat := 1.
-(** 1655/5 = 331; 0,4 = 2/5 **)
-Definition cst1:Q := 1657 # 5.
-
-(** Define abbreviations **)
-Definition varU:exp Q := Param Q u.
-Definition valCst:exp Q := Const cst1.
-Definition valCstAddVarU:exp Q := Binop Plus valCst varU.
-
-(** Error values **)
-Definition errCst1 :Q := rationalFromNum (36792791036077685#1) 16 14.
-Definition errVaru := rationalFromNum (11102230246251565#1) 16 14.
-Definition lowerBoundAddUCst:Q := 1157 # 5.
-Definition upperBoundAddUCst:Q := 2157 # 5.
-Definition errAddUCst := rationalFromNum (9579004256465851#1) 15 14.
-
-(** The added assertion becomes the precondition for us **)
-Definition precondition := fun n:nat => (- (100#1),100#1).
-Definition absenv := fun e:exp Q => match e with
-                                 |Const n => (cst1,cst1,0)
-                                 |Binop b e1 e2 => (lowerBoundAddUCst,upperBoundAddUCst,0)
-                                 | Param v => (-(100#1),100#1,0)
-                                 | _ => (0,0,0)
-                                 end.
-
-Eval compute in isSupersetIntv (lowerBoundAddUCst,upperBoundAddUCst) (lowerBoundAddUCst,upperBoundAddUCst).
-Eval compute in addIntv (cst1,cst1) (-(100#1),100#1).
-
-Eval compute in validIntervalbounds valCst (fun _ => (cst1,cst1,0)) (fun _ => (cst1,cst1)).
-Eval compute in validIntervalbounds varU (fun _ => (- (100#1),100#1,0)) precondition.
\ No newline at end of file
+      apply Qle_bool_iff in valid_lo.
+      apply Qle_Rle in valid_lo; auto.
+    + apply Is_true_eq_true in valid_hi.
+      unfold Qleb in *.
+      apply Qle_bool_iff in valid_hi.
+      apply Qle_Rle in valid_hi; auto.
+  - intros absenv P cenv vR env_approx_p valid_precond valid_bounds eval_e;
+    inversion eval_e; subst.
+    rewrite perturb_0_val in eval_e; auto.
+    rewrite perturb_0_val; auto.
+    simpl in valid_bounds.
+    env_assert absenv (Binop b e1 e2) absenv_bin.
+    env_assert absenv e1 absenv_e1.
+    env_assert absenv e2 absenv_e2.
+    destruct absenv_bin as [iv [err absenv_bin]]; rewrite absenv_bin in valid_bounds; rewrite absenv_bin.
+    destruct absenv_e1 as [iv1 [err1 absenv_e1]]; rewrite absenv_e1 in valid_bounds.
+    destruct absenv_e2 as [iv2 [err2 absenv_e2]]; rewrite absenv_e2 in valid_bounds.
+    apply Is_true_eq_left in valid_bounds.
+    apply andb_prop_elim in valid_bounds.
+    destruct valid_bounds as [valid_rec valid_bin].
+    apply andb_prop_elim in valid_rec.
+    destruct valid_rec as [valid_e1 valid_e2].
+    apply Is_true_eq_true in valid_e1; apply Is_true_eq_true in  valid_e2.
+    specialize (IHe1 absenv P cenv v1 env_approx_p valid_precond valid_e1 H4);
+      specialize (IHe2 absenv P cenv v2 env_approx_p valid_precond valid_e2 H5).
+    rewrite absenv_e1 in IHe1.
+    rewrite absenv_e2 in IHe2.
+      destruct b; simpl in *.
+    + pose proof (additionIsValid (Q2R (fst iv1),Q2R (snd iv1)) (Q2R (fst iv2), Q2R (snd iv2))) as valid_add.
+      unfold validIntervalAdd in valid_add.
+      specialize (valid_add v1 v2 IHe1 IHe2).
+      unfold contained in valid_add.
+      unfold isSupersetIntv in valid_bin.
+      apply andb_prop_elim in valid_bin; destruct valid_bin as [valid_lo valid_hi].
+      apply Is_true_eq_true in valid_lo; apply Is_true_eq_true in valid_hi.
+      apply Qle_bool_iff in valid_lo; apply Qle_bool_iff in valid_hi.
+      apply Qle_Rle in valid_lo; apply Qle_Rle in valid_hi.
+      destruct valid_add as [valid_add_lo valid_add_hi].
+      split.
+      * eapply Rle_trans. apply valid_lo.
+        unfold ivlo. unfold addIntv.
+        simpl in valid_add_lo.
+        repeat rewrite <- Q2R_plus in valid_add_lo.
+        rewrite <- Q2R_min4 in valid_add_lo.
+        unfold absIvUpd; auto.
+      * eapply Rle_trans.
+        Focus 2.
+        apply valid_hi.
+        unfold ivlo, addIntv.
+        simpl in valid_add_hi.
+        repeat rewrite <- Q2R_plus in valid_add_hi.
+        rewrite <- Q2R_max4 in valid_add_hi.
+        unfold absIvUpd; auto.
+    + pose proof (subtractionIsValid (Q2R (fst iv1),Q2R (snd iv1)) (Q2R (fst iv2), Q2R (snd iv2))) as valid_sub.
+      specialize (valid_sub v1 v2 IHe1 IHe2).
+      unfold contained in valid_sub.
+      unfold isSupersetIntv in valid_bin.
+      apply andb_prop_elim in valid_bin; destruct valid_bin as [valid_lo valid_hi].
+      apply Is_true_eq_true in valid_lo; apply Is_true_eq_true in valid_hi.
+      apply Qle_bool_iff in valid_lo; apply Qle_bool_iff in valid_hi.
+      apply Qle_Rle in valid_lo; apply Qle_Rle in valid_hi.
+      destruct valid_sub as [valid_sub_lo valid_sub_hi].
+      split.
+      * eapply Rle_trans. apply valid_lo.
+        unfold ivlo. unfold subtractIntv.
+        simpl in valid_sub_lo.
+        repeat rewrite <- Rsub_eq_Ropp_Rplus in valid_sub_lo.
+        repeat rewrite <- Q2R_minus in valid_sub_lo.
+        rewrite <- Q2R_min4 in valid_sub_lo.
+        unfold absIvUpd; auto.
+      * eapply Rle_trans.
+        Focus 2.
+        apply valid_hi.
+        unfold ivlo, addIntv.
+        simpl in valid_sub_hi.
+        repeat rewrite <- Rsub_eq_Ropp_Rplus in valid_sub_hi.
+        repeat rewrite <- Q2R_minus in valid_sub_hi.
+        rewrite <- Q2R_max4 in valid_sub_hi.
+        unfold absIvUpd; auto.
+    + pose proof (interval_multiplication_valid (Q2R (fst iv1),Q2R (snd iv1)) (Q2R (fst iv2), Q2R (snd iv2))) as valid_mul.
+      specialize (valid_mul v1 v2 IHe1 IHe2).
+      unfold contained in valid_mul.
+      unfold isSupersetIntv in valid_bin.
+      apply andb_prop_elim in valid_bin; destruct valid_bin as [valid_lo valid_hi].
+      apply Is_true_eq_true in valid_lo; apply Is_true_eq_true in valid_hi.
+      apply Qle_bool_iff in valid_lo; apply Qle_bool_iff in valid_hi.
+      apply Qle_Rle in valid_lo; apply Qle_Rle in valid_hi.
+      destruct valid_mul as [valid_mul_lo valid_mul_hi].
+      split.
+      * eapply Rle_trans. apply valid_lo.
+        unfold ivlo. unfold multIntv.
+        simpl in valid_mul_lo.
+        repeat rewrite <- Q2R_mult in valid_mul_lo.
+        rewrite <- Q2R_min4 in valid_mul_lo.
+        unfold absIvUpd; auto.
+      * eapply Rle_trans.
+        Focus 2.
+        apply valid_hi.
+        unfold ivlo, addIntv.
+        simpl in valid_mul_hi.
+        repeat rewrite <- Q2R_mult in valid_mul_hi.
+        rewrite <- Q2R_max4 in valid_mul_hi.
+        unfold absIvUpd; auto.
+    + contradiction.
+Qed.
\ No newline at end of file