(** Precondition agreement checker and its soundness proof **) Require Import Coq.Reals.Reals Coq.Lists.List Coq.QArith.QArith. Require Import Flover.Infra.Abbrevs Flover.Expressions Flover.Infra.RationalSimps Flover.Infra.ExpressionAbbrevs Flover.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 (vprelo, vprehi) := P v 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 approximatesPrecond. - 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.