Revert "Solve admits of approxEnv proofs"

This reverts commit 71f97008.

coq/ErrorAnalysis.v

@@ -42,16 +42,13 @@ Proof.
       destruct validError_e as (? & ? & ?); eauto.
 Qed.
 
-Fixpoint validErrorBoundsCmd (c: cmd Q) E1 E2 A Gamma DeltaMap fVars dVars: Prop :=
+Fixpoint validErrorBoundsCmd (c: cmd Q) E1 E2 A Gamma DeltaMap: Prop :=
   match c with
   | Let m x e k => validErrorBounds e E1 E2 A Gamma DeltaMap /\
                   (forall v__R v__FP,
                       eval_expr E1 (toRTMap (toRExpMap Gamma)) DeltaMapR (toREval (toRExp e)) v__R REAL ->
                       eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e) v__FP m ->
-                      approxEnv (updEnv x v__R E1) (toRExpMap Gamma) A fVars
-                                (NatSet.add x dVars) (updEnv x v__FP E2) /\
-                      validErrorBoundsCmd k (updEnv x v__R E1) (updEnv x v__FP E2) A Gamma DeltaMap
-                        fVars (NatSet.add x dVars))
+                      validErrorBoundsCmd k (updEnv x v__R E1) (updEnv x v__FP E2) A Gamma DeltaMap)
   | Ret e => validErrorBounds e E1 E2 A Gamma DeltaMap
   end  /\
   forall v__R (iv: intv) (err: error),
@@ -63,8 +60,8 @@ Fixpoint validErrorBoundsCmd (c: cmd Q) E1 E2 A Gamma DeltaMap fVars dVars: Prop
         bstep (toRCmd c) E2 (toRExpMap Gamma) DeltaMap v__FP m__FP ->
         (Rabs (v__R - v__FP) <= (Q2R err))%R).
 
-Lemma validErrorBoundsCmd_single c E1 E2 A Gamma DeltaMap fVars dVars:
-  validErrorBoundsCmd c E1 E2 A Gamma DeltaMap fVars dVars ->
+Lemma validErrorBoundsCmd_single c E1 E2 A Gamma DeltaMap:
+  validErrorBoundsCmd c E1 E2 A Gamma DeltaMap ->
   forall v__R (iv: intv) (err: error),
     bstep (toREvalCmd (toRCmd c)) E1 (toRTMap (toRExpMap Gamma)) DeltaMapR v__R REAL ->
     FloverMap.find (getRetExp c) A = Some (iv, err) ->

coq/ErrorValidation.v

@@ -2426,7 +2426,7 @@ Theorem validErrorboundCmd_sound (f:cmd Q):
     validErrorboundCmd f Gamma A dVars = true ->
     validTypesCmd f Gamma ->
     validRangesCmd f A E1 (toRTMap (toRExpMap Gamma)) ->
-    validErrorBoundsCmd f E1 E2 A Gamma DeltaMap fVars dVars.
+    validErrorBoundsCmd f E1 E2 A Gamma DeltaMap.
 Proof.
   induction f;
     intros * deltas_matched approxc1c2 ssa_f freeVars_subset valid_bounds valid_types valid_intv;
@@ -2454,17 +2454,12 @@ Proof.
         rename R into valid_rec.
         eapply validTypes_exec in find_me; eauto; subst.
         type_conv; subst.
-        assert (approxEnv (updEnv n vR E1) (toRExpMap Gamma) A
-                          fVars (NatSet.add n dVars) (updEnv n vF E2)).
-        {
-          eapply approxUpdBound; try eauto; simpl in *.
-          - eapply toRExpMap_some; eauto.
+        eapply IHf with (fVars := fVars) (outVars := outVars); eauto.
+        + eapply approxUpdBound; try eauto; simpl in *.
+          * eapply toRExpMap_some; eauto.
             simpl; auto.
-          - apply Rle_trans with (r2:= Q2R e0); try lra.
+          * apply Rle_trans with (r2:= Q2R e0); try lra.
             eapply bounded_e; eauto.
-        }
-        split; auto.
-        eapply IHf with (fVars := fVars) (outVars := outVars); eauto.
         + eapply ssa_equal_set; eauto.
           hnf. intros a; split; intros in_set.
           * rewrite NatSet.add_spec, NatSet.union_spec;
