Add precondition validator and soundness proof for it

coq/PreconditionValidation.v

+Require Import Coq.Reals.Reals Coq.Lists.List Coq.QArith.QArith.
+Require Import Daisy.Infra.Abbrevs Daisy.Expressions Daisy.Infra.RationalSimps Daisy.Infra.ExpressionAbbrevs Daisy.IntervalArithQ.
+
+Import Lists.List.ListNotations.
+
+Fixpoint freeVars (V:Type) (e:exp V) : list nat:=
+  match e with
+  |Const n => []
+  |Var v => []
+  |Param v => [v]
+  |Binop b e1 e2 => (freeVars V e1) ++ (freeVars V e2)
+  end.
+
+Fixpoint approximatesPrecond (e:exp Q) (absenv:analysisResult) (P:precond) :=
+  match e with
+  |Const n => true
+  |Var v => true
+  |Param v =>
+   let iv_pre := P v in
+   let (vprelo, vprehi) := iv_pre in
+   let (iv,err) := absenv (Param Q v) in
+   let (vlo,vhi) := iv in
+   andb (Qleb vlo vprelo) (Qleb vprehi vhi)
+  |Binop b e1 e2 => andb (approximatesPrecond e1 absenv P) (approximatesPrecond e2 absenv P)
+  end.
+
+Theorem approximatesPrecond_sound e absenv P:
+  approximatesPrecond e absenv P = true ->
+  forall v, In v (freeVars Q e) ->
+       Is_true(isSupersetIntv (P v) (fst (absenv (Param Q v)))).
+Proof.
+  induction e; unfold envApproximatesPrecond.
+  - intros approx_true v v_in_fV; simpl in *; contradiction.
+  - intros approx_true v v_in_fV; simpl in *.
+    unfold isSupersetIntv.
+    destruct v_in_fV; try contradiction.
+    subst.
+    destruct (P v); destruct (absenv (Param Q v)); simpl in *.
+    destruct i; simpl in *.
+    apply Is_true_eq_left in approx_true; auto.
+  - intros approx_true v0 v_in_fV; simpl in *; contradiction.
+  - intros approx_bin_true v v_in_fV.
+    unfold freeVars in v_in_fV.
+    apply in_app_or in v_in_fV.
+    unfold approximatesPrecond in approx_bin_true.
+    apply Is_true_eq_left in approx_bin_true.
+    apply andb_prop_elim in approx_bin_true.
+    destruct approx_bin_true.
+    destruct v_in_fV as [v_in_fV_e1 | v_in_fV_e2].
+    + apply IHe1; auto.
+      apply Is_true_eq_true; auto.
+    + apply IHe2; auto.
+      apply Is_true_eq_true; auto.
+Qed.