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

minor improvements

parent aca05c91
......@@ -33,37 +33,36 @@ Fixpoint inlineLets (L: nat -> option (expr Q)) (e: expr Q) :=
| Downcast m e' => Downcast m (inlineLets L e')
end.
Lemma inlineLets_sound E1 E2 Gamma e L v :
(forall x v, L x = None -> E1 x = Some v -> E2 x = Some v) ->
Lemma inlineLets_sound E Gamma e L v :
(forall x e' v, L x = Some e' ->
eval_expr E1 (toRTMap (toRExpMap Gamma)) DeltaMapR (toREval (toRExp (Var Q x))) v REAL ->
eval_expr E2 (toRTMap (toRExpMap Gamma)) DeltaMapR (toREval (toRExp e')) v REAL) ->
eval_expr E1 (toRTMap (toRExpMap Gamma)) DeltaMapR (toREval (toRExp e)) v REAL ->
eval_expr E2 (toRTMap (toRExpMap Gamma)) DeltaMapR (toREval (toRExp (inlineLets L e))) v
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) ->
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.
Proof.
intros Esound Lsound.
induction e in v |- *.
- intros H. cbn. Flover_compute; eauto. inversion H; subst. econstructor; eauto.
- cbn. intros H; inversion H. econstructor; eauto. (* auto. *)
- cbn. intros H. inversion H; subst; econstructor; eauto.
intros Lsound.
induction e in v |- *; cbn; intros H.
- Flover_compute; eauto.
- auto.
- inversion H; subst; econstructor; eauto.
+ destruct m; try discriminate.
eauto.
+ destruct m; try discriminate.
eauto.
- cbn. intros H. inversion H; subst; econstructor; eauto.
- inversion H; subst; econstructor; eauto.
+ assert (m1 = REAL) by (eapply toRTMap_eval_REAL; eauto).
subst. eauto.
+ assert (m2 = REAL) by (eapply toRTMap_eval_REAL; eauto).
subst. eauto.
- cbn. intros H. inversion H; subst; econstructor; eauto.
- inversion H; subst; econstructor; eauto.
+ assert (m1 = REAL) by (eapply toRTMap_eval_REAL; eauto).
subst. eauto.
+ assert (m2 = REAL) by (eapply toRTMap_eval_REAL; eauto).
subst. eauto.
+ assert (m3 = REAL) by (eapply toRTMap_eval_REAL; eauto).
subst. eauto.
- cbn. intros H. inversion H; subst; econstructor; eauto.
- inversion H; subst; econstructor; eauto.
assert (m1 = REAL) by (eapply toRTMap_eval_REAL; eauto).
subst. eauto.
Qed.
......@@ -263,7 +262,6 @@ Theorem validSMTIntervalbounds_sound (f: expr Q) (A: analysisResult) (P: precond
(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) ->
(* TODO (forall x e, L x = Some e -> x dVars) -> *)
validSMTIntervalbounds f A P Q L dVars = true ->
dVars_range_valid dVars E A ->
NatSet.Subset ((Expressions.usedVars f) -- dVars) fVars ->
......@@ -300,7 +298,6 @@ Proof.
eapply Rle_trans2; eauto.
eapply tightenBounds_sound; eauto.
cbn. Flover_compute; eauto.
(* exfalso. eauto. *)
- split; [auto |].
Flover_compute; canonize_hyps; cbn in *.
kill_trivial_exists.
......@@ -528,7 +525,7 @@ Theorem validSMTIntervalboundsCmd_sound (f:cmd Q) (A:analysisResult)
validRangesCmd f A E (toRTMap (toRExpMap Gamma)).
Proof.
induction f;
intros * ssa_f dVars_sound fVars_valid preVars_free usedVars_subset Lsound Lsound'
intros * ssa_f dVars_sound fVars_valid preVars_free usedVars_subset Lsound Lvars_valid
unsat_qs valid_bounds_f valid_types_f;
cbn in *.
- Flover_compute.
......@@ -582,15 +579,6 @@ Proof.
repeat split; try auto.
+ hnf; intros; subst. apply H1; set_tac.
+ hnf; intros. apply H1; set_tac.
(* - unfold updLets. intros E' x e' v'. set_tac. destruct (x =? n) eqn: Heq.
+ (* auto using beq_nat_true. *)
intros He. injection He; subst. intros <- H0.
inversion H0; subst.
admit.
+ (* right. eapply Lsound. eauto. *)
intros H0 H1.
inversion H1; subst.
eapply Lsound; eauto. *)
- intros x e' v'. unfold updLets, updEnv.
destruct (x =? n) eqn: Heq.
+ intros He. injection He.
......@@ -605,7 +593,9 @@ Proof.
apply eval_expr_ignore_bind.
* eapply Lsound; eauto.
* rewrite usedVars_toREval_toRExp_compat.
set_tac. intros ?. apply H6. apply (Lsound' x e'); auto.
set_tac. intros ?.
assert (n fVars dVars) by (eapply Lvars_valid; eauto).
eauto.
- intros x e'. unfold updLets. destruct (x =? n) eqn: Heq.
+ intros H0. injection H0. intros <-.
rewrite <- H.
......
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