Commit 448e732c authored by Joachim Bard's avatar Joachim Bard

theorem almost finished

parent b55195aa
......@@ -14,7 +14,7 @@ From Flover
Infra.Ltacs Infra.RealSimps TypeValidator.
From Flover
Require Export SMTArith2 IntervalArith IntervalArithQ ssaPrgs RealRangeArith.
Require Export IntervalArithQ IntervalArith SMTArith2 ssaPrgs RealRangeArith.
Definition tightenLowerBound (e: expr Q) (lo: Q) (q: SMTLogic) P :=
match q with
......@@ -95,6 +95,24 @@ Proof.
exact H.
Qed.
Lemma tightenBounds_sound E Gamma e v iv qMap P :
eval_precond E P
-> (forall ql qh, FloverMap.find e qMap = Some (ql, qh) -> ~ eval_smt_logic E ql /\ ~ eval_smt_logic E qh)
-> eval_expr E (toRTMap (toRExpMap Gamma)) (toREval (toRExp e)) v REAL
-> (Q2R (fst iv) <= v <= Q2R (snd iv))%R
-> (Q2R (fst (tightenBounds e iv qMap P)) <= v <= Q2R (snd (tightenBounds e iv qMap P)))%R.
Proof.
intros H unsatQ ? ?. split.
- eapply tightenBounds_low_sound; try eassumption; [| lra].
intros. edestruct unsatQ; eauto.
- eapply tightenBounds_high_sound; try eassumption; [| lra].
intros. edestruct unsatQ; eauto.
Qed.
Lemma Rle_trans2 a b x y z :
(a <= x)%R -> (z <= b)%R -> (x <= y <= z)%R -> (a <= y <= b)%R.
Proof. lra. Qed.
Fixpoint validSMTIntervalbounds (e: expr Q) (A: analysisResult) (P: FloverMap.t intv)
(Q: FloverMap.t (SMTLogic * SMTLogic)) (validVars: NatSet.t) : bool:=
match FloverMap.find e A with
......@@ -261,37 +279,17 @@ Proof.
(a :=vF))
as inv_valid.
unfold invertInterval in inv_valid; cbn in *.
destruct inv_valid; try auto.
{ destruct nodiv0; rewrite <- Q2R0_is_0; [left | right]; apply Qlt_Rlt; auto. }
{ split.
- eapply Rle_trans; try apply L1.
apply (@tightenBounds_low_sound E Gamma); auto.
{ intros ql qh F. destruct (unsat_queries _ ql qh F). auto. }
cbn. rewrite Q2R_inv; auto.
destruct nodiv0; try lra.
hnf; intros.
assert (0 < Q2R (snd iv_f))%R.
{ eapply Rlt_le_trans.
apply Qlt_Rlt in H1.
rewrite <- Q2R0_is_0.
apply H1. lra.
}
rewrite <- Q2R0_is_0 in H3.
apply Rlt_Qlt in H3.
lra.
- eapply Rle_trans; try apply R.
apply (@tightenBounds_high_sound E Gamma); auto.
{ intros ql qh F. destruct (unsat_queries _ ql qh F). auto. }
cbn. rewrite Q2R_inv; try auto.
hnf; intros.
destruct nodiv0; try lra.
assert (Q2R (fst iv_f) < 0)%R.
{ rewrite <- Q2R0_is_0.
apply Qlt_Rlt in H2.
eapply Rle_lt_trans; try eauto.
lra. }
rewrite <- Q2R0_is_0 in H3.
apply Rlt_Qlt in H3. lra. }
eapply Rle_trans2; eauto.
eapply tightenBounds_sound; eauto.
cbn. rewrite ?Q2R_inv.
* apply inv_valid; auto.
destruct nodiv0; rewrite <- Q2R0_is_0; [left | right]; apply Qlt_Rlt; auto.
* hnf; intros. destruct nodiv0; try lra.
assert ((fst iv_f) < 0) by (apply Rlt_Qlt; apply Qlt_Rlt in H0; lra).
lra.
* hnf; intros. destruct nodiv0; try lra.
assert (0 < (snd iv_f)) by (apply Rlt_Qlt; apply Qlt_Rlt in H0; lra).
lra.
- destruct types_defined
as [? [? [[? [? ?]]?]]].
assert (validRanges f1 A E (toRTMap (toRExpMap Gamma))) as valid_f1
......@@ -307,67 +305,60 @@ Proof.
destruct valid_f2 as [iv_f2 [err2 [vF2 [env2 [eval_f2 valid_f2]]]]].
Flover_compute; try congruence.
kill_trivial_exists.
exists (perturb (evalBinop b vF1 vF2) REAL 0);
split; [destruct i; auto | ].
pose (v := perturb (evalBinop b vF1 vF2) REAL 0).
exists v.
assert (Heval: eval_expr E (toRTMap (toRExpMap Gamma)) (Binop b (toREval (toRExp f1)) (toREval (toRExp f2))) v REAL).
{ destruct b; cbn in *;
eapply Binop_dist' with (delta := 0%R); try congruence;
try rewrite Rabs_R0; cbn; try lra; try reflexivity; eauto.
andb_to_prop R. intros. rename L into nodiv0.
apply le_neq_bool_to_lt_prop in nodiv0.
hnf. destruct nodiv0 as [nodiv0 | nodiv0]; apply Qlt_Rlt in nodiv0;
rewrite Q2R0_is_0 in nodiv0; lra. }
split; [destruct i; auto | split; auto].
inversion env1; inversion env2; subst.
destruct b; cbn in *.
* split;
[eapply Binop_dist' with (delta := 0%R); eauto; try congruence;
try rewrite Rabs_R0; cbn; try auto; try lra|].
pose proof (interval_addition_valid ((Q2R (fst iv_f1)), Q2R (snd iv_f1))
destruct b; cbn in *.
* andb_to_prop R.
canonize_hyps.
pose proof (@interval_addition_valid ((Q2R (fst iv_f1)), Q2R (snd iv_f1))
(Q2R (fst iv_f2), Q2R (snd iv_f2)))
as valid_add.
specialize (valid_add vF1 vF2 valid_f1 valid_f2).
unfold isSupersetIntv in R.
andb_to_prop R.
cbn in *. unfold min4, max4 in valid_add.
rewrite <- ?Q2R_plus, ?Q2R_min, ?Q2R_max in valid_add.
eapply Rle_trans2; eauto.
eapply tightenBounds_sound; eauto.
* andb_to_prop R.
canonize_hyps; cbn in *.
repeat rewrite <- Q2R_plus in *;
rewrite <- Q2R_min4, <- Q2R_max4 in *.
unfold perturb. lra.
* split;
[eapply Binop_dist' with (delta := 0%R); eauto; try congruence;
try rewrite Rabs_R0; cbn; try auto; lra|].
pose proof (interval_subtraction_valid ((Q2R (fst iv_f1)), Q2R (snd iv_f1))
(Q2R (fst iv_f2), Q2R (snd iv_f2)))
as valid_sub.
specialize (valid_sub vF1 vF2 valid_f1 valid_f2).
unfold isSupersetIntv in R.
andb_to_prop R.
cbn in *. unfold min4, max4 in valid_sub.
rewrite <- ?Q2R_opp, <- ?Q2R_plus, ?Q2R_min, ?Q2R_max in valid_sub.
eapply Rle_trans2; eauto.
eapply tightenBounds_sound; eauto.
* andb_to_prop R.
canonize_hyps; cbn in *.
repeat rewrite <- Q2R_opp in *;
repeat rewrite <- Q2R_plus in *;
rewrite <- Q2R_min4, <- Q2R_max4 in *.
unfold perturb; lra.
* split;
[eapply Binop_dist' with (delta := 0%R); eauto; try congruence;
try rewrite Rabs_R0; cbn; try auto; lra|].
pose proof (interval_multiplication_valid ((Q2R (fst iv_f1)), Q2R (snd iv_f1))
(Q2R (fst iv_f2), Q2R (snd iv_f2)))
as valid_mul.
specialize (valid_mul vF1 vF2 valid_f1 valid_f2).
unfold isSupersetIntv in R.
andb_to_prop R.
canonize_hyps; cbn in *.
repeat rewrite <- Q2R_mult in *;
rewrite <- Q2R_min4, <- Q2R_max4 in *.
unfold perturb; lra.
cbn in *. unfold min4, max4 in valid_mul.
rewrite <- ?Q2R_mult, ?Q2R_min, ?Q2R_max in valid_mul.
eapply Rle_trans2; eauto.
eapply tightenBounds_sound; eauto.
* andb_to_prop R.
canonize_hyps.
apply le_neq_bool_to_lt_prop in L.
split;
[eapply Binop_dist' with (delta := 0%R); eauto; try congruence;
try rewrite Rabs_R0; cbn; try auto; try lra|].
(* No division by zero proof *)
{ hnf; intros.
destruct L as [L | L]; apply Qlt_Rlt in L; rewrite Q2R0_is_0 in L; lra. }
{ pose proof (interval_division_valid (a:=vF1) (b:=vF2)
pose proof (interval_division_valid (a:=vF1) (b:=vF2)
((Q2R (fst iv_f1)), Q2R (snd iv_f1))
(Q2R (fst iv_f2), Q2R (snd iv_f2)))
as valid_div.
cbn in *.
destruct valid_div; try auto.
- destruct L; rewrite <- Q2R0_is_0; [left | right]; apply Qlt_Rlt; auto.
- assert (~ (snd iv_f2) == 0).
{ destruct L; rewrite <- Q2R0_is_0; [left | right]; apply Qlt_Rlt; auto. }
assert (~ (snd iv_f2) == 0).
{ hnf; intros. destruct L; try lra.
assert (0 < (snd iv_f2)) by (apply Rlt_Qlt; apply Qlt_Rlt in H9; lra).
lra. }
......@@ -376,11 +367,10 @@ Proof.
assert ((fst iv_f2) < 0) by (apply Rlt_Qlt; apply Qlt_Rlt in H10; lra).
lra. }
repeat (rewrite <- Q2R_inv in *; try auto).
repeat rewrite <- Q2R_mult in *.
rewrite <- Q2R_min4, <- Q2R_max4 in *.
unfold perturb.
lra.
}
unfold min4, max4 in *.
rewrite <- ?Q2R_mult, ?Q2R_min, ?Q2R_max in *.
eapply Rle_trans2; eauto.
eapply tightenBounds_sound; eauto.
- destruct types_defined
as [mG [find_mg [[validt_f1 [validt_f2 [validt_f3 valid_join]]] valid_exec]]].
assert (validRanges f1 A E (toRTMap (toRExpMap Gamma))) as valid_f1
......@@ -401,8 +391,8 @@ Proof.
exists (perturb (evalFma vF1 vF2 vF3) REAL 0); split; try auto.
inversion env1; inversion env2; inversion env3; subst.
split; [auto | ].
* eapply Fma_dist' with (delta := 0%R); eauto; try congruence; cbn;
try rewrite Rabs_R0; try auto; lra.
* eapply Fma_dist' with (delta := 0%R); try congruence; cbn;
try rewrite Rabs_R0; try auto; try lra; eauto.
* pose proof (interval_multiplication_valid (Q2R (fst iv_f2),Q2R (snd iv_f2)) (Q2R (fst iv_f3), Q2R (snd iv_f3))) as valid_mul.
specialize (valid_mul vF2 vF3 valid_f2 valid_f3).
remember (multInterval (Q2R (fst iv_f2), Q2R (snd iv_f2)) (Q2R (fst iv_f3), Q2R (snd iv_f3))) as iv_f23prod.
......@@ -410,14 +400,11 @@ Proof.
rewrite Heqiv_f23prod in valid_add, valid_mul.
unfold multIntv in valid_add.
canonize_hyps.
cbn in *.
repeat rewrite <- Q2R_mult in *;
repeat rewrite <- Q2R_min4, <- Q2R_max4 in *;
repeat rewrite <- Q2R_plus in *;
repeat rewrite <- Q2R_min4, <- Q2R_max4 in *.
cbn in *. unfold min4, max4 in *.
rewrite <- ?Q2R_mult, ?Q2R_min , ?Q2R_max in *.
rewrite <- ?Q2R_plus, ?Q2R_min, ?Q2R_max in *.
specialize (valid_add vF1 (vF2 * vF3)%R valid_f1 valid_mul).
unfold evalFma, evalBinop, perturb.
lra.
eapply Rle_trans2; eauto.
- destruct types_defined
as [mG [find_mG [[validt_f _] _]]].
assert (validRanges f A E (toRTMap (toRExpMap Gamma))) as valid_f1
......@@ -433,6 +420,5 @@ Proof.
split; [eapply Downcast_dist'; try eauto; cbn; try rewrite Rabs_R0 |];
try lra; try auto.
canonize_hyps.
unfold perturb.
cbn in *; lra.
Abort.
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