more work on subdivchecker

coq/SubdivsChecker.v

@@ -133,46 +133,54 @@ Definition checkDimensionStep x (ivAcc: result (option intv)) P (* (ivNew: optio
 
 Definition checkDimension x iv Ps :=
   match fold_left (checkDimensionStep x) Ps (Succes None) with
-  | Succes (Some ivU) => isSupersetIntv iv ivU
-  | _ => false
-          (*
+  | 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) => b && checkDimension x iv Ps
+  | (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 true.
+  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 = true ->
+  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).
-  - admit.
+  - cbn in chk. discriminate chk.
   - cbn in chk.
-    assert (checkAllDimensionsStep Ps true a = true) as Heq by admit.
-    rewrite Heq in chk.
-    apply IHl; auto.
-    intros x iv.
-    intros ?. apply H. now right.
-    (*
-    assert (a = (Var Q x, iv) \/ a <> (Var Q x, iv)) as CA by admit.
-    destruct CA as [? | Hneq].
-    + subst.
+    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.
-      intros ?. apply H. now right.
-    + intros ?. apply H. now right.
-*)
+      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 *)