moving another old version to attic

coq/SubdivsChecker2.v → 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 ->