proposition: Theorem equivFloat {Tl T} : forall (t: ArithExpr Tl T) (lC : evalExprTypeFloat_list Tl) md, convertibleFloat_list lC -> let lM := C2M_list lC in wellBehaved t lM md -> wellFormed t = true -> eqExprTypeFloat (evalFloat t lC md) (evalRounded t lM md).
proof: Proof. simpl. intros t lC md HlC. rewrite wellBehaved_decompose. intros [IWD IOE] IWF. induction t as [| | | Tl T OP | Tl OP | | | | | | | | Tl T | | | |]. 2: { simpl in IWF |- *; intros. rewrite <-B2SF_Prim2B in IWF |- *. rewrite SF2R_B2SF. split; [| easy]. simpl. now rewrite <-is_finite_SF_B2SF. } 15, 16: now apply IHt. - apply equivFloat_Int. simpl in IWF. apply andb_prop in IWF. now rewrite <-Zle_is_le_bool, <-Zlt_is_lt_bool in IWF. - revert n IWD IOE IWF. induction Tl as [| T Tl]; [now destruct n |]. destruct T; (destruct n; simpl in *; [| apply IHTl]); [| easy..]. intros _ _ _. split; [apply Int32.in_bounds_norm | now apply Int32.norm_in_bounds]. - simpl in IWF. apply andb_prop in IWF. destruct IWF as [IWFt1 IWFt2]. destruct T. + destruct OP; simpl in *. * now apply equivFloat_Op_ADD_Integer; [apply IHt1 | apply IHt2 |]. * now apply equivFloat_Op_SUB_Integer; [apply IHt1 | apply IHt2 |]. * now apply equivFloat_Op_MUL_Integer; [apply IHt1 | apply IHt2 |]. * now apply equivFloat_Op_DIV_Integer; [apply IHt1 | apply IHt2 | |]. + destruct OP; simpl in *. * now apply equivFloat_Op_ADD_BinFloat; [apply IHt1 | apply IHt2 |]. * now apply equivFloat_Op_SUB_BinFloat; [apply IHt1 | apply IHt2 |]. * now apply equivFloat_Op_MUL_BinFloat; [apply IHt1 | apply IHt2 |]. * now apply equivFloat_Op_DIV_BinFloat; [apply IHt1 | apply IHt2 | |]. - simpl in IWF. apply andb_prop in IWF. destruct IWF as [IWFt1 IWFt2]. destruct IOE as [IOEt1 [IOEt2 morphOp]]. now apply equivFloat_OpExact; destruct OP; simpl in *; try apply IHt1; try apply IHt2. - simpl in *. apply andb_prop in IWF. destruct IWF as [IWF IWFt3]. apply andb_prop in IWF. destruct IWF as [IWFt1 IWFt2]. destruct IOE as [IOEt1 [IOEt2 [IOEt3 morphOp]]]. destruct IWD as [IWDt1 [IWDt2 IWDt3]]. now apply equivFloat_Fma; [apply IHt1 | apply IHt2 | apply IHt3 |]. - simpl in *. apply andb_prop in IWF. destruct IWF as [IWF IWFt3]. apply andb_prop in IWF. destruct IWF as [IWFt1 IWFt2]. destruct IOE as [IOEt1 [IOEt2 [IOEt3 morphOp]]]. destruct IWD as [IWDt1 [IWDt2 IWDt3]]. now apply equivFloat_FmaExact; [apply IHt1 | apply IHt2 | apply IHt3 | |]. - now apply equivFloat_Nearbyint, IHt. - simpl in *. now apply equivFloat_FastNearbyint; [apply IHt |]. - simpl in *. now apply equivFloat_FastNearbyintToInt; [apply IHt |]. - simpl in *. now apply equivFloat_TruncToInt; [apply IHt |]. - simpl in *. now apply equivFloat_FloatInj; [apply IHt |]. - destruct T; simpl in *. + apply equivFloat_Sqrt_Integer; [now apply IHt |]. destruct IWD as [_ IWD]. apply le_IZR. lra. + apply equivFloat_Sqrt_BinFloat; [now apply IHt | lra]. - simpl in IWF. apply andb_prop in IWF. destruct IWF as [IWFt1 IWFt2]. destruct IWD as [IWDt1 IWDt2]. destruct IOE as [IOEt1 IOEt2]. destruct (IHt1 lC) as [fint1 B2Rt1]; try easy. destruct T1; simpl in *; [now rewrite B2Rt1 in fint1 |- *; try easy; apply IHt2 |]. specialize (IHt2 (evalFloat t1 lC md, lC)). simpl in IHt2. rewrite B2Rt1 in IHt2. now apply IHt2. - simpl in *. apply andb_prop in IWF. now apply equivFloat_ArrayAcc; [| apply IHt |]. Qed.
imports: Coq(PrimInt63 Sint63 Floats PArray) Coq(Bool List Reals Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations)