Commit a870c10a authored by Joachim Bard's avatar Joachim Bard

changing eval_precond and adjusting the rest to it

no admitted lemmas
parent aca4ef84
......@@ -168,7 +168,7 @@ Proof.
eapply toRExpMap_some in find_m; simpl; eauto.
match_simpl; auto.
+ Flover_compute.
destruct (valid_freeVars n i0) as [vR [env_valid bounds_valid]];
destruct (valid_freeVars n i0) as [free_n [vR [env_valid bounds_valid]]];
auto using find_in_precond; set_tac.
kill_trivial_exists.
eexists; split; [auto | split].
......@@ -444,8 +444,10 @@ Proof.
unfold updEnv.
case_eq (x =? n); intros case_x; auto.
rewrite Nat.eqb_eq in case_x. subst.
assert (NatSet.In n (NatSet.union fVars dVars)) as in_union by set_tac.
exfalso; set_tac. apply H6; set_tac; auto.
set_tac.
assert (NatSet.In n (NatSet.union fVars dVars)) as in_union
by (destruct (fVars_valid n iv); auto; set_tac).
exfalso. now apply H6.
- intros x x_contained.
set_tac.
repeat split; try auto.
......
......@@ -257,7 +257,7 @@ Definition eval_precond E (P: FloverMap.t intv) :=
-> exists vR: R, E x = Some vR /\ Q2R (fst iv) <= vR <= Q2R (snd iv).
*)
(* TODO: move eqb_var, find_in_precond and eval_precond and somewhere else *)
(* TODO: move eqb_var, find_in_precond and eval_precond somewhere else *)
Lemma eqb_var x e : FloverMapFacts.P.F.eqb (Var Q x) e = true -> e = Var Q x.
Proof.
rewrite eqb_cmp_eq. destruct e; cbn; try discriminate.
......@@ -275,8 +275,8 @@ Proof.
Qed.
Definition eval_precond fVars E (P: FloverMap.t intv) :=
forall x iv, (x fVars) ->
List.In (Var Q x, iv) (FloverMap.elements P) ->
forall x iv, List.In (Var Q x, iv) (FloverMap.elements P) ->
(x fVars) /\
exists vR: R, E x = Some vR /\ Q2R (fst iv) <= vR <= Q2R (snd iv).
Definition addVarConstraint (el: expr Q * intv) q :=
......@@ -288,6 +288,7 @@ Definition addVarConstraint (el: expr Q * intv) q :=
Definition precond2SMT (P: FloverMap.t intv) :=
List.fold_right addVarConstraint TrueQ (FloverMap.elements P).
(*
Lemma pre_to_smt_correct fVars E P :
eval_precond fVars E P -> eval_smt_logic E (precond2SMT P).
Proof.
......@@ -297,14 +298,15 @@ Proof.
- intros H. cbn.
destruct e; try (apply IHl; intros x iv infv inl; apply H; cbn; auto).
repeat split.
+ destruct (H n (lo, hi)) as [v [? ?]]; cbn; auto.
+ destruct (H n (lo, hi)) as [? [v [? ?]]]; cbn; auto.
admit.
exists (Q2R lo), v. repeat split; try now constructor. tauto.
+ destruct (H n (lo, hi)) as [v H']; cbn; auto.
+ destruct (H n (lo, hi)) as [? [v H']]; cbn; auto.
admit.
exists v, (Q2R hi). repeat split; try now constructor. tauto.
+ apply IHl. intros x iv infv inl. apply H; cbn; auto.
+ apply IHl. intros x iv infv. apply H; cbn; auto.
Abort.
*)
(*
Lemma smt_to_pre_correct E P :
......@@ -403,9 +405,42 @@ Proof.
Qed.
*)
Lemma precond_free_vars fVars E P q :
eval_precond fVars E P ->
checkPre P q = true ->
NatSet.Subset (varsLogic q) fVars.
Proof with try discriminate.
unfold eval_precond, checkPre.
induction (FloverMap.elements P) as [|[e [lo hi]] l IHl] in q |- *;
intros prec_valid eq.
- destruct q... intros x H. cbn in H. set_tac.
- destruct e as [x| | | | |].
2-6: revert eq; apply IHl; intros; apply prec_valid; cbn; auto.
cbn in eq.
destruct q as [? ?|? ?|? ?| |?|q1 q2|? ?]...
destruct q1 as [? ?|e1 e2|? ?| |?|? ?|? ?]...
destruct e1 as [r| | | | | |]... destruct e2 as [|y| | | | |]...
destruct q2 as [? ?|? ?|? ?| |?|q1 q2|? ?]...
destruct q1 as [? ?|e1 e2|? ?| |?|? ?|? ?]...
destruct e1 as [|z| | | | |]... destruct e2 as [r'| | | | | |]...
intros a H.
apply andb_prop in eq as [eq chk].
apply andb_prop in eq as [eq _].
apply andb_prop in eq as [eq _].
apply andb_prop in eq as [eqy eqz].
apply beq_nat_true in eqy. apply beq_nat_true in eqz.
cbn in *. set_tac.
destruct H as [H|H]; set_tac.
+ destruct H as [H|H]; set_tac.
apply (prec_valid a (lo, hi)). subst. auto.
+ destruct H as [H|H]; set_tac.
* destruct H; set_tac.
apply (prec_valid a (lo, hi)). subst. auto.
* eapply IHl; eauto.
Qed.
Lemma checkPre_pre_smt fVars E P q :
checkPre P q = true ->
NatSet.Subset (varsLogic q) fVars ->
eval_precond fVars E P ->
eval_smt_logic E q.
Proof with try discriminate.
......@@ -413,15 +448,16 @@ Proof with try discriminate.
induction (FloverMap.elements P) as [|[e [lo hi]] l IHl] in q |- *.
- destruct q; cbn; intros chk... now auto.
- destruct e as [x| | | | |].
all: cbn; try (intros H0 H1 H2; apply IHl; auto; intros e' x iv Hin Heq;
apply (H2 e'); auto).
2-6: cbn; try (intros H0 H1; apply IHl; auto). (* ; intros x iv Hin;
apply (H2 e'); auto). *)
cbn.
destruct q as [? ?|? ?|? ?| |?|q1 q2|? ?]...
intros chk sub H.
destruct q1 as [? ?|e1 e2|? ?| |?|? ?|? ?]...
destruct e1 as [r| | | | | |]... destruct e2 as [|y| | | | |]...
destruct q2 as [? ?|? ?|? ?| |?|q1 q2|? ?]...
destruct q1 as [? ?|e1 e2|? ?| |?|? ?|? ?]...
destruct e1 as [|z| | | | |]... destruct e2 as [r'| | | | | |]...
intros chk H.
apply andb_prop in chk as [chk chk0].
apply andb_prop in chk as [chk chk1].
apply andb_prop in chk as [chk chk2].
......@@ -430,13 +466,13 @@ Proof with try discriminate.
apply Qeq_bool_eq in chk2. apply Qeq_bool_eq in chk1.
rewrite <- chk3, <- chk4.
apply Qeq_sym in chk2. apply Qeq_sym in chk1.
assert (x fVars) as fx by (subst; set_tac; set_tac).
(* assert (x fVars) as fx by (subst; set_tac; set_tac). *)
repeat split.
+ destruct (H x (lo, hi)) as [v [H0 [H1 H2]]]; cbn; auto.
+ destruct (H x (lo, hi)) as [Hin [v [H0 [H1 H2]]]]; cbn; auto.
exists (Q2R r), v. repeat split; try now constructor. erewrite Qeq_eqR; now eauto.
+ destruct (H x (lo, hi)) as [v [H0 [H1 H2]]]; cbn; auto.
+ destruct (H x (lo, hi)) as [Hin [v [H0 [H1 H2]]]]; cbn; auto.
exists v, (Q2R r'). repeat split; try now constructor. erewrite Qeq_eqR; now eauto.
+ apply IHl; auto. set_tac. set_tac.
+ apply IHl; auto.
Qed.
(*
......
......@@ -55,14 +55,11 @@ Proof.
symmetry in Hchk.
andb_to_prop Hchk.
rewrite <- Q2R_max. apply Rmax_lub; auto.
eapply RangeBound_low_sound; eauto.
eapply RangeBound_low_sound; eauto using precond_free_vars.
erewrite eval_smt_expr_complete in H; eauto.
(*
rewrite SMTArith2Expr_exact.
exact H.
Qed.
*)
Admitted.
Lemma tightenBounds_high_sound fVars E Gamma e v iv qMap P :
eval_precond fVars E P
......@@ -85,14 +82,11 @@ Proof.
symmetry in Hchk.
andb_to_prop Hchk.
rewrite <- Q2R_min. apply Rmin_glb; auto.
eapply RangeBound_high_sound; eauto.
(*
eapply RangeBound_high_sound; eauto using precond_free_vars.
erewrite eval_smt_expr_complete in H; eauto.
rewrite SMTArith2Expr_exact.
exact H.
Qed.
*)
Admitted.
Lemma tightenBounds_sound fVars E Gamma e v iv qMap P :
eval_precond fVars E P
......@@ -226,7 +220,7 @@ Proof.
eapply toRExpMap_some in find_m; cbn; eauto.
match_simpl; auto.
+ Flover_compute.
destruct (valid_precond n i0) as [vR [env_valid bounds_valid]];
destruct (valid_precond n i0) as [free_n [vR [env_valid bounds_valid]]];
auto using find_in_precond; set_tac.
canonize_hyps.
kill_trivial_exists.
......
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