proposition: Theorem equivPrim {Tl T} : forall (t: ArithExpr Tl T) (lP : evalExprTypePrim_list Tl), convertiblePrim_list lP -> let lM := P2M_list lP in wellBehaved t lM mode_NE -> wellFormed t = true -> eqExprTypePrim (evalPrim t lP) (evalRounded t lM mode_NE).
proof: Proof. simpl. intros t lP HlP. rewrite wellBehaved_decompose. intros [IWD IOE] IWF. induction t as [| | | Tl T OP | Tl OP | | | | | | | | Tl T | | | |]; [| easy | ..]. 15, 16: now apply IHt. - apply equivPrim_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.. | split; [easy |] | easy]. unfold isConversionPrim. now rewrite <-B2SF_Prim2B, SF2R_B2SF. - simpl in IWF. apply andb_prop in IWF. destruct IWF as [IWFt1 IWFt2]. destruct T. + destruct OP; simpl in *. * now apply equivPrim_Op_ADD_Integer; [apply IHt1 | apply IHt2 |]. * now apply equivPrim_Op_SUB_Integer; [apply IHt1 | apply IHt2 |]. * now apply equivPrim_Op_MUL_Integer; [apply IHt1 | apply IHt2 |]. * now apply equivPrim_Op_DIV_Integer; [apply IHt1 | apply IHt2 | |]. + destruct OP; simpl in *. * now apply equivPrim_Op_ADD_BinFloat; [apply IHt1 | apply IHt2 |]. * now apply equivPrim_Op_SUB_BinFloat; [apply IHt1 | apply IHt2 |]. * now apply equivPrim_Op_MUL_BinFloat; [apply IHt1 | apply IHt2 |]. * now apply equivPrim_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 equivPrim_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 equivPrim_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 equivPrim_FmaExact; [apply IHt1 | apply IHt2 | apply IHt3 | |]. - now apply equivPrim_Nearbyint, IHt. - simpl in *. now apply equivPrim_FastNearbyint; [apply IHt |]. - simpl in *. now apply equivPrim_FastNearbyintToInt; [apply IHt |]. - simpl in *. now apply equivPrim_TruncToInt; [apply IHt |]. - simpl in *. now apply equivPrim_FloatInj; [apply IHt |]. - destruct T; simpl in *. + apply equivPrim_Sqrt_Integer; [now apply IHt |]. destruct IWD as [_ IWD]. apply le_IZR. lra. + apply equivPrim_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 lP) as [fint1 B2Rt1]; try easy. destruct T1; simpl in *; [now rewrite <-B2Rt1 in IWDt2, IOEt2 |- *; now apply IHt2 |]. specialize (IHt2 (evalPrim t1 lP, lP)). simpl in IHt2. rewrite <-B2Rt1 in IWDt2, IOEt2 |- *. now apply IHt2. - simpl in *. apply andb_prop in IWF. now apply equivPrim_ArrayAcc; [| apply IHt |]. Qed.
imports: Coq(PrimInt63 Sint63 Floats PArray) Coq(Bool List Reals Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations)