diff --git a/coq/SubdivsChecker.v b/coq/SubdivsChecker.v index 78ff12066a6a4bd4b6f9882b53977f313c0ab7a8..6bf61647c156b802ce9b5d19260c910a622b9094 100644 --- a/coq/SubdivsChecker.v +++ b/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 *)