Commit f1d00ce8 authored by Joachim Bard's avatar Joachim Bard

cleanup

parent 1d337e62
......@@ -183,6 +183,10 @@ Qed.
Open Scope R.
Lemma Rle_trans2 a b x y z :
a <= x -> z <= b -> x <= y <= z -> a <= y <= b.
Proof. lra. Qed.
Lemma Req_dec_sum (x y: R):
{x = y} + {x <> y}.
Proof.
......
This diff is collapsed.
......@@ -17,10 +17,18 @@ From Flover
Require Export IntervalArithQ IntervalArith IntervalValidation SMTArith ssaPrgs
RealRangeArith.
Definition updLets x (e: expr Q) (L: nat -> option (expr Q)) (y: nat) :=
Definition let_env := nat -> option (expr Q).
Definition lets_sound L E Gamma :=
forall x e v,
L x = Some e ->
eval_expr E (toRTMap (toRExpMap Gamma)) DeltaMapR (toREval (toRExp (Var _ x))) v REAL ->
eval_expr E (toRTMap (toRExpMap Gamma)) DeltaMapR (toREval (toRExp e)) v REAL.
Definition updLets x (e: expr Q) (L: let_env) (y: nat) :=
if y =? x then Some e else L y.
Fixpoint inlineLets (L: nat -> option (expr Q)) (e: expr Q) :=
Fixpoint inlineLets (L: let_env) (e: expr Q) :=
match e with
| Var _ x => match L x with
| Some e' => e'
......@@ -33,10 +41,8 @@ Fixpoint inlineLets (L: nat -> option (expr Q)) (e: expr Q) :=
| Downcast m e' => Downcast m (inlineLets L e')
end.
Lemma inlineLets_sound E Gamma e L v :
(forall x e' v, L x = Some e' ->
eval_expr E (toRTMap (toRExpMap Gamma)) DeltaMapR (toREval (toRExp (Var Q x))) v REAL ->
eval_expr E (toRTMap (toRExpMap Gamma)) DeltaMapR (toREval (toRExp e')) v REAL) ->
Lemma inlineLets_sound L E Gamma e v :
lets_sound L E Gamma ->
eval_expr E (toRTMap (toRExpMap Gamma)) DeltaMapR (toREval (toRExp e)) v REAL ->
eval_expr E (toRTMap (toRExpMap Gamma)) DeltaMapR (toREval (toRExp (inlineLets L e))) v
REAL.
......@@ -160,11 +166,6 @@ Proof.
intros. edestruct unsatQ; eauto.
Qed.
(* TODO: move this somewher else *)
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: precond)
(Q: usedQueries) L (validVars: NatSet.t) : bool :=
match FloverMap.find e A with
......@@ -248,8 +249,7 @@ Fixpoint validSMTIntervalbounds (e: expr Q) (A: analysisResult) (P: precond)
match FloverMap.find f1 A with
| None => false
| Some (iv1, _) =>
(* TODO: need tightening here or will f1 be tightened? *)
isSupersetIntv iv1 intv
isSupersetIntv (tightenBounds e iv1 Q P L) intv
end
else
false
......@@ -259,9 +259,7 @@ Fixpoint validSMTIntervalbounds (e: expr Q) (A: analysisResult) (P: precond)
Theorem validSMTIntervalbounds_sound (f: expr Q) (A: analysisResult) (P: precond)
(Q: usedQueries) L fVars dVars (E: env) Gamma :
unsat_queries Q ->
(forall x e v, L x = Some e ->
eval_expr E (toRTMap (toRExpMap Gamma)) DeltaMapR (toREval (toRExp (Var _ x))) v REAL ->
eval_expr E (toRTMap (toRExpMap Gamma)) DeltaMapR (toREval (toRExp e)) v REAL) ->
lets_sound L E Gamma ->
validSMTIntervalbounds f A P Q L dVars = true ->
dVars_range_valid dVars E A ->
NatSet.Subset ((Expressions.usedVars f) -- dVars) fVars ->
......@@ -482,12 +480,17 @@ Proof.
Flover_compute.
inversion env_f; subst.
kill_trivial_exists.
exists (perturb vF REAL 0).
pose (v := perturb vF REAL 0).
exists v.
split; [destruct i; auto |].
canonize_hyps.
split; [| cbn in *; lra].
eapply Downcast_dist'; try eassumption; auto; auto.
cbn; rewrite Rabs_R0. lra.
assert (Heval: eval_expr E (toRTMap (toRExpMap Gamma)) DeltaMapR
(Downcast REAL (toREval (toRExp f))) v REAL).
{ eapply Downcast_dist'; try eassumption; cbn; auto; try reflexivity.
rewrite Rabs_R0; lra. }
split; auto.
eapply Rle_trans2; eauto.
eapply tightenBounds_sound; eauto using inlineLets_sound.
Qed.
Fixpoint validSMTIntervalboundsCmd (f:cmd Q) (A:analysisResult) (P: precond)
......@@ -515,9 +518,7 @@ Theorem validSMTIntervalboundsCmd_sound (f:cmd Q) (A:analysisResult)
eval_precond E P ->
NatSet.Subset (preVars P) fVars ->
NatSet.Subset (freeVars f -- dVars) fVars ->
(forall x e v, Lets x = Some e ->
eval_expr E (toRTMap (toRExpMap Gamma)) DeltaMapR (toREval (toRExp (Var _ x))) v REAL ->
eval_expr E (toRTMap (toRExpMap Gamma)) DeltaMapR (toREval (toRExp e)) v REAL) ->
lets_sound Lets E Gamma ->
(forall x e, Lets x = Some e -> NatSet.Subset (usedVars e) (fVars dVars)) ->
unsat_queries Q ->
validSMTIntervalboundsCmd f A P Q Lets dVars = true ->
......@@ -531,7 +532,7 @@ Proof.
- Flover_compute.
inversion ssa_f; subst.
canonize_hyps.
pose proof (validSMTIntervalbounds_sound e Lets (fVars:=fVars) (E:=E) (Gamma:=Gamma) unsat_qs Lsound L)
pose proof (validSMTIntervalbounds_sound e (fVars:=fVars) unsat_qs Lsound L)
as validIV_e.
destruct valid_types_f
as [[mG [find_mG [_ [_ [validt_e validt_f]]]]] _].
......@@ -540,7 +541,8 @@ Proof.
set_tac. repeat split; auto.
hnf; intros; subst.
set_tac. }
assert (NatSet.Equal (NatSet.add n (NatSet.union fVars dVars)) (NatSet.union fVars (NatSet.add n dVars))).
assert (NatSet.Equal (NatSet.add n (NatSet.union fVars dVars))
(NatSet.union fVars (NatSet.add n dVars))).
{ hnf. intros a; split; intros in_set; set_tac.
- destruct in_set as [ ? | [? ?]]; try auto; set_tac.
destruct H0; auto.
......@@ -549,7 +551,8 @@ Proof.
pose proof (validRanges_single _ _ _ _ valid_e) as valid_single_e.
destruct valid_single_e as [iv_e [err_v [v [find_v [eval_e valid_bounds_e]]]]].
rewrite find_v in *; inversion Heqo; subst.
specialize (IHf (updLets n e Lets) Gamma (updEnv n v E) fVars (NatSet.add n dVars)) as IHf_spec.
specialize (IHf (updLets n e Lets) Gamma (updEnv n v E) fVars (NatSet.add n dVars))
as IHf_spec.
assert (validRangesCmd f A (updEnv n v E) (toRTMap (toRExpMap Gamma))).
{ eapply IHf_spec; eauto.
- symmetry in H. eapply ssa_equal_set; eauto.
......@@ -591,7 +594,7 @@ Proof.
+ intros H0 H1.
inversion H1; subst. rewrite Heq in *.
apply eval_expr_ignore_bind.
* eapply Lsound; eauto.
* eapply Lsound; eauto. now constructor.
* rewrite usedVars_toREval_toRExp_compat.
set_tac. intros ?.
assert (n fVars dVars) by (eapply Lvars_valid; eauto).
......@@ -643,9 +646,11 @@ Proof.
repeat eexists; eauto.
econstructor; eauto.
- unfold validIntervalboundsCmd in valid_bounds_f.
pose proof (validSMTIntervalbounds_sound e Lets (E:=E) (Gamma:=Gamma) unsat_qs Lsound valid_bounds_f dVars_sound usedVars_subset) as valid_iv_e.
pose proof (validSMTIntervalbounds_sound e (fVars:=fVars) unsat_qs Lsound
valid_bounds_f) as valid_iv_e.
destruct valid_types_f as [? ?].
assert (validRanges e A E (toRTMap (toRExpMap Gamma))) as valid_e by (apply valid_iv_e; auto).
assert (validRanges e A E (toRTMap (toRExpMap Gamma))) as valid_e
by (apply valid_iv_e; auto).
split; try auto.
apply validRanges_single in valid_e.
destruct valid_e as [?[?[? [? [? ?]]]]]; try auto.
......
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