proposition: Lemma equivPrim_ArrayAcc {Tl} : forall (t : ArithExpr Tl Integer) a (lP : evalExprTypePrim_list Tl), finite_array a = true -> let lM := P2M_list lP in eqExprTypePrim (evalPrim t lP) (evalRounded t lM mode_NE) -> (0 <= evalRounded t lM mode_NE < Uint63.to_Z (PArray.length a))%Z -> eqExprTypePrim (evalPrim (ArrayAcc a t) lP) (evalRounded (ArrayAcc a t) lM mode_NE).
proof: Proof. intros t a lP H' lM [fint B2Rt] H. simpl. unfold eqExprTypeFloat. apply (f_equal of_Z) in B2Rt. rewrite of_to_Z in B2Rt. rewrite B2Rt. split; [| easy]. unfold finite_array in H'. set (P := fun n '(i, b) => (Z.of_N n <= Uint63.to_Z (PArray.length a))%Z -> b = true -> i = Z.of_N n /\ forall j, (0 <= j < Z.of_N n)%Z -> is_finite (Prim2B a.[of_Z j]) = true). set (f := fun '(i, b) => (Z.succ i, b && is_finite_SF (Prim2SF a.[of_Z i]))). generalize (N.iter_ind (Z * bool) f (0%Z, true) P). intros H''. cut (forall n, P n (N.iter n f (0%Z, true))). 2: { apply H''; [intros _ _; split; [easy | lia] |]. intros n [i b]. simpl. intros IHn H1 H2. destruct IHn as [IHn_1 IHn_2]; [lia | now apply andb_prop in H2 |]. split; [lia |]. intros j Hj'. rewrite IHn_1 in H2. rewrite <-B2SF_Prim2B, is_finite_SF_B2SF in H2. assert (Hj : (0 <= j < Z.of_N n)%Z \/ j = Z.of_N n) by lia. clear Hj'. now destruct Hj as [Hj | ->]; [now apply IHn_2 | now apply andb_prop in H2]. } intros Haux. specialize (Haux (Z.to_N φ (PArray.length a)%uint63)). unfold P in Haux. revert H' Haux. destruct N.iter as [i b] eqn:Hô. simpl. intros -> Hè. rewrite <-B2SF_Prim2B, is_finite_SF_B2SF. now apply Hè; [lia | | lia]. Qed.
imports: Coq(PrimInt63 Sint63 Floats PArray) Coq(Bool List Reals Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations)