Commit b55195aa authored by Joachim Bard's avatar Joachim Bard

finished proof for invert expr, i.e. 1 / expr

parent 42fa192a
......@@ -14,26 +14,87 @@ From Flover
Infra.Ltacs Infra.RealSimps TypeValidator.
From Flover
Require Export SMTArith2 IntervalArithQ ssaPrgs RealRangeArith.
Require Export SMTArith2 IntervalArith IntervalArithQ ssaPrgs RealRangeArith.
Definition tightenLowerBound (e: expr Q) (lo: Q) (q: SMTLogic) P :=
match getBound q, getPrecond q with
| Some (LessQ e' (ConstQ v)), Some qP => if checkPre P qP && smt_expr_eq e' e then Qmax lo v else lo
| _, _ => lo
match q with
| AndQ qP (AndQ (LessQ e' (ConstQ v)) TrueQ) => if checkPre P qP && smt_expr_eq e' e then Qmax lo v else lo
| _ => lo
end.
Definition tightenUpperBound (e: expr Q) (hi: Q) (q: SMTLogic) P :=
match getBound q, getPrecond q with
| Some (LessQ (ConstQ v) e'), Some qP => if checkPre P qP && smt_expr_eq e' e then Qmin hi v else hi
| _, _ => hi
match q with
| AndQ qP (AndQ (LessQ (ConstQ v) e') TrueQ) => if checkPre P qP && smt_expr_eq e' e then Qmin hi v else hi
| _ => hi
end.
Definition tightenBounds (e: expr Q) (iv: intv) (qMap: FloverMap.t (SMTLogic * SMTLogic)) P :=
match FloverMap.find e qMap, iv with
| None, _ => iv
| Some (loQ, hiQ), (lo, hi) => (tightenLowerBound e lo loQ P, tightenUpperBound e hi hiQ P)
match FloverMap.find e qMap with
| None => iv
| Some (loQ, hiQ) => (tightenLowerBound e (fst iv) loQ P, tightenUpperBound e (snd iv) hiQ P)
end.
(* TODO: debug this ltac *)
Ltac query_simpl :=
match goal with
| [ |- context[match ?q with | _ => _ end ]] => fail; destruct q; query_simpl
| _ => idtac
end.
Lemma tightenBounds_low_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_expr E (toRTMap (toRExpMap Gamma)) (toREval (toRExp e)) v REAL
-> (Q2R (fst iv) <= v)%R
-> (Q2R (fst (tightenBounds e iv qMap P)) <= v)%R.
Proof.
intros prec_valid unsatQ H Hlo.
unfold tightenBounds.
destruct (FloverMap.find e qMap) as [[q ?]|]; auto.
cbn. unfold tightenLowerBound.
destruct q; auto. cbn.
destruct q2; auto.
destruct q2_1; auto.
destruct e2; auto.
destruct q2_2; auto.
remember (checkPre P q1 && smt_expr_eq e1 e) as b eqn: Hchk.
destruct b; auto.
symmetry in Hchk.
andb_to_prop Hchk.
rewrite <- Q2R_max. apply Rmax_lub; auto.
eapply RangeBound_low_sound; eauto.
erewrite eval_smt_expr_complete in H; eauto.
rewrite SMTArith2Expr_exact.
exact H.
Qed.
Lemma tightenBounds_high_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 qh)
-> eval_expr E (toRTMap (toRExpMap Gamma)) (toREval (toRExp e)) v REAL
-> (v <= Q2R (snd iv))%R
-> (v <= Q2R (snd (tightenBounds e iv qMap P)))%R.
Proof.
intros prec_valid unsatQ H Hlo.
unfold tightenBounds.
destruct (FloverMap.find e qMap) as [[q ?]|]; auto.
cbn. unfold tightenUpperBound.
destruct s; auto.
destruct s2; auto.
destruct s2_1; auto.
destruct e1; auto.
destruct s2_2; auto.
remember (checkPre P s1 && smt_expr_eq e2 e) as b eqn: Hchk.
destruct b; auto.
symmetry in Hchk.
andb_to_prop Hchk.
rewrite <- Q2R_min. apply Rmin_glb; auto.
eapply RangeBound_high_sound; eauto.
erewrite eval_smt_expr_complete in H; eauto.
rewrite SMTArith2Expr_exact.
exact H.
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
......@@ -186,25 +247,27 @@ Proof.
+ rename L0 into nodiv0.
apply le_neq_bool_to_lt_prop in nodiv0.
kill_trivial_exists.
exists (perturb (evalUnop Inv vF) REAL 0); split;
[destruct i; auto | split].
* econstructor; eauto.
{ auto. }
{ cbn. rewrite Rabs_R0; lra. }
(* Absence of division by zero *)
{ hnf. destruct nodiv0 as [nodiv0 | nodiv0]; apply Qlt_Rlt in nodiv0;
pose (v := (perturb (evalUnop Inv vF) REAL 0)).
exists v.
assert (Heval: eval_expr E (toRTMap (toRExpMap Gamma)) (Unop Inv (toREval (toRExp f))) v REAL).
{ econstructor; eauto.
- auto.
- cbn. rewrite Rabs_R0. lra.
- hnf. destruct nodiv0 as [nodiv0 | nodiv0]; apply Qlt_Rlt in nodiv0;
rewrite Q2R0_is_0 in nodiv0; lra. }
* canonize_hyps. unfold tightenBounds in *. Flover_compute.
{ admit. }
split; [destruct i; auto | split; auto].
canonize_hyps.
pose proof (interval_inversion_valid ((Q2R (fst iv_f)),(Q2R (snd iv_f)))
(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.
- apply L1.
- rewrite Q2R_inv; try 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.
......@@ -216,8 +279,10 @@ Proof.
rewrite <- Q2R0_is_0 in H3.
apply Rlt_Qlt in H3.
lra.
- apply H0.
- rewrite <- Q2R_inv; try auto.
- 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.
......
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