more work on subdiv checker

coq/CertificateChecker.v

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

coq/SubdivsChecker2.v

@@ -2,7 +2,7 @@ From Flover
      Require Import Infra.RealSimps Infra.RationalSimps Infra.RealRationalProps
      Infra.Ltacs RealRangeArith RealRangeValidator RoundoffErrorValidator
      Environments TypeValidator FPRangeValidator ExpressionAbbrevs ResultChecker
-     IntervalArithQ Expressions.
+     IntervalArithQ.
 (*
 From Flover
      Require Import Infra.RealRationalProps Environments ExpressionSemantics
@@ -148,80 +148,89 @@ Fixpoint coverIntv iv intvs :=
     Qleb (ivlo intv) (ivlo iv) && coverIntv (ivhi intv, ivhi iv) intvs
   end.
 
-Lemma coverIntv_sound iv intvs a :
+Lemma coverIntv_sound iv intvs v :
   coverIntv iv intvs = true ->
-  contained a iv ->
-  exists intv, In intv intvs /\ contained a intv.
+  (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. repeat canonize_Q_prop. unfold contained in *. lra.
-  - destruct (Qleb a (ivhi intv0)) eqn: Heq.
+  - 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.
-      repeat canonize_Q_prop.
+      canonize_hyps.
       exists intv0. split; cbn; auto.
-      unfold contained in *.
       cbn in *. lra.
     + andb_to_prop H.
-      destruct (IHintvs (ivhi intv0, ivhi iv)) as [intv [inl Hin1]].
-      * auto.
-      * assert (ivhi intv0 <= a) as H.
-        { apply Qnot_lt_le.
-          intros Hlt.
-          apply Qlt_le_weak in Hlt.
-          apply Qle_bool_iff in Hlt. unfold Qleb in Heq. rewrite Heq in Hlt.
-          discriminate Hlt. }
-        unfold contained in *. cbn in *. lra.
-      * exists intv. auto.
+      destruct (IHintvs (ivhi intv0, ivhi iv)) as [intv [inl Hin1]]; eauto.
+      cbn in *. lra.
 Qed.
 
-Definition addToBucketResb x ivO P :=
+Definition addToBucket x iv P :=
   match P with
   | nil => Fail _ "var not found in precond"
   | (e, ivE) :: P =>
     match Q_orderedExps.exprCompare e (Var Q x) with
     | Eq =>
-      match ivO with
-      | Some iv =>
-        if isSupersetIntv iv ivE then Succes (ivO, Some P) else Succes (Some ivE, None)
-      | None => Succes (Some ivE, Some P)
-      end
+      if isSupersetIntv iv ivE then Succes (iv, Some P) else Succes (ivE, None)
     | _ => Fail _ "var not found in precond"
     end
   end.
 
-Fixpoint mergeDim x Ps ivO b :=
+Fixpoint mergeDim_aux x Ps iv b :=
   match Ps with
-  | nil => match ivO with
-          | Some iv => Succes ((iv, rev b) :: nil)
-          | None => Fail _ "no interval for bucket"
-          end
+  | nil => Succes ((iv, rev b) :: nil)
   | P :: Ps =>
-    match addToBucketResb x ivO P with
-    | Succes (ivN, Some P') => mergeDim x Ps ivN (P' :: b)
-    | Succes (ivN, None) => resultBind (mergeDim x Ps ivN nil)
-                                      (fun rest => match ivO with
-                                                | Some iv => Succes ((iv, rev b) :: rest)
-                                                | None => Fail _ "no interval for bucket"
-                                                end)
+    match addToBucket x iv P with
+    | Succes (ivN, Some P') => mergeDim_aux x Ps iv (P' :: b)
+    | Succes (ivN, None) => resultBind (mergeDim_aux x Ps ivN nil)
+                                      (fun rest => Succes ((iv, rev b) :: rest))
     | Fail _ msg | FailDet msg _ => Fail _ msg
     end
   end.
 
-Lemma mergeDim_sound x Ps ivO iv b Psb res :
-  mergeDim x Ps ivO b = Succes res ->
-  In (iv, Psb) res ->
-  forall P, In P Psb -> exists iv', In ((Var Q x, iv') :: P) Ps /\ isSupersetIntv iv iv' = true.
+Definition mergeDim x Ps :=
+  match Ps with
+  | nil => Fail _ "precond not found"
+  | nil :: _ => Fail _ "var not found in precond"
+  | ((e, iv) :: P) :: _ => mergeDim_aux x 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.
 Proof.
-  induction Ps.
-  - cbn; intros H; inversion H.
+  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.
+    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' *)
+
+      assert (Pb <> P') as Hneq by admit.
+      edestruct IHPs as [iv' [Hin Hsub]]; eauto.
+      intros [<- | inb]; auto.
+    + destruct (mergeDim_aux x Ps ivN nil) eqn:Hrec; try discriminate H.
+      cbn in *.
+      symmetry in H.
+      inversion H; subst.
+      destruct inRes as [beq|inL].
+      * 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.
 
 Fixpoint covers (P: list (expr Q * intv)) Ps :=
   match P with
   | nil => match Ps with nil :: nil => true | _ => false end
   | (Var _ x, iv) :: P =>
-    match mergeDim x Ps None nil with
+    match mergeDim x Ps with
     | Succes res =>
       let intvs := map fst res in
       let buckets := map snd res in
@@ -247,10 +256,10 @@ Proof.
     destruct P'; try discriminate chk. auto.
   - cbn in chk.
     destruct e; try discriminate chk.
-    destruct (mergeDim n  Ps None nil) as [res| |] eqn:Hres; try discriminate chk.
+    destruct (mergeDim n  Ps) as [res| |] eqn:Hres; try discriminate chk.
     apply andb_prop in chk as [rec curr].
     destruct (H n iv) as [v [Hf Hc]]; try now constructor.
-    (* destruct (coverIntv_sound *)
+    destruct (coverIntv_sound _ _ curr Hc) as [iv' [Hin Hc']].
     admit.
 
 Admitted.
@@ -260,7 +269,7 @@ Definition checkCoverage (subdivs: list precond) (P: precond) :=
   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 precond *)
+(* 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 ->