Commit 36ce0269 authored by Heiko Becker's avatar Heiko Becker
Browse files

Merge branch 'master' into 'master'

Add Interval Subdivision support

See merge request AVA/FloVer!19
parents 72bb2be1 66883af7
......@@ -11,7 +11,7 @@ Require Export Flover.Infra.ExpressionAbbrevs Flover.Infra.NatSet.
Only assignments and return statement
**)
Inductive cmd (V:Type) :Type :=
Let: mType -> nat -> expr V -> cmd V -> cmd V
Let: mType -> nat -> cmd V -> cmd V -> cmd V
| Ret: expr V -> cmd V.
Fixpoint getRetExp (V:Type) (f:cmd V) :=
......@@ -22,13 +22,13 @@ Fixpoint getRetExp (V:Type) (f:cmd V) :=
Fixpoint toRCmd (f:cmd Q) :=
match f with
|Let m x e g => Let m x (toRExp e) (toRCmd g)
|Let m x e g => Let m x (toRCmd e) (toRCmd g)
|Ret e => Ret (toRExp e)
end.
Fixpoint toREvalCmd (f:cmd R) :=
match f with
|Let m x e g => Let REAL x (toREval e) (toREvalCmd g)
|Let m x e g => Let REAL x (toREvalCmd e) (toREvalCmd g)
|Ret e => Ret (toREval e)
end.
......@@ -51,7 +51,7 @@ Inductive sstep : cmd R -> env -> R -> cmd R -> env -> Prop :=
Inductive bstep : cmd R -> env -> (expr R -> option mType) -> (R -> mType -> option R) ->
R -> mType -> Prop :=
let_b m m' x e s E v res defVars DeltaMap:
eval_expr E defVars DeltaMap e v m ->
bstep e E defVars DeltaMap v m ->
bstep s (updEnv x v E) defVars DeltaMap res m' -> (* (updDefVars (Var R x) m defVars) res m' -> *)
bstep (Let m x e s) E defVars DeltaMap res m'
|ret_b m e E v defVars DeltaMap:
......@@ -64,7 +64,7 @@ Inductive bstep : cmd R -> env -> (expr R -> option mType) -> (R -> mType -> opt
**)
Fixpoint freeVars V (f:cmd V) :NatSet.t :=
match f with
| Let _ x e1 g => NatSet.remove x (NatSet.union (Expressions.usedVars e1) (freeVars g))
| Let _ x e1 g => (freeVars e1 ) (NatSet.remove x (freeVars g))
| Ret e => Expressions.usedVars e
end.
......@@ -83,7 +83,7 @@ Fixpoint definedVars V (f:cmd V) :NatSet.t :=
**)
Fixpoint liveVars V (f:cmd V) :NatSet.t :=
match f with
| Let _ _ e g => NatSet.union (usedVars e) (liveVars g)
| Let _ _ e g => NatSet.union (liveVars e) (liveVars g)
| Ret e => usedVars e
end.
......@@ -95,11 +95,10 @@ Lemma bstep_eq_env f:
Proof.
induction f; intros * eq_envs bstep_E1;
inversion bstep_E1; subst; simpl in *.
- eapply eval_eq_env in H8; eauto. eapply let_b; eauto.
eapply IHf. instantiate (1:=(updEnv n v0 E1)).
+ intros; unfold updEnv.
destruct (x=? n); auto.
+ auto.
- econstructor; eauto.
apply (IHf2 (updEnv n v0 E1)); auto.
intros; unfold updEnv.
destruct (x=? n); auto.
- apply ret_b. eapply eval_eq_env; eauto.
Qed.
......@@ -108,11 +107,10 @@ Lemma swap_Gamma_bstep f E vR m Gamma1 Gamma2 DeltaMap:
bstep f E Gamma1 DeltaMap vR m ->
bstep f E Gamma2 DeltaMap vR m.
Proof.
revert E Gamma1 Gamma2 DeltaMap;
revert E Gamma1 Gamma2 DeltaMap vR m;
induction f; intros * Gamma_eq eval_f.
- inversion eval_f; subst.
econstructor; try eauto.
eapply swap_Gamma_eval_expr; eauto.
- inversion eval_f; subst.
econstructor; try eauto.
eapply swap_Gamma_eval_expr; eauto.
......@@ -127,7 +125,7 @@ Proof.
induction f; intros * eval_f1 eval_f2;
inversion eval_f1; subst;
inversion eval_f2; subst; try auto.
- eapply IHf; eauto.
- eapply IHf2; eauto.
- eapply Gamma_det; eauto.
Qed.
......@@ -141,6 +139,6 @@ Proof.
inversion eval_f1; subst;
inversion eval_f2; subst; try auto.
- replace v with v0 in * by eauto using eval_expr_functional.
eapply IHf; eauto.
eapply IHf2; eauto.
- eapply eval_expr_functional; eauto.
Qed.
From Flover
Require Import Infra.RealSimps Infra.RationalSimps Infra.RealRationalProps
Infra.Ltacs RealRangeArith RealRangeValidator RoundoffErrorValidator
Environments TypeValidator FPRangeValidator ExpressionAbbrevs ResultChecker.
(*
From Flover
Require Import Infra.RealRationalProps Environments ExpressionSemantics
IntervalArithQ SMTArith RealRangeArith RealRangeValidator RoundoffErrorValidator
ssaPrgs TypeValidator ErrorAnalysis ResultChecker.
*)
Require Import List.
Fixpoint resultLeq e (A1 A2: analysisResult) :=
match e with
| Unop _ e1 | Downcast _ e1 => resultLeq e1 A1 A2
| Binop _ e1 e2 | Let _ _ e1 e2 => resultLeq e1 A1 A2 && resultLeq e2 A1 A2
| Fma e1 e2 e3 => resultLeq e1 A1 A2 && resultLeq e2 A1 A2 && resultLeq e3 A1 A2
| _ => true
end &&
match FloverMap.find e A1, FloverMap.find e A2 with
| Some (ivA1, errA1), Some (ivA2, errA2) => isSupersetIntv ivA1 ivA2 && (Qleb errA1 errA2)
| _, _ => false
end.
Lemma resultLeq_sound e A1 A2 :
resultLeq e A1 A2 = true ->
exists iv1 err1 iv2 err2,
FloverMap.find e A1 = Some (iv1, err1) /\
FloverMap.find e A2 = Some (iv2, err2) /\
isSupersetIntv iv1 iv2 = true /\
err1 <= err2.
Proof.
intros H.
assert (
match FloverMap.find e A1, FloverMap.find e A2 with
| Some (ivA1, errA1), Some (ivA2, errA2) => isSupersetIntv ivA1 ivA2 && (Qleb errA1 errA2)
| _, _ => false
end = true).
{ unfold resultLeq in H. destruct e;
apply andb_prop in H as [_ H]; auto. }
Flover_compute.
repeat eexists; auto.
- unfold isSupersetIntv. now rewrite L0.
- apply (reflect_iff _ _ (Z.leb_spec0 _ _)). auto.
Qed.
(* TODO: maybe put this somewhere else *)
Lemma approxEnv_empty_dVars A1 A2 Gamma fVars dVars E1 E2 :
NatSet.Empty dVars ->
approxEnv E1 Gamma A1 fVars dVars E2 ->
approxEnv E1 Gamma A2 fVars dVars E2.
Proof.
intros He H.
induction H.
- constructor.
- econstructor; eauto.
- exfalso. eapply He. set_tac.
Qed.
Definition checkSubdivsStep e absenv defVars Gamma (b: bool) (PA: precond * analysisResult) :=
let (P, A) := PA in
b && (RangeErrorChecker e A P (FloverMap.empty(SMTLogic * SMTLogic)) defVars Gamma) &&
resultLeq e A absenv.
Definition checkSubdivs e absenv subdivs defVars Gamma :=
fold_left (checkSubdivsStep e absenv defVars Gamma) subdivs true.
Lemma checkSubdivs_false_fp e absenv subdivs defVars Gamma :
fold_left (checkSubdivsStep e absenv defVars Gamma) subdivs false = false.
Proof.
induction subdivs as [|[P A] subdivs]; auto.
Qed.
Lemma checkSubdivs_sound e absenv subdivs defVars Gamma P A :
checkSubdivs e absenv subdivs defVars Gamma = true ->
In (P, A) subdivs ->
RangeErrorChecker e A P (FloverMap.empty(SMTLogic * SMTLogic)) defVars Gamma = true /\
resultLeq e A absenv = true.
Proof.
intros H Hin.
induction subdivs; cbn in Hin; auto.
destruct Hin; subst; auto.
- cbn in *.
destruct (RangeErrorChecker e A P (FloverMap.empty (SMTLogic * SMTLogic)) defVars Gamma) eqn:?;
try (rewrite checkSubdivs_false_fp in H; discriminate H).
split; auto.
destruct (resultLeq e A absenv) eqn: ?; auto.
rewrite checkSubdivs_false_fp in H; auto.
- apply IHsubdivs; auto. cbn in H.
unfold checkSubdivs.
destruct (checkSubdivsStep e absenv defVars Gamma true a) eqn:?; auto.
rewrite checkSubdivs_false_fp in H. discriminate H.
Qed.
(*
Fixpoint merge_subdivs_step (e: expr Q) (acc A1 A2: analysisResult) :=
match FloverMap.find e A1, FloverMap.find e A2 with
| Some (iv1, err1), Some (iv2, err2) =>
let acc1 := FloverMap.add e (unionIntv iv1 iv2, Qmax err1 err2) acc in
match e with
| Unop _ e1 | Downcast _ e1 => merge_subdivs_step e1 acc1 A1 A2
| Binop _ e1 e2 | Let _ _ e1 e2 => let acc2 := merge_subdivs_step e1 acc1 A1 A2 in
merge_subdivs_step e2 acc2 A1 A2
| Fma e1 e2 e3 => let acc2 := merge_subdivs_step e1 acc1 A1 A2 in
let acc3 := merge_subdivs_step e2 acc2 A1 A2 in
merge_subdivs_step e3 acc3 A1 A2
| _ => acc1
end
| _, _ => FloverMap.empty (intv * error)
end.
(* TODO: it might be better to merge all results for one specific expression,
instead of merging 2 results for all expressions *)
Definition merge_subdivs e hd tl : analysisResult :=
fold_left (merge_subdivs_step e (FloverMap.empty (intv * error))) tl hd.
*)
(* TODO: joining of subintervals *)
Definition joinIntv iv1 iv2 : result (option intv) :=
if isSupersetIntv iv2 iv1 then Succes (Some iv1) else
if Qeqb (ivhi iv1) (ivlo iv2) then Succes (Some (ivlo iv1, ivhi iv2)) else Fail _ "intervals don't align".
Definition checkDimensionStep x (ivAcc: result (option intv)) P (* (ivNew: option intv) *) :=
let ivNew := FloverMap.find (Var Q x) P in
match ivAcc with
| Succes ivAcc => match ivNew with
| Some ivNew => optionBind ivAcc (fun iv => joinIntv iv ivNew) (Succes (Some ivNew))
| None => Fail _ "var not found in precond"
end
| f => f
end.
Definition checkDimension x iv Ps :=
match fold_left (checkDimensionStep x) Ps (Succes None) with
| Succes (Some ivU) => if isSupersetIntv iv ivU then Succes true else Fail _ "var not covered"
| Succes None => Fail _ "no subdivisions given"
| Fail _ msg | FailDet msg _ => Fail _ msg
end.
Definition checkAllDimensionsStep Ps b (p: expr Q * intv) :=
match p with
| (Var _ x, iv) => resultBind b (fun _ => checkDimension x iv Ps) (* b && checkDimension x iv Ps *)
| _ => b
end.
Definition checkAllDimensions P Ps :=
fold_left (checkAllDimensionsStep Ps) P (Succes false).
Lemma checkAllDimensionsStep_fail_fp Ps P s :
fold_left (checkAllDimensionsStep Ps) P (Fail bool s) = Fail bool s.
Proof.
induction P as [|p P]; auto.
destruct p as [e iv]. destruct e; auto.
Qed.
Lemma checkAllDimensionsStep_faildet_fp Ps P s b :
fold_left (checkAllDimensionsStep Ps) P (FailDet s b) = FailDet s b.
Proof.
induction P as [|p P]; auto.
destruct p as [e iv]. destruct e; auto.
Qed.
Lemma in_subdivs_intv (Ps: list precondIntv) E (P: precondIntv) :
checkAllDimensions (FloverMap.elements P) Ps = Succes true ->
P_intv_sound E P ->
exists P', In P' Ps /\ P_intv_sound E P'.
Proof.
intros chk H.
unfold P_intv_sound in H.
induction (FloverMap.elements P).
- cbn in chk. discriminate chk.
- cbn in chk.
destruct (checkAllDimensionsStep Ps (Succes false) a) eqn:Heq;
try (rewrite ?checkAllDimensionsStep_fail_fp, ?checkAllDimensionsStep_faildet_fp in chk;
discriminate chk).
destruct b.
+ destruct a as [e iv].
destruct e; try discriminate Heq.
cbn in Heq.
admit. (* this might not work *)
+ apply IHl; auto.
intros x iv inl. apply H. now right.
Abort.
(* TODO: needs more assumptions, i.e. checker for precond *)
Lemma in_subdivs (subdivs: list (precond * analysisResult)) E P :
eval_precond E P ->
exists P' A, In (P', A) subdivs /\ eval_precond E P'.
Admitted.
(* TODO: check precond sound wrt. subdivs *)
(* TODO: merge hd and tl again *)
(** Interval subdivisions checking function **)
Definition SubdivsChecker (e: expr Q) (absenv: analysisResult)
(P: precond) hd tl (defVars: FloverMap.t mType) Gamma :=
validSSA e (preVars P) &&
checkSubdivs e absenv (hd :: tl) defVars Gamma.
(**
Soundness proof for the interval subdivs checker.
**)
Theorem subdivs_checking_sound (e: expr Q) (absenv: analysisResult) P hd_subdivs tl_subdivs defVars Gamma:
forall (E1 E2: env) DeltaMap,
(forall (e': expr R) (m': mType),
exists d: R, DeltaMap e' m' = Some d /\ (Rabs d <= mTypeToR m')%R) ->
eval_precond E1 P ->
getValidMap defVars e (FloverMap.empty mType) = Succes Gamma ->
SubdivsChecker e absenv P hd_subdivs tl_subdivs defVars Gamma = true ->
exists Gamma,
approxEnv E1 (toRExpMap Gamma) absenv (freeVars e) NatSet.empty E2 ->
exists iv err vR vF m,
FloverMap.find e absenv = Some (iv, err) /\
eval_expr E1 (toRTMap (toRExpMap Gamma)) DeltaMapR (toREval (toRExp e)) vR REAL /\
eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e) vF m /\
(forall vF m,
eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e) vF m ->
(Rabs (vR - vF) <= Q2R err))%R.
Proof.
intros * deltas_matched P_valid valid_typeMap subdivs_valid.
andb_to_prop subdivs_valid.
rename L into valid_ssa.
rename R into valid_subdivs.
apply (in_subdivs (hd_subdivs :: tl_subdivs)) in P_valid as [P' [A [in_subdivs P_valid]]].
(* preVars P == preVars P' should hold *)
assert (validSSA e (preVars P') = true) as valid_ssa' by admit.
pose proof (checkSubdivs_sound e _ _ _ _ _ _ valid_subdivs in_subdivs) as [range_err_check A_leq].
assert (ResultChecker e A P' (FloverMap.empty(SMTLogic * SMTLogic)) defVars Gamma = true) as res_check
by (unfold ResultChecker; now rewrite valid_ssa', range_err_check).
exists Gamma; intros approxE1E2.
assert (approxEnv E1 (toRExpMap Gamma) A (freeVars e) NatSet.empty E2) as approxE1E2'
by (eapply approxEnv_empty_dVars; eauto).
assert (validRanges e A E1 (toRTMap (toRExpMap Gamma))) as validRange.
{ eapply result_checking_sound; eauto.
admit. (* unsat_queries of empty map *) }
assert (validErrorBounds e E1 E2 A Gamma DeltaMap) as Hsound.
{ eapply result_checking_sound; eauto.
admit. (* unsat_queries of empty map *) }
eapply validRanges_single in validRange.
destruct validRange as [iv [err [vR [Hfind [eval_real validRange]]]]].
eapply validErrorBounds_single in Hsound; eauto.
destruct Hsound as [[vF [mF eval_float]] err_bounded]; auto.
destruct (resultLeq_sound _ _ _ A_leq) as [iv1 [err1 [iv2 [err2 H]]]].
destruct H as [F1 [F2 [sub err_leq]]].
exists iv2, err2, vR, vF, mF; repeat split; auto.
assert (err = err1) by congruence; subst.
apply Qle_Rle in err_leq.
intros vF0 m Heval.
specialize (err_bounded vF0 m Heval).
lra.
Admitted.
\ No newline at end of file
From Flover
Require Import Infra.RealSimps Infra.RationalSimps Infra.RealRationalProps
Infra.Ltacs RealRangeArith RealRangeValidator RoundoffErrorValidator
Environments TypeValidator FPRangeValidator ExpressionAbbrevs ResultChecker
IntervalArithQ.
(*
From Flover
Require Import Infra.RealRationalProps Environments ExpressionSemantics
IntervalArithQ SMTArith RealRangeArith RealRangeValidator RoundoffErrorValidator
ssaPrgs TypeValidator ErrorAnalysis ResultChecker.
*)
Require Import List.
Fixpoint resultLeq e (A1 A2: analysisResult) :=
match e with
| Unop _ e1 | Downcast _ e1 => resultLeq e1 A1 A2
| Binop _ e1 e2 | Let _ _ e1 e2 => resultLeq e1 A1 A2 && resultLeq e2 A1 A2
| Fma e1 e2 e3 => resultLeq e1 A1 A2 && resultLeq e2 A1 A2 && resultLeq e3 A1 A2
| _ => true
end &&
match FloverMap.find e A1, FloverMap.find e A2 with
| Some (ivA1, errA1), Some (ivA2, errA2) => isSupersetIntv ivA1 ivA2 && (Qleb errA1 errA2)
| _, _ => false
end.
Lemma resultLeq_sound e A1 A2 :
resultLeq e A1 A2 = true ->
exists iv1 err1 iv2 err2,
FloverMap.find e A1 = Some (iv1, err1) /\
FloverMap.find e A2 = Some (iv2, err2) /\
isSupersetIntv iv1 iv2 = true /\
err1 <= err2.
Proof.
intros H.
assert (
match FloverMap.find e A1, FloverMap.find e A2 with
| Some (ivA1, errA1), Some (ivA2, errA2) => isSupersetIntv ivA1 ivA2 && (Qleb errA1 errA2)
| _, _ => false
end = true).
{ unfold resultLeq in H. destruct e;
apply andb_prop in H as [_ H]; auto. }
Flover_compute.
repeat eexists; auto.
- unfold isSupersetIntv. now rewrite L0.
- apply (reflect_iff _ _ (Z.leb_spec0 _ _)). auto.
Qed.
(* TODO: maybe put this somewhere else *)
Lemma approxEnv_empty_dVars A1 A2 Gamma fVars dVars E1 E2 :
NatSet.Empty dVars ->
approxEnv E1 Gamma A1 fVars dVars E2 ->
approxEnv E1 Gamma A2 fVars dVars E2.
Proof.
intros He H.
induction H.
- constructor.
- econstructor; eauto.
- exfalso. eapply He. set_tac.
Qed.
Definition checkSubdivsStep e absenv defVars Gamma (b: bool) (PA: precond * analysisResult) :=
let (P, A) := PA in
b && (RangeErrorChecker e A P (FloverMap.empty(SMTLogic * SMTLogic)) defVars Gamma) &&
resultLeq e A absenv.
Definition checkSubdivs e absenv subdivs defVars Gamma :=
fold_left (checkSubdivsStep e absenv defVars Gamma) subdivs true.
Lemma checkSubdivs_false_fp e absenv subdivs defVars Gamma :
fold_left (checkSubdivsStep e absenv defVars Gamma) subdivs false = false.
Proof.
induction subdivs as [|[P A] subdivs]; auto.
Qed.
Lemma checkSubdivs_sound e absenv subdivs defVars Gamma P A :
checkSubdivs e absenv subdivs defVars Gamma = true ->
In (P, A) subdivs ->
RangeErrorChecker e A P (FloverMap.empty(SMTLogic * SMTLogic)) defVars Gamma = true /\
resultLeq e A absenv = true.
Proof.
intros H Hin.
induction subdivs; cbn in Hin; auto.
destruct Hin; subst; auto.
- cbn in *.
destruct (RangeErrorChecker e A P (FloverMap.empty (SMTLogic * SMTLogic)) defVars Gamma) eqn:?;
try (rewrite checkSubdivs_false_fp in H; discriminate H).
split; auto.
destruct (resultLeq e A absenv) eqn: ?; auto.
rewrite checkSubdivs_false_fp in H; auto.
- apply IHsubdivs; auto. cbn in H.
unfold checkSubdivs.
destruct (checkSubdivsStep e absenv defVars Gamma true a) eqn:?; auto.
rewrite checkSubdivs_false_fp in H. discriminate H.
Qed.
(*
Definition joinIntv iv1 iv2 : result (option intv) :=
if isSupersetIntv iv2 iv1 then Succes (Some iv1) else
if Qeqb (ivhi iv1) (ivlo iv2) then Succes (Some (ivlo iv1, ivhi iv2)) else Fail _ "intervals don't align".
Definition checkDimensionStep x (ivAcc: result (option intv)) P (* (ivNew: option intv) *) :=
let ivNew := FloverMap.find (Var Q x) P in
match ivAcc with
| Succes ivAcc => match ivNew with
| Some ivNew => optionBind ivAcc (fun iv => joinIntv iv ivNew) (Succes (Some ivNew))
| None => Fail _ "var not found in precond"
end
| f => f
end.
Definition checkDimension x iv Ps :=
match fold_left (checkDimensionStep x) Ps (Succes None) with
| Succes (Some ivU) => if isSupersetIntv iv ivU then Succes true else Fail _ "var not covered"
| Succes None => Fail _ "no subdivisions given"
| Fail _ msg | FailDet msg _ => Fail _ msg
end.
Definition checkAllDimensionsStep Ps b (p: expr Q * intv) :=
match p with
| (Var _ x, iv) => resultBind b (fun _ => checkDimension x iv Ps) (* b && checkDimension x iv Ps *)
| _ => b
end.
Definition checkAllDimensions P Ps :=
fold_left (checkAllDimensionsStep Ps) P (Succes false).
Lemma checkAllDimensionsStep_fail_fp Ps P s :
fold_left (checkAllDimensionsStep Ps) P (Fail bool s) = Fail bool s.
Proof.
induction P as [|p P]; auto.
destruct p as [e iv]. destruct e; auto.
Qed.
Lemma checkAllDimensionsStep_faildet_fp Ps P s b :
fold_left (checkAllDimensionsStep Ps) P (FailDet s b) = FailDet s b.
Proof.
induction P as [|p P]; auto.
destruct p as [e iv]. destruct e; auto.
Qed.
*)
Fixpoint coverIntv iv intvs :=
match intvs with
| nil => false
| intv :: nil => isSupersetIntv iv intv
| intv :: intvs =>
Qleb (ivlo intv) (ivlo iv) && coverIntv (ivhi intv, ivhi iv) intvs
end.
Lemma coverIntv_sound iv intvs v :
coverIntv iv intvs = true ->
(Q2R (ivlo iv) <= v <= Q2R (ivhi iv))%R ->
exists intv, In intv intvs /\ (Q2R (ivlo intv) <= v <= Q2R (ivhi intv))%R.
Proof.
induction intvs as [|intv0 intvs] in iv |- *; [intros H; discriminate H|].
destruct intvs as [|intv1 intvs]; cbn; intros H Hin.
- exists intv0. split; auto. andb_to_prop H. canonize_hyps. cbn in *. lra.
- destruct (Rle_or_lt v (Q2R (ivhi intv0))) as [Hle|Hlt].
+ andb_to_prop H.
canonize_hyps.
exists intv0. split; cbn; auto.
cbn in *. lra.
+ andb_to_prop H.
destruct (IHintvs (ivhi intv0, ivhi iv)) as [intv [inl Hin1]]; eauto.
cbn in *. lra.
Qed.
Definition addToBucket x iv P :=
match P with
| nil => Fail _ "var not found in precond"
| (e, ivE) :: P =>
match Q_orderedExps.exprCompare e (Var Q x) with
| Eq =>
if isSupersetIntv iv ivE then Succes (iv, Some P) else Succes (ivE, None)
| _ => Fail _ "var not found in precond"
end
end.
Fixpoint mergeDim_aux x Ps iv b :=
match Ps with
| nil => Succes ((iv, rev b) :: nil)
| P :: Ps =>
match addToBucket x iv P with
| Succes (ivN, Some P') => mergeDim_aux x Ps iv (P' :: b)
| Succes (ivN, None) => resultBind (mergeDim_aux x Ps ivN nil)
(fun rest => Succes ((iv, rev b) :: rest))
| Fail _ msg | FailDet msg _ => Fail _ msg
end
end.
(* x := current variable being checked
Ps := list of preconditions for the subdivision
*)
Definition mergeDim x Ps :=
match Ps with
| nil => Fail _ "precond not found"
| nil :: _ => Fail _ "var not found in precond"
| ((e, iv) :: P) :: _ => mergeDim_aux x Ps iv nil
end.
(* x := current variable being checked
Px := global precondition for x
Ps := list of preconditions for the subdivision
last_iv := option of last seen interval
*)
(*
Definition checkDim x Px Ps curr_iv :=
match Ps with
| nil => (* check Px upper bounded by curr_iv *)
| Ps1::Ps_rem =>
let iv_x := find (fun e => isEq (Q_orderedExps.exprCompare (Var Q x) e)) Ps1 in
match iv_x with
| None => Fail _ "var not found"
| Some iv_x =>
match Ps with
| nil => Fail _ "precond not found"
| nil :: _ => Fail _ "var not found in precond"
| ((e, iv) :: P) :: _ => checkDim_aux x Px Ps iv nil
end.
*)
Lemma mergeDim_aux_sound x Ps iv b res :
mergeDim_aux x Ps iv b = Succes res ->
forall ivb Psb P,
In (ivb, Psb) res ->
In P Psb ->
(In P b -> forall iv', ~ In ((Var Q x, iv') :: P) Ps \/ isSupersetIntv ivb iv' = false) /\
(~ In P b -> exists iv', In ((Var Q x, iv') :: P) Ps /\ isSupersetIntv ivb iv' = true).
Proof.
induction Ps as [|P Ps] in iv, b, res |- *.
- cbn; intros H; inversion H. intros * Hin HinR.
inversion Hin; inversion H0; subst. admit. (* exfalso. now eapply Hnin, in_rev. *)
- cbn; intros H ivb Psb Pb inRes inPsb.
destruct (addToBucket x iv P) eqn:Heq; try discriminate H.