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.