proposition: Lemma evalReal_evalRounded {Tl T} : forall (t: ArithExpr Tl T) (lM : evalExprTypeRounded_list Tl) md, let lR := M2R_list lM in evalReal t lR md = M2R (evalRounded t lM md).
proof: Proof. induction t as [| | | Tl T OP | Tl OP | | | | | | | | Tl T | | | |]. - easy. - simpl. intros _ _. now rewrite <-B2SF_Prim2B, SF2R_B2SF. - intros lM. revert n. induction Tl as [| T Tl]; [now destruct n |]. destruct T; (destruct n; [easy |]); simpl in *; apply IHTl. - intros lM md lR. destruct OP; destruct T; simpl; unfold lR; rewrite (IHt1 lM), (IHt2 lM); try reflexivity; [| | | now unfold Rrnd.nearbyint, round, F2R, scaled_mantissa; simpl; rewrite !Rmult_1_r, Ztrunc_div_]. + now rewrite <-plus_IZR. + now rewrite <-minus_IZR. + now rewrite <-mult_IZR. - intros lM md lR. now destruct OP; simpl; unfold lR; rewrite (IHt1 lM), (IHt2 lM). - intros lM md lR. simpl in *. unfold lR. now rewrite IHt1, IHt2, IHt3. - intros lM md lR. simpl in *. unfold lR. now rewrite IHt1, IHt2, IHt3. - intros lM md lR. simpl in *. unfold lR. now rewrite IHt. - intros lM md lR. simpl in *. unfold lR. now rewrite IHt. - intros lM md lR. simpl in *. unfold lR, Rrnd.nearbyint. now rewrite IHt, round_FIX_IZR. - intros lM md lR. simpl in *. unfold lR. rewrite <-round_FIX_IZR. now rewrite IHt. - intros lM md lR. simpl in *. unfold lR. apply IHt. - intros lM md lR. simpl in *. unfold lR. destruct T. + unfold Rrnd.nearbyint, round, F2R, scaled_mantissa. simpl. rewrite 2Rmult_1_r. rewrite Ztrunc_floor by apply sqrt_ge_0. apply f_equal. rewrite IHt. apply trunc_sqrt. + now rewrite IHt. - intros lM md lR. now destruct T1; unfold lR in *; simpl in *; rewrite IHt1; fold evalExprTypeReal_list in *; fold evalExprTypeRounded_list in *; specialize (IHt2 (evalRounded t1 lM md, lM)); simpl in IHt2; rewrite IHt2. - intros lM md lR. simpl in *. unfold lR. now rewrite IHt, Ztrunc_IZR. - easy. - intros lM md lR. simpl in *. unfold lR. now apply IHt. Qed.
imports: Coq(PrimInt63 Sint63 Floats PArray) Coq(Bool List Reals Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations)