moving old versions of subdiv checker to attic

coq/SubdivsChecker3.v → attic/coq/SubdivsChecker1.v

 From Flover
      Require Import Infra.RealSimps Infra.RationalSimps Infra.RealRationalProps
      Infra.Ltacs RealRangeArith RealRangeValidator RoundoffErrorValidator
-     Environments TypeValidator FPRangeValidator ExpressionAbbrevs ResultChecker
-     IntervalArithQ.
+     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.
-Require Import FunInd.
 
 Fixpoint resultLeq e (A1 A2: analysisResult) :=
   match e with
@@ -89,276 +93,108 @@ Proof.
     rewrite checkSubdivs_false_fp in H. discriminate H.
 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.
-
-Fixpoint getBucket x iv Ps :=
-  match Ps with
-  | nil => (nil, nil)
-  | P :: Ps' =>
-    match P with
-    | nil => (nil, Ps) (* fail *)
-    | (e, ivE) :: P' =>
-       match Q_orderedExps.compare e (Var Q x) with
-       | Eq =>
-         if isSupersetIntv iv ivE then
-           let (b, rest) := getBucket x iv Ps' in (P' :: b, rest)
-         else (nil, Ps)
-       | _ => (nil, Ps) (* fail *)
-       end
+(*
+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.
 
-Lemma getBucket_length x iv Ps b rest :
-  getBucket x iv Ps = (b, rest) ->
-  length Ps = length (b ++ rest).
-Proof with try now injection 1; intros; subst.
-  induction Ps as [|P Ps] in b |- *; cbn...
-  destruct P as [|[e ivE] P]...
-  destruct (Q_orderedExps.compare e (Var Q x)) eqn:?...
-  destruct (isSupersetIntv iv ivE) eqn:?...
-  destruct (getBucket x iv Ps) eqn:?...
-  injection 1; intros; subst.
-  cbn. now rewrite <- IHPs.
-Qed.
-
-Lemma getBucket_sound x iv Ps b rest :
-  getBucket x iv Ps = (b, rest) ->
-  forall P, In P b ->
-       exists ivx, In ((Var Q x, ivx) :: P) Ps /\ isSupersetIntv iv ivx = true.
-Proof with try now injection 1; intros; subst.
-  induction Ps as [|P1 Ps] in b |- *; cbn...
-  destruct P1 as [|[e ivE] P1]...
-  cbn.
-  destruct (Q_orderedExps.compare e (Var Q x)) eqn:Heqc...
-  destruct (isSupersetIntv iv ivE) eqn:?...
-  destruct (getBucket x iv Ps) eqn:?...
-  injection 1; intros; subst.
-  destruct H2 as [-> | Hin].
-  - assert (e = Var Q x)
-      by (destruct e; try discriminate Heqc;
-        now rewrite (nat_compare_eq _ _ Heqc)).
-    exists ivE. subst. split; auto.
-  - edestruct IHPs as [ivx [inPs sub]]; eauto.
-Qed.
+(* 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.
+*)
 
-Lemma getBucket_rest_sound x iv Ps b rest :
-  getBucket x iv Ps = (b, rest) ->
-  forall P, In P rest -> In P Ps.
-Proof with try now injection 1; intros; subst.
-  induction Ps as [|P Ps] in b |- *; cbn...
-  destruct P as [|[e ivE] P]...
-  destruct (Q_orderedExps.compare e (Var Q x)) eqn:?...
-  destruct (isSupersetIntv iv ivE) eqn:?...
-  destruct (getBucket x iv Ps) eqn:?...
-  injection 1; intros; subst.
-  right. eapply IHPs; eauto.
-Qed.
-(*
-Function checkDim cov x iv Ps {measure length Ps} :=
-  match Ps with
-  | nil => false
-  | P :: _ =>
-    match FloverMap.find (Var Q x) P with
-    | Some ivx =>
-      let (b, rest) := getBucket_aux x ivx Ps in
-      let covb := cov b in
-      covb && match rest with
-              | nil => isSupersetIntv iv ivx
-              | _ => checkDim cov x (snd ivx, snd iv) rest
-              end
-    | None => false
-    end
+(* 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.
-intros cov x iv Ps P Ps' HPs ivx Hfind b rest P' rest' Hrest.
-rewrite <- Hrest.
-rewrite <- HPs at 2.
-cbn.
-unfold addToBucket.
-rewrite Hfind.
-unfold isSupersetIntv, Qleb, Qle_bool.
-rewrite !Z.leb_refl.
-rewrite <- HPs.
-cbn.
-destruct (getBucket_aux x ivx Ps') eqn:Heq.
-apply getBucket_aux_sound in Heq.
-clear Hrest rest'.
-injection 1; intros; subst.
-cbn.
-rewrite Heq, app_length.
-apply le_lt_n_Sm, le_plus_r.
-Defined.
-*)
 
-Function checkDim cov x iv Ps {measure length Ps} :=
-  match Ps with
-  | nil => false
-  | P :: _ =>
-    match P with
-    | (e, ivx) :: _ =>
-      match Q_orderedExps.compare e (Var Q x) with
-      | Eq =>
-        let (b, rest) := getBucket x ivx Ps in
-        if isSupersetIntv iv ivx then cov b
-        else cov b && Qleb (fst ivx) (fst iv) && checkDim cov x (snd ivx, snd iv) rest
-      | _ => false
-      end
-    | _ => false
-    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.
-intros cov x iv Ps P rest [e ivE] b e' ivx H HP HPs Heq b' rest'.
-rewrite <- HPs at 2.
-cbn.
-rewrite Heq.
-unfold isSupersetIntv, Qleb, Qle_bool.
-rewrite !Z.leb_refl.
-rewrite <- HPs.
-destruct (getBucket x ivx rest) eqn:Hb.
-injection 1; intros; subst.
-cbn.
-rewrite (getBucket_length _ _ _ Hb); eauto.
-rewrite app_length.
-apply le_lt_n_Sm, le_plus_r.
-Defined.
 
-Fixpoint covers (P: list (expr Q * intv)) Ps :=
-  match P with
-  | nil => match Ps with nil::nil => true | _ => false end
-  | (Var _ x, iv) :: P =>
-    checkDim (covers P) x iv Ps
-  | _ :: P => false
+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.
 
-Lemma covers_sound P Ps E :
-  covers P Ps = true ->
-  eval_preIntv E P ->
-  exists P', In P' Ps /\ eval_preIntv E P'.
-Proof.
-  induction P as [|[e iv] P] in Ps |- *.
-  - cbn. destruct Ps as [|[|? ?] [|? ?]] eqn:Heq; try discriminate 1.
-    intros _ _.
-    exists nil; split; try now constructor.
-    intros x iv H. exfalso. apply (in_nil H).
-  - destruct e; cbn; intros H; try discriminate H.
-    intros HPl.
-    assert (exists vR : R, E n = Some vR /\ (Q2R (fst iv) <= vR <= Q2R (snd iv))%R)
-      as [v [inE iniv]]
-        by (apply HPl; now constructor).
-    functional induction checkDim (covers P) n iv Ps; try discriminate H.
-    + destruct (IHP _ H) as [P' [inb HP']].
-      { hnf. intros. apply HPl. now constructor. }
-      destruct (getBucket_sound _ _ _ e3 _ inb) as [iv1 [Hin1 Hsub1]].
-      eexists; split; eauto.
-      intros x iv' [Heq | inP']; auto.
-      injection Heq. intros; subst.
-      cbn in *.
-      Flover_compute.
-      canonize_hyps.
-      cbn in *; subst.
-      exists v. split; [auto | lra].
-    + Flover_compute.
-      destruct (Rle_or_lt v (Q2R (snd ivx))) as [Hle|Hlt].
-      * destruct (IHP _ L0) as [P' [inb HP']].
-        { hnf. intros. apply HPl. now constructor. }
-        destruct (getBucket_sound _ _ _ e3 _ inb) as [iv1 [Hin1 Hsub1]].
-        eexists; split; eauto.
-        intros x iv' [Heq | inP']; auto.
-        injection Heq. intros; subst.
-        cbn in *.
-        Flover_compute.
-        canonize_hyps.
-        cbn in *; subst.
-        exists v. split; [auto | lra].
-      * assert (Q2R (snd ivx) <= v <= Q2R (snd iv))%R as Hv.
-        { unfold isSupersetIntv in *. cbn in *.
-          rewrite R0 in *. cbn in *.
-          canonize_hyps. split; lra. }
-        destruct IHb0 as [P' [inrest H]]; auto.
-        { intros x iv' [Heq | inP]; auto.
-          injection Heq; intros; subst.
-          cbn. exists v. split; auto. apply HPl; cbn; auto. }
-        exists P'; split; auto.
-        eapply getBucket_rest_sound; eauto.
-Qed.
+Definition checkAllDimensions P Ps :=
+  fold_left (checkAllDimensionsStep Ps) P (Succes false).
 
-Lemma covers_preVars P Ps :
-  covers P Ps = true ->
-  forall P1, In P1 Ps -> NatSet.Equal (preIntvVars P1) (preIntvVars P).
+Lemma checkAllDimensionsStep_fail_fp Ps P s :
+  fold_left (checkAllDimensionsStep Ps) P (Fail bool s) = Fail bool s.
 Proof.
-  induction P as [|[e iv] P] in Ps |- *.
-  - cbn. destruct Ps as [|[|? ?] [|? ?]] eqn:Heq; try discriminate 1.
-    intros _ P [H|[]].
-    rewrite <- H. cbn. apply NatSetProps.equal_refl.
-  - cbn. destruct e; try discriminate 1.
-Admitted.
-
-Definition checkPreconds (subdivs: list precond) (P: precond) :=
-  let Piv := FloverMap.elements (fst P) in
-  let Ps := map (fun P => FloverMap.elements (fst P)) subdivs in
-  let S_qs := map snd subdivs in
-  covers Piv Ps && forallb (fun q => SMTLogic_eqb q (snd P)) S_qs.
+  induction P as [|p P]; auto.
+  destruct p as [e iv]. destruct e; auto.
+Qed.
 
-Lemma checkPreconds_sound (subdivs: list precond) E P :
-  checkPreconds subdivs P = true ->
-  eval_precond E P ->
-  exists P1, In P1 subdivs /\ eval_precond E P1.
+Lemma checkAllDimensionsStep_faildet_fp Ps P s b :
+  fold_left (checkAllDimensionsStep Ps) P (FailDet s b) = FailDet s b.
 Proof.
-  intros H [Pintv Hq].
-  apply andb_true_iff in H as [cov Hqs].
-  eapply covers_sound in cov; eauto.
-  destruct cov as [Pl1 [Hin H]].
-  apply in_map_iff in Hin as [P1 [Heq1 Hin]].
-  exists P1. split; auto.
-  rewrite <- Heq1 in H.
-  split; auto.
-  eapply forallb_forall in Hqs.
-  - eapply SMTLogic_eqb_sound; eauto.
-  - apply in_map_iff; eauto.
+  induction P as [|p P]; auto.
+  destruct p as [e iv]. destruct e; auto.
 Qed.
 
-Lemma checkPreconds_preVars subdivs P :
-  checkPreconds subdivs P = true ->
-  forall P1, In P1 subdivs -> NatSet.Equal (preVars P1) (preVars P).
+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 P1 Hin. Flover_compute.
-  unfold preVars.
-  eapply forallb_forall in R.
-  2: apply in_map_iff; eauto.
-  erewrite SMTLogic_eqb_varsLogic; eauto.
-  apply NatSetProps.union_equal_1.
-  eapply covers_preVars; eauto.
-  apply in_map_iff; eauto.
-Qed.
+  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) &&
-           checkPreconds (map fst (hd :: tl)) P &&
            checkSubdivs e absenv (hd :: tl) defVars Gamma.
 
 (**
@@ -381,16 +217,15 @@ Theorem subdivs_checking_sound (e: expr Q) (absenv: analysisResult) P hd_subdivs
             eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e) vF m ->
             (Rabs (vR - vF) <= Q2R err))%R.
 Proof.
