From Coq
     Require Import Reals.Reals QArith.Qreals.

From Flover
     Require Import Commands ExpressionSemantics Environments RealRangeArith TypeValidator.

Fixpoint validErrorBoundsRec (e:expr Q) E1 E2 A Gamma DeltaMap :Prop :=
  (match e with
  | Unop u e => validErrorBoundsRec e E1 E2 A Gamma DeltaMap
  | Downcast m e => validErrorBoundsRec e E1 E2 A Gamma DeltaMap
  | Binop b e1 e2 =>
    validErrorBoundsRec e1 E1 E2 A Gamma DeltaMap /\
    validErrorBoundsRec e2 E1 E2 A Gamma DeltaMap
  | Fma e1 e2 e3 =>
    validErrorBoundsRec e1 E1 E2 A Gamma DeltaMap /\
    validErrorBoundsRec e2 E1 E2 A Gamma DeltaMap /\
    validErrorBoundsRec e3 E1 E2 A Gamma DeltaMap
  | _ => True
   end)  /\
  forall v__R (iv: intv) (err: error),
    eval_expr E1 (toRTMap (toRExpMap Gamma)) DeltaMapR (toREval (toRExp e)) v__R REAL ->
    FloverMap.find e A = Some (iv, err) ->
    (exists v__FP m__FP,
      eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e) v__FP m__FP) /\
    (forall v__FP m__FP,
        eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e) v__FP m__FP ->
        (Rabs (v__R - v__FP) <= (Q2R err))%R).

Definition validErrorBounds e E1 E2 A Gamma: Prop :=
  forall DeltaMap,
    (forall (v : R) (m' : mType),
        exists d : R, DeltaMap v m' = Some d /\ (Rabs d <= mTypeToR m')%R) ->
    validErrorBoundsRec e E1 E2 A Gamma DeltaMap.

Lemma validErrorBoundsRec_single e E1 E2 A Gamma DeltaMap:
  validErrorBoundsRec e E1 E2 A Gamma DeltaMap ->
  forall v__R iv err,
    eval_expr E1 (toRTMap (toRExpMap Gamma)) DeltaMapR (toREval (toRExp e)) v__R REAL ->
    FloverMap.find e A = Some (iv, err) ->
    (exists v__FP m__FP,
      eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e) v__FP m__FP) /\
    (forall v__FP m__FP,
        eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e) v__FP m__FP ->
        (Rabs (v__R - v__FP) <= (Q2R err))%R).
Proof.
  intros validError_e;
    intros;  destruct e; cbn in *; split;
      edestruct validError_e as (? & ? & ?); eauto.
Qed.

Fixpoint validErrorBoundsCmdRec (c: cmd Q) E1 E2 A Gamma DeltaMap: Prop :=
  match c with
  | Let m x e k =>
    validErrorBoundsRec e E1 E2 A Gamma DeltaMap /\
    (exists iv_e err_e iv_x err_x,
       FloverMap.find e A = Some (iv_e, err_e) /\
       FloverMap.find (Var Q x) A = Some (iv_x, err_x) /\
       Qeq_bool err_e err_x = true) /\
    (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 ->
        validErrorBoundsCmdRec k (updEnv x v__R E1) (updEnv x v__FP E2) A Gamma DeltaMap)
  | Ret e => validErrorBoundsRec e E1 E2 A Gamma DeltaMap
  end  /\
  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) ->
    (exists v__FP m__FP,
      bstep (toRCmd c) E2 (toRExpMap Gamma) DeltaMap v__FP m__FP) /\
    (forall v__FP m__FP,
        bstep (toRCmd c) E2 (toRExpMap Gamma) DeltaMap v__FP m__FP ->
        (Rabs (v__R - v__FP) <= (Q2R err))%R).

Definition validErrorBoundsCmd (c: cmd Q) E1 E2 A Gamma: Prop :=
  forall DeltaMap,
    (forall (v : R) (m' : mType),
        exists d : R, DeltaMap v m' = Some d /\ (Rabs d <= mTypeToR m')%R) ->
    validErrorBoundsCmdRec c E1 E2 A Gamma DeltaMap.

Lemma validErrorBoundsCmdRec_single c E1 E2 A Gamma DeltaMap:
  validErrorBoundsCmdRec 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) ->
    (exists v__FP m__FP,
      bstep (toRCmd c) E2 (toRExpMap Gamma) DeltaMap v__FP m__FP) /\
    (forall v__FP m__FP,
        bstep (toRCmd c) E2 (toRExpMap Gamma) DeltaMap v__FP m__FP ->
        (Rabs (v__R - v__FP) <= (Q2R err))%R).
Proof.
  intros validError_e;
    intros;  destruct c; cbn in *; split;
      edestruct validError_e as (? & ? & ?); eauto.
Qed.