Commit 2ae8fcbd authored by Joachim Bard's avatar Joachim Bard

simplified soundness proof of SMT interval checker

parent 4f514011
......@@ -14,7 +14,7 @@ From Flover
Infra.Ltacs Infra.RealSimps TypeValidator.
From Flover
Require Export IntervalArithQ IntervalArith SMTArith ssaPrgs RealRangeArith.
Require Export IntervalArithQ IntervalArith IntervalValidation SMTArith ssaPrgs RealRangeArith.
Definition tightenLowerBound (e: expr Q) (lo: Q) (q: SMTLogic) P :=
match q with
......@@ -324,8 +324,8 @@ Proof.
(Q2R (fst iv_f2), Q2R (snd iv_f2)))
as valid_add.
specialize (valid_add vF1 vF2 valid_f1 valid_f2).
cbn in *. unfold min4, max4 in valid_add.
rewrite <- ?Q2R_plus, ?Q2R_min, ?Q2R_max in valid_add.
cbn in *.
rewrite <- ?Q2R_plus, <- ?Q2R_min4, <- ?Q2R_max4 in valid_add.
eapply Rle_trans2; eauto.
eapply tightenBounds_sound; eauto.
* andb_to_prop R.
......@@ -334,8 +334,8 @@ Proof.
(Q2R (fst iv_f2), Q2R (snd iv_f2)))
as valid_sub.
specialize (valid_sub vF1 vF2 valid_f1 valid_f2).
cbn in *. unfold min4, max4 in valid_sub.
rewrite <- ?Q2R_opp, <- ?Q2R_plus, ?Q2R_min, ?Q2R_max in valid_sub.
cbn in *.
rewrite <- ?Q2R_opp, <- ?Q2R_plus, <- ?Q2R_min4, <- ?Q2R_max4 in valid_sub.
eapply Rle_trans2; eauto.
eapply tightenBounds_sound; eauto.
* andb_to_prop R.
......@@ -344,8 +344,8 @@ Proof.
(Q2R (fst iv_f2), Q2R (snd iv_f2)))
as valid_mul.
specialize (valid_mul vF1 vF2 valid_f1 valid_f2).
cbn in *. unfold min4, max4 in valid_mul.
rewrite <- ?Q2R_mult, ?Q2R_min, ?Q2R_max in valid_mul.
cbn in *.
rewrite <- ?Q2R_mult, <- ?Q2R_min4, <- ?Q2R_max4 in valid_mul.
eapply Rle_trans2; eauto.
eapply tightenBounds_sound; eauto.
* andb_to_prop R.
......@@ -367,8 +367,7 @@ Proof.
assert ((fst iv_f2) < 0) by (apply Rlt_Qlt; apply Qlt_Rlt in H10; lra).
lra. }
repeat (rewrite <- Q2R_inv in *; try auto).
unfold min4, max4 in *.
rewrite <- ?Q2R_mult, ?Q2R_min, ?Q2R_max in *.
rewrite <- ?Q2R_mult, <- ?Q2R_min4, <- ?Q2R_max4 in *.
eapply Rle_trans2; eauto.
eapply tightenBounds_sound; eauto.
- destruct types_defined
......@@ -400,9 +399,9 @@ Proof.
rewrite Heqiv_f23prod in valid_add, valid_mul.
unfold multIntv in valid_add.
canonize_hyps.
cbn in *. unfold min4, max4 in *.
rewrite <- ?Q2R_mult, ?Q2R_min , ?Q2R_max in *.
rewrite <- ?Q2R_plus, ?Q2R_min, ?Q2R_max in *.
cbn in *.
rewrite <- ?Q2R_mult, <- ?Q2R_min4 , <- ?Q2R_max4 in *.
rewrite <- ?Q2R_plus, <- ?Q2R_min4, <- ?Q2R_max4 in *.
specialize (valid_add vF1 (vF2 * vF3)%R valid_f1 valid_mul).
eapply Rle_trans2; eauto.
- destruct types_defined
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment