diff --git a/coq/SubdivsChecker2.v b/attic/coq/SubdivsChecker2.v similarity index 86% rename from coq/SubdivsChecker2.v rename to attic/coq/SubdivsChecker2.v index 2d2eefe3b73ab44267fac2e0f0957732bc59012f..edcffb6031781a4f35e371d8aa4b3fc2b54d2fc9 100644 --- a/coq/SubdivsChecker2.v +++ b/attic/coq/SubdivsChecker2.v @@ -189,6 +189,9 @@ Fixpoint mergeDim_aux x Ps iv b := 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" @@ -196,22 +199,46 @@ Definition mergeDim x Ps := | ((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 -> - exists iv', In ((Var Q x, iv') :: P) Ps /\ isSupersetIntv ivb iv' = true. + (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 Hnin. - inversion Hin; inversion H0; subst. exfalso. now eapply Hnin, in_rev. - - cbn; intros H ivb Psb Pb inRes inPsb Hnin. + - 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. destruct p as [ivN [P'|]]. + (* specialize (IHPs _ _ _ H ivb Psb Pb inRes inPsb). *) - (* P = (Var _ x, ivE) :: P' *) + (* P = (Var _ x, ivE) :: P' by addToBucket_sound *) + (* assert (Pb = P') as HPb by admit; subst. *) assert (Pb <> P') as Hneq by admit. edestruct IHPs as [iv' [Hin Hsub]]; eauto. @@ -224,7 +251,20 @@ Proof. * exfalso. inversion beq; subst. now apply Hnin, in_rev. * specialize (IHPs _ _ _ Hrec ivb Psb Pb inL inPsb). destruct IHPs as [iv' [Hin Hsub]]; eauto. -Abort. +Admitted. + +Lemma mergeDim_sound x Ps res : + mergeDim x Ps = Succes res -> + forall ivb Psb P, + In (ivb, Psb) res -> + In P Psb -> + exists iv', In ((Var Q x, iv') :: P) Ps /\ isSupersetIntv ivb iv' = true. +Proof. + intros chk. + destruct Ps as [|[|[e iv] P] Ps]; try discriminate chk. + intros. + eapply mergeDim_aux_sound; eauto. +Qed. Fixpoint covers (P: list (expr Q * intv)) Ps := match P with @@ -260,16 +300,26 @@ Proof. apply andb_prop in chk as [rec curr]. destruct (H n iv) as [v [Hf Hc]]; try now constructor. destruct (coverIntv_sound _ _ curr Hc) as [iv' [Hin Hc']]. - admit. - -Admitted. + apply in_map_iff in Hin as [[iv0 b] [Hiv0 Hin]]. + cbn in *; subst. + eapply forallb_forall in rec; [| apply in_map_iff; eauto]. + destruct (IHP _ rec) as [P' [inb valid_P']]; auto. + destruct (mergeDim_sound _ _ Hres _ _ _ Hin inb) as [iv0 [inPs Hsub]]. + eexists; split; eauto. + intros x iv1 [Heq| inP']. + + inversion Heq; subst. + eexists; split; eauto. + Flover_compute. + canonize_hyps. + cbn in *. lra. + + auto. +Qed. Definition checkCoverage (subdivs: list precond) (P: precond) := let Piv := FloverMap.elements (fst P) in let Ps := map (fun P => FloverMap.elements (fst P)) subdivs in covers Piv Ps && true. (* TODO check additional constraints *) -(* TODO: needs more assumptions, i.e. checker for additional constraints *) Lemma in_subdivs (subdivs: list (precond * analysisResult)) E P : checkCoverage (map fst subdivs) P = true -> eval_precond E P ->