Commit 48cc1d69 authored by Joachim Bard's avatar Joachim Bard

simplified eval_precond

parent 83c1c774
......@@ -13,10 +13,11 @@ From Flover
Require Import Infra.Abbrevs Infra.RationalSimps Infra.RealRationalProps
Infra.Ltacs Infra.RealSimps TypeValidator.
(* TODO: SMTArith is only needed for eval_precond, change that *)
From Flover
Require Export IntervalArithQ IntervalArith ssaPrgs RealRangeArith.
Require Export IntervalArithQ IntervalArith SMTArith ssaPrgs RealRangeArith.
Fixpoint validIntervalbounds (e:expr Q) (A:analysisResult) (P:precond)
Fixpoint validIntervalbounds (e:expr Q) (A:analysisResult) (P: FloverMap.t intv)
(validVars:NatSet.t) :bool:=
match FloverMap.find e A with
| None => false
......@@ -25,7 +26,12 @@ Fixpoint validIntervalbounds (e:expr Q) (A:analysisResult) (P:precond)
| Var _ v =>
if NatSet.mem v validVars
then true
else isSupersetIntv (P v) intv && (Qleb (ivlo (P v)) (ivhi (P v)))
else
match FloverMap.find e P with
| None => false
| Some new_iv => isSupersetIntv new_iv intv
(* && (Qleb lo hi) *)
end
| Const _ n => isSupersetIntv (n,n) intv
| Unop o f =>
if validIntervalbounds f A P validVars
......@@ -99,7 +105,7 @@ Fixpoint validIntervalbounds (e:expr Q) (A:analysisResult) (P:precond)
end
end.
Fixpoint validIntervalboundsCmd (f:cmd Q) (A:analysisResult) (P:precond)
Fixpoint validIntervalboundsCmd (f:cmd Q) (A:analysisResult) (P: FloverMap.t intv)
(validVars:NatSet.t) :bool:=
match f with
| Let m x e g =>
......@@ -138,41 +144,36 @@ Proof.
apply le_neq_bool_to_lt_prop; auto.
Qed.
Theorem validIntervalbounds_sound (f:expr Q) (A:analysisResult) (P:precond)
fVars dVars (E:env) Gamma:
Theorem validIntervalbounds_sound (f:expr Q) (A:analysisResult) (P: FloverMap.t intv)
dVars (E:env) Gamma:
validIntervalbounds f A P dVars = true ->
dVars_range_valid dVars E A ->
NatSet.Subset (NatSet.diff (Expressions.usedVars f) dVars) fVars ->
fVars_P_sound fVars E P ->
eval_precond E P ->
validTypes f Gamma ->
validRanges f A E (toRTMap (toRExpMap Gamma)).
Proof.
induction f;
intros valid_bounds valid_definedVars usedVars_subset valid_freeVars types_defined;
intros valid_bounds valid_definedVars valid_freeVars types_defined;
cbn in *.
- Flover_compute.
split; try auto.
destruct (NatSet.mem n dVars) eqn:?; simpl in *.
- destruct (NatSet.mem n dVars) eqn:?; cbn in *; split; auto.
+ destruct (valid_definedVars n)
as [vR [iv_n [err_n [env_valid [map_n bounds_valid]]]]];
try set_tac.
rewrite map_n in *.
inversion Heqo; subst.
kill_trivial_exists.
eexists; split; [auto| split; try eauto ].
eapply Var_load; simpl; try auto.
destruct (types_defined) as [m [find_m _]].
eapply toRExpMap_some in find_m; simpl; eauto.
match_simpl; auto.
+ destruct (valid_freeVars n) as [vR [env_valid bounds_valid]];
set_tac; try auto.
assert (NatSet.In n fVars) by set_tac.
andb_to_prop valid_bounds.
+ Flover_compute.
destruct (valid_freeVars n i0) as [vR [env_valid bounds_valid]];
auto using find_in_precond.
canonize_hyps; simpl in *.
kill_trivial_exists.
eexists; split; [auto | split].
* econstructor; try eauto.
destruct (types_defined) as [m [find_m _]].
destruct types_defined as [m [find_m _]].
eapply toRExpMap_some in find_m; simpl; eauto.
match_simpl; auto.
* lra.
......@@ -247,9 +248,9 @@ Proof.
- destruct types_defined
as [? [? [[? [? ?]]?]]].
assert (validRanges f1 A E (toRTMap (toRExpMap Gamma))) as valid_f1
by (Flover_compute; try congruence; apply IHf1; try auto; set_tac).
by (Flover_compute; try congruence; apply IHf1; try auto).
assert (validRanges f2 A E (toRTMap (toRExpMap Gamma))) as valid_f2
by (Flover_compute; try congruence; apply IHf2; try auto; set_tac).
by (Flover_compute; try congruence; apply IHf2; try auto).
repeat split;
[ intros; subst; Flover_compute; congruence |
auto | auto |].
......@@ -336,11 +337,11 @@ Proof.
- destruct types_defined
as [mG [find_mg [[validt_f1 [validt_f2 [validt_f3 valid_join]]] valid_exec]]].
assert (validRanges f1 A E (toRTMap (toRExpMap Gamma))) as valid_f1
by (Flover_compute; try congruence; apply IHf1; try auto; set_tac).
by (Flover_compute; try congruence; apply IHf1; try auto).
assert (validRanges f2 A E (toRTMap (toRExpMap Gamma))) as valid_f2
by (Flover_compute; try congruence; apply IHf2; try auto; set_tac).
by (Flover_compute; try congruence; apply IHf2; try auto).
assert (validRanges f3 A E (toRTMap (toRExpMap Gamma))) as valid_f3
by (Flover_compute; try congruence; apply IHf3; try auto; set_tac).
by (Flover_compute; try congruence; apply IHf3; try auto).
repeat split; try auto.
apply validRanges_single in valid_f1;
apply validRanges_single in valid_f2;
......@@ -393,27 +394,30 @@ Theorem validIntervalboundsCmd_sound (f:cmd Q) (A:analysisResult):
forall Gamma E fVars dVars outVars P,
ssa f (NatSet.union fVars dVars) outVars ->
dVars_range_valid dVars E A ->
fVars_P_sound fVars E P ->
NatSet.Subset (NatSet.diff (Commands.freeVars f) dVars) fVars ->
eval_precond E P ->
(* NatSet.Subset (NatSet.diff (Commands.freeVars f) dVars) fVars -> *)
validIntervalboundsCmd f A P dVars = true ->
validTypesCmd f Gamma ->
validRangesCmd f A E (toRTMap (toRExpMap Gamma)).
Proof.
induction f;
intros * ssa_f dVars_sound fVars_valid usedVars_subset
intros * ssa_f dVars_sound fVars_valid (* usedVars_subset *)
valid_bounds_f valid_types_f;
cbn in *.
- Flover_compute.
inversion ssa_f; subst.
canonize_hyps.
pose proof (validIntervalbounds_sound e Gamma (E:=E) (fVars:=fVars) L) as validIV_e.
pose proof (validIntervalbounds_sound e Gamma (E:=E) L) as validIV_e.
destruct valid_types_f
as [[mG [find_mG [_ [_ [validt_e validt_f]]]]] _].
assert (validRanges e A E (toRTMap (toRExpMap Gamma))) as valid_e.
assert (validRanges e A E (toRTMap (toRExpMap Gamma))) as valid_e
by now apply validIV_e.
(*
{ apply validIV_e; try auto.
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))).
{ hnf. intros a; split; intros in_set; set_tac.
- destruct in_set as [ ? | [? ?]]; try auto; set_tac.
......@@ -439,17 +443,23 @@ Proof.
destruct mem_v0 as [? | [? ?]]; try auto.
rewrite Nat.eqb_neq in v0_eq.
congruence.
- intros v0 mem_fVars.
- hnf. intros x ? ?.
unfold updEnv.
case_eq (v0 =? n); intros case_v0; auto.
rewrite Nat.eqb_eq in case_v0; subst.
assert (NatSet.In n (NatSet.union fVars dVars)) as in_union by set_tac.
case_eq (x =? n); intros case_x; try eapply fVars_valid; eauto.
rewrite Nat.eqb_eq in case_x. subst.
exists v. split; auto.
admit.
(*
assert (NatSet.In n (NatSet.union fVars dVars)) as in_union. set_tac.
exfalso; set_tac. apply H6; set_tac; auto.
*)
} (*
- intros x x_contained.
set_tac.
repeat split; try auto.
+ hnf; intros; subst. apply H1; set_tac.
+ hnf; intros. apply H1; set_tac. }
*)
(*
destruct x_contained as [x_free | x_def].
+ destruct (types_valid x) as [m_x Gamma_x]; try set_tac.
......@@ -492,11 +502,11 @@ Proof.
+ lra.
+ lra. }
- unfold validIntervalboundsCmd in valid_bounds_f.
pose proof (validIntervalbounds_sound e (E:=E) Gamma valid_bounds_f dVars_sound usedVars_subset) as valid_iv_e.
pose proof (validIntervalbounds_sound e (E:=E) Gamma valid_bounds_f dVars_sound (* usedVars_subset*) ) 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).
split; try auto.
apply validRanges_single in valid_e.
destruct valid_e as [?[?[? [? [? ?]]]]]; try auto.
simpl in *. repeat eexists; repeat split; try eauto; [econstructor; eauto| | ]; lra.
Qed.
\ No newline at end of file
Admitted.
......@@ -265,9 +265,17 @@ Proof.
apply Nat.compare_eq in H. now subst.
Qed.
Lemma find_in_precond P x (iv: intv) :
FloverMap.find (Var Q x) P = Some iv -> List.In (Var Q x, iv) (FloverMap.elements P).
Proof.
rewrite FloverMapFacts.P.F.elements_o.
intros H. apply findA_find in H as [e [H _]].
apply List.find_some in H as [Hin Heq].
apply eqb_var in Heq. cbn in *. now subst.
Qed.
Definition eval_precond E (P: FloverMap.t intv) :=
forall e x iv, List.In (e, iv) (FloverMap.elements P)
-> (FloverMapFacts.P.F.eqb (Var Q x) e = true)
forall x iv, List.In (Var Q x, iv) (FloverMap.elements P)
-> exists vR: R, E x = Some vR /\ Q2R (fst iv) <= vR <= Q2R (snd iv).
Definition addVarConstraint (el: expr Q * intv) q :=
......@@ -286,15 +294,13 @@ Proof.
induction (FloverMap.elements P) as [|[e [lo hi]] l IHl].
- intros. cbn. auto.
- intros H. cbn.
destruct e; try (apply IHl; intros e' x iv inl Heq; apply (H e'); cbn; auto).
destruct e; try (apply IHl; intros x iv inl; apply H; cbn; auto).
repeat split.
+ destruct (H (Var Q n) n (lo, hi)) as [v H']; cbn; auto.
* now rewrite eqb_cmp_eq, Q_orderedExps.exprCompare_refl.
* exists (Q2R lo), v. repeat split. 3: tauto. 1-2: constructor. tauto.
+ destruct (H (Var Q n) n (lo, hi)) as [v H']; cbn; auto.
* now rewrite eqb_cmp_eq, Q_orderedExps.exprCompare_refl.
* exists v, (Q2R hi). repeat split. 3: tauto. 1-2: constructor. tauto.
+ apply IHl. intros e x iv inl Heq. apply (H e); cbn; auto.
+ destruct (H n (lo, hi)) as [v H']; cbn; auto.
exists (Q2R lo), v. repeat split. 3: tauto. 1-2: constructor. tauto.
+ destruct (H n (lo, hi)) as [v H']; cbn; auto.
exists v, (Q2R hi). repeat split. 3: tauto. 1-2: constructor. tauto.
+ apply IHl. intros x iv inl. apply H; cbn; auto.
Qed.
(*
......@@ -419,14 +425,11 @@ Proof with try discriminate.
rewrite <- chk3, <- chk4.
apply Qeq_sym in chk2. apply Qeq_sym in chk1.
repeat split.
+ destruct (H (Var Q x) x (lo, hi)) as [v [H0 [H1 H2]]]; cbn; auto.
* now rewrite eqb_cmp_eq, Q_orderedExps.exprCompare_refl.
* exists (Q2R r), v. repeat split; try now constructor. erewrite Qeq_eqR; now eauto.
+ destruct (H (Var Q x) x (lo, hi)) as [v [H0 [H1 H2]]]; cbn; auto.
* now rewrite eqb_cmp_eq, Q_orderedExps.exprCompare_refl.
* exists v, (Q2R r'). repeat split; try now constructor. erewrite Qeq_eqR; now eauto.
+ destruct (H x (lo, hi)) as [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.
exists v, (Q2R r'). repeat split; try now constructor. erewrite Qeq_eqR; now eauto.
+ apply IHl; auto.
intros. apply (H e); auto.
Qed.
(*
......
......@@ -225,15 +225,13 @@ Proof.
eapply toRExpMap_some in find_m; cbn; eauto.
match_simpl; auto.
+ Flover_compute.
rewrite FloverMapFacts.P.F.elements_o in Heqo0.
apply findA_find in Heqo0 as [e' [? ?]].
apply find_some in H as [? ?].
destruct (valid_precond e' n i0) as [vR [env_valid bounds_valid]]; auto.
destruct (valid_precond n i0) as [vR [env_valid bounds_valid]];
auto using find_in_precond.
canonize_hyps.
kill_trivial_exists.
eexists; split; [auto | split].
* econstructor; try eauto.
destruct (types_defined) as [m [find_m _]].
destruct types_defined as [m [find_m _]].
eapply toRExpMap_some in find_m; cbn; eauto.
match_simpl; auto.
* cbn in *. lra.
......
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