-  intros * deltas_matched P_valid valid_typeMap chk.
-  apply andb_prop in chk as [chk valid_subdivs].
-  apply andb_prop in chk as [valid_ssa valid_cover].
-  eapply (checkPreconds_sound (* (hd_subdivs :: tl_subdivs) *)) in P_valid as [P1 [in_subdivs P_valid]]; eauto.
-  assert (validSSA e (preVars P1) = true) as valid_ssa'.
-  { eapply validSSA_eq_set; eauto. eapply checkPreconds_preVars; eauto. }
-  apply in_map_iff in in_subdivs as [[P2 A] [Heq in_subdivs]].
-  cbn in Heq; subst.
+  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 P1 (FloverMap.empty(SMTLogic * SMTLogic))  defVars Gamma = true) as res_check
+  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'

coq/CertificateChecker.v

@@ -6,7 +6,7 @@
 **)
 From Flover
      Require Import Infra.RealRationalProps Environments TypeValidator
-     ResultChecker SubdivsChecker3.
+     ResultChecker SubdivsChecker.
 
 Require Export List ExpressionSemantics Coq.QArith.QArith Flover.SMTArith.
 Export ListNotations.

coq/SubdivsChecker.v

 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.
-*)
+     Environments TypeValidator FPRangeValidator ExpressionAbbrevs ResultChecker
+     IntervalArithQ.
 
 Require Import List.
