adjusting eval_precond

coq/IntervalValidation.v

@@ -145,9 +145,9 @@ Theorem validIntervalbounds_sound (f:expr Q) (A:analysisResult) (P: FloverMap.t
   ssa f (NatSet.union fVars dVars) outVars ->
   validIntervalbounds f A P dVars = true ->
   dVars_range_valid dVars E A ->
-  NatSet.Subset (preIntvVars P) fVars ->
+  NatSet.Subset (preIntvVars (FloverMap.elements P)) fVars ->
   NatSet.Subset ((Expressions.freeVars f) -- dVars) fVars ->
-  P_intv_sound E P ->
+  eval_preIntv E (FloverMap.elements P) ->
   validTypes f Gamma ->
   validRanges f A E (toRTMap (toRExpMap Gamma)).
 Proof.

coq/RealRangeArith.v

@@ -28,8 +28,8 @@ Definition P_intv_sound E (P: precond) :=
              -> exists vR: R, E x = Some vR /\ Q2R (fst iv) <= vR <= Q2R (snd iv).
 *)
 
-Definition P_intv_sound E (P: precondIntv) :=
-  forall x iv, List.In (Var Q x, iv) (FloverMap.elements P) ->
+Definition eval_preIntv E P :=
+  forall x iv, List.In (Var Q x, iv) P ->
           exists vR: R, E x = Some vR /\ (Q2R (fst iv) <= vR <= Q2R (snd iv))%R.
 
 Definition addVar2Set (elt: (expr Q * intv)) s :=
@@ -38,14 +38,14 @@ Definition addVar2Set (elt: (expr Q * intv)) s :=
   | _ => s
   end.
 
-Definition preIntvVars (P: precondIntv) :=
-  List.fold_right addVar2Set NatSet.empty (FloverMap.elements P).
+Definition preIntvVars P :=
+  List.fold_right addVar2Set NatSet.empty P.
 
 Lemma preIntvVars_sound P x iv :
-  List.In (Var Q x, iv) (FloverMap.elements P) -> x ∈ (preIntvVars P).
+  List.In (Var Q x, iv) P -> x ∈ (preIntvVars P).
 Proof.
   unfold preIntvVars.
-  induction (FloverMap.elements P).
+  induction P.
   - cbn. tauto.
   - cbn. intros [-> | ?]; cbn; set_tac.
     destruct a as [e ?]; destruct e; auto. cbn. set_tac.

coq/SMTArith.v

@@ -338,6 +338,33 @@ Fixpoint varsLogic (q: SMTLogic) :=
   | OrQ q1 q2 => varsLogic q1 ∪ varsLogic q2
   end.
 
+Lemma SMTArith_eqb_varsSMT e1 e2 :
+  SMTArith_eqb e1 e2 = true ->
+  varsSMT e1 = varsSMT e2.
+Proof.
+  induction e1 in e2 |- *; destruct e2; try discriminate 1; cbn; auto; intros H.
+  - apply beq_nat_true in H. now subst.
+  - Flover_compute. erewrite IHe1_1; eauto. erewrite IHe1_2; eauto.
+  - Flover_compute. erewrite IHe1_1; eauto. erewrite IHe1_2; eauto.
+  - Flover_compute. erewrite IHe1_1; eauto. erewrite IHe1_2; eauto.
+  - Flover_compute. erewrite IHe1_1; eauto. erewrite IHe1_2; eauto.
+Qed.
+
+Lemma SMTLogic_eqb_varsLogic q1 q2 :
+  SMTLogic_eqb q1 q2 = true ->
+  varsLogic q1 = varsLogic q2.
+Proof.
+  induction q1 in q2 |- *; destruct q2; try discriminate 1; cbn; auto; intros H.
+  - Flover_compute. erewrite SMTArith_eqb_varsSMT; eauto.
+    erewrite (SMTArith_eqb_varsSMT e2); eauto.
+  - Flover_compute. erewrite SMTArith_eqb_varsSMT; eauto.
+    erewrite (SMTArith_eqb_varsSMT e2); eauto.
+  - Flover_compute. erewrite SMTArith_eqb_varsSMT; eauto.
+    erewrite (SMTArith_eqb_varsSMT e2); eauto.
+  - Flover_compute. erewrite IHq1_1; eauto. erewrite IHq1_2; eauto.
+  - Flover_compute. erewrite IHq1_1; eauto. erewrite IHq1_2; eauto.
+Qed.
+
 Lemma eval_smt_updEnv x v r E e :
   ~ (x ∈ varsSMT e) ->
   eval_smt E e v <-> eval_smt (updEnv x r E) e v.
@@ -399,10 +426,11 @@ Qed.
 
 Definition precond : Type := precondIntv * SMTLogic.
 
-Definition preVars (P: precond) := preIntvVars (fst P) ∪ varsLogic (snd P).
+Definition preVars (P: precond) :=
+  preIntvVars (FloverMap.elements (fst P)) ∪ varsLogic (snd P).
 
 Definition eval_precond E (P: precond) :=
-  P_intv_sound E (fst P) /\ eval_smt_logic E (snd P).
+  eval_preIntv E (FloverMap.elements (fst P)) /\ eval_smt_logic E (snd P).
 
 Lemma eval_precond_updEnv E x v P :
   eval_precond E P ->
@@ -410,7 +438,7 @@ Lemma eval_precond_updEnv E x v P :
   eval_precond (updEnv x v E) P.
 Proof.
   unfold preVars. destruct P as [Piv C]. cbn. intros [HPiv HC] H. split.
-  - unfold P_intv_sound in *.
+  - unfold eval_preIntv in *.
     intros y iv inl. destruct (HPiv y iv) as [r [H1 H2]]; auto.
     exists r. split; auto. unfold updEnv. case_eq (y =? x); intros Heq; auto.
     exfalso. apply H. set_tac. left. apply beq_nat_true in Heq. subst.
@@ -436,7 +464,7 @@ Definition precond2SMT (P: precond) :=
 Lemma pre_to_smt_correct E P :
   eval_precond E P -> eval_smt_logic E (precond2SMT P).
 Proof.
-  unfold eval_precond, P_intv_sound, precond2SMT.
+  unfold eval_precond, eval_preIntv, precond2SMT.
   destruct P as [intvs q]. cbn.
   induction (FloverMap.elements intvs) as [|[e [lo hi]] l IHl].
   - intros. now cbn.
@@ -453,7 +481,7 @@ Qed.
 Lemma smt_to_pre_correct E P :
   eval_smt_logic E (precond2SMT P) -> eval_precond E P.
 Proof.
-  unfold precond2SMT, eval_precond, P_intv_sound.
+  unfold precond2SMT, eval_precond, eval_preIntv.
   destruct P as [intvs q]. cbn.
   induction (FloverMap.elements intvs) as [|p l IHl]; try (cbn; tauto).
   cbn. intros H. split.
@@ -531,7 +559,7 @@ Lemma checkPre_pre_smt E P q :
   eval_precond E P ->
   eval_smt_logic E q.
 Proof with try discriminate.
-  unfold checkPre, eval_precond, P_intv_sound.
+  unfold checkPre, eval_precond, eval_preIntv.
   destruct P as [Piv C]. cbn.
   induction (FloverMap.elements Piv) as [|[e [lo hi]] l IHl] in q |- *.
   - cbn. intros Heq [_ H]. now apply (SMTLogic_eqb_sound _ C).

coq/SubdivsChecker3.v

@@ -3,15 +3,8 @@ From Flover
      Infra.Ltacs RealRangeArith RealRangeValidator RoundoffErrorValidator
      Environments TypeValidator FPRangeValidator ExpressionAbbrevs ResultChecker
      IntervalArithQ.
-(*
-From Flover
-     Require Import Infra.RealRationalProps Environments ExpressionSemantics
-     IntervalArithQ SMTArith RealRangeArith RealRangeValidator RoundoffErrorValidator
-     ssaPrgs TypeValidator ErrorAnalysis ResultChecker.
-*)
 
 Require Import List.
-Require Import Program.
 Require Import FunInd.
 
 Fixpoint resultLeq e (A1 A2: analysisResult) :=
@@ -259,29 +252,10 @@ Fixpoint covers (P: list (expr Q * intv)) Ps :=
   | _ :: P => false
   end.
 
-Lemma checkDim_sound cov x iv Ps v E :
-  checkDim cov x iv Ps = true ->
-  E x = Some v ->
-  (Q2R (fst iv) <= v <= Q2R (snd iv))%R ->
-  exists P, In P Ps /\
-       (forall (x : nat) (iv : intv),
-           In (Var Q x, iv) P ->
-           exists vR : R, E x = Some vR /\ (Q2R (fst iv) <= vR <= Q2R (snd iv))%R).
-Proof.
-  functional induction (checkDim cov x iv Ps); try discriminate 1.
-  - admit.
-  - cbn in *.
-Abort.
-  
 Lemma covers_sound P Ps E :
   covers P Ps = true ->
-  (forall (x : nat) (iv : intv),
-      In (Var Q x, iv) P ->
-      exists vR : R, E x = Some vR /\ (Q2R (fst iv) <= vR <= Q2R (snd iv))%R) ->
-  exists P', In P' Ps /\
-        (forall (x : nat) (iv : intv),
-            In (Var Q x, iv) P' ->
-            exists vR : R, E x = Some vR /\ (Q2R (fst iv) <= vR <= Q2R (snd iv))%R).
+  eval_preIntv E P ->
+  exists P', In P' Ps /\ eval_preIntv E P'.
 Proof.
   induction P as [|[e iv] P] in Ps |- *.
   - cbn. destruct Ps as [|[|? ?] [|? ?]] eqn:Heq; try discriminate 1.
@@ -292,10 +266,10 @@ Proof.
     intros HPl.
     assert (exists vR : R, E n = Some vR /\ (Q2R (fst iv) <= vR <= Q2R (snd iv))%R)
       as [v [inE iniv]]
-        by (apply HPl; auto).
+        by (apply HPl; now constructor).
     functional induction checkDim (covers P) n iv Ps; try discriminate H.
     + destruct (IHP _ H) as [P' [inb HP']].
-      { intros. apply HPl. auto. }
+      { hnf. intros. apply HPl. now constructor. }
       destruct (getBucket_sound _ _ _ e3 _ inb) as [iv1 [Hin1 Hsub1]].
       eexists; split; eauto.
       intros x iv' [Heq | inP']; auto.
@@ -308,7 +282,7 @@ Proof.
     + Flover_compute.
       destruct (Rle_or_lt v (Q2R (snd ivx))) as [Hle|Hlt].
       * destruct (IHP _ L0) as [P' [inb HP']].
-        { intros. apply HPl. auto. }
+        { hnf. intros. apply HPl. now constructor. }
         destruct (getBucket_sound _ _ _ e3 _ inb) as [iv1 [Hin1 Hsub1]].
         eexists; split; eauto.
         intros x iv' [Heq | inP']; auto.
@@ -325,71 +299,60 @@ Proof.
         destruct IHb0 as [P' [inrest H]]; auto.
         { intros x iv' [Heq | inP]; auto.
           injection Heq; intros; subst.
-          cbn. exists v. split; auto. }
+          cbn. exists v. split; auto. apply HPl; cbn; auto. }
         exists P'; split; auto.
         eapply getBucket_rest_sound; eauto.
 Qed.
 
-(*
-Lemma in_subdivs_intv P Ps E :
+Lemma covers_preVars P Ps :
   covers P Ps = true ->
-  (forall (x : nat) (iv : intv),
-      In (Var Q x, iv) P ->
-      exists vR : R, E x = Some vR /\ (Q2R (fst iv) <= vR <= Q2R (snd iv))%R) ->
-  exists P', In P' Ps /\
-        (forall (x : nat) (iv : intv),
-            In (Var Q x, iv) P' ->
-            exists vR : R, E x = Some vR /\ (Q2R (fst iv) <= vR <= Q2R (snd iv))%R).
+  forall P1, In P1 Ps -> NatSet.Equal (preIntvVars P1) (preIntvVars P).
 Proof.
-  induction P as [|[e iv] P] in Ps |- *; intros chk H.
-  - destruct Ps as [|P' Ps]; cbn in chk; try discriminate chk.
-    exists P'; split; [now constructor |].
-    destruct P'; try discriminate chk. auto.
-  - cbn in chk.
-    destruct e; 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 _ _ curr Hc) as [iv' [Hin Hc']].
-    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.
-*)
+  induction P as [|[e iv] P] in Ps |- *.
+  - cbn. destruct Ps as [|[|? ?] [|? ?]] eqn:Heq; try discriminate 1.
+    intros _ P [H|[]].
+    rewrite <- H. cbn. apply NatSetProps.equal_refl.
+  - cbn. destruct e; try discriminate 1.
+Admitted.
 
 Definition checkPreconds (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 *)
+  let S_qs := map snd subdivs in
+  covers Piv Ps && forallb (fun q => SMTLogic_eqb q (snd P)) S_qs.
 
-Lemma checkPreconds_sound (subdivs: list (precond * analysisResult)) E P :
-  checkPreconds (map fst subdivs) P = true ->
+Lemma checkPreconds_sound (subdivs: list precond) E P :
+  checkPreconds subdivs P = true ->
   eval_precond E P ->
-  exists PA, In PA subdivs /\ eval_precond E (fst PA).
+  exists P1, In P1 subdivs /\ eval_precond E P1.
 Proof.
-  intros H [Pintv Hadd].
-  andb_to_prop H.
-  eapply covers_sound in L; eauto.
-  destruct L as [Pl1 [Hin H]].
+  intros H [Pintv Hq].
+  apply andb_true_iff in H as [cov Hqs].
+  eapply covers_sound in cov; eauto.
+  destruct cov as [Pl1 [Hin H]].
   apply in_map_iff in Hin as [P1 [Heq1 Hin]].
-  apply in_map_iff in Hin as [PA1 [Heq2 Hin]].
-  exists PA1. split; auto.
-  split.
-  - rewrite Heq2.
-    now rewrite <- Heq1 in H.
-  - rewrite Heq2. admit. (* snd P == snd P1 should hold *)
-Admitted.
+  exists P1. split; auto.
+  rewrite <- Heq1 in H.
+  split; auto.
+  eapply forallb_forall in Hqs.
+  - eapply SMTLogic_eqb_sound; eauto.
+  - apply in_map_iff; eauto.
+Qed.
 
+Lemma checkPreconds_preVars subdivs P :
+  checkPreconds subdivs P = true ->
+  forall P1, In P1 subdivs -> NatSet.Equal (preVars P1) (preVars P).
+Proof.
+  intros chk P1 Hin. Flover_compute.
+  unfold preVars.
+  eapply forallb_forall in R.
+  2: apply in_map_iff; eauto.
+  erewrite SMTLogic_eqb_varsLogic; eauto.
+  apply NatSetProps.union_equal_1.
+  eapply covers_preVars; eauto.
+  apply in_map_iff; eauto.
+Qed.
+  
 (* TODO: merge hd and tl again *)
 (** Interval subdivisions checking function **)
 Definition SubdivsChecker (e: expr Q) (absenv: analysisResult)
@@ -421,11 +384,13 @@ Proof.
   intros * deltas_matched P_valid valid_typeMap chk.
   apply andb_prop in chk as [chk valid_subdivs].
   apply andb_prop in chk as [valid_ssa valid_cover].
-  apply (checkPreconds_sound (hd_subdivs :: tl_subdivs)) in P_valid as [[P' A] [in_subdivs P_valid]]; auto.
-  (* preVars P == preVars P' should hold *)
-  assert (validSSA e (preVars P') = true) as valid_ssa' by admit.
+  eapply (checkPreconds_sound (* (hd_subdivs :: tl_subdivs) *)) in P_valid as [P1 [in_subdivs P_valid]]; eauto.
+  assert (validSSA e (preVars P1) = true) as valid_ssa'.
+  { eapply validSSA_eq_set; eauto. eapply checkPreconds_preVars; eauto. }
+  apply in_map_iff in in_subdivs as [[P2 A] [Heq in_subdivs]].
+  cbn in Heq; subst.
   pose proof (checkSubdivs_sound  e _ _ _ _ _ _ valid_subdivs in_subdivs) as [range_err_check A_leq].
-  assert (ResultChecker e A P' (FloverMap.empty(SMTLogic * SMTLogic))  defVars Gamma = true) as res_check
+  assert (ResultChecker e A P1 (FloverMap.empty(SMTLogic * SMTLogic))  defVars Gamma = true) as res_check
     by (unfold ResultChecker; now rewrite valid_ssa', range_err_check).
   exists Gamma; intros approxE1E2.
   assert (approxEnv E1 (toRExpMap Gamma) A (freeVars e) NatSet.empty E2) as approxE1E2'