Add unverified interval validation, division unsupported

coq/IntervalArithQ.v

@@ -25,16 +25,24 @@ Qed.
   Subset definition; when an intv is a subintv of another
 **)
 Definition isSupersetIntv (iv1:intv) (iv2:intv) :=
-  (ivlo iv2 <= ivlo iv1)%Q /\ (ivhi iv1 <= ivhi iv2)%Q.
+  andb (Qleb (ivlo iv2) (ivlo iv1)) (Qleb (ivhi iv1) (ivhi iv2)).
 
 Definition pointIntv (x:Q) := mkIntv x x.
 
 Lemma contained_implies_subset (x:Q) (iv:intv):
   contained x iv ->
-  isSupersetIntv (pointIntv x) iv.
+  isSupersetIntv (pointIntv x) iv = true.
 Proof.
   intros containedIv.
-  unfold contained, isSupersetIntv, pointIntv in *; destruct containedIv; split; auto.
+  unfold contained, isSupersetIntv, pointIntv in *; destruct containedIv.
+  apply Is_true_eq_true. apply andb_prop_intro.
+  split.
+  - apply Qle_bool_iff in H.
+    unfold Qleb; simpl in *.
+    rewrite H; unfold Is_true; auto.
+  - apply Qle_bool_iff in H0.
+    unfold Qleb; simpl in *.
+    rewrite H0. unfold Is_true; auto.
 Qed.
 
 (**
@@ -171,13 +179,13 @@ Proof.
     apply (Qle_trans _ (snd iv1 + snd iv2) _); [ apply Qle_refl; auto | Qmax_r].
 Qed.
 
-Definition substractIntv (I1:intv) (I2:intv) :=
+Definition subtractIntv (I1:intv) (I2:intv) :=
   addIntv I1 (negateIntv I2).
 
 Corollary subtractionIsValid iv1 iv2:
-  validIntvSub iv1 iv2 (substractIntv iv1 iv2).
+  validIntvSub iv1 iv2 (subtractIntv iv1 iv2).
 Proof.
-  unfold substractIntv.
+  unfold subtractIntv.
   intros a b.
   intros contained_1 contained_I2.
   rewrite Qsub_eq_Qopp_Qplus.

coq/IntervalValidation.v

+Require Import Coq.QArith.QArith.
+Require Import Daisy.Expressions Daisy.Infra.Abbrevs Daisy.Infra.RationalSimps Daisy.IntervalArithQ Daisy.Infra.RationalConstruction.
+
+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 (Qeqb (fst intv) (fst (bounds_v))) (Qeqb (snd intv) (snd (bounds_v)))
+    | Param v =>
+      let bounds_v := P v in
+      andb (Qeq_bool (fst intv) (fst (bounds_v))) (Qeq_bool (snd intv) (snd (bounds_v)))
+    | Const n =>
+      andb (Qleb (fst intv) n) (Qleb (snd intv) n)
+    | Binop b e1 e2 =>
+      let rec := andb (validIntervalbounds e1 absenv P) (validIntervalbounds e2 absenv P) in
+      let (iv1,_) := absenv e1 in
+      let (iv2,_) := absenv e2 in
+      let opres :=
+          match b with
+          | Plus =>
+            let new_iv := addIntv iv1 iv2 in
+            isSupersetIntv new_iv intv
+          | Sub =>
+            let new_iv := subtractIntv iv1 iv2 in
+            isSupersetIntv new_iv intv
+          | Mult =>
+            let new_iv := multIntv iv1 iv2 in
+            isSupersetIntv new_iv intv
+          | Div => false
+          end
+      in
+      andb rec opres
+    end.
+
+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