+Require Import FunInd.
 
 Fixpoint resultLeq e (A1 A2: analysisResult) :=
   match e with
@@ -93,108 +89,276 @@ Proof.
     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)
+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.
 
-(* 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.
-*)
+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.
 
-(* 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
+Fixpoint getBucket x iv Ps :=
+  match Ps with
+  | nil => (nil, nil)
+  | P :: Ps' =>
+    match P with
+    | nil => (nil, Ps) (* fail *)
+    | (e, ivE) :: P' =>
+       match Q_orderedExps.compare e (Var Q x) with
+       | Eq =>
+         if isSupersetIntv iv ivE then
+           let (b, rest) := getBucket x iv Ps' in (P' :: b, rest)
+         else (nil, Ps)
+       | _ => (nil, Ps) (* fail *)
+       end
+    end
   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
+Lemma getBucket_length x iv Ps b rest :
+  getBucket x iv Ps = (b, rest) ->
+  length Ps = length (b ++ rest).
+Proof with try now injection 1; intros; subst.
+  induction Ps as [|P Ps] in b |- *; cbn...
+  destruct P as [|[e ivE] P]...
+  destruct (Q_orderedExps.compare e (Var Q x)) eqn:?...
+  destruct (isSupersetIntv iv ivE) eqn:?...
+  destruct (getBucket x iv Ps) eqn:?...
+  injection 1; intros; subst.
+  cbn. now rewrite <- IHPs.
+Qed.
+
+Lemma getBucket_sound x iv Ps b rest :
+  getBucket x iv Ps = (b, rest) ->
+  forall P, In P b ->
+       exists ivx, In ((Var Q x, ivx) :: P) Ps /\ isSupersetIntv iv ivx = true.
+Proof with try now injection 1; intros; subst.
+  induction Ps as [|P1 Ps] in b |- *; cbn...
+  destruct P1 as [|[e ivE] P1]...
+  cbn.
+  destruct (Q_orderedExps.compare e (Var Q x)) eqn:Heqc...
+  destruct (isSupersetIntv iv ivE) eqn:?...
+  destruct (getBucket x iv Ps) eqn:?...
+  injection 1; intros; subst.
+  destruct H2 as [-> | Hin].
+  - assert (e = Var Q x)
+      by (destruct e; try discriminate Heqc;
+        now rewrite (nat_compare_eq _ _ Heqc)).
+    exists ivE. subst. split; auto.
+  - edestruct IHPs as [ivx [inPs sub]]; eauto.
+Qed.
+
+Lemma getBucket_rest_sound x iv Ps b rest :
+  getBucket x iv Ps = (b, rest) ->
+  forall P, In P rest -> In P Ps.
+Proof with try now injection 1; intros; subst.
+  induction Ps as [|P Ps] in b |- *; cbn...
+  destruct P as [|[e ivE] P]...
+  destruct (Q_orderedExps.compare e (Var Q x)) eqn:?...
+  destruct (isSupersetIntv iv ivE) eqn:?...
+  destruct (getBucket x iv Ps) eqn:?...
+  injection 1; intros; subst.
+  right. eapply IHPs; eauto.
+Qed.
+(*
+Function checkDim cov x iv Ps {measure length Ps} :=
+  match Ps with
+  | nil => false
+  | P :: _ =>
+    match FloverMap.find (Var Q x) P with
+    | Some ivx =>
+      let (b, rest) := getBucket_aux x ivx Ps in
+      let covb := cov b in
+      covb && match rest with
+              | nil => isSupersetIntv iv ivx
+              | _ => checkDim cov x (snd ivx, snd iv) rest
+              end
+    | None => false
+    end
   end.
+intros cov x iv Ps P Ps' HPs ivx Hfind b rest P' rest' Hrest.
+rewrite <- Hrest.
+rewrite <- HPs at 2.
+cbn.
+unfold addToBucket.
+rewrite Hfind.
+unfold isSupersetIntv, Qleb, Qle_bool.
+rewrite !Z.leb_refl.
+rewrite <- HPs.
+cbn.
+destruct (getBucket_aux