Start working on division

coq/Infra/RealRationalProps.v

@@ -9,8 +9,8 @@ Require Import Daisy.Infra.RationalSimps Daisy.Infra.Abbrevs Daisy.Expressions D
 
 Fixpoint toRExp (e:exp Q) :=
   match e with
-  |Var v => Var R v
-  |Param v => Param R v
+  |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.

coq/IntervalArith.v

@@ -3,7 +3,6 @@
   TODO: Package this into a class or module that depends only on proving the existence of basic operators instead
 **)
 Require Import Coq.Reals.Reals Coq.micromega.Psatz Coq.QArith.Qreals.
-Require Import Coquelicot.Rcomplements.
 Require Import Daisy.Infra.Abbrevs Daisy.Expressions Daisy.Infra.RealSimps.
 (**
   Define validity of an interval, requiring that the lower bound is less than or equal to the upper bound.
@@ -142,6 +141,29 @@ Qed.
 
 Definition invertInterval (intv:interval) := mkInterval (/ IVhi intv) (/ IVlo intv).
 
+Lemma interval_inversion_valid (iv:interval) (a:R) :
+  (IVhi iv < 0 \/ 0 < IVlo iv -> contained a iv -> contained (/ a) (invertInterval iv))%R.
+Proof.
+  unfold contained; destruct iv as [ivlo ivhi]; simpl;
+    intros [ivhi_lt_zero | zero_lt_ivlo]; intros [ivlo_le_a a_le_ivhi];
+      assert (ivlo <= ivhi)%R by (eapply Rle_trans; eauto);
+      split.
+  - assert (- / a <= - / ivhi)%R.
+    + assert (0 < - ivhi)%R by lra.
+      repeat rewrite Ropp_inv_permute; try lra.
+      eapply RIneq.Rinv_le_contravar; try lra.
+    + apply Ropp_le_ge_contravar in H0;
+        repeat rewrite Ropp_involutive in H0; lra.
+  - assert (- / ivlo <= - / a)%R.
+    +  repeat rewrite Ropp_inv_permute; try lra.
+       eapply RIneq.Rinv_le_contravar; try lra.
+    + apply Ropp_le_ge_contravar in H0;
+        repeat rewrite Ropp_involutive in H0; lra.
+  - eapply RIneq.Rinv_le_contravar; try lra.
+  - eapply RIneq.Rinv_le_contravar; try lra.
+Qed.
+
+
 Definition addInterval (iv1:interval) (iv2:interval) :=
   absIntvUpd Rplus iv1 iv2.
 
@@ -263,6 +285,16 @@ Qed.
 Definition divideInterval (I1:interval) (I2:interval) :=
   multInterval I1 (mkInterval (/ (IVhi I2)) (/ (IVlo I2))).
 
+Corollary divisionIsValid a b I1 I2:
+  (IVhi I2 < 0 \/ 0 < IVlo I2 -> contained a I1 -> contained b I2 -> contained (a / b) (divideInterval I1 I2))%R.
+Proof.
+  intros nodiv0 c_a c_b.
+  unfold divideInterval.
+  unfold Rdiv.
+  eapply interval_multiplication_valid; auto.
+  apply interval_inversion_valid; auto.
+Qed.
+
 (** Define the maxAbs function on R and prove some minor properties of it. **)
 Definition RmaxAbsFun (iv:interval) :=
   Rmax (Rabs (fst iv)) (Rabs (snd iv)).
@@ -338,14 +370,9 @@ Proof.
   intros contained_a abs_le; unfold contained in *; simpl in *.
   destruct contained_a as [lo_a a_hi].
   rewrite Rabs_minus_sym in abs_le.
-  apply Rcomplements.Rabs_le_between' in abs_le.
-  destruct abs_le as [lo_le le_hi].
-  split.
-  - eapply Rle_trans.
-    Focus 2. apply lo_le.
-    repeat rewrite Rsub_eq_Ropp_Rplus.
-    apply Rplus_le_compat_r; auto.
-  - eapply Rle_trans.
-    apply le_hi.
-    apply Rplus_le_compat_r; auto.
+  unfold Rabs in abs_le.
+  destruct Rcase_abs in abs_le.
+  - rewrite Ropp_minus_distr in abs_le.
+    split; lra.
+  - lra.
 Qed.

coq/IntervalArithQ.v

@@ -2,7 +2,7 @@
   Formalization of real valued intv arithmetic
   TODO: Package this into a class or module that depends only on proving the existence of basic operators instead
 **)