@@ -2496,8 +2491,7 @@ Proof.
       subst.
     eapply validErrorBounds_single in Hsound; eauto.
     destruct Hsound as [[vFe [mFe eval_float_e]] bounded_e].
-    assert (validErrorBoundsCmd f (updEnv n v E1) (updEnv n v0 E2)
-                                A Gamma DeltaMap fVars (NatSet.add n dVars)) as IHf'.
+    assert (validErrorBoundsCmd f (updEnv n v E1) (updEnv n v0 E2) A Gamma DeltaMap) as IHf'.
     {
       apply (IHf A (updEnv n v E1) (updEnv n v0 E2) outVars fVars
                  (NatSet.add n dVars) Gamma DeltaMap);

coq/ErrorValidationAA.v

@@ -3331,7 +3331,7 @@ Theorem validErrorboundAACmd_sound c:
           toInterval (afQ2R af) = ((- err__af)%R, err__af) /\
           (err__af <= Q2R err__A)%R /\
           af_evals (afQ2R af) (v__R - v__FP) noise_map2 /\
-          validErrorBoundsCmd c E1 E2 A Gamma DeltaMap fVars dVars /\
+          validErrorBoundsCmd c E1 E2 A Gamma DeltaMap /\
           (forall e' : FloverMap.key,
               ~ FloverMap.In (elt:=affine_form Q) e' expr_map1 ->
               FloverMap.In (elt:=affine_form Q) e' expr_map2 ->
@@ -3633,11 +3633,7 @@ Proof.
         }
         edestruct validErrorboundAA_contained_subexpr as (? & ? & ?);
           try exact Hvalidbounds'; eauto.
-      * rename H36 into Heval__R0; rename H37 into Heval__FP0.
-        apply eval_expr_functional with (v1 := v) in Heval__R0; eauto.
-        apply eval_expr_functional with (v1 := v__FP) in Heval__FP0; eauto.
-        subst; auto.
-      * rename H36 into Heval__R0; rename H37 into Heval__FP0.
+      * intros v__R0 v__FP0 Heval__R0 Heval__FP0.
         apply eval_expr_functional with (v1 := v) in Heval__R0; eauto.
         apply eval_expr_functional with (v1 := v__FP) in Heval__FP0; eauto.
         subst; auto.

coq/FPRangeValidator.v

@@ -154,7 +154,7 @@ Lemma FPRangeValidatorCmd_sound (f:cmd Q):
   bstep (toRCmd f) E2 (toRExpMap Gamma) DeltaMap v m ->
   validTypesCmd f Gamma ->
   validRangesCmd f A E1 (toRTMap (toRExpMap Gamma)) ->
-  validErrorBoundsCmd f E1 E2 A Gamma DeltaMap fVars dVars ->
+  validErrorBoundsCmd f E1 E2 A Gamma DeltaMap ->
   FPRangeValidatorCmd f A Gamma dVars = true ->
   NatSet.Subset (NatSet.diff (freeVars f) dVars) fVars ->
   (forall v, NatSet.In v dVars ->
@@ -184,11 +184,23 @@ Proof.
     pose proof (validErrorBounds_single _ _ _ _ validerr_e) as validerr_e_single.
     specialize (validerr_e_single v0 iv_e err_e H19 map_e) as
         ((vF_e & m_e & eval_float_e) & err_bounded_e).
+    (* destr_factorize.
+    edestruct (validErrorbound_sound (e:=e) (E1:=E1) (E2:=E2) (fVars:=fVars)
+                                     (dVars := dVars) (A:=A)
+                                     (nR:=v0) (err:=err_e) (elo:=fst iv_e) (ehi:=snd iv_e))
+      as [[vF_e [m_e eval_float_e]] err_bounded_e]; eauto.
+    + set_tac. split; try auto.
+      split; try auto.
+      hnf; intros; subst; set_tac.
+    + destruct iv_e; auto.
+    + *)
       rewrite <- (meps_0_deterministic (toRExp e) eval_e_real H19) in *; try auto.
       apply (IHf (updEnv n vR_e E1) (updEnv n v1 E2)
                  Gamma DeltaMap v vR m0 A fVars
                  (NatSet.add n dVars) (outVars)); eauto.
-      * edestruct validerr_rec; eauto.
+      * eapply approxUpdBound; eauto; simpl in *.
+        { eapply toRExpMap_some; eauto. simpl; auto. }
+        { admit. }
       * eapply ssa_equal_set; eauto.
         hnf. intros a; split; intros in_set.
         { rewrite NatSet.add_spec, NatSet.union_spec;
@@ -197,13 +209,28 @@ Proof.
         { rewrite NatSet.add_spec, NatSet.union_spec in in_set;
             rewrite NatSet.union_spec, NatSet.add_spec.
           destruct in_set as [P1 | [ P2 | P3]]; auto. }
-      * edestruct validerr_rec; eauto.
+        (*
+         * eapply (swap_Gamma_bstep (Gamma1 := updDefVars n REAL (toRMap Gamma))); eauto.
+        eauto using Rmap_updVars_comm.
+          * apply validRangesCmd_swap with (Gamma1:=updDefVars n REAL Gamma).
+            { intros x; unfold toRMap, updDefVars.
+              destruct (x =? n) eqn:?; auto. }
+            { eapply valid_rec. auto. } *)
       * set_tac; split.
         { split; try auto.
           hnf; intros; subst.
           apply H6; rewrite NatSet.add_spec; auto. }
         { hnf; intros.
           apply H6; rewrite NatSet.add_spec; auto. }
+        (*
+      * unfold vars_typed. intros.
+        unfold updDefVars.
+        destruct (v2 =? n) eqn:?; eauto.
+        apply H8. rewrite NatSet.union_spec in *.
+        destruct H4; try auto.
+        rewrite NatSet.add_spec in H4.
+        rewrite Nat.eqb_neq in *.
+        destruct H4; subst; try congruence; auto. *)
       * intros. unfold updEnv.
         type_conv; subst.
         destruct (v2 =? n) eqn:?; try rewrite Nat.eqb_eq in *;
@@ -217,4 +244,4 @@ Proof.
           rewrite NatSet.add_spec in H5; destruct H5;
             auto; subst; congruence. }
   - destruct H5. destruct H4. destruct H6. eapply FPRangeValidator_sound; eauto.
-Qed.
+Admitted.

coq/IEEE_connection.v

@@ -829,7 +829,7 @@ Lemma bstep_gives_IEEE (f:cmd fl64) :
     ssa (B2Qcmd f) (NatSet.union fVars dVars) outVars ->
     validTypesCmd (B2Qcmd f) Gamma ->
     validRangesCmd (B2Qcmd f) A E1 (toRTMap (toRExpMap Gamma)) ->
-    validErrorBoundsCmd (B2Qcmd f) E1 E2_real A Gamma DeltaMap fVars dVars ->
+    validErrorBoundsCmd (B2Qcmd f) E1 E2_real A Gamma DeltaMap ->
     FPRangeValidatorCmd (B2Qcmd f) A Gamma dVars = true ->
     bstep (toREvalCmd (toRCmd (B2Qcmd f))) E1 (toRTMap (toRExpMap Gamma)) DeltaMapR vR REAL ->
     bstep (toRCmd (B2Qcmd f)) (toREnv E2) (toRExpMap Gamma) DeltaMap vF M64 ->
@@ -913,8 +913,9 @@ Proof.
                   vR vF_new A fVars (NatSet.add n dVars) outVars); try eauto.
     + intros. unfold toREnv, updFlEnv, updEnv.
       destruct (x1 =? n); auto. rewrite <- envs_eq. unfold toREnv; auto.
-    + edestruct valid_error_cmd; eauto.
-      eapply eval_eq_env; eauto.
+    + eapply approxUpdBound; eauto.
+      * eapply toRExpMap_some with (e:=Var Q n); eauto.
+      * admit.
     + eapply ssa_equal_set; eauto.
       hnf; split; intros.
       * rewrite NatSet.add_spec, NatSet.union_spec in *.

coq/RoundoffErrorValidator.v

@@ -82,7 +82,7 @@ Theorem RoundoffErrorValidatorCmd_sound f:
     RoundoffErrorValidatorCmd f Gamma A dVars = true ->
     validRangesCmd f A E1 (toRTMap (toRExpMap Gamma)) ->
     validTypesCmd f Gamma ->
-    validErrorBoundsCmd f E1 E2 A Gamma DeltaMap fVars dVars.
+    validErrorBoundsCmd f E1 E2 A Gamma DeltaMap.
 Proof.
   intros.
   unfold RoundoffErrorValidatorCmd in *.