Proof draft for interval bounds correctness

coq/ErrorValidation.v

@@ -8,14 +8,6 @@ Section ComputableErrors.
 
   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

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.
+Require Import Daisy.Infra.RationalSimps Daisy.Infra.Abbrevs Daisy.Expressions.
 
-  Definition RmaxAbsFun (iv:intv) :=
-    Rmax (Rabs (Q2R (fst iv))) (Rabs (Q2R (snd iv))).
+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 Q2R0_is_0:
-    Q2R 0 = 0%R.
-  Proof.
-    unfold Q2R; simpl; lra.
-  Qed.
+Definition RmaxAbsFun (iv:intv) :=
+  Rmax (Rabs (Q2R (fst iv))) (Rabs (Q2R (snd iv))).
 
-  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 Q2R0_is_0:
+  Q2R 0 = 0%R.
+Proof.
+  unfold Q2R; simpl; 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
+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/IntervalValidation.v

-Require Import Coq.QArith.QArith.
-Require Import Daisy.Expressions Daisy.Infra.Abbrevs Daisy.Infra.RationalSimps Daisy.IntervalArithQ Daisy.Infra.RationalConstruction.
+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.
 
 Fixpoint validIntervalbounds (e:exp Q) (absenv:analysisResult) (P:precond):=
   let (intv, _) := absenv e in
@@ -33,6 +33,53 @@ 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 ->
+  eval_exp 0%R cenv (toRExp e) vR ->
+  contained vR (Q2R (fst (fst(absenv e))), Q2R (snd (fst (absenv e)))).
+Proof.
+  induction e.
+  - intros absenv P cenv vR 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.
+    unfold validIntervalbounds in valid_bounds.
+    destruct (absenv (Param Q n)) as [intv err].
+    (* same *)
+    admit.
+  - intros absenv P cenv vR 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.
+    unfold contained; simpl.
+    split.
+    + apply Is_true_eq_true in H.
+      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.