Prove validErrorBoundsCmd from soundness of validErrorboundAA_sound

coq/Commands.v

@@ -130,3 +130,17 @@ Proof.
   - eapply IHf; eauto.
   - eapply Gamma_det; eauto.
 Qed.
+
+Lemma bstep_det f:
+  forall E Gamma DeltaMap v1 v2 m,
+  bstep f E Gamma DeltaMap v1 m ->
+  bstep f E Gamma DeltaMap v2 m ->
+  v1 = v2.
+Proof.
+  induction f; intros * eval_f1 eval_f2;
+    inversion eval_f1; subst;
+      inversion eval_f2; subst; try auto.
+  - replace v with v0 in * by eauto using eval_expr_functional.
+    eapply IHf; eauto.
+  - eapply eval_expr_functional; eauto.
+Qed.

coq/RoundoffErrorValidator.v

@@ -54,7 +54,7 @@ Proof.
       specialize (Hall v__e m__e Hev) as (? & ? & ? & ? & ? & ? & ? & ? & ? & ? & ? & ? & ? & Hall).
       eapply validErrorbound_sound_validErrorBounds; eauto.
       intros e' Hin.
-      specialize Hexchecked as (_ & Hex); eauto;
+      specialize Hexchecked as (_ & _ & Hex); eauto;
         [now rewrite FloverMapFacts.P.F.empty_in_iff|].
       split; eauto.
       eapply Hall; eauto; now rewrite FloverMapFacts.P.F.empty_in_iff.
@@ -71,12 +71,13 @@ Definition RoundoffErrorValidatorCmd (f:cmd Q) (tMap:FloverMap.t mType)
        end.
 
 Theorem RoundoffErrorValidatorCmd_sound f:
-  forall A E1 E2 outVars fVars dVars Gamma DeltaMap,
+  forall A E1 E2 outVars fVars dVars Gamma DeltaMap v__R,
     (forall (e' : expr R) (m' : mType),
         exists d : R, DeltaMap e' m' = Some d /\ (Rabs d <= mTypeToR m')%R) ->
     approxEnv E1 (toRExpMap Gamma) A fVars dVars E2 ->
     ssa f (NatSet.union fVars dVars) outVars ->
     NatSet.Subset (NatSet.diff (Commands.freeVars f) dVars) fVars ->
+    bstep (toREvalCmd (toRCmd f)) E1 (toRTMap (toRExpMap Gamma)) DeltaMapR v__R REAL ->
     dVars_contained dVars (FloverMap.empty (affine_form Q)) ->
     RoundoffErrorValidatorCmd f Gamma A dVars = true ->
     validRangesCmd f A E1 (toRTMap (toRExpMap Gamma)) ->
@@ -90,12 +91,19 @@ Proof.
   - destruct (validErrorboundAACmd f Gamma A dVars 1 (FloverMap.empty (affine_form Q)))
              eqn: Hvalid; [|congruence].
     destruct p as (expr_map2, noise2).
-    eapply validErrorboundAACmd_validErrorBoundsCmd with
-        (expr_map1 := FloverMap.empty (affine_form Q)) (noise1 := 1%nat)
-        (expr_map2 := expr_map2) (noise2 := noise2)
-        (noise_map1 := fun x => None); eauto.
-    + intros ? Hin.
-      now rewrite FloverMapFacts.P.F.empty_in_iff in Hin.
-    + intros ? Hin.
-      now rewrite FloverMapFacts.P.F.empty_in_iff in Hin.
+    edestruct validErrorboundAACmd_sound; eauto.
+    + instantiate (1 := fun x => None).
+      auto.
+    + intros ? Hin; now rewrite FloverMapFacts.P.F.empty_in_iff in Hin.
+    + intros ? Hin; now rewrite FloverMapFacts.P.F.empty_in_iff in Hin.
+    + intros ? Hin; now rewrite FloverMapFacts.P.F.empty_in_iff in Hin.
+    + destruct H8 as ((v__FP & m__FP & Heval) & ?).
+      edestruct validErrorBoundAACmd_contained_command_subexpr; eauto.
+      1: intros ? Hin; now rewrite FloverMapFacts.P.F.empty_in_iff in Hin.
+      apply contained_command_subexpr_get_retexp_in in H11.
+      edestruct H8 as (? & (iv__A & err__A & Hcert) & ?); eauto.
+      1: intros Hin; now rewrite FloverMapFacts.P.F.empty_in_iff in Hin.
+      specialize (H9 v__FP m__FP iv__A err__A Heval Hcert).
+      edestruct H9 as (? & ? & ? & ?); eauto.
+      intuition.
 Qed.