-Require Import Coq.QArith.QArith Coq.QArith.Qminmax.
+Require Import Coq.QArith.QArith Coq.QArith.Qminmax Coq.micromega.Psatz.
 Require Import Daisy.Infra.Abbrevs Daisy.Expressions Daisy.Infra.RationalSimps.
 (**
   Define validity of an intv, requiring that the lower bound is less than or equal to the upper bound.
@@ -156,6 +156,65 @@ Qed.
 
 Definition invertIntv (iv:intv) := mkIntv (/ ivhi iv) (/ ivlo iv).
 
+(*
+Lemma zero_not_contained_cases (iv:intv) :
+  ivlo iv <= ivhi iv -> ~ contained 0 iv -> ivhi iv < 0 \/ 0 < ivlo iv.
+Proof.
+  unfold contained; destruct iv as [lo hi]; simpl; intros.
+  hnf in H0; rewrite Decidable.not_and_iff in H0.
+  case_eq (lo ?= 0); case_eq (hi ?= 0); intros.
+  - exfalso.
+    rewrite <- Qeq_alt in H1, H2.
+    apply H0; [rewrite H2; auto | rewrite H1; auto]; apply Qle_refl.
+  - rewrite <- Qlt_alt in H1.
+    rewrite <- Qeq_alt in H2.
+    rewrite H2 in H.
+    exfalso.
+    apply Qle_not_lt in H; auto.
+  - rewrite <- Qgt_alt in H1.
+    rewrite <- Qeq_alt in H2.
+ *)
+Lemma Qinv_Qopp_compat (a:Q) :
+  / - a = - / a.
+Proof.
+  unfold Qinv.
+  case_eq (Qnum a); intros; unfold Qopp; rewrite H; simpl; auto.
+Qed.
+
+Lemma intv_inversion_valid (iv:intv) (a:Q) :
+  ivhi iv < 0 \/ 0 < ivlo iv -> contained a iv -> contained (/ a) (invertIntv iv).
+Proof.
+  unfold contained; destruct iv as [ivlo ivhi]; simpl;
+    intros [ivhi_lt_zero | zero_lt_ivlo]; intros [ivlo_le_a a_le_ivhi];
+      assert (ivlo <= ivhi) by (eapply Qle_trans; eauto);
+      split.
+  - assert (- / a <= - / ivhi).
+    + assert (0 < - ivhi) by lra.
+      repeat rewrite <- Qinv_Qopp_compat.
+      eapply Qle_shift_inv_l; try auto.
+      assert (- ivhi <= - a) by lra.
+      apply (Qmult_le_r _ 1 (- a)); try lra.
+      rewrite Qmult_1_l.
+      setoid_rewrite Qmult_comm at 1.
+      rewrite Qmult_assoc.
+      rewrite Qmult_inv_r; lra.
+    + apply Qopp_le_compat in H0;
+        repeat rewrite Qopp_involutive in H0; auto.
+  - assert (- / ivlo <= - / a).
+    +  repeat rewrite <- Qinv_Qopp_compat.
+       eapply Qle_shift_inv_l; try lra.
+       apply (Qmult_le_r _ _ (- ivlo)); try lra.
+       rewrite Qmult_comm, Qmult_assoc, Qmult_inv_r, Qmult_1_l; lra.
+    + apply Qopp_le_compat in H0.
+      repeat rewrite Qopp_involutive in H0; auto.
+  - apply Qle_shift_inv_l; try lra.
+    apply (Qmult_le_r _ _ (ivhi)); try lra.
+    rewrite Qmult_comm, Qmult_assoc, Qmult_inv_r, Qmult_1_l; lra.
+  - apply Qle_shift_inv_l; try lra.
+    apply (Qmult_le_r _ _ a); try lra.
+    rewrite Qmult_comm, Qmult_assoc, Qmult_inv_r, Qmult_1_l; lra.
+Qed.
+
 Definition addIntv (iv1:intv) (iv2:intv) :=
   absIvUpd Qplus iv1 iv2.
 
@@ -286,4 +345,13 @@ Proof.
 Qed.
 
 Definition divideIntv (I1:intv) (I2:intv) :=
-  multIntv I1 (mkIntv (/ (ivhi I2)) (/ (ivlo I2))).
+  multIntv I1 (mkIntv (/ (ivhi I2)) (/ (ivlo I2))).
\ No newline at end of file
+
+Corollary divisionIsValid a b (I1:intv) (I2:intv) :
+  ivhi I2 < 0 \/ 0 < ivlo I2 -> contained a I1 -> contained b I2 -> contained (a / b) (divideIntv I1 I2).
+Proof.
+  intros nodiv0 c_a c_b.
+  pose proof (intv_inversion_valid I2 b nodiv0 c_b).
+  unfold divideIntv, Qdiv.
+  apply intv_multiplication_valid; auto.
+Qed.
\ No newline at end of file

coq/IntervalValidation.v

@@ -38,7 +38,10 @@ Fixpoint validIntervalbounds (e:exp Q) (absenv:analysisResult) (P:precond):=
           | Mult =>
             let new_iv := multIntv iv1 iv2 in
             isSupersetIntv new_iv intv
-          | Div => false
+          | Div =>
+            let nodiv0 := orb (Qleb (ivhi iv2) 0) (Qleb 0 (ivlo iv2)) in
+            let new_iv := divideIntv iv1 iv2 in
+            isSupersetIntv new_iv intv
           end
       in
       andb rec opres
@@ -75,7 +78,6 @@ Proof.
       apply Is_true_eq_true; auto.
 Qed.
 
-
 Corollary Q2R_max4 a b c d:
   Q2R (IntervalArithQ.max4 a b c d) = max4 (Q2R a) (Q2R b) (Q2R c) (Q2R d).
 Proof.
@@ -257,5 +259,5 @@ Proof.
         repeat rewrite <- Q2R_mult in valid_mul_hi.
         rewrite <- Q2R_max4 in valid_mul_hi.
         unfold absIvUpd; auto.
-    + contradiction.
+    + pose proof (divisionIsValid (Q2R v1) v2 (Q2R (fst iv1), Q2R (snd iv1)) (Q2R (fst iv2),Q2R (snd iv2))) as valid_div.  contradiction.
 Qed.
\ No newline at end of file