(** Interval arithmetic checker and its soundness proof Explained in section 4 of the paper, used in CertificateChecker.v to build full checker, **) Require Import Coq.QArith.QArith Coq.QArith.Qreals QArith.Qminmax Coq.Lists.List Coq.micromega.Psatz. Require Import Daisy.Infra.Abbrevs Daisy.Infra.RationalSimps Daisy.Infra.RealRationalProps. Require Import Daisy.Infra.ExpressionAbbrevs Daisy.IntervalArithQ Daisy.IntervalArith Daisy.Infra.RealSimps. 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 validIntervalbounds (e:exp Q) (absenv:analysisResult) (P:precond):= let (intv, _) := absenv e in match e with | Var _ v => false | Param _ v => isSupersetIntv (P v) intv | Const n => isSupersetIntv (n,n) intv | 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 => let nodiv0 := orb (andb (Qleb (ivhi iv2) 0) (negb (Qeq_bool (ivhi iv2) 0))) (andb (Qleb 0 (ivlo iv2)) (negb (Qeq_bool (ivlo iv2) 0))) in let new_iv := divideIntv iv1 iv2 in andb (isSupersetIntv new_iv intv) nodiv0 end in andb rec opres end. Theorem ivbounds_approximatesPrecond_sound e absenv P: validIntervalbounds 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 validIntervalbounds. - 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. apply Is_true_eq_left in approx_bin_true. destruct (absenv (Binop b e1 e2)); destruct (absenv e1); destruct (absenv e2); simpl in *. apply andb_prop_elim in approx_bin_true. destruct approx_bin_true. apply andb_prop_elim in H. destruct H. 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. Corollary Q2R_max4 a b c d: Q2R (IntervalArithQ.max4 a b c d) = max4 (Q2R a) (Q2R b) (Q2R c) (Q2R d). Proof. unfold IntervalArithQ.max4, max4; repeat rewrite Q2R_max; auto. Qed. Corollary Q2R_min4 a b c d: Q2R (IntervalArithQ.min4 a b c d) = min4 (Q2R a) (Q2R b) (Q2R c) (Q2R d). Proof. unfold IntervalArith.min4, min4; repeat rewrite Q2R_min; auto. Qed. Ltac env_assert absenv e name := assert (exists iv err, absenv e = (iv,err)) as name by (destruct (absenv e); repeat eexists; auto). Lemma validBoundsDiv_uneq_zero e1 e2 absenv P ivlo_e2 ivhi_e2 err: absenv e2 = ((ivlo_e2,ivhi_e2), err) -> validIntervalbounds (Binop Div e1 e2) absenv P = true -> (ivhi_e2 < 0) \/ (0 < ivlo_e2). Proof. intros absenv_eq validBounds. unfold validIntervalbounds in validBounds. env_assert absenv (Binop Div e1 e2) abs_div; destruct abs_div as [iv_div [err_div abs_div]]. env_assert absenv e1 abs_e1; destruct abs_e1 as [iv_e1 [err_e1 abs_e1]]. rewrite abs_div, abs_e1, absenv_eq in validBounds. apply Is_true_eq_left in validBounds. apply andb_prop_elim in validBounds. destruct validBounds as [_ validBounds]; apply andb_prop_elim in validBounds. destruct validBounds as [_ nodiv0]. apply orb_prop_elim in nodiv0. destruct nodiv0 as [lt_0 | lt_0]; apply andb_prop_elim in lt_0; destruct lt_0 as [le_0 neq_0]; apply Is_true_eq_true in le_0; apply Is_true_eq_true in neq_0; apply negb_true_iff in neq_0; apply Qeq_bool_neq in neq_0; rewrite Qle_bool_iff in le_0; rewrite Qle_lteq in le_0; destruct le_0 as [lt_0 | eq_0]; [ | exfalso; apply neq_0; auto | | exfalso; apply neq_0; symmetry; auto]; auto. Qed. Theorem validIntervalbounds_sound (e:exp Q): forall (absenv:analysisResult) (P:precond) cenv vR, precondValidForExec P cenv -> validIntervalbounds e absenv P = true -> eval_exp 0%R cenv (toRExp e) vR -> (Q2R (fst (fst(absenv e))) <= vR <= Q2R (snd (fst (absenv e))))%R. Proof. induction e. - intros absenv P cenv vR precond_valid valid_bounds eval_e. pose proof (ivbounds_approximatesPrecond_sound (Var Q n) absenv P valid_bounds) as env_approx_p. unfold validIntervalbounds in valid_bounds. destruct (absenv (Var Q n)); inversion valid_bounds. - intros absenv P cenv vR precond_valid valid_bounds eval_e. pose proof (ivbounds_approximatesPrecond_sound (Param Q n) absenv P valid_bounds) as env_approx_p. unfold validIntervalbounds in valid_bounds. assert (exists intv err, absenv (Param Q n) = (intv,err)) as absenv_n by (destruct (absenv (Param Q n)); repeat eexists; auto). destruct absenv_n as [intv [err absenv_n]]. rewrite absenv_n in valid_bounds. unfold precondValidForExec in precond_valid. specialize (env_approx_p n). assert (exists ivlo ivhi, P n = (ivlo, ivhi)) as p_n by (destruct (P n); repeat eexists; auto). destruct p_n as [ivlo [ivhi p_n]]. unfold isSupersetIntv, freeVars in env_approx_p. assert (In n (n::nil)) by (unfold In; auto). specialize (env_approx_p H). rewrite p_n, absenv_n in env_approx_p. specialize (precond_valid n); rewrite p_n in precond_valid. inversion eval_e; subst. rewrite absenv_n; simpl. rewrite perturb_0_val; auto. destruct intv as [abslo abshi]; simpl in *. apply andb_prop_elim in env_approx_p. destruct env_approx_p as [abslo_le_ivlo ivhi_le_abshi]. destruct precond_valid as [ivlo_le_env env_le_ivhi]. apply Is_true_eq_true in abslo_le_ivlo; apply Is_true_eq_true in ivhi_le_abshi. unfold Qleb in abslo_le_ivlo, ivhi_le_abshi. apply Qle_bool_iff in abslo_le_ivlo; apply Qle_bool_iff in ivhi_le_abshi. apply Qle_Rle in abslo_le_ivlo; apply Qle_Rle in ivhi_le_abshi. split. + eapply Rle_trans. apply abslo_le_ivlo. apply ivlo_le_env. + eapply Rle_trans. apply env_le_ivhi. apply ivhi_le_abshi. - intros absenv P cenv vR valid_precond valid_bounds eval_e. pose proof (ivbounds_approximatesPrecond_sound (Const v) absenv P valid_bounds) as env_approx_p. unfold validIntervalbounds in valid_bounds. destruct (absenv (Const v)) as [intv err]. simpl. apply Is_true_eq_left in valid_bounds. apply andb_prop_elim in valid_bounds. destruct valid_bounds as [valid_lo valid_hi]. inversion eval_e; subst. rewrite perturb_0_val; auto. unfold contained; simpl. split. + apply Is_true_eq_true in valid_lo. unfold Qleb in *. apply Qle_bool_iff in valid_lo. apply Qle_Rle in valid_lo; auto. + apply Is_true_eq_true in valid_hi. unfold Qleb in *. apply Qle_bool_iff in valid_hi. apply Qle_Rle in valid_hi; auto. - intros absenv P cenv vR valid_precond valid_bounds eval_e; inversion eval_e; subst. pose proof (ivbounds_approximatesPrecond_sound (Binop b e1 e2) absenv P valid_bounds) as env_approx_p. rewrite perturb_0_val in eval_e; auto. rewrite perturb_0_val; auto. simpl in valid_bounds. env_assert absenv (Binop b e1 e2) absenv_bin. env_assert absenv e1 absenv_e1. env_assert absenv e2 absenv_e2. destruct absenv_bin as [iv [err absenv_bin]]; rewrite absenv_bin in valid_bounds; rewrite absenv_bin. destruct absenv_e1 as [iv1 [err1 absenv_e1]]; rewrite absenv_e1 in valid_bounds. destruct absenv_e2 as [iv2 [err2 absenv_e2]]; rewrite absenv_e2 in valid_bounds. apply Is_true_eq_left in valid_bounds. apply andb_prop_elim in valid_bounds. destruct valid_bounds as [valid_rec valid_bin]. apply andb_prop_elim in valid_rec. destruct valid_rec as [valid_e1 valid_e2]. apply Is_true_eq_true in valid_e1; apply Is_true_eq_true in valid_e2. specialize (IHe1 absenv P cenv v1 valid_precond valid_e1 H4); specialize (IHe2 absenv P cenv v2 valid_precond valid_e2 H5). rewrite absenv_e1 in IHe1. rewrite absenv_e2 in IHe2. destruct b; simpl in *. + pose proof (additionIsValid (Q2R (fst iv1),Q2R (snd iv1)) (Q2R (fst iv2), Q2R (snd iv2))) as valid_add. unfold validIntervalAdd in valid_add. specialize (valid_add v1 v2 IHe1 IHe2). unfold contained in valid_add. unfold isSupersetIntv in valid_bin. apply andb_prop_elim in valid_bin; destruct valid_bin as [valid_lo valid_hi]. apply Is_true_eq_true in valid_lo; apply Is_true_eq_true in valid_hi. apply Qle_bool_iff in valid_lo; apply Qle_bool_iff in valid_hi. apply Qle_Rle in valid_lo; apply Qle_Rle in valid_hi. destruct valid_add as [valid_add_lo valid_add_hi]. split. { eapply Rle_trans. apply valid_lo. unfold ivlo. unfold addIntv. simpl in valid_add_lo. repeat rewrite <- Q2R_plus in valid_add_lo. rewrite <- Q2R_min4 in valid_add_lo. unfold absIvUpd; auto. } { eapply Rle_trans. Focus 2. apply valid_hi. unfold ivlo, addIntv. simpl in valid_add_hi. repeat rewrite <- Q2R_plus in valid_add_hi. rewrite <- Q2R_max4 in valid_add_hi. unfold absIvUpd; auto. } + pose proof (subtractionIsValid (Q2R (fst iv1),Q2R (snd iv1)) (Q2R (fst iv2), Q2R (snd iv2))) as valid_sub. specialize (valid_sub v1 v2 IHe1 IHe2). unfold contained in valid_sub. unfold isSupersetIntv in valid_bin. apply andb_prop_elim in valid_bin; destruct valid_bin as [valid_lo valid_hi]. apply Is_true_eq_true in valid_lo; apply Is_true_eq_true in valid_hi. apply Qle_bool_iff in valid_lo; apply Qle_bool_iff in valid_hi. apply Qle_Rle in valid_lo; apply Qle_Rle in valid_hi. destruct valid_sub as [valid_sub_lo valid_sub_hi]. split. * eapply Rle_trans. apply valid_lo. unfold ivlo. unfold subtractIntv. simpl in valid_sub_lo. repeat rewrite <- Rsub_eq_Ropp_Rplus in valid_sub_lo. repeat rewrite <- Q2R_minus in valid_sub_lo. rewrite <- Q2R_min4 in valid_sub_lo. unfold absIvUpd; auto. * eapply Rle_trans. Focus 2. apply valid_hi. unfold ivlo, addIntv. simpl in valid_sub_hi. repeat rewrite <- Rsub_eq_Ropp_Rplus in valid_sub_hi. repeat rewrite <- Q2R_minus in valid_sub_hi. rewrite <- Q2R_max4 in valid_sub_hi. unfold absIvUpd; auto. + pose proof (interval_multiplication_valid (Q2R (fst iv1),Q2R (snd iv1)) (Q2R (fst iv2), Q2R (snd iv2))) as valid_mul. specialize (valid_mul v1 v2 IHe1 IHe2). unfold contained in valid_mul. unfold isSupersetIntv in valid_bin. apply andb_prop_elim in valid_bin; destruct valid_bin as [valid_lo valid_hi]. apply Is_true_eq_true in valid_lo; apply Is_true_eq_true in valid_hi. apply Qle_bool_iff in valid_lo; apply Qle_bool_iff in valid_hi. apply Qle_Rle in valid_lo; apply Qle_Rle in valid_hi. destruct valid_mul as [valid_mul_lo valid_mul_hi]. split. * eapply Rle_trans. apply valid_lo. unfold ivlo. unfold multIntv. simpl in valid_mul_lo. repeat rewrite <- Q2R_mult in valid_mul_lo. rewrite <- Q2R_min4 in valid_mul_lo. unfold absIvUpd; auto. * eapply Rle_trans. Focus 2. apply valid_hi. unfold ivlo, addIntv. simpl in valid_mul_hi. repeat rewrite <- Q2R_mult in valid_mul_hi. rewrite <- Q2R_max4 in valid_mul_hi. unfold absIvUpd; auto. + pose proof (divisionIsValid v1 v2 (Q2R (fst iv1), Q2R (snd iv1)) (Q2R (fst iv2),Q2R (snd iv2))) as valid_div. unfold contained in valid_div. unfold isSupersetIntv in valid_bin. apply andb_prop_elim in valid_bin; destruct valid_bin as [valid_bin nodiv0]. apply andb_prop_elim in valid_bin; destruct valid_bin as [valid_lo valid_hi]. apply Is_true_eq_true in valid_lo; apply Is_true_eq_true in valid_hi. apply Qle_bool_iff in valid_lo; apply Qle_bool_iff in valid_hi. apply Qle_Rle in valid_lo; apply Qle_Rle in valid_hi. apply orb_prop_elim in nodiv0. assert (snd iv2 < 0 \/ 0 < fst iv2). * destruct nodiv0 as [lt_0 | lt_0]; apply andb_prop_elim in lt_0; destruct lt_0 as [le_0 neq_0]; apply Is_true_eq_true in le_0; apply Is_true_eq_true in neq_0; apply negb_true_iff in neq_0; apply Qeq_bool_neq in neq_0; rewrite Qle_bool_iff in le_0; rewrite Qle_lteq in le_0; destruct le_0 as [lt_0 | eq_0]; [ | exfalso; apply neq_0; auto | | exfalso; apply neq_0; symmetry; auto]; auto. * destruct valid_div as [valid_div_lo valid_div_hi]; simpl; try auto. { rewrite <- Q2R0_is_0. destruct H; [left | right]; apply Qlt_Rlt; auto. } { unfold divideInterval, IVlo, IVhi in valid_div_lo, valid_div_hi. simpl in *. assert (Q2R (fst iv2) <= (Q2R (snd iv2)))%R by lra. assert (~ snd iv2 == 0). - destruct H; try lra. hnf; intros ivhi2_0. apply Rle_Qle in H0. rewrite ivhi2_0 in H0. lra. - assert (~ fst iv2 == 0). + destruct H; try lra. hnf; intros ivlo2_0. apply Rle_Qle in H0. rewrite ivlo2_0 in H0. lra. + split. * eapply Rle_trans. apply valid_lo. unfold ivlo. unfold multIntv. simpl in valid_div_lo. rewrite <- Q2R_inv in valid_div_lo; [ | auto]. rewrite <- Q2R_inv in valid_div_lo; [ | auto]. repeat rewrite <- Q2R_mult in valid_div_lo. rewrite <- Q2R_min4 in valid_div_lo; auto. * eapply Rle_trans. Focus 2. apply valid_hi. simpl in valid_div_hi. rewrite <- Q2R_inv in valid_div_hi; [ | auto]. rewrite <- Q2R_inv in valid_div_hi; [ | auto]. repeat rewrite <- Q2R_mult in valid_div_hi. rewrite <- Q2R_max4 in valid_div_hi; auto. } Qed.