Toy example proven with holes, these should be formally showing some...

Toy example proven with holes, these should be formally showing some transitivity rules and upper bounds

coq/Expressions.v

@@ -113,6 +113,22 @@ Proof.
   field_simplify; reflexivity.
 Qed.
 
+Lemma Rabs_err_simpl:
+  forall a b,
+    (Rabs (a - (a * (1 + b))) = Rabs (a * b))%R.
+Proof.
+  intros a b.
+  rewrite Rmult_plus_distr_l.
+  rewrite Rmult_1_r.
+  rewrite Rsub_eq_Ropp_Rplus.
+  rewrite Ropp_plus_distr.
+  assert (- a + (- (a * b)) = ( - (a * b) + - a))%R by (rewrite Rplus_comm; auto).
+  rewrite H.
+  rewrite <- Rsub_eq_Ropp_Rplus.
+  rewrite Rplus_minus.
+  rewrite Rabs_Ropp; reflexivity.
+Qed.
+
 (**
   TODO: Check wether we need Rabs (n * machineEpsilon) instead
 **)
@@ -127,15 +143,7 @@ Proof.
   rewrite perturb_0_val; auto.
   inversion eval_float; subst.
   unfold perturb; simpl.
-  rewrite Rmult_plus_distr_l.
-  rewrite Rmult_1_r.
-  rewrite Rsub_eq_Ropp_Rplus.
-  rewrite Ropp_plus_distr.
-  assert (-n + (- (n * delta0)) = ( -(n * delta0) + - n))%R by (rewrite Rplus_comm; auto).
-  rewrite H.
-  rewrite <- Rsub_eq_Ropp_Rplus.
-  rewrite Rplus_minus.
-  rewrite Rabs_Ropp.
+  rewrite Rabs_err_simpl.
   repeat rewrite Rabs_mult.
   apply Rmult_le_compat_l; [apply Rabs_pos | auto].
 Qed.
@@ -144,7 +152,7 @@ Qed.
   TODO: Maybe improve bound by adding interval constraint and proving that it is leq than maxAbs of bounds
   (nlo <= cenv n <= nhi)%R ->   (Rabs (nR - nF) <= Rabs ((Rmax (Rabs nlo) (Rabs nhi)) * machineEpsilon))%R.
 **)
-Lemma var_abs_err_bounded (n:nat) (nR:R) (nF:R) (cenv:nat->R) (nlo:R) (nhi:R):
+Lemma param_abs_err_bounded (n:nat) (nR:R) (nF:R) (cenv:nat->R):
   eval_exp 0%R cenv (Param R n) nR ->
   eval_exp machineEpsilon cenv (Param R n) nF ->
   (Rabs (nR - nF) <= Rabs (cenv n) * machineEpsilon)%R.
@@ -154,18 +162,37 @@ Proof.
   rewrite perturb_0_val; auto.
   inversion eval_float; subst.
   unfold perturb; simpl.
