Commit aca05c91 authored by Joachim Bard's avatar Joachim Bard

completing proof for validSMTIntervalboundsCmd

parent 2a8888a2
......@@ -33,18 +33,19 @@ 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 :
Lemma inlineLets_sound E1 E2 Gamma e L v :
(forall x v, L x = None -> E1 x = Some v -> E2 x = Some 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) ->
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
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
REAL.
Proof.
intros Lsound.
intros Esound Lsound.
induction e in v |- *.
- intros H. cbn. Flover_compute; eauto.
- auto.
- 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.
+ destruct m; try discriminate.
eauto.
......@@ -100,7 +101,7 @@ Proof.
unfold tightenBounds.
destruct (FloverMap.find e qMap) as [[q ?]|]; auto.
cbn. unfold tightenLowerBound.
destruct q; auto. cbn.
destruct q; auto.
destruct q2; auto.
destruct q2_1; auto.
destruct e2; auto.
......@@ -260,8 +261,9 @@ 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) ->
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 ->
......@@ -298,6 +300,7 @@ 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.
......@@ -518,13 +521,14 @@ Theorem validSMTIntervalboundsCmd_sound (f:cmd Q) (A:analysisResult)
(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) ->
(forall x e, Lets x = Some e -> NatSet.Subset (usedVars e) (fVars dVars)) ->
unsat_queries Q ->
validSMTIntervalboundsCmd f A P Q Lets dVars = true ->
validTypesCmd f Gamma ->
validRangesCmd f A E (toRTMap (toRExpMap Gamma)).
Proof.
induction f;
intros * ssa_f dVars_sound fVars_valid preVars_free usedVars_subset Lsound
intros * ssa_f dVars_sound fVars_valid preVars_free usedVars_subset Lsound Lsound'
unsat_qs valid_bounds_f valid_types_f;
cbn in *.
- Flover_compute.
......@@ -578,12 +582,19 @@ 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.
remember (x =? n) as b eqn: Heq.
symmetry in Heq.
destruct b.
+ intros He. injection He. clear He; intros He. symmetry in He; subst.
intros H0. inversion H0; subst.
destruct (x =? n) eqn: Heq.
+ intros He. injection He.
intros <- H0. inversion H0; subst.
rewrite Heq in *.
assert (v' = v) by congruence. subst.
apply eval_expr_ignore_bind; auto.
......@@ -594,7 +605,13 @@ Proof.
apply eval_expr_ignore_bind.
* eapply Lsound; eauto.
* rewrite usedVars_toREval_toRExp_compat.
admit.
set_tac. intros ?. apply H6. apply (Lsound' x e'); auto.
- intros x e'. unfold updLets. destruct (x =? n) eqn: Heq.
+ intros H0. injection H0. intros <-.
rewrite <- H.
eapply NatSetProps.subset_trans; eauto. set_tac.
+ intros H0. rewrite <- H.
eapply NatSetProps.subset_trans. eauto. set_tac.
}
(*
destruct x_contained as [x_free | x_def].
......@@ -643,4 +660,4 @@ Proof.
apply validRanges_single in valid_e.
destruct valid_e as [?[?[? [? [? ?]]]]]; try auto.
simpl in *. repeat eexists; repeat split; try eauto; [econstructor; eauto| | ]; lra.
Admitted.
Qed.
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