+  rewrite Rabs_err_simpl.
+  repeat rewrite Rabs_mult.
+  apply Rmult_le_compat_l; [ apply Rabs_pos | auto].
+Qed.
+
+(*
+
+Lemma add_abs_err_bounded (e1:exp R) (e1R:R) (e1F:R) (e2:exp R) (e2R:R) (e2F:R) (vR:R) (vF:R) (cenv:nat->R) (err1:R) (err2:R):
+  eval_exp 0%R cenv e1 e1R ->
+  eval_exp machineEpsilon cenv e1 e1F ->
+  eval_exp 0%R cenv e2 e2R ->
+  eval_exp machineEpsilon cenv e2 e2F ->
+  eval_exp 0%R cenv (Binop Plus e1 e2) vR ->
+  eval_exp machineEpsilon cenv (Binop Plus e1 e2) vF ->
+  (Rabs (e1R - e1F) <= err1)%R ->
+  (Rabs (e2R - e2F) <= err2)%R ->
+  (Rabs (vR - vF) <= err1 + err2 + Rabs vR * machineEpsilon)%R.
+Proof.
+  intros e1_real e1_float e2_real e2_float plus_real plus_float bound_e1 bound_e2.
+  inversion plus_real; subst.
+  rewrite perturb_0_val; auto.
+  inversion plus_float; subst.
+  unfold perturb; simpl.
   rewrite Rmult_plus_distr_l.
   rewrite Rmult_1_r.
   rewrite Rsub_eq_Ropp_Rplus.
   rewrite Ropp_plus_distr.
-  assert (- cenv n + - (cenv n * delta0) = - (cenv n * delta0) + - cenv n)%R by (rewrite Rplus_comm; auto).
-  rewrite H.
-  rewrite <- Rsub_eq_Ropp_Rplus.
-  rewrite Rplus_minus.
-  rewrite Rabs_Ropp.
-  repeat rewrite Rabs_mult.
-  apply Rmult_le_compat_l; [ apply Rabs_pos | auto].
-Qed.
+  rewrite (eval_det e1_real H4) in e1_real.
+  rewrite (eval_det e2_real H5) in e2_real.
+  pose proof (Rabs_triang (v1 + v2) (- (v0 + v3) + - ((v0 + v3) * delta0))).
+ *)
 
 (**
   Using the parametric expressions, define boolean expressions for conditionals

coq/SimpleDoppler.v

 Require Import Coq.Reals.Reals Interval.Interval_tactic Coq.micromega.Psatz.
+Require Import Coq.Setoids.Setoid.
 Require Import Daisy.AbsoluteError Daisy.Commands Daisy.IntervalArith Daisy.Expressions Daisy.Infra.RealConstruction.
 
 (*
@@ -23,12 +24,31 @@ Require Import Daisy.AbsoluteError Daisy.Commands Daisy.IntervalArith Daisy.Expr
 [  Info  ] info:      9 ms, rangeError:    149 ms, analysis:     15 ms, frontend:   2709 ms,
  *)
 
+Lemma Rplus_minus_general:
+  forall a b c,
+    (a + b + (- a) + c = b + c)%R.
+Proof.
+  intros a b c.
+  repeat rewrite Rplus_assoc.
+  assert (b + (-a + c) = (b + c) + - a)%R.
+  - rewrite Rplus_comm.
+    rewrite Rplus_assoc.
+    assert (c + b = b + c)%R by (rewrite Rplus_comm; auto).
+    rewrite H.
+    rewrite Rplus_comm; auto.
+  - rewrite H.
+    rewrite <- Rplus_assoc.
+    rewrite (Rplus_assoc a (b + c)).
+    rewrite <- Rsub_eq_Ropp_Rplus.
+    rewrite Rplus_minus; auto.
+Qed.
+
 Definition u:nat := 1.
 (** 1655/5 = 331; 0,4 = 2/5 **)
 Definition cst1:R := 1657 / 5.
 
 (** Define abbreviations **)
-Definition varU:exp R := Var R u.
+Definition varU:exp R := Param R u.
 Definition valCst:exp R := Const cst1.
 Definition valCstAddVarU:exp R := Binop Plus valCst varU.
 
@@ -76,7 +96,7 @@ Proof.
       rewrite Rmax_left; [ | apply Req_le; auto].
       unfold realFromNum, negativePower.
       interval.
-    + apply (AbsErrVar u (mkInterval (- 100) (100)) errVaru); [constructor | ].
+    + apply (AbsErrParam u (mkInterval (- 100) (100)) errVaru); [constructor | ].
       unfold isSoundErr; simpl.
       unfold machineEpsilon, errVaru.
       unfold realFromNum.
@@ -114,48 +134,102 @@ Proof.
         interval.
   (* Semantic judgement  Rabs_triang_gen, Rabs_triang! triangle property? *)
   - inversion eval_real; subst.
+    rewrite perturb_0_val; auto.
+    rewrite perturb_0_val in eval_real; auto.
+    clear H2 delta.
+    inversion eval_float; subst.
     inversion H4; subst.
     inversion H5; subst.
-    apply Rabs_0_impl_eq in H2.
-    apply Rabs_0_impl_eq in H0.
-    subst.
-    inversion eval_float; subst.
-    inversion H6; inversion H7; subst.
-    unfold perturb in *; simpl.
-    unfold precondition in precond.
-    destruct precond.
-    assert (contained (cenv u) (mkInterval (-100) (100))) as uContained by (split; auto).
-    assert (contained (cst1) (mkInterval cst1 cst1)) as cst1Contained by (apply validPointInterval).
-    assert (contained (cenv u + cst1) (addInterval  (mkInterval (-100) (100)) (mkInterval cst1 cst1)))
-      as containedAdd
-        by (apply additionIsValid; auto).
-    assert (contained (errCst1) (mkInterval (-errCst1) (errCst1))) as errCst1Contained.
-    + unfold contained; simpl; split.
-      * unfold errCst1. unfold realFromNum. unfold negativePower. interval.
-      * apply Req_le; auto.
-    + assert (contained (errVaru) (mkInterval (-errVaru) (errVaru)))
-        as errVaruContained
-          by (split; [ simpl; unfold errVaru, realFromNum, negativePower; interval | apply Req_le; auto]).
-      assert (contained (cst1 + errCst1) (addInterval (mkInterval cst1 cst1) (mkInterval (-errCst1) (errCst1))))
-        as floatCst1Contained
-          by (apply additionIsValid; auto).
-      assert (contained (cenv u + errVaru) (addInterval (mkInterval (-100) (100)) (mkInterval (-errVaru) (errVaru))))
-        as floatVarUContained
-          by (apply additionIsValid; auto).
-      assert (contained ((cst1 + errCst1) + (cenv u + errVaru))
-                        (addInterval (addInterval (mkInterval cst1 cst1) (mkInterval (-errCst1) (errCst1)))
-                                     (addInterval (mkInterval (-100) (100)) (mkInterval (-errVaru) (errVaru)))))
-        as floatAddContained
-          by (apply additionIsValid; auto).
-      assert (contained errAddUCst (mkInterval (- errAddUCst) errAddUCst))
-        as errAddUCstContained
-          by (split; [ simpl; unfold errAddUCst, realFromNum, negativePower; interval | apply Req_le; auto]).
-      assert (contained ((cst1 + errCst1) + (cenv u + errVaru) + errAddUCst)
-             (addInterval
-                (addInterval (addInterval (mkInterval cst1 cst1) (mkInterval (-errCst1) (errCst1)))
-                             (addInterval (mkInterval (-100) (100)) (mkInterval (-errVaru) (errVaru))))
-                (mkInterval (- errAddUCst) errAddUCst)))
-        as floatAddErrContained
+    rewrite (perturb_0_val _ delta0) in H4; auto.
+    rewrite (perturb_0_val _ delta0) in eval_real; auto.
+    rewrite (perturb_0_val _ delta0); auto.
+    rewrite (perturb_0_val _ delta1) in H5; auto.
+    rewrite (perturb_0_val _ delta1) in eval_real; auto.
+    rewrite (perturb_0_val _ delta1); auto.
+    clear H0 H1 delta0 delta1.
+    inversion H6; subst.
+    inversion H7; subst.
+    pose proof (const_abs_err_bounded H4 H6).
+    pose proof (param_abs_err_bounded H5 H7).
+    unfold eval_binop.
+    unfold perturb in *; simpl in *.
+    rewrite Rabs_err_simpl in *.
+    repeat rewrite Rmult_plus_distr_l.
+    repeat rewrite Rmult_1_r.
+    repeat rewrite Rmult_plus_distr_r.
+    rewrite Rsub_eq_Ropp_Rplus.
+    repeat rewrite Ropp_plus_distr.
+    repeat rewrite <- Rplus_assoc.
+    rewrite Rplus_assoc at 1.
+    repeat rewrite Rplus_minus_general.
+    rewrite <- Rplus_assoc.
+    assert (
+        Rabs
+          (- (cst1 * delta0) + - (cenv u * delta1) + - (cst1 * delta) + - (cst1 * delta0 * delta) + - (cenv u * delta) +
+           - (cenv u * delta1 * delta)) <=
+         Rabs (cst1 * delta0) + Rabs (cenv u * delta1) + Rabs (cst1 * delta) + Rabs (cst1 * delta0 * delta) +
+         Rabs (cenv u * delta) + Rabs (cenv u * delta1 * delta)
+        )%R.
+  - eapply Rle_trans.
+    eapply Rabs_triang.
+    assert (Rabs (- (cst1 * delta0) + - (cenv u * delta1) + - (cst1 * delta) + - (cst1 * delta0 * delta) + - (cenv u * delta)) <= Rabs (- (cst1 * delta0)) + Rabs (- (cenv u * delta1)) + Rabs (- (cst1 * delta)) + Rabs (- (cst1 * delta0 * delta)) + Rabs (- (cenv u * delta)))%R.
+    + eapply Rle_trans.
+      eapply Rabs_triang.
+      assert (Rabs (- (cst1 * delta0) + - (cenv u * delta1) + - (cst1 * delta) + - (cst1 * delta0 * delta)) <= Rabs (- (cst1 * delta0)) + Rabs (- (cenv u * delta1)) + Rabs (- (cst1 * delta)) + Rabs (- (cst1 * delta0 * delta)))%R.
+      * eapply Rle_trans.
+        eapply Rabs_triang.
+        assert (Rabs (- (cst1 * delta0) + - (cenv u * delta1) + - (cst1 * delta)) <= Rabs (- (cst1 * delta0)) + Rabs (- (cenv u * delta1)) + Rabs (- (cst1 * delta)))%R.
+        {
+          eapply Rle_trans.
+          eapply Rabs_triang.
+          pose proof (Rabs_triang (- (cst1 * delta0)) (- (cenv u * delta1))).
+          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].
+    + eapply Rplus_le_compat; [auto | apply Req_le; auto].
+      repeat rewrite Rabs_Ropp in H8; auto.
+      rewrite Rabs_Ropp; auto.
+    + eapply Rle_trans. apply H8.
+      repeat rewrite Rplus_assoc.
+      eapply Rle_trans.
+      apply Rplus_le_compat. apply H.
+      apply Req_le; auto.
+      eapply Rle_trans.
+      eapply Rplus_le_compat.
+      eapply Req_le; auto.
+      eapply Rplus_le_compat.
+      apply H3.
+      apply Req_le; auto.
+      rewrite (Rabs_mult (cst1 * delta0) _).
+      rewrite (Rabs_mult (cenv u * delta1) _).
+      rewrite (Rabs_mult cst1 delta).
+      rewrite (Rabs_mult (cenv u) delta).
+
+      (* Now prove interval bounds *)
+      unfold precondition in precond.
+      destruct precond.
+      assert (contained (cenv u) (mkInterval (-100) (100))) as uContained by (split; auto).
+      assert (contained (cst1) (mkInterval cst1 cst1)) as cst1Contained by (apply validPointInterval).
+      assert (contained (cenv u + cst1) (addInterval  (mkInterval (-100) (100)) (mkInterval cst1 cst1)))
+        as containedAdd
           by (apply additionIsValid; auto).
-      admit.
-Admitted.
+      unfold contained in *; simpl in *.
+      destruct uContained, cst1Contained, containedAdd.
+      assert (Rabs cst1 = cst1) by admit.
+      rewrite H17.
+      assert (cst1 * machineEpsilon + (Rabs (cenv u) * machineEpsilon +
+                                       (cst1 * machineEpsilon +
+                                        (Rabs cst1 * machineEpsilon) * machineEpsilon + (Rabs (cenv u) * machineEpsilon + Rabs (cenv u) * machineEpsilon) * machineEpsilon)) <=
+              errAddUCst)%R.
+      * rewrite H17.
+        assert (Rabs (cenv u) = 100)%R by admit (* FIXME: Upper bound! *).
+        rewrite H18.
+        unfold cst1, machineEpsilon, errAddUCst.
+        unfold realFromNum, negativePower.
+        field_simplify.
+        interval.
+      * admit.
+Admitted.
\ No newline